Theory Sepref_Conc_Post

section Concrete Equality Constraints
theory Sepref_Conc_Post
imports
  Main 
  Automatic_Refinement.Misc
begin
  subsection Basic Combinators
  named_theorems CP_defs
  
  definition [CP_defs]: "CP_JOIN CP1 CP2  λr. CP1 r  CP2 r"
  definition [CP_defs]: "CP_EX CP  λr. x. CP x r"
  definition [CP_defs]: "CP_SEQ CP1 CP2  λr. x. CP1 x  CP2 x r"
  definition [CP_defs]: "CP_RPT CP  CP**"
  definition [CP_defs]: "CP_SPLIT CP p  λr. case p of (a,b)  CP a b r"
  definition [CP_defs]: "CP_EX32 CP  λ(x1,x2). x3. CP (x1,x2,x3)"

  definition [CP_defs]: "CP_pred P  P::bool" ― ‹Predicate, not further interpreted, but variables inside rewritten
  
  subsection Normalization

  subsubsection Simplification
  named_theorems CP_simps
  
  lemma [CP_simps]: 
    "CP_SEQ (λ_. True) CP = CP_EX CP"
    "CP_EX (λ_. P) = P"
    by (auto simp add: CP_defs)
  
  lemma [CP_simps]: "CP_SEQ (λr. r = x) CP = CP x"  
    by (simp add: CP_defs)
    
  lemma [CP_simps]: "CP_JOIN A A = A"  
    by (simp add: CP_defs)

  lemma [CP_simps]: "p=(a,b)  fst p = a  snd p = b" by auto

  lemma [CP_simps]: "case_prod f = (λp. f (fst p) (snd p))" by auto
  
        
  subsubsection Monotonicity
  
  definition [CP_defs]: "CP_TAG x  x::bool"   ― ‹Tag that protects schematic goal that receives simplified version
  definition [CP_defs]: "CP_HANDLE x  x::bool" ― ‹Tag that marks combinator with normalized arguments

  lemma CP_HANDLEI: "X  CP_HANDLE X" by (simp add: CP_defs)
  lemma CP_HANDLED: "CP_HANDLE X  X" by (simp add: CP_defs)
  
    
  named_theorems CP_monos
  
  lemma CP_JOIN_mono[CP_monos]:
    "CP_JOIN A B r   r. A r  CP_TAG (A' r); r. B r  CP_TAG (B' r)    CP_JOIN A' B' r"  
    by (auto simp: CP_defs)
    
  lemma CP_EX_mono[CP_monos]: "CP_EX A r  x r. A x r  CP_TAG (A' x r)  CP_EX A' r"  
    by (auto simp: CP_defs)

  lemma CP_EX32_mono[CP_monos]: "CP_EX32 A r  r. A r  CP_TAG (A' r)  CP_EX32 A' r"  
    by (auto simp: CP_defs)
        
  lemma CP_SEQ_mono[CP_monos]: "CP_SEQ A B r  x. A x  CP_TAG (A' x); x r. B x r  CP_TAG (B' x r)  CP_SEQ A' B' r"  
    by (auto simp: CP_defs)

  lemma CP_RPT_mono[CP_monos]: "CP_RPT A x r   x r. A x r  CP_TAG (A' x r)   CP_RPT A' x r"
    apply (auto simp: CP_defs)
    by (metis mono_rtranclp)
    
  lemma CP_SPLIT_unfold[CP_simps]: "CP_SPLIT P = (λp. P (fst p) (snd p))"
    by (auto simp: CP_defs split: prod.splits)
    
  lemma CP_tagI: "A  CP_TAG A"  
    by (auto simp: CP_defs)
    
  lemma CP_tag_cong: "CP_TAG A = CP_TAG A" by simp 
  
  subsection Combinator Normalization
  
  subsubsection Basics
  
  text Transfer information into tag
  lemma CP_tag_resolve1:
    assumes "a=b"
    assumes "CP_TAG B"
    shows "CP_TAG (a=b  B)"
    using assms by auto
    
  lemma CP_tag_resolve2:
    assumes "CP_pred P"
    assumes "CP_TAG B"
    shows "CP_TAG (P  B)"
    using assms by (auto simp: CP_defs)

        
  lemma CP_tag_triv: "CP_TAG True"  
    by (auto simp: CP_TAG_def)
    
  method cp_resolve_tag = (((determ erule CP_tag_resolve1 CP_tag_resolve2)+)?,rule CP_tag_triv)

  text Explode products
  (* TODO: This is too fine-grained! Only split as much as required! *)
  method cp_explode_prod = (simp only: prod_eq_iff prod.inject cnv_conj_to_meta fst_conv snd_conv cong: CP_tag_cong)
  

  subsubsection Plain equality
  method handle_plain_eqs =
    drule asm_rl[of "_=_"] asm_rl[of "__"] asm_rl[of True] asm_rl[of "CP_pred _"],
    (elim conjE)?,
    cp_resolve_tag

  subsubsection Sequence  
    
  lemma CP_SEQE:
    assumes "CP_SEQ (λx. A x) (λx r. B x r) r" 
    obtains x where "A x" "B x r"
    using assms by (auto simp: CP_defs)
    
  method handle_CP_SEQ =  
    drule CP_HANDLED,
    erule CP_SEQE,
    (elim conjE)?,
    (*cp_sels_to_vars?,
    cp_vars_to_sels?,*)
    cp_explode_prod?,
    cp_resolve_tag

  subsubsection Ex      
    
  lemma CP_EXE:
    assumes "CP_EX (λx. A x) r"  
    obtains x where "A x r"
    using assms by (auto simp: CP_defs)
    
  method handle_CP_EX =  
    drule CP_HANDLED,
    erule CP_EXE,
    (elim conjE)?,
    cp_explode_prod?,
    cp_resolve_tag

  subsubsection Ex32      
    
  lemma CP_EX32E:
    assumes "CP_EX32 CP r"  
    obtains x where "CP (fst r,snd r,x)"
    using assms by (auto simp: CP_defs)
    
  method handle_CP_EX32 =  
    drule CP_HANDLED,
    erule CP_EX32E,
    (elim conjE)?,
    cp_explode_prod?,
    cp_resolve_tag
    
    
  subsubsection Join  
  lemma handle_join_take:
    assumes "CP_JOIN (λr. a r  as r) bs r"
    assumes "r. bs r  a r"
    obtains "a r" "CP_JOIN as bs r"
    using assms
    by (auto simp: CP_defs)
    
  lemma handle_join_drop:
    assumes "CP_JOIN (λr. a r  as r) bs r" 
    obtains "CP_JOIN as bs r"  
    using assms
    by (auto simp: CP_defs)

  lemma handle_join_last_take: 
    assumes "CP_JOIN (λr. a r) bs r"
    assumes "r. bs r  a r"
    obtains "a r"
    using assms
    by (auto simp: CP_defs)
       
  lemma handle_join_last_drop:
    "CP_JOIN (λr. a r) bs r  P  P" .
    
    
  method handle_CP_JOIN =   
    drule CP_HANDLED,
    drule asm_rl[of "CP_JOIN _ _ _"],
    (simp only: prod_eq_iff conj_assoc)?,
    (((erule handle_join_take, blast) | erule handle_join_drop)+)?,
    ((erule handle_join_last_take, blast) | erule handle_join_last_drop),
    cp_resolve_tag

  subsubsection Repeat  
  lemma CP_RPT_split_conj: "CP_RPT (λa b. A a b  B a b) a b  CP_RPT A a b  CP_RPT B a b"
    by (simp add: CP_RPT_mono CP_tag_triv)  
    
  lemma handle_rpt_take:
    "CP_RPT (λa b. f b = f a) a b  f b = f a"  
    by (smt (verit, del_insts) CP_RPT_def rtranclp_induct)
    
  method handle_CP_RPT =  
    (drule CP_HANDLED),
    (elim CP_RPT_split_conj[elim_format] conjE handle_rpt_take[elim_format])?,
    cp_resolve_tag
          

  method cp_normalize_step =
    drule CP_monos[THEN CP_HANDLEI] | handle_plain_eqs|handle_CP_SEQ|handle_CP_EX|handle_CP_EX32|handle_CP_JOIN|handle_CP_RPT
    
  method cp_normalize =
    (simp only: CP_simps cong: CP_tag_cong)?;
    (determ cp_normalize_step)+  
    
    
  subsection High-Level Methods
  
  definition [CP_defs]: "CP_assm CP  (CP::bool)" ― ‹Assumption on concrete preconds
  definition [CP_defs]: "CP_cond CP  (CP::bool)" ― ‹Proof obligation on concrete preconds
  definition [CP_defs]: "CP_simplify A B  r. A r  B r" ― ‹Intermediate simp-step

  named_theorems cp_solve_cond_pre
  lemma [cp_solve_cond_pre]: "CP_cond True"
    by (auto simp: CP_defs)

  lemma cp_simplify_expose_assmI:
    assumes "CP_assm CP"
    assumes "CP  CP_TAG CP'"
    shows "CP'"
    using assms by (auto simp: CP_defs)
  
  method cp_simplify_expose_assm =
    determ drule cp_simplify_expose_assmI,
    determ ((thin_tac "_")+)?, rule impI,
    (cp_normalize;fail)
    
  method cp_solve_cond = 
    solves intro cp_solve_cond_pre |
    ((cp_simplify_expose_assm+)?;
     auto simp: CP_cond_def CP_pred_def CP_simps)

  lemma CP_simplify_triv: "CP_simplify (λ_. True) (λ_. True)"  
    by (auto simp: CP_defs)    
    
  lemma CP_simplifyI: 
    assumes "r. A r  CP_TAG (B r)"
    shows "CP_simplify A B"  
    using assms by (auto simp: CP_defs)

  method cp_simplify =
    rule CP_simplify_triv
    |
    rule CP_simplifyI,
    determ ((thin_tac "_")+)?, rule impI,
    (cp_normalize;fail)

    
  thm CP_simps  
    
end