Theory Sepref_HOL_Bindings (Isabelle2014: August 2014)

theory Sepref_HOL_Bindings
imports Sepref_Tool
begin

(* TODO: Move *)
lemma (in -) param_map_option[param]: "(map_option, map_option) ∈ (A -> B) -> ⟨A⟩option_rel -> ⟨B⟩option_rel"
  apply (intro fun_relI)
  apply (auto elim!: option_relE dest: fun_relD)
  done

(* TODO: Move to convenince lemmas ? *)
lemma return_refine_prop_return:
  assumes "nofail m"
  assumes "RETURN x ≤ \<Down>R m"
  obtains x' where "(x,x')∈R" "RETURN x' ≤ m"
  using assms
  by (auto simp: refine_pw_simps pw_le_iff)

subsection ‹Identity Relations›

definition "IS_PURE_ID R ≡ R = (λx y. \<up>(y=x))"
definition [simp]: "FORCE_PURE_ID R ≡ IS_PURE_ID R"

lemma IS_PURE_ID_I: "(!!x y. R x y = \<up>(y=x)) ==> IS_PURE_ID R"
  unfolding IS_PURE_ID_def
  by (auto intro!: ext)

lemma IS_PURE_ID_D: "IS_PURE_ID R ==> R=(λx y. \<up>(y=x))"
  unfolding IS_PURE_ID_def
  by (auto intro!: ext)

lemma IS_PURE_ID_trigger: "IS_PURE_ID R ==> IS_PURE_ID R" by simp
lemma FORCE_PURE_ID_trigger: "IS_PURE_ID R ==> FORCE_PURE_ID R" by simp

declaration {* Tagged_Solver.add_triggers 
  "Relators.relator_props_solver" @{thms IS_PURE_ID_trigger} *}

declaration {* Tagged_Solver.add_triggers 
  "Relators.force_relator_props_solver" @{thms FORCE_PURE_ID_trigger} *}

lemma IS_PURE_ID_alt_def: "IS_PURE_ID R <-> R = pure Id"
  by (auto simp: IS_PURE_ID_def pure_def)

lemma IS_PURE_ID_pure[relator_props]: "R=Id ==> IS_PURE_ID (pure R)"
  by (auto simp add: IS_PURE_ID_alt_def)
  
lemma IS_PURE_ID_pure_Id[solve_relator_props]: 
  "IS_PURE_ID (pure Id)"
  by (auto simp add: IS_PURE_ID_def pure_def)

(* Test: Id as constraint rules *)

lemma [constraint_rules, forced_constraint_rules]:
  "REL_IS_ID Id"
  "REL_IS_ID R ==> IS_PURE_ID (pure R)"
  by (simp_all add: IS_PURE_ID_alt_def)

lemma [constraint_rules]:
  "REL_IS_ID A ==> REL_IS_ID B ==> REL_IS_ID (A -> B)"
  "REL_IS_ID A ==> REL_IS_ID B ==> REL_IS_ID (A×⇩_rB)"
  "REL_IS_ID A ==> REL_IS_ID (⟨A⟩option_rel)"
  "REL_IS_ID A ==> REL_IS_ID (⟨A⟩list_rel)"
  "REL_IS_ID A ==> REL_IS_ID B ==> REL_IS_ID (⟨A,B⟩sum_rel)"
  by simp_all  

subsection ‹HOL Combinators›
lemma hn_if[sepref_comb_rules]:
  assumes P: "Γ ==>⇩_A Γ1 * hn_val bool_rel a a'"
  assumes RT: "a ==> hn_refine (Γ1 * hn_val bool_rel a a') b' Γ2b R b"
  assumes RE: "¬a ==> hn_refine (Γ1 * hn_val bool_rel a a') c' Γ2c R c"
  assumes IMP: "TERM If ==> Γ2b ∨⇩_A Γ2c ==>⇩_A Γ'"
  shows "hn_refine Γ (if a' then b' else c') Γ' R (If$(LIN_ANNOT a A)$b$c)"
  using P RT RE IMP[OF TERMI]
  unfolding APP_def PROTECT2_def LIN_ANNOT_def
  by (rule hnr_If)

lemma hn_let[sepref_comb_rules]:
  assumes P: "Γ ==>⇩_A Γ1 * hn_ctxt R v v'"
  assumes R: "!!x x'. hn_refine (Γ1 * hn_ctxt R x x') (f' x') 
    (Γ' x x') R2 (f x)"
  assumes F: "!!x x'. Γ' x x' ==>⇩_A Γ2 * hn_ctxt R' x x'"
  shows 
    "hn_refine Γ (Let v' f') (Γ2 * hn_ctxt R' v v') R2 (Let$(v⇧^L)$(λ⇩₂x. f x))"
  apply rule
  apply (rule cons_pre_rule[OF P])
  apply (vcg)
  apply (rule cons_post_rule)
  apply (rule hn_refineD[OF R])
  apply simp
  apply (rule ent_frame_fwd[OF F])
  apply (fr_rot 2)
  apply (fr_rot_rhs 1)
  apply (rule fr_refl)
  apply (rule ent_refl)
  apply sep_auto
  done

(* TODO: Copying is only needed if v is really destroyed! *)
lemma hn_let_nl[sepref_comb_rules]:
  assumes "hn_refine Γ t' Γ' R2 (bind$(COPY$v)$(λ⇩₂v. Let$(v⇧^L)$f))"
  shows "hn_refine Γ t' Γ' R2 (Let$(v⇧^N)$f)"
  using assms
  by simp


subsection ‹Basic HOL types›

lemmas [sepref_import_param] = 
  param_bool
  param_nat1
  param_int

lemma hn_nat[sepref_fr_rules]:
  "hn_refine emp (return x) emp (pure Id) (RETURN$(PR_CONST (x::nat)))"
  by rule (sep_auto simp: pure_def hn_ctxt_def)

lemma hn_int[sepref_fr_rules]:
  "hn_refine emp (return x) emp (pure Id) (RETURN$(PR_CONST (x::int)))"
  by rule (sep_auto simp: pure_def hn_ctxt_def)

subsection "Product"

definition hn_prod_aux :: "('a1=>'c1=>assn) => ('a2=>'c2=>assn) 
  => 'a1*'a2 => 'c1*'c2 => assn" where
  "hn_prod_aux P1 P2 a c ≡ case (a,c) of ((a1,a2),(c1,c2)) =>
  P1 a1 c1 * P2 a2 c2"

lemma hn_prod_pure_conv: "hn_prod_aux (pure R1) (pure R2) = pure (R1 ×⇩_r R2)"
  by (auto simp: pure_def hn_prod_aux_def intro!: ext)

lemmas [sepref_import_rewrite, sepref_normrel_eqs] = hn_prod_pure_conv[symmetric]

abbreviation "hn_prod P1 P2 ≡ hn_ctxt (hn_prod_aux P1 P2)"

lemma hn_prod_precise[constraint_rules]: 
  "precise P1 ==> precise P2 ==> precise (hn_prod_aux P1 P2)"
  apply rule
  apply (clarsimp simp: hn_prod_aux_def)
proof (rule conjI)
  fix F F' h as a b a' b' ap bp
  assume P1: "precise P1" and P2: "precise P2"
  assume F: "(h, as) \<Turnstile> P1 a ap * P2 b bp * F ∧⇩_A P1 a' ap * P2 b' bp * F'"

  from F have "(h, as) \<Turnstile> P1 a ap * (P2 b bp * F) ∧⇩_A P1 a' ap * (P2 b' bp * F')"
    by (simp add: star_aci)
  with preciseD[OF P1] show "a=a'" .
  from F have "(h, as) \<Turnstile> P2 b bp * (P1 a ap * F) ∧⇩_A P2 b' bp * (P1 a' ap * F')"
    by (simp add: star_aci)
  with preciseD[OF P2] show "b=b'" .
qed

lemma pure_prod[constraint_rules]: 
  assumes P1: "is_pure P1" and P2: "is_pure P2"
  shows "is_pure (hn_prod_aux P1 P2)"
proof -
  from P1 obtain P1' where P1': "!!x x'. P1 x x' = \<up>(P1' x x')"
    using is_pureE by blast
  from P2 obtain P2' where P2': "!!x x'. P2 x x' = \<up>(P2' x x')"
    using is_pureE by blast

  show ?thesis proof
    fix x x'
    show "hn_prod_aux P1 P2 x x' =
         \<up> (case (x, x') of ((a1, a2), c1, c2) => P1' a1 c1 ∧ P2' a2 c2)"
      unfolding hn_prod_aux_def
      apply (simp add: P1' P2' split: prod.split)
      done
  qed
qed


lemma hn_case_prod[sepref_comb_rules]:
  assumes P: "Γ==>⇩_AΓ1 * hn_prod P1 P2 p' p"
  assumes R: "!!a1 a2 a1' a2'. [|p'=(a1',a2')|] 
    ==> hn_refine (Γ1 * hn_ctxt P1 a1' a1 * hn_ctxt P2 a2' a2) (f a1 a2) 
          (Γh a1 a1' a2 a2') R (f' a1' a2')"
  assumes M: "!!a1 a1' a2 a2'. Γh a1 a1' a2 a2' 
    ==>⇩_A Γ' * hn_ctxt P1' a1' a1 * hn_ctxt P2' a2' a2"
  shows "hn_refine Γ (case_prod f p) (Γ' * hn_prod P1' P2' p' p)
    R (case_prod$(λ⇩₂a b. f' a b)$(p'⇧^L))"
  apply rule
  apply (rule cons_pre_rule[OF P])
  unfolding hn_prod_aux_def hn_ctxt_def
  apply vcg
  apply (simp split: prod.splits)
  apply (rule cons_post_rule)
  apply (simp only: star_assoc[symmetric])
  apply (rule hn_refineD[OF R[unfolded hn_ctxt_def]])
  apply simp_all
  apply solve_entails
  apply clarsimp
  apply assumption

  apply (rule ent_frame_fwd[OF M])
  apply frame_inference
  apply (simp only: hn_ctxt_def)
  apply solve_entails
  done

lemma hn_case_prod_nl[sepref_comb_rules]:
  assumes "hn_refine Γ t (Γ' * hn_prod P1' P2' p' p) 
    R (bind$(COPY$p')$(λ⇩₂p'. case_prod$(λ⇩₂a b. f' a b)$(p'⇧^L)))"
  shows "hn_refine Γ t (Γ' * hn_prod P1' P2' p' p) 
    R (case_prod$(λ⇩₂a b. f' a b)$(p'⇧^N))"
  using assms by simp
 

lemma hn_Pair[sepref_fr_rules]: "hn_refine 
  (hn_ctxt P1 x1 x1' * hn_ctxt P2 x2 x2')
  (return (x1',x2'))
  (hn_invalid x1 x1' * hn_invalid x2 x2')
  (hn_prod_aux P1 P2)
  (RETURN$(Pair$x1$x2))"
  unfolding hn_refine_def
  apply (sep_auto simp: hn_ctxt_def hn_prod_aux_def)
  done

lemma IS_PURE_ID_prod[relator_props]: "[|IS_PURE_ID R1; IS_PURE_ID R2|] 
  ==> IS_PURE_ID (hn_prod_aux R1 R2)"
  by (auto simp: hn_ctxt_def hn_prod_aux_def IS_PURE_ID_alt_def pure_def intro!: ext)
lemmas [constraint_rules] = IS_PURE_ID_prod


subsection "Option"
fun hn_option_aux :: "('a => 'c => assn) => 'a option => 'c option => assn" where
  "hn_option_aux P None None = emp"
| "hn_option_aux P (Some a) (Some c) = P a c"
| "hn_option_aux _ _ _ = false"

lemma hn_option_aux_simps[simp]:
  "hn_option_aux P None v' = \<up>(v'=None)"
  "hn_option_aux P v None = \<up>(v=None)"
  apply (cases v', simp_all)
  apply (cases v, simp_all)
  done

lemma hn_option_pure_conv: "hn_option_aux (pure R) = pure (⟨R⟩option_rel)"
  apply (intro ext)
  apply (rename_tac a c)
  apply (case_tac "(pure R,a,c)" rule: hn_option_aux.cases)
  by (auto simp: pure_def)

lemmas [sepref_import_rewrite, sepref_normrel_eqs] = hn_option_pure_conv[symmetric]


abbreviation "hn_option P ≡ hn_ctxt (hn_option_aux P)"

lemma hn_option_precise[constraint_rules]: 
  assumes "precise P"  
  shows "precise (hn_option_aux P)"
proof
  fix a a' p h F F'
  assume A: "h \<Turnstile> hn_option_aux P a p * F ∧⇩_A hn_option_aux P a' p * F'"
  thus "a=a'" proof (cases "(P,a,p)" rule: hn_option_aux.cases)
    case (2 _ av pv) hence [simp]: "a=Some av" "p=Some pv" by simp_all

    from A obtain av' where [simp]: "a'=Some av'" by (cases a', simp_all)

    from A have "h \<Turnstile> P av pv * F ∧⇩_A P av' pv * F'" by simp
    with `precise P` have "av=av'" by (rule preciseD)
    thus ?thesis by simp
  qed simp_all
qed

lemma pure_option[constraint_rules]: 
  assumes P: "is_pure P"
  shows "is_pure (hn_option_aux P)"
proof -
  from P obtain P' where P': "!!x x'. P x x' = \<up>(P' x x')"
    using is_pureE by blast

  show ?thesis proof
    fix x x'
    show "hn_option_aux P x x' =
         \<up> (case (x, x') of 
             (None,None) => True | (Some v, Some v') => P' v v' | _ => False
           )"
      apply (simp add: P' split: prod.split option.split)
      done
  qed
qed

lemma hn_case_option[sepref_comb_rules]:
  assumes P: "Γ==>⇩_AΓ1 * hn_option P p p'"
  assumes Rn: "p=None ==> hn_refine Γ1 fn' Γ2a R fn"
  assumes Rs: "!!x x'. [| p=Some x |] ==> 
    hn_refine (Γ1 * hn_ctxt P x x') (fs' x') (Γ2b x x') R (fs x)"
  assumes F2: "!!x x'. Γ2b x x' ==>⇩_A Γ2b' * hn_ctxt Px' x x'"
  assumes MERGE2: "TERM case_list ==> Γ2a ∨⇩_A Γ2b' ==>⇩_A Γ'"
  shows "hn_refine Γ (case_option fn' fs' p') (Γ' * hn_option Px' p p') R 
    (case_option$fn$(λ⇩₂x. fs x)$(p⇧^L))"
  apply rule
  apply (rule cons_pre_rule[OF P])
  unfolding hn_ctxt_def
  apply vcg
  apply (simp, intro impI)
  apply (rule cons_post_rule)
  apply (rule hn_refineD[OF Rn[unfolded hn_ctxt_def]])
  apply simp_all
  apply solve_entails
  apply clarsimp
  apply assumption
  apply (auto 
    simp: hn_ctxt_def 
    intro!: ent_star_mono ent_disjI1[OF MERGE2[OF TERMI]]) []

  apply (simp split: option.split, intro impI allI)
  apply (rule cons_post_rule)
  apply (rule hn_refineD[OF Rs[unfolded hn_ctxt_def]])
  apply assumption
  apply simp

  (* TODO: Fix frame-inference such that it handles cases like the one below *)
  apply (simp only: assn_aci)
  apply (rule ent_frame_fwd[OF F2])
  apply (fr_rot 2)
  apply (fr_rot_rhs 1)
  apply (rule fr_refl)
  apply (rule ent_refl)
  
  apply (rule ent_frame_fwd[OF ent_disjI2[OF MERGE2[OF TERMI]]])
  apply (fr_rot 2)
  apply (fr_rot_rhs 1)
  apply (rule fr_refl)
  apply (rule ent_refl)
  apply (simp add: hn_ctxt_def assn_aci)
  done

lemma hn_case_option_nl[sepref_comb_rules]:
  assumes "hn_refine Γ c Γ' R 
    (bind$(COPY$p)$(λ⇩₂p. case_option$fn$fs$(p⇧^L)))"
  shows "hn_refine Γ c Γ' R (case_option$fn$fs$(p⇧^N))"
  using assms by simp

lemma hn_None[sepref_fr_rules]:
  "hn_refine emp (return None) emp (hn_option_aux P) (RETURN$None)"
  by rule sep_auto

lemma hn_Some[sepref_fr_rules]: "hn_refine 
  (hn_ctxt P v v')
  (return (Some v'))
  (hn_invalid v v')
  (hn_option_aux P)
  (RETURN$(Some$v))"
  by rule (sep_auto simp: hn_ctxt_def)

definition "imp_option_eq eq a b ≡ case (a,b) of 
  (None,None) => return True
| (Some a, Some b) => eq a b
| _ => return False"

lemma hn_option_eq[sepref_comb_rules]:
  fixes a b :: "'a option"
  assumes F1: "Γ ==>⇩_A hn_option P a a' * hn_option P b b' * Γ1"
  assumes EQ: "!!va va' vb vb'. hn_refine 
    (hn_ctxt P va va' * hn_ctxt P vb vb' * Γ1)
    (eq' va' vb') 
    (Γ' va va' vb vb') 
    (pure bool_rel)
    (RETURN$(op=$LIN_ANNOT va Aa$LIN_ANNOT vb Ab))"
  assumes F2: 
    "!!va va' vb vb'. 
      Γ' va va' vb vb' ==>⇩_A hn_ctxt P va va' * hn_ctxt P vb vb' * Γ1"
  shows "hn_refine 
    Γ 
    (imp_option_eq eq' a' b') 
    (hn_option P a a' * hn_option P b b' * Γ1)
    (pure bool_rel) 
    (RETURN$(op=$LIN_ANNOT a Aa$LIN_ANNOT b Ab))"
  apply (rule hn_refine_cons_pre[OF F1])
  unfolding imp_option_eq_def
  apply rule
  apply (simp split: option.split add: hn_ctxt_def, intro impI conjI)

  apply (sep_auto split: option.split simp: hn_ctxt_def pure_def)
  apply (cases a, (sep_auto split: option.split simp: hn_ctxt_def pure_def)+)[]
  apply (cases a, (sep_auto split: option.split simp: hn_ctxt_def pure_def)+)[]
  apply (cases b, (sep_auto split: option.split simp: hn_ctxt_def pure_def)+)[]
  apply (rule cons_post_rule)
  apply (rule hn_refineD[OF EQ[unfolded hn_ctxt_def]])
  apply simp
  apply (rule ent_frame_fwd[OF F2[unfolded hn_ctxt_def]])
  apply (fr_rot 2)
  apply (fr_rot_rhs 1)
  apply (rule fr_refl)
  apply (rule ent_refl)
  apply (sep_auto simp: pure_def)
  done

lemma [pat_rules]: 
  "op=$a$None ≡ is_None$a"
  "op=$None$a ≡ is_None$a"
  apply (rule eq_reflection, simp split: option.split)+
  done

lemma hn_is_None[sepref_fr_rules]: "hn_refine 
  (hn_option P a a')
  (return (is_None a'))
  (hn_option P a a')
  (pure bool_rel)
  (RETURN$(is_None$a))"
  apply rule
  apply (sep_auto split: option.split simp: hn_ctxt_def pure_def)
  done

lemma (in -) sepref_the_complete:
  assumes "SIDE_PRECOND (x≠None)"
  shows "hn_refine 
    (hn_option R x xi) 
    (return (the xi)) 
    (hn_invalid x xi)
    (R)
    (RETURN$(the$x))"
    using assms
    apply (cases x)
    apply simp
    apply (cases xi)
    apply (simp add: hn_ctxt_def)
    apply rule
    apply (sep_auto simp: hn_ctxt_def)
    done

(* As the sepref_the_complete rule does not work for us 
  --- the assertion ensuring the side-condition gets decoupled from its variable by a copy-operation ---
  we use the following rule that only works for the identity relation *)
lemma (in -) sepref_the_id[sepref_fr_rules]:
  assumes "CONSTRAINT IS_PURE_ID R"
  shows "hn_refine 
    (hn_option R x xi) 
    (return (the xi)) 
    (hn_invalid x xi)
    (R)
    (RETURN$(the$x))"
    using assms 
    apply (simp add: IS_PURE_ID_alt_def hn_ctxt_def)
    apply (cases x)
    apply simp
    apply (cases xi)
    apply (simp add: hn_ctxt_def)
    apply rule apply (sep_auto simp: pure_def)
    apply rule apply (sep_auto)
    apply (simp add: hn_option_pure_conv)
    apply rule apply (sep_auto simp: pure_def)
    done

lemma IS_PURE_ID_option[relator_props]: "[|IS_PURE_ID R|] 
  ==> IS_PURE_ID (hn_option_aux R)"
  unfolding IS_PURE_ID_alt_def
  apply (intro ext)
  apply (rename_tac x y)
  apply (case_tac "(R,x,y)" rule: hn_option_aux.cases)
  apply (auto simp: hn_ctxt_def pure_def)
  done

lemmas [constraint_rules] = IS_PURE_ID_option

subsection "Lists"

fun hn_list_aux :: "('a => 'c => assn) => 'a list => 'c list => assn" where
  "hn_list_aux P [] [] = emp"
| "hn_list_aux P (a#as) (c#cs) = P a c * hn_list_aux P as cs"
| "hn_list_aux _ _ _ = false"

lemma hn_list_aux_simps[simp]:
  "hn_list_aux P [] l' = (\<up>(l'=[]))"
  "hn_list_aux P l [] = (\<up>(l=[]))"
  unfolding hn_ctxt_def
  apply (cases l')
  apply simp
  apply simp
  apply (cases l)
  apply simp
  apply simp
  done

lemma hn_list_aux_append[simp]:
  "length l1=length l1' ==> 
    hn_list_aux P (l1@l2) (l1'@l2') 
    = hn_list_aux P l1 l1' * hn_list_aux P l2 l2'"
  apply (induct rule: list_induct2)
  apply simp
  apply (simp add: star_assoc)
  done

lemma hn_list_pure_conv: "hn_list_aux (pure R) = pure (⟨R⟩list_rel)"
proof (intro ext)
  fix l li
  show "hn_list_aux (pure R) l li = pure (⟨R⟩list_rel) l li"
    apply (induction "pure R" l li rule: hn_list_aux.induct)
    by (auto simp: pure_def)
qed

lemmas [sepref_import_rewrite, sepref_normrel_eqs] = hn_list_pure_conv[symmetric]


abbreviation "hn_list P ≡ hn_ctxt (hn_list_aux P)"

lemma hn_list_simps[simp]:
  "hn_list P [] l' = (\<up>(l'=[]))"
  "hn_list P l [] = (\<up>(l=[]))"
  "hn_list P [] [] = emp"
  "hn_list P (a#as) (c#cs) = hn_ctxt P a c * hn_list P as cs"
  "hn_list P (a#as) [] = false"
  "hn_list P [] (c#cs) = false"
  unfolding hn_ctxt_def
  apply (cases l')
  apply simp
  apply simp
  apply (cases l)
  apply simp
  apply simp
  apply simp_all
  done

lemma hn_list_precise[constraint_rules]: "precise P ==> precise (hn_list_aux P)"
proof
  fix l1 l2 l h F1 F2
  assume P: "precise P"
  assume "h\<Turnstile>hn_list_aux P l1 l * F1 ∧⇩_A hn_list_aux P l2 l * F2"
  thus "l1=l2"
  proof (induct l arbitrary: l1 l2 F1 F2)
    case Nil thus ?case by simp
  next
    case (Cons a ls)
    from Cons obtain a1 ls1 where [simp]: "l1=a1#ls1"
      by (cases l1, simp)
    from Cons obtain a2 ls2 where [simp]: "l2=a2#ls2"
      by (cases l2, simp)
    
    from Cons.prems have M:
      "h \<Turnstile> P a1 a * hn_list_aux P ls1 ls * F1 
        ∧⇩_A P a2 a * hn_list_aux P ls2 ls * F2" by simp
    have "a1=a2"
      apply (rule preciseD[OF P, where a=a1 and a'=a2 and p=a
        and F= "hn_list_aux P ls1 ls * F1" 
        and F'="hn_list_aux P ls2 ls * F2"
        ])
      using M
      by (simp add: star_assoc)
    
    moreover have "ls1=ls2"
      apply (rule Cons.hyps[where ?F1.0="P a1 a * F1" and ?F2.0="P a2 a * F2"])
      using M
      by (simp only: star_aci)
    ultimately show ?case by simp
  qed
qed
lemma hn_list_pure[constraint_rules]: 
  assumes P: "is_pure P" 
  shows "is_pure (hn_list_aux P)"
proof -
  from P obtain P' where P_eq: "!!x x'. P x x' = \<up>(P' x x')" 
    by (rule is_pureE) blast

  {
    fix l l'
    have "hn_list_aux P l l' = \<up>(list_all2 P' l l')"
      by (induct P≡P l l' rule: hn_list_aux.induct)
         (simp_all add: P_eq)
  } thus ?thesis by rule
qed

lemma hn_list_mono: 
  "[|!!x x'. P x x'==>⇩_AP' x x'|] ==> hn_list P l l' ==>⇩_A hn_list P' l l'"
  unfolding hn_ctxt_def
  apply (induct P l l' rule: hn_list_aux.induct)
  by (auto intro: ent_star_mono)

lemma hn_case_list[sepref_comb_rules]:
  assumes P: "Γ ==>⇩_A Γ1 * hn_list P l l'"
  assumes Rn: "l=[] ==> hn_refine Γ1 fn' Γ2a R fn"
  assumes Rc: "!!x xs x' xs'. [| l=x#xs |] ==> 
    hn_refine (Γ1 * hn_ctxt P x x' * hn_list P xs xs') (fc' x' xs') 
      (Γ2b x xs x' xs') R (fc x xs)"
  assumes F2: "!!x xs x' xs'. Γ2b x xs x' xs' 
    ==>⇩_A Γ2b' * hn_ctxt Px' x x' * hn_ctxt Pxs' xs xs'"
  assumes MERGE2: "TERM case_list ==> Γ2a ∨⇩_A Γ2b' ==>⇩_A Γ'"
  shows "hn_refine Γ (case_list fn' fc' l') (Γ' * hn_invalid l l') R 
    (case_list$fn$(λ⇩₂x xs. fc x xs)$(l⇧^L))"
proof (cases l)
  case Nil[simp]

  from Rn have Rn':
    "nofail fn ==> 
      <Γ1> fn' <λr. ∃⇩_Ax. Γ2a * hn_ctxt R x r * true * \<up> (RETURN x ≤ fn)>"
    by (simp add: hn_refine_def hn_ctxt_def)

  show ?thesis
    apply (rule hn_refine_cons_pre[OF P])
    apply simp
    apply rule
    apply clarsimp
    apply (rule cons_post_rule)
    apply (erule Rn')
    apply (rule ent_ex_preI ent_ex_postI)+
    apply (auto 
      simp: hn_ctxt_def 
      intro!: ent_star_mono ent_disjI1[OF MERGE2[OF TERMI]])
    done
next
  case (Cons x xs)[simp]
  show ?thesis
  proof (cases l')
    case Nil thus ?thesis
      apply (rule_tac hn_refine_cons_pre[OF P])
      apply rule
      apply (simp)
      done
  next
    case (Cons x' xs')[simp]

    from Rc[OF `l=x#xs`] have Rc': "!!x' xs'.
      nofail (fc x xs) ==> <Γ1 * hn_ctxt P x x' * hn_list P xs xs'> fc' x' xs'
        <λr. ∃⇩_Axa. Γ2b x xs x' xs' * hn_ctxt R xa r * true *
                   \<up> (RETURN xa ≤ fc x xs)>"
      by (clarsimp simp: hn_refine_def hn_ctxt_def)

    show ?thesis
      apply (rule hn_refine_cons_pre[OF P])
      apply rule
      apply (clarsimp)
      apply (simp only: star_assoc[symmetric])
      apply (rule cons_post_rule)
      apply (erule Rc')
      apply (rule ent_ex_preI ent_ex_postI ent_star_mono)+
      apply (rule ent_trans)
      apply (rule F2)
      apply (simp add: hn_ctxt_def)
      apply (intro ent_true_drop)
      apply (rule ent_disjI2[OF MERGE2[OF TERMI]])
      unfolding hn_ctxt_def apply (rule ent_refl)+
      done
  qed
qed  

lemma hn_case_list_nl[sepref_comb_rules]:
  assumes "hn_refine Γ t' (Γ' * hn_invalid l l') R 
    (bind$(COPY$l)$(λ⇩₂l. case_list$fn$(λ⇩₂x xs. fc x xs)$(l⇧^L)))"
  shows "hn_refine Γ t' (Γ' * hn_invalid l l') R 
    (case_list$fn$(λ⇩₂x xs. fc x xs)$(l⇧^N))"
  using assms by simp

lemma hn_Nil[sepref_fr_rules]: 
  "hn_refine emp (return []) emp (hn_list_aux P) (RETURN$[])"
  unfolding hn_refine_def
  by sep_auto

lemma hn_Cons[sepref_fr_rules]: "hn_refine (hn_ctxt P x x' * hn_list P xs xs') 
  (return (x'#xs')) (hn_invalid x x' * hn_invalid xs xs') (hn_list_aux P)
  (RETURN$(op #$x$xs))"
  unfolding hn_refine_def
  by (sep_auto simp: hn_ctxt_def)

lemma hn_list_aux_len: 
  "hn_list_aux P l l' = hn_list_aux P l l' * \<up>(length l = length l')"
  apply (induct P≡P l l' rule: hn_list_aux.induct)
  apply simp_all
  apply (erule_tac t="hn_list_aux P as cs" in subst[OF sym])
  apply simp
  done

lemma hn_append[sepref_fr_rules]: "hn_refine (hn_list P l1 l1' * hn_list P l2 l2')
  (return (l1'@l2')) (hn_invalid l1 l1' * hn_invalid l2 l2') (hn_list_aux P)
  (RETURN$(op @$l1$l2))"
  apply rule
  apply (sep_auto simp: hn_ctxt_def)
  apply (subst hn_list_aux_len)
  apply (sep_auto simp: hn_list_aux_append)
  done


lemma pure_hn_list_eq_list_rel:
  "hn_val (⟨R⟩list_rel) = hn_list (pure R)"
proof (intro ext)
  fix a c
  show "hn_val (⟨R⟩list_rel) a c = hn_list (pure R) a c"
    apply (induct "pure R" a c rule: hn_list_aux.induct)
    apply (auto simp: hn_ctxt_def pure_def)
    apply (drule sym)
    apply (simp add: conj_commute)
    done
qed

lemma IS_PURE_ID_list[relator_props]: "[|IS_PURE_ID R|] 
  ==> IS_PURE_ID (hn_list_aux R)"
  unfolding IS_PURE_ID_alt_def
proof (simp,intro ext)
  fix x :: "'a list" and y :: "'a list"
  show "hn_list_aux (pure Id) x y = pure Id x y"
    apply (induction R x y rule: hn_list_aux.induct)
    apply (auto simp: pure_def)
    done
qed

lemmas [constraint_rules] = IS_PURE_ID_list



end