Theory EPAC_Perfectly

theory EPAC_Perfectly_Shared imports EPAC_Checker_Specification PAC_Checker.PAC_Checker (*for vars_llist*) EPAC_Checker (*for vars_llist*) begin text ‹We now introduce sharing of variables to make a more efficient representation possible.› section ‹Perfectly sharing of elements› subsection ‹Definition› type_synonym ('nat, 'string) shared_vars = ‹'string multiset × ('nat, 'string) fmap × ('string, 'nat) fmap› definition perfectly_shared_vars :: ‹'string multiset ⇒ ('nat, 'string) shared_vars ⇒ bool› where ‹perfectly_shared_vars 𝒱 = (λ(𝒟, V, V'). set_mset (dom_m V') = set_mset 𝒱 ∧ 𝒟 = 𝒱 ∧ (∀i ∈#dom_m V. fmlookup V' (the (fmlookup V i)) = Some i) ∧ (∀str ∈#dom_m V'. fmlookup V (the (fmlookup V' str)) = Some str) ∧ (∀i j. i∈#dom_m V ⟶ j∈#dom_m V ⟶ (fmlookup V i = fmlookup V j ⟷ i = j)))› abbreviation fmlookup_direct :: ‹('a, 'b) fmap ⇒ 'a ⇒ 'b› (infix "∝" 70) where ‹fmlookup_direct A b ≡ the (fmlookup A b)› lemma perfectly_shared_vars_simps: assumes ‹perfectly_shared_vars 𝒱 (VV')› shows ‹str ∈# 𝒱 ⟷ str ∈# dom_m (snd (snd VV'))› using assms unfolding perfectly_shared_vars_def apply auto done lemma perfectly_shared_add_new_var: fixes V :: ‹('nat, 'string) fmap› and v :: ‹'string› assumes ‹perfectly_shared_vars 𝒱 (D, V, V')› and ‹v ∉# 𝒱› and k_notin[simp]: ‹k ∉# dom_m V› shows ‹perfectly_shared_vars (add_mset v 𝒱) (add_mset v D, fmupd k v V, fmupd v k V')› proof - have DV[simp]: ‹D = 𝒱› and V'𝒱: ‹set_mset (dom_m V') = set_mset 𝒱› and map: ‹⋀i. i ∈#dom_m V ⟹ fmlookup V' (the (fmlookup V i)) = Some i› and map_str: ‹⋀str. str ∈#dom_m V' ⟹ fmlookup V (the (fmlookup V' str)) = Some str› and perfect: ‹⋀i j. i∈#dom_m V ⟹ j∈#dom_m V ⟹ fmlookup V i = fmlookup V j ⟷ i = j› using assms unfolding perfectly_shared_vars_def by auto have v_notin[simp]: ‹v ∉# dom_m V'› using V'𝒱 assms(2) by blast show ?thesis unfolding perfectly_shared_vars_def prod.simps proof (intro conjI allI ballI impI) show ‹add_mset v D = add_mset v 𝒱› using DV by auto show ‹set_mset (dom_m (fmupd v k V')) = set_mset (add_mset v 𝒱)› using V'𝒱 in_remove1_mset_neq by fastforce show ‹fmlookup (fmupd v k V') (fmupd k v V ∝ i) = Some i› if ‹i ∈# dom_m (fmupd k v V)› for i using map[of i] that v_notin by (auto dest!: indom_mI simp del: v_notin) show ‹fmlookup (fmupd k v V) (fmupd v k V' ∝ str) = Some str› if ‹str ∈# dom_m (fmupd v k V')› for str using map_str[of str] that k_notin by (auto dest!: indom_mI simp del: k_notin) show ‹(fmlookup (fmupd k v V) i = fmlookup (fmupd k v V) j) = (i = j)› if ‹i ∈# dom_m (fmupd k v V)› and ‹j ∈# dom_m (fmupd k v V)› for i j using perfect[of i j] that using indom_mI[of V i] map[of i] indom_mI[of V j] map[of j] indom_mI[of V' v] apply (auto simp: eq_commute[of ‹Some _› ‹fmlookup V _›]) done qed qed lemma perfectly_shared_vars_remove_update: assumes ‹perfectly_shared_vars (add_mset v 𝒱) (D, V, V')› and ‹v ∉# 𝒱› shows ‹perfectly_shared_vars 𝒱 (remove1_mset v D, fmdrop (V' ∝ v) V, fmdrop v V')› using assms unfolding perfectly_shared_vars_def by (fastforce simp: distinct_mset_dom distinct_mset_remove1_All) section ‹Refinement› datatype memory_allocation = Allocated | alloc_failed: Mem_Out type_synonym ('nat, 'string) vars = ‹'string multiset› definition perfectly_shared_var_rel :: ‹('nat,'string) shared_vars ⇒ ('nat × 'string) set› where ‹perfectly_shared_var_rel = (λ(𝒟, 𝒱, 𝒱'). br (λi. 𝒱 ∝ i) (λi. i ∈# dom_m 𝒱))› definition perfectly_shared_vars_rel :: ‹(('nat,'string) shared_vars × ('nat, 'string) vars) set› where ‹perfectly_shared_vars_rel = {(𝒜, 𝒱). perfectly_shared_vars 𝒱 𝒜}› definition find_new_idx :: ‹('nat,'string) shared_vars ⇒ _› where ‹find_new_idx = (λ(_, 𝒱, _). SPEC (λ(mem, k). ¬ alloc_failed mem ⟶ k ∉# dom_m 𝒱))› definition import_variableS :: ‹'string ⇒ ('nat, 'string) shared_vars ⇒ (memory_allocation × ('nat, 'string) shared_vars × 'nat) nres› where ‹import_variableS v = (λ(𝒟, 𝒱, 𝒱'). do { (mem, k) ← find_new_idx (𝒟, 𝒱, 𝒱'); if alloc_failed mem then do {k ← RES (UNIV :: 'nat set); RETURN (mem, (𝒟, 𝒱, 𝒱'), k)} else RETURN (Allocated, (add_mset v 𝒟, fmupd k v 𝒱, fmupd v k 𝒱'), k) })› definition import_variable :: ‹'string ⇒ ('nat, 'string) vars ⇒ (memory_allocation × ('nat, 'string) vars × 'string) nres› where ‹import_variable v = (λ𝒱. do { ASSERT(v ∉# 𝒱); SPEC(λ(mem, 𝒱', k::'string). ¬alloc_failed mem ⟶ 𝒱' = add_mset k 𝒱 ∧ k = v) })› definition is_new_variableS :: ‹'string ⇒ ('nat, 'string) shared_vars ⇒ bool nres› where ‹is_new_variableS v = (λ(𝒟, 𝒱, 𝒱'). RETURN (v ∉# dom_m 𝒱') )› definition is_new_variable :: ‹'string ⇒ ('nat, 'string) vars ⇒ bool nres› where ‹is_new_variable v = (λ𝒱'. RETURN (v ∉# 𝒱') )› lemma import_variableS_import_variable: fixes 𝒱 :: ‹('nat, 'string) vars› assumes ‹(𝒜, 𝒱) ∈ perfectly_shared_vars_rel› and ‹(v, v') ∈ Id› shows ‹import_variableS v 𝒜 ≤ ⇓({((mem, 𝒜', i), (mem', 𝒱', j)). mem = mem' ∧ (𝒜', 𝒱') ∈ perfectly_shared_vars_rel ∧ (¬alloc_failed mem' ⟶ (i, j) ∈ perfectly_shared_var_rel 𝒜') ∧ (∀xs. xs ∈ perfectly_shared_var_rel 𝒜 ⟶ xs ∈ perfectly_shared_var_rel 𝒜')}) (import_variable v' 𝒱)› using assms unfolding import_variableS_def import_variable_def find_new_idx_def by (refine_vcg lhs_step_If) (auto intro!: RETURN_RES_refine simp: perfectly_shared_add_new_var perfectly_shared_vars_rel_def perfectly_shared_var_rel_def br_def) lemma is_new_variable_spec: assumes ‹(𝒜, 𝒟𝒱) ∈ perfectly_shared_vars_rel› ‹(v,v') ∈ Id› shows ‹is_new_variableS v 𝒜 ≤ ⇓bool_rel (is_new_variable v' 𝒟𝒱)› using assms unfolding is_new_variable_def is_new_variableS_def by (auto simp: perfectly_shared_vars_rel_def perfectly_shared_vars_simps split: prod.splits) definition import_variables :: ‹'string list ⇒ ('nat, 'string) vars ⇒ (memory_allocation × ('nat, 'string) vars) nres› where ‹import_variables vs 𝒱 = do { (mem, 𝒱, _, _) ← WHILE_T(λ(mem, 𝒱, vs, _). ¬alloc_failed mem ∧ vs ≠ []) (λ(_, 𝒱, vs, vs'). do { ASSERT(vs ≠ []); let v = hd vs; a ← is_new_variable v 𝒱; if ¬a then RETURN (Allocated ,𝒱, tl vs, vs' @ [v]) else do { (mem, 𝒱, _) ← import_variable v 𝒱; RETURN(mem, 𝒱, tl vs, vs' @ [v]) } }) (Allocated, 𝒱, vs, []); RETURN (mem, 𝒱) }› definition import_variablesS :: ‹'string list ⇒ ('nat, 'string) shared_vars ⇒ (memory_allocation × ('nat, 'string) shared_vars) nres› where ‹import_variablesS vs 𝒱 = do { (mem, 𝒱, _) ← WHILE_T(λ(mem, 𝒱, vs). ¬alloc_failed mem ∧ vs ≠ []) (λ(_, 𝒱, vs). do { ASSERT(vs ≠ []); let v = hd vs; a ← is_new_variableS v 𝒱; if ¬a then RETURN (Allocated ,𝒱, tl vs) else do { (mem, 𝒱, _) ← import_variableS v 𝒱; RETURN(mem, 𝒱, tl vs) } }) (Allocated, 𝒱, vs); RETURN (mem, 𝒱) }› lemma import_variables_spec: ‹import_variables vs 𝒱 ≤ ⇓Id (SPEC(λ(mem, 𝒱'). ¬alloc_failed mem ⟶ set_mset 𝒱' = set_mset 𝒱 ∪ set vs))› proof - define I where ‹I ≡ (λ(mem, 𝒱', vs', vs''). (¬alloc_failed mem ⟶ (vs = vs'' @ vs') ∧ set_mset 𝒱' = set_mset 𝒱 ∪ set vs''))› show ?thesis unfolding import_variables_def is_new_variable_def apply (refine_vcg WHILET_rule[where I = ‹I› and R = ‹measure (λ(mem, 𝒱', vs', _). (if ¬alloc_failed mem then 1 else 0) + length vs')›] is_new_variable_spec) subgoal by auto subgoal unfolding I_def by auto subgoal by auto subgoal for s a b aa ba ab bb unfolding I_def by auto subgoal for s a b aa ba ab bb by auto subgoal by (clarsimp simp: neq_Nil_conv import_variable_def I_def) subgoal by (auto simp: I_def) done qed lemma import_variablesS_import_variables: assumes ‹(𝒱, 𝒱') ∈ perfectly_shared_vars_rel› and ‹(vs, vs') ∈ Id› shows ‹import_variablesS vs 𝒱 ≤ ⇓{(a,b). (a,b)∈Id ×_r perfectly_shared_vars_rel ∧ (¬alloc_failed (fst a) ⟶ perfectly_shared_var_rel 𝒱 ⊆ perfectly_shared_var_rel (snd a))} (import_variables vs' 𝒱')› proof - show ?thesis unfolding import_variablesS_def import_variables_def apply (refine_rcg WHILET_refine[where R = ‹{((mem, 𝒱𝒱, vs), (mem', 𝒱', vs', _)). (mem, mem') ∈ Id ∧ (𝒱𝒱, 𝒱') ∈ perfectly_shared_vars_rel ∧ (vs, vs') ∈ Id ∧ (¬alloc_failed mem ⟶ perfectly_shared_var_rel 𝒱 ⊆ perfectly_shared_var_rel 𝒱𝒱)}›] is_new_variable_spec import_variableS_import_variable) subgoal using assms by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed definition get_var_name :: ‹('nat, 'string) vars ⇒ 'string ⇒ 'string nres› where ‹get_var_name 𝒱 x = do { ASSERT(x ∈# 𝒱); RETURN x }› definition get_var_posS :: ‹('nat, 'string) shared_vars ⇒ 'string ⇒ 'nat nres› where ‹get_var_posS 𝒱 x = do { ASSERT(x ∈# dom_m (snd (snd 𝒱))); RETURN (snd (snd 𝒱) ∝ x) }› definition get_var_nameS :: ‹('nat, 'string) shared_vars ⇒ 'nat ⇒ 'string nres› where ‹get_var_nameS 𝒱 x = do { ASSERT(x ∈# dom_m (fst (snd 𝒱))); RETURN (fst (snd 𝒱) ∝ x) }› lemma get_var_posS_spec: fixes 𝒟𝒱 :: ‹('nat, 'string) vars› and 𝒜 :: ‹('nat, 'string) shared_vars› and x :: 'string assumes ‹(𝒜, 𝒟𝒱) ∈ perfectly_shared_vars_rel› and ‹(x,x') ∈ Id› shows ‹get_var_posS 𝒜 x ≤ ⇓(perfectly_shared_var_rel 𝒜) (get_var_name 𝒟𝒱 x')› using assms unfolding get_var_posS_def get_var_name_def apply refine_vcg apply (auto simp: perfectly_shared_var_rel_def perfectly_shared_vars_rel_def perfectly_shared_vars_simps br_def intro!: ASSERT_leI) apply (simp_all add: perfectly_shared_vars_def in_dom_m_lookup_iff) done abbreviation perfectly_shared_monom :: ‹('nat,'string) shared_vars ⇒ ('nat list × 'string list) set› where ‹perfectly_shared_monom 𝒱 ≡ ⟨perfectly_shared_var_rel 𝒱⟩list_rel › definition import_monom_no_newS :: ‹('nat, 'string) shared_vars ⇒ 'string list ⇒ (bool × 'nat list) nres› where ‹import_monom_no_newS 𝒜 xs = do { (new, _, xs) ← WHILE_T (λ(new, xs, _). ¬new ∧ xs ≠ []) (λ(_, xs, ys). do { ASSERT(xs ≠ []); let x = hd xs; b ← is_new_variableS x 𝒜; if b then RETURN (True, tl xs, ys) else do { x ← get_var_posS 𝒜 x; RETURN (False, tl xs, x # ys) } }) (False, xs, []); RETURN (new, rev xs) }› definition import_monom_no_new :: ‹('nat, 'string) vars ⇒ 'string list ⇒ (bool × 'string list) nres› where ‹import_monom_no_new 𝒜 xs = do { (new, _, xs) ← WHILE_T (λ(new, xs, _). ¬new ∧ xs ≠ []) (λ(_, xs, ys). do { ASSERT(xs ≠ []); let x = hd xs; b ← is_new_variable x 𝒜; if b then RETURN (True, tl xs, ys) else do { x ← get_var_name 𝒜 x; RETURN (False, tl xs, ys @ [x]) } }) (False, xs, []); RETURN (new, xs) }› lemma import_monom_no_new_spec: shows ‹import_monom_no_new 𝒜 xs ≤ ⇓ Id (SPEC(λ(new, ys). (new ⟷ ¬set xs ⊆ set_mset 𝒜) ∧ (¬new ⟶ ys = xs)))› unfolding import_monom_no_new_def is_new_variable_def get_var_name_def apply (refine_vcg WHILET_rule[where I = ‹(λ(new, ys, zs). (¬new ⟶ xs = zs @ ys) ∧ (¬new ⟶ set zs ⊆ set_mset 𝒜) ∧ (new ⟶ ¬set xs ⊆ set_mset 𝒜))› and R = ‹measure (λ(_, ys, _). length ys)›]) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: neq_Nil_conv) subgoal by (auto simp: neq_Nil_conv) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done lemma import_monom_no_newS_import_monom_no_new: assumes ‹(𝒜, 𝒱𝒟) ∈ perfectly_shared_vars_rel› ‹(xs, xs') ∈ Id› shows ‹import_monom_no_newS 𝒜 xs ≤ ⇓(bool_rel ×_r perfectly_shared_monom 𝒜) (import_monom_no_new 𝒱𝒟 xs')› using assms unfolding import_monom_no_new_def import_monom_no_newS_def apply (refine_rcg WHILET_refine[where R = ‹bool_rel ×_r ⟨Id⟩list_rel ×_r {(as, bs). (rev as, bs) ∈ perfectly_shared_monom 𝒜}›] is_new_variable_spec get_var_posS_spec) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (force simp: list_rel_append1) subgoal by auto done definition import_poly_no_newS :: ‹('nat, 'string) shared_vars ⇒ ('string list × 'a) list ⇒ (bool × ('nat list × 'a)list) nres› where ‹import_poly_no_newS 𝒜 xs = do { (new, _, xs) ← WHILE_T (λ(new, xs, _). ¬new ∧ xs ≠ []) (λ(_, xs, ys). do { ASSERT(xs ≠ []); let (x, n) = hd xs; (b, x) ← import_monom_no_newS 𝒜 x; if b then RETURN (True, tl xs, ys) else do { RETURN (False, tl xs, (x, n) # ys) } }) (False, xs, []); RETURN (new, rev xs) }› definition import_poly_no_new :: ‹('nat, 'string) vars ⇒ ('string list × 'a) list ⇒ (bool × ('string list × 'a) list) nres› where ‹import_poly_no_new 𝒜 xs = do { (new, _, xs) ← WHILE_T (λ(new, xs, _). ¬new ∧ xs ≠ []) (λ(_, xs, ys). do { ASSERT(xs ≠ []); let (x, n) = hd xs; (b, x) ← import_monom_no_new 𝒜 x; if b then RETURN (True, tl xs, ys) else do { RETURN (False, tl xs, ys @ [(x, n)]) } }) (False, xs, []); RETURN (new, xs) }› lemma import_poly_no_newS_import_poly_no_new: assumes ‹(𝒜, 𝒱𝒟) ∈ perfectly_shared_vars_rel› ‹(xs, xs') ∈ Id› shows ‹import_poly_no_newS 𝒜 xs ≤ ⇓(bool_rel ×_r ⟨perfectly_shared_monom 𝒜 ×_r Id⟩list_rel) (import_poly_no_new 𝒱𝒟 xs')› using assms unfolding import_poly_no_new_def import_poly_no_newS_def apply (refine_rcg WHILET_refine[where R = ‹bool_rel ×_r ⟨Id⟩list_rel ×_r {(as, bs). (rev as, bs) ∈ ⟨perfectly_shared_monom 𝒜 ×_r Id⟩list_rel}›] import_monom_no_newS_import_monom_no_new) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (force simp: list_rel_append1) subgoal by auto done lemma import_poly_no_new_spec: shows ‹import_poly_no_new 𝒜 xs ≤ ⇓ Id (SPEC(λ(new, ys). ¬new ⟶ ys = xs ∧ vars_llist xs ⊆ set_mset 𝒜))› proof - define I where [simp]: ‹I = (λ(new, ys, zs). ¬new ⟶ (xs = zs @ ys ∧ vars_llist zs ⊆ set_mset 𝒜))› show ?thesis unfolding import_poly_no_new_def is_new_variable_def get_var_name_def import_variable_def apply (refine_vcg import_monom_no_new_spec[THEN order_trans] WHILET_rule[where I = ‹I› and R = ‹measure (λ(mem, ys, _). (if mem then 0 else 1) + length ys)›]) subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: neq_Nil_conv) subgoal by auto subgoal by auto done qed definition import_monomS :: ‹('nat, 'string) shared_vars ⇒ 'string list ⇒ (_ × 'nat list × ('nat, 'string) shared_vars) nres› where ‹import_monomS 𝒜 xs = do { (new, _, xs, 𝒜) ← WHILE_T (λ(mem, xs, _, _). ¬alloc_failed mem ∧ xs ≠ []) (λ(_, xs, ys, 𝒜). do { ASSERT(xs ≠ []); let x = hd xs; b ← is_new_variableS x 𝒜; if b then do { (mem, 𝒜, x) ← import_variableS x 𝒜; if alloc_failed mem then RETURN (mem, xs, ys, 𝒜) else RETURN (mem, tl xs, x # ys, 𝒜) } else do { x ← get_var_posS 𝒜 x; RETURN (Allocated, tl xs, x # ys, 𝒜) } }) (Allocated, xs, [], 𝒜); RETURN (new, rev xs, 𝒜) }› definition import_monom :: ‹('nat, 'string) vars ⇒ 'string list ⇒ (memory_allocation × 'string list × ('nat, 'string) vars) nres› where ‹import_monom 𝒜 xs = do { (new, _, xs, 𝒜) ← WHILE_T (λ(new, xs, _, _). ¬alloc_failed new ∧ xs ≠ []) (λ(mem, xs, ys, 𝒜). do { ASSERT(xs ≠ []); let x = hd xs; b ← is_new_variable x 𝒜; if b then do { (mem, 𝒜, x) ← import_variable x 𝒜; if alloc_failed mem then RETURN (mem, xs, ys, 𝒜) else RETURN (mem, tl xs, ys @ [x], 𝒜) } else do { x ← get_var_name 𝒜 x; RETURN (mem, tl xs, ys @ [x], 𝒜) } }) (Allocated, xs, [], 𝒜); RETURN (new, xs, 𝒜) }› lemma import_monom_spec: shows ‹import_monom 𝒜 xs ≤ ⇓ Id (SPEC(λ(new, ys, 𝒜'). ¬alloc_failed new ⟶ ys = xs ∧ set_mset 𝒜' = set_mset 𝒜 ∪ set xs))› proof - define I where [simp]: ‹I = (λ(new, ys, zs, 𝒜'). ¬alloc_failed new ⟶ (xs = zs @ ys ∧ set_mset 𝒜' = set_mset 𝒜 ∪ set zs))› show ?thesis unfolding import_monom_def is_new_variable_def get_var_name_def import_variable_def apply (refine_vcg WHILET_rule[where I = ‹I› and R = ‹measure (λ(mem, ys, _). (if alloc_failed mem then 0 else 1) + length ys)›]) subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: neq_Nil_conv) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed definition import_polyS :: ‹('nat, 'string) shared_vars ⇒ ('string list × 'a) list ⇒ (memory_allocation × ('nat list × 'a)list × ('nat, 'string) shared_vars) nres› where ‹import_polyS 𝒜 xs = do { (mem,_, xs, 𝒜) ← WHILE_T (λ(mem, xs, _, _). ¬alloc_failed mem ∧ xs ≠ []) (λ(mem, xs, ys, 𝒜). do { ASSERT(xs ≠ []); let (x, n) = hd xs; (mem, x, 𝒜) ← import_monomS 𝒜 x; if alloc_failed mem then RETURN (mem, xs, ys, 𝒜) else do { RETURN (mem, tl xs, (x, n) # ys, 𝒜) } }) (Allocated, xs, [], 𝒜); RETURN (mem, rev xs, 𝒜) }› definition import_poly :: ‹('nat, 'string) vars ⇒ ('string list × 'a) list ⇒ (memory_allocation × ('string list × 'a) list × ('nat, 'string)vars) nres› where ‹import_poly 𝒜 xs0 = do { (new, _, xs, 𝒜) ← WHILE_T (λ(new, xs, _). ¬alloc_failed new ∧ xs ≠ []) (λ(_, xs, ys, 𝒜). do { ASSERT(xs ≠ []); let (x, n) = hd xs; (b, x, 𝒜) ← import_monom 𝒜 x; if alloc_failed b then RETURN (b, xs, ys, 𝒜) else do { RETURN (Allocated, tl xs, ys @ [(x, n)], 𝒜) } }) (Allocated, xs0, [], 𝒜); ASSERT(¬alloc_failed new ⟶ xs0 = xs); RETURN (new, xs, 𝒜) }› lemma import_poly_spec: fixes 𝒜 :: ‹('nat, 'string) vars› shows ‹import_poly 𝒜 xs ≤ ⇓ Id (SPEC(λ(new, ys, 𝒜'). ¬alloc_failed new ⟶ ys = xs ∧ set_mset 𝒜' = set_mset 𝒜 ∪ ⋃(set `fst ` set xs)))› proof - define I where [simp]: ‹I = (λ(new, ys, zs, 𝒜'). ¬alloc_failed new ⟶ (xs = zs @ ys ∧ set_mset 𝒜' = set_mset 𝒜 ∪ ⋃(set ` fst ` set zs)))› show ?thesis unfolding import_poly_def is_new_variable_def get_var_name_def import_variable_def apply (refine_vcg import_monom_spec[THEN order_trans] WHILET_rule[where I = ‹I› and R = ‹measure (λ(mem, ys, _). (if alloc_failed mem then 0 else 1) + length ys)›]) subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: neq_Nil_conv) subgoal by auto subgoal by auto subgoal by auto done qed lemma list_rel_append_single: ‹(xs, ys) ∈ ⟨R⟩list_rel ⟹ (x, y) ∈ R ⟹ (xs @ [x], ys @ [y]) ∈ ⟨R⟩list_rel› by (meson list_rel_append1 list_rel_simp(4) refine_list(1)) lemma list_rel_mono: ‹A ∈ ⟨R⟩list_rel ⟹ (⋀xs. xs ∈ R ⟹ xs ∈ R') ⟹ A ∈ ⟨R'⟩list_rel› unfolding list_rel_def apply (cases A) by (simp add: list_all2_mono) lemma import_monomS_import_monom: fixes 𝒱𝒟 :: ‹('nat, 'string) vars› and 𝒜₀ :: ‹('nat, 'string)shared_vars› and xs xs' :: ‹'string list› assumes ‹(𝒜₀, 𝒱𝒟) ∈ perfectly_shared_vars_rel› ‹(xs, xs') ∈ ⟨Id⟩list_rel› shows ‹import_monomS 𝒜₀ xs ≤ ⇓ {((mem, xs₀, 𝒜), (mem', ys₀, 𝒜')). mem = mem' ∧ (𝒜, 𝒜') ∈ perfectly_shared_vars_rel ∧ (¬alloc_failed mem ⟶ (xs₀, ys₀) ∈ perfectly_shared_monom 𝒜)∧ (¬alloc_failed mem ⟶ (∀xs. xs ∈ perfectly_shared_monom 𝒜₀ ⟶ xs ∈ perfectly_shared_monom 𝒜))} (import_monom 𝒱𝒟 xs')› using assms unfolding import_monom_def import_monomS_def apply (refine_rcg WHILET_refine[where R = ‹{((mem::memory_allocation, xs₀::'string list, zs₀::'nat list, 𝒜 :: ('nat, 'string)shared_vars), (mem', ys₀::'string list, zs₀'::'string list, 𝒜' :: ('nat, 'string)vars)). mem = mem' ∧ (𝒜, 𝒜') ∈ perfectly_shared_vars_rel ∧ (¬alloc_failed mem ⟶ (rev zs₀, zs₀') ∈ perfectly_shared_monom 𝒜) ∧ (xs₀, ys₀) ∈ ⟨Id⟩list_rel ∧ (¬alloc_failed mem ⟶ (∀xs. xs ∈ perfectly_shared_monom 𝒜₀ ⟶ xs ∈ perfectly_shared_monom 𝒜))}›] import_variableS_import_variable is_new_variable_spec get_var_posS_spec) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal apply (auto intro!: list_rel_append_single intro: list_rel_mono) by (metis (full_types) list_rel_mono surj_pair) subgoal by auto subgoal by auto subgoal using memory_allocation.exhaust_disc by (auto intro!: list_rel_append_single intro: list_rel_mono) subgoal by auto done abbreviation perfectly_shared_polynom :: ‹('nat,'string) shared_vars ⇒ (('nat list × int) list × ('string list × int) list) set› where ‹perfectly_shared_polynom 𝒱 ≡ ⟨perfectly_shared_monom 𝒱 ×_r int_rel⟩list_rel› abbreviation import_poly_rel :: ‹_› where ‹import_poly_rel 𝒜₀ xs' ≡ {((mem, xs₀, 𝒜), (mem', ys₀, 𝒜')). mem = mem' ∧ (¬alloc_failed mem ⟶ (𝒜, 𝒜') ∈ perfectly_shared_vars_rel ∧ ys₀ = xs' ∧ (xs₀, ys₀) ∈ perfectly_shared_polynom 𝒜) ∧ (¬alloc_failed mem ⟶ perfectly_shared_polynom 𝒜₀ ⊆ perfectly_shared_polynom 𝒜)}› lemma import_polyS_import_poly: assumes ‹(𝒜₀, 𝒱𝒟) ∈ perfectly_shared_vars_rel› ‹(xs, xs') ∈ ⟨⟨Id⟩list_rel×_rId⟩list_rel› shows ‹import_polyS 𝒜₀ xs ≤ ⇓(import_poly_rel 𝒜₀ xs) (import_poly 𝒱𝒟 xs')› using assms unfolding import_poly_def import_polyS_def apply (refine_rcg WHILET_refine[where R = ‹{((mem, zs, xs₀, 𝒜), (mem', zs', ys₀, 𝒜')). mem = mem' ∧ (𝒜, 𝒜') ∈ perfectly_shared_vars_rel ∧ (zs, zs') ∈ ⟨⟨Id⟩list_rel ×_r Id⟩list_rel ∧ (¬alloc_failed mem ⟶ (rev xs₀, ys₀) ∈ perfectly_shared_polynom 𝒜) ∧ (¬alloc_failed mem ⟶ perfectly_shared_polynom 𝒜₀ ⊆ perfectly_shared_polynom 𝒜)}›] import_monomS_import_monom) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: list_rel_append1) subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g xa x'a x1h x2h x1i x2i x1j x2j x1k x2k using memory_allocation.exhaust_disc[of x1h ‹x1h = Allocated›] by (auto intro!: list_rel_append_single intro: list_rel_mono) subgoal by auto done definition drop_content :: ‹'string ⇒ ('nat, 'string) vars ⇒ ('nat, 'string) vars nres› where ‹drop_content = (λv 𝒱'. do { ASSERT(v ∈# 𝒱'); RETURN (remove1_mset v 𝒱') })› definition drop_contentS :: ‹'string ⇒ ('nat, 'string) shared_vars ⇒ ('nat, 'string) shared_vars nres› where ‹drop_contentS = (λv (𝒟, 𝒱, 𝒱'). do { ASSERT(v ∈# dom_m 𝒱'); if count 𝒟 v = 1 then do { let i = 𝒱' ∝ v; RETURN (remove1_mset v 𝒟, fmdrop i 𝒱, fmdrop v 𝒱') } else RETURN (remove1_mset v 𝒟, 𝒱, 𝒱') })› lemma drop_contentS_drop_content: assumes ‹(𝒜, 𝒱𝒟) ∈ perfectly_shared_vars_rel› ‹(v, v') ∈ Id› shows ‹drop_contentS v 𝒜 ≤ ⇓perfectly_shared_vars_rel (drop_content v' 𝒱𝒟)› proof - have [simp]: ‹count xs x = 1 ⟹ y ∈# remove1_mset x xs ⟷ y ∈# xs ∧ x ≠y› for x xs y by (auto simp add: in_diff_count) have [simp]: ‹count xs x ≠ 1 ⟹ x ∈# xs ⟹ y ∈# remove1_mset x xs ⟷ y ∈# xs› for x xs y by (metis One_nat_def add_mset_remove_trivial_eq count_add_mset count_inI in_remove1_mset_neq) show ?thesis using assms unfolding drop_content_def drop_contentS_def apply refine_vcg apply (auto simp: perfectly_shared_vars_rel_def perfectly_shared_vars_def distinct_mset_dom distinct_mset_remove1_All) by (metis option.inject) qed definition perfectly_shared_strings_equal :: ‹('nat, 'string) vars ⇒ 'string ⇒ 'string ⇒ bool nres› where ‹perfectly_shared_strings_equal 𝒱 x y = do { ASSERT(x ∈# 𝒱 ∧ y ∈# 𝒱); RETURN (x = y) }› definition perfectly_shared_strings_equal_l :: ‹('nat,'string)shared_vars ⇒ 'nat ⇒ 'nat ⇒ bool nres› where ‹perfectly_shared_strings_equal_l 𝒱 x y = do { RETURN (x = y) }› lemma perfectly_shared_strings_equal_l_perfectly_shared_strings_equal: assumes ‹(𝒜, 𝒱) ∈ perfectly_shared_vars_rel› and ‹(x, x') ∈ perfectly_shared_var_rel 𝒜› and ‹(y, y') ∈ perfectly_shared_var_rel 𝒜› shows ‹perfectly_shared_strings_equal_l 𝒜 x y ≤ ⇓bool_rel (perfectly_shared_strings_equal 𝒱 x' y')› using assms unfolding perfectly_shared_strings_equal_l_def perfectly_shared_strings_equal_def perfectly_shared_vars_rel_def perfectly_shared_var_rel_def br_def by refine_rcg (auto simp: perfectly_shared_vars_def simp: add_mset_eq_add_mset dest!: multi_member_split) datatype(in -) ordered = LESS | EQUAL | GREATER | UNKNOWN definition (in -)perfect_shared_var_order :: ‹(nat, string)vars ⇒ string ⇒ string ⇒ ordered nres› where ‹perfect_shared_var_order 𝒟 x y = do { ASSERT(x ∈# 𝒟 ∧ y ∈# 𝒟); eq ← perfectly_shared_strings_equal 𝒟 x y; if eq then RETURN EQUAL else do { x ← get_var_name 𝒟 x; y ← get_var_name 𝒟 y; if (x, y) ∈ var_order_rel then RETURN (LESS) else RETURN (GREATER) } }› lemma var_roder_rel_total: ‹y ≠ ya ⟹ (y, ya) ∉ var_order_rel ⟹ (ya, y) ∈ var_order_rel› unfolding var_order_rel_def using less_than_char_linear lexord_linear by blast lemma perfect_shared_var_order_spec: assumes ‹xs ∈# 𝒱› ‹ys ∈# 𝒱› shows ‹perfect_shared_var_order 𝒱 xs ys ≤ ⇓ Id (SPEC(λb. ((b=LESS ⟶ (xs, ys) ∈ var_order_rel) ∧ (b=GREATER ⟶ (ys, xs) ∈ var_order_rel ∧ ¬(xs, ys) ∈ var_order_rel) ∧ (b=EQUAL ⟶ xs = ys)) ∧ b ≠ UNKNOWN))› using assms unfolding perfect_shared_var_order_def perfectly_shared_strings_equal_def nres_monad3 get_var_name_def by refine_vcg (auto dest: var_roder_rel_total) definition (in -) perfect_shared_term_order_rel_pre :: ‹(nat, string) vars ⇒ string list ⇒ string list ⇒ bool› where ‹perfect_shared_term_order_rel_pre 𝒱 xs ys ⟷ set xs ⊆ set_mset 𝒱 ∧ set ys ⊆ set_mset 𝒱› definition (in -) perfect_shared_term_order_rel :: ‹(nat, string) vars ⇒ string list ⇒ string list ⇒ ordered nres› where ‹perfect_shared_term_order_rel 𝒱 xs ys = do { ASSERT (perfect_shared_term_order_rel_pre 𝒱 xs ys); (b, _, _) ← WHILE_T (λ(b, xs, ys). b = UNKNOWN) (λ(b, xs, ys). do { if xs = [] ∧ ys = [] then RETURN (EQUAL, xs, ys) else if xs = [] then RETURN (LESS, xs, ys) else if ys = [] then RETURN (GREATER, xs, ys) else do { ASSERT(xs ≠ [] ∧ ys ≠ []); eq ← perfect_shared_var_order 𝒱 (hd xs) (hd ys); if eq = EQUAL then RETURN (b, tl xs, tl ys) else RETURN (eq, xs, ys) } }) (UNKNOWN, xs, ys); RETURN b }› lemma (in -)perfect_shared_term_order_rel_spec: assumes ‹set xs ⊆ set_mset 𝒱› ‹set ys ⊆ set_mset 𝒱› shows ‹perfect_shared_term_order_rel 𝒱 xs ys ≤ ⇓ Id (SPEC(λb. ((b=LESS ⟶ (xs, ys) ∈ term_order_rel) ∧ (b=GREATER ⟶ (ys, xs) ∈ term_order_rel) ∧ (b=EQUAL ⟶ xs = ys)) ∧ b ≠ UNKNOWN))› (is ‹_ ≤ ⇓ _ (SPEC (λb. ?f b ∧ b ≠ UNKNOWN))›) proof - define I where [simp]: ‹I= (λ(b, xs0, ys0). ?f b ∧ (∃xs'. xs = xs' @ xs0 ∧ ys = xs' @ ys0))› show ?thesis using assms unfolding perfect_shared_term_order_rel_def get_var_name_def perfectly_shared_strings_equal_def perfectly_shared_strings_equal_def apply (refine_vcg WHILET_rule[where I= ‹I› and R = ‹measure (λ(b, xs, ys). length xs + (if b = UNKNOWN then 1 else 0))›] perfect_shared_var_order_spec[THEN order_trans]) subgoal by (auto simp: perfect_shared_term_order_rel_pre_def) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: neq_Nil_conv lexord_append_leftI lexord_append_rightI) subgoal by auto subgoal by (auto simp: neq_Nil_conv lexord_append_leftI lexord_append_rightI) subgoal by auto subgoal by (auto simp: neq_Nil_conv lexord_append_leftI) subgoal by (auto simp: neq_Nil_conv) subgoal by ((subst conc_Id id_apply)+, rule SPEC_rule, rename_tac x, case_tac x) (auto simp: neq_Nil_conv intro: var_roder_rel_total intro!: lexord_append_leftI lexord_append_rightI) subgoal by (auto simp: neq_Nil_conv lexord_append_leftI) subgoal by (auto simp: neq_Nil_conv) subgoal by (auto simp: neq_Nil_conv) subgoal by (auto simp: neq_Nil_conv) done qed lemma (in-) trans_var_order_rel[simp]: ‹trans var_order_rel› unfolding trans_def var_order_rel_def apply (intro conjI impI allI) by (meson lexord_partial_trans trans_def trans_less_than_char) lemma (in-) term_order_rel_irreflexive: ‹(x1f, x1d) ∈ term_order_rel ⟹ (x1d, x1f) ∈ term_order_rel ⟹ x1f = x1d› using lexord_trans[of x1f x1d var_order_rel x1f] lexord_irreflexive[of var_order_rel x1f] by simp lemma get_var_nameS_spec: fixes 𝒟𝒱 :: ‹('nat, 'string) vars› and 𝒜 :: ‹('nat, 'string) shared_vars› and x' :: 'string assumes ‹(𝒜, 𝒟𝒱) ∈ perfectly_shared_vars_rel› and ‹(x,x') ∈ perfectly_shared_var_rel 𝒜› shows ‹get_var_nameS 𝒜 x ≤ ⇓(Id) (get_var_name 𝒟𝒱 x')› using assms unfolding get_var_nameS_def get_var_name_def apply refine_vcg apply (auto simp: perfectly_shared_var_rel_def perfectly_shared_vars_rel_def perfectly_shared_vars_simps br_def intro!: ASSERT_leI) done lemma get_var_nameS_spec2: fixes 𝒟𝒱 :: ‹('nat, 'string) vars› and 𝒜 :: ‹('nat, 'string) shared_vars› and x' :: 'string assumes ‹(𝒜, 𝒟𝒱) ∈ perfectly_shared_vars_rel› and ‹(x,x') ∈ perfectly_shared_var_rel 𝒜› ‹x' ∈# 𝒟𝒱› shows ‹get_var_nameS 𝒜 x ≤ ⇓(Id) (RETURN x')› apply (rule get_var_nameS_spec[THEN order_trans, OF assms(1,2)]) apply (use assms(3) in ‹auto simp: get_var_name_def›) done end

Theory EPAC_Perfectly_Shared