theory ArityConsistent imports ArityAnalysisSpec ArityStack ArityAnalysisStack begin context ArityAnalysisLetSafe begin type_synonym astate = "(AEnv × Arity × Arity list)" inductive stack_consistent :: "Arity list ⇒ stack ⇒ bool" where "stack_consistent [] []" | "Astack S ⊑ a ⟹ stack_consistent as S ⟹ stack_consistent (a#as) (Alts e1 e2 # S)" | "stack_consistent as S ⟹ stack_consistent as (Upd x # S)" | "stack_consistent as S ⟹ stack_consistent as (Arg x # S)" inductive_simps stack_consistent_foo[simp]: "stack_consistent [] []" "stack_consistent (a#as) (Alts e1 e2 # S)" "stack_consistent as (Upd x # S)" "stack_consistent as (Arg x # S)" inductive_cases [elim!]: "stack_consistent as (Alts e1 e2 # S)" inductive a_consistent :: "astate ⇒ conf ⇒ bool" where a_consistentI: "edom ae ⊆ domA Γ ∪ upds S ⟹ Astack S ⊑ a ⟹ (ABinds Γ⋅ae ⊔ Aexp e⋅a ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae ⟹ stack_consistent as S ⟹ a_consistent (ae, a, as) (Γ, e, S)" inductive_cases a_consistentE: "a_consistent (ae, a, as) (Γ, e, S)" lemma a_consistent_restrictA: assumes "a_consistent (ae, a, as) (Γ, e, S)" assumes "edom ae ⊆ V" shows "a_consistent (ae, a, as) (restrictA V Γ, e, S)" proof- have "domA Γ ∩ V ∪ upds S ⊆ domA Γ ∪ upds S" by auto note * = below_trans[OF env_restr_mono2[OF this]] show " a_consistent (ae, a, as) (restrictA V Γ, e, S)" using assms by (auto simp add: a_consistent.simps env_restr_join join_below_iff ABinds_restrict_edom intro: * below_trans[OF env_restr_mono[OF ABinds_restrict_below]]) qed lemma a_consistent_edom_subsetD: "a_consistent (ae, a, as) (Γ, e, S) ⟹ edom ae ⊆ domA Γ ∪ upds S" by (rule a_consistentE) lemma a_consistent_stackD: "a_consistent (ae, a, as) (Γ, e, S) ⟹ Astack S ⊑ a" by (rule a_consistentE) lemma a_consistent_app⇩1: "a_consistent (ae, a, as) (Γ, App e x, S) ⟹ a_consistent (ae, inc⋅a, as) (Γ, e, Arg x # S)" by (auto simp add: join_below_iff env_restr_join a_consistent.simps dest!: below_trans[OF env_restr_mono[OF Aexp_App]] elim: below_trans) lemma a_consistent_app⇩2: assumes "a_consistent (ae, a, as) (Γ, (Lam [y]. e), Arg x # S)" shows "a_consistent (ae, (pred⋅a), as) (Γ, e[y::=x], S)" proof- have "Aexp (e[y::=x])⋅(pred⋅a) f|` (domA Γ ∪ upds S) ⊑ (env_delete y ((Aexp e)⋅(pred⋅a)) ⊔ esing x⋅(up⋅0)) f|` (domA Γ ∪ upds S)" by (rule env_restr_mono[OF Aexp_subst]) also have "… = env_delete y ((Aexp e)⋅(pred⋅a)) f|` (domA Γ ∪ upds S) ⊔ esing x⋅(up⋅0) f|` (domA Γ ∪ upds S)" by (simp add: env_restr_join) also have "env_delete y ((Aexp e)⋅(pred⋅a)) ⊑ Aexp (Lam [y]. e)⋅a" by (rule Aexp_Lam) also have "… f|` (domA Γ ∪ upds S) ⊑ ae" using assms by (auto simp add: join_below_iff env_restr_join a_consistent.simps) also have "esing x⋅(up⋅0) f|` (domA Γ ∪ upds S) ⊑ ae" using assms by (cases "x∈edom ae") (auto simp add: env_restr_join join_below_iff a_consistent.simps) also have "ae ⊔ ae = ae" by simp finally have "Aexp (e[y::=x])⋅(pred⋅a) f|` (domA Γ ∪ upds S) ⊑ ae" by this simp_all thus ?thesis using assms by (auto elim: below_trans edom_mono simp add: join_below_iff env_restr_join a_consistent.simps) qed lemma a_consistent_thunk_0: assumes "a_consistent (ae, a, as) (Γ, Var x, S)" assumes "map_of Γ x = Some e" assumes "ae x = up⋅0" shows "a_consistent (ae, 0, as) (delete x Γ, e, Upd x # S)" proof- from assms(2) have [simp]: "x ∈ domA Γ" by (metis domI dom_map_of_conv_domA) from assms(3) have [simp]: "x ∈ edom ae" by (auto simp add: edom_def) have "x ∈ domA Γ" by (metis assms(2) domI dom_map_of_conv_domA) hence [simp]: "insert x (domA Γ - {x} ∪ upds S) = (domA Γ ∪ upds S)" by auto from Abinds_reorder1[OF `map_of Γ x = Some e`] `ae x = up⋅0` have "ABinds (delete x Γ)⋅ae ⊔ Aexp e⋅0 = ABinds Γ⋅ae" by (auto intro: join_comm) moreover have "(… ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps) ultimately have "((ABinds (delete x Γ))⋅ae ⊔ Aexp e⋅0 ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" by simp then show ?thesis using `ae x = up⋅0` assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps) qed lemma a_consistent_thunk_once: assumes "a_consistent (ae, a, as) (Γ, Var x, S)" assumes "map_of Γ x = Some e" assumes [simp]: "ae x = up⋅u" assumes "heap_upds_ok (Γ, S)" shows "a_consistent (env_delete x ae, u, as) (delete x Γ, e, S)" proof- from assms(2) have [simp]: "x ∈ domA Γ" by (metis domI dom_map_of_conv_domA) from assms(1) have "Aexp (Var x)⋅a f|` (domA Γ ∪ upds S) ⊑ ae" by (auto simp add: join_below_iff env_restr_join a_consistent.simps) from fun_belowD[where x = x, OF this] have "(Aexp (Var x)⋅a) x ⊑ up⋅u" by simp from below_trans[OF Aexp_Var this] have "a ⊑ u" by simp from `heap_upds_ok (Γ, S)` have "x ∉ upds S" by (auto simp add: a_consistent.simps elim!: heap_upds_okE) hence [simp]: "(- {x} ∩ (domA Γ ∪ upds S)) = (domA Γ - {x} ∪ upds S)" by auto have "Astack S ⊑ u" using assms(1) `a ⊑ u` by (auto elim: below_trans simp add: a_consistent.simps) from Abinds_reorder1[OF `map_of Γ x = Some e`] `ae x = up⋅u` have "ABinds (delete x Γ)⋅ae ⊔ Aexp e⋅u = ABinds Γ⋅ae" by (auto intro: join_comm) moreover have "(… ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps) ultimately have "((ABinds (delete x Γ))⋅ae ⊔ Aexp e⋅u ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" by simp hence "((ABinds (delete x Γ))⋅(env_delete x ae) ⊔ Aexp e⋅u ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" by (auto simp add: join_below_iff env_restr_join elim: below_trans[OF env_restr_mono[OF monofun_cfun_arg[OF env_delete_below_arg]]]) hence "env_delete x (((ABinds (delete x Γ))⋅(env_delete x ae) ⊔ Aexp e⋅u ⊔ AEstack as S) f|` (domA Γ ∪ upds S)) ⊑ env_delete x ae" by (rule env_delete_mono) hence "(((ABinds (delete x Γ))⋅(env_delete x ae) ⊔ Aexp e⋅u ⊔ AEstack as S) f|` (domA (delete x Γ) ∪ upds S)) ⊑ env_delete x ae" by (simp add: env_delete_restr) then show ?thesis using `ae x = up⋅u` `Astack S ⊑ u` assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps elim : below_trans) qed lemma a_consistent_lamvar: assumes "a_consistent (ae, a, as) (Γ, Var x, S)" assumes "map_of Γ x = Some e" assumes [simp]: "ae x = up⋅u" shows "a_consistent (ae, u, as) ((x,e)# delete x Γ, e, S)" proof- have [simp]: "x ∈ domA Γ" by (metis assms(2) domI dom_map_of_conv_domA) have [simp]: "insert x (domA Γ ∪ upds S) = (domA Γ ∪ upds S)" by auto from assms(1) have "Aexp (Var x)⋅a f|` (domA Γ ∪ upds S) ⊑ ae" by (auto simp add: join_below_iff env_restr_join a_consistent.simps) from fun_belowD[where x = x, OF this] have "(Aexp (Var x)⋅a) x ⊑ up⋅u" by simp from below_trans[OF Aexp_Var this] have "a ⊑ u" by simp have "Astack S ⊑ u" using assms(1) `a ⊑ u` by (auto elim: below_trans simp add: a_consistent.simps) from Abinds_reorder1[OF `map_of Γ x = Some e`] `ae x = up⋅u` have "ABinds ((x,e) # delete x Γ)⋅ae ⊔ Aexp e⋅u = ABinds Γ⋅ae" by (auto intro: join_comm) moreover have "(… ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps) ultimately have "((ABinds ((x,e) # delete x Γ))⋅ae ⊔ Aexp e⋅u ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" by simp then show ?thesis using `ae x = up⋅u` `Astack S ⊑ u` assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps) qed lemma assumes "a_consistent (ae, a, as) (Γ, e, Upd x # S)" shows a_consistent_var⇩2: "a_consistent (ae, a, as) ((x, e) # Γ, e, S)" and a_consistent_UpdD: "ae x = up⋅0""a = 0" using assms by (auto simp add: join_below_iff env_restr_join a_consistent.simps elim:below_trans[OF env_restr_mono[OF ABinds_delete_below]]) lemma a_consistent_let: assumes "a_consistent (ae, a, as) (Γ, Let Δ e, S)" assumes "atom ` domA Δ ♯* Γ" assumes "atom ` domA Δ ♯* S" assumes "edom ae ∩ domA Δ = {}" shows "a_consistent (Aheap Δ e⋅a ⊔ ae, a, as) (Δ @ Γ, e, S)" proof- txt {* First some boring stuff about scope: *} have [simp]: "⋀ S. S ⊆ domA Δ ⟹ ae f|` S = ⊥" using assms(4) by auto have [simp]: "ABinds Δ⋅(Aheap Δ e⋅a ⊔ ae) = ABinds Δ⋅(Aheap Δ e⋅a)" by (rule Abinds_env_restr_cong) (simp add: env_restr_join) have [simp]: "Aheap Δ e⋅a f|` domA Γ = ⊥" using fresh_distinct[OF assms(2)] by (auto intro: env_restr_empty dest!: set_mp[OF edom_Aheap]) have [simp]: "ABinds Γ⋅(Aheap Δ e⋅a ⊔ ae) = ABinds Γ⋅ae" by (rule Abinds_env_restr_cong) (simp add: env_restr_join) have [simp]: "ABinds Γ⋅ae f|` (domA Δ ∪ domA Γ ∪ upds S) = ABinds Γ⋅ae f|` (domA Γ ∪ upds S)" using fresh_distinct_fv[OF assms(2)] by (auto intro: env_restr_cong dest!: set_mp[OF edom_AnalBinds]) have [simp]: "AEstack as S f|` (domA Δ ∪ domA Γ ∪ upds S) = AEstack as S f|` (domA Γ ∪ upds S)" using fresh_distinct_fv[OF assms(3)] by (auto intro: env_restr_cong dest!: set_mp[OF edom_AEstack]) have [simp]: "Aexp (Let Δ e)⋅a f|` (domA Δ ∪ domA Γ ∪ upds S) = Aexp (Terms.Let Δ e)⋅a f|` (domA Γ ∪ upds S)" by (rule env_restr_cong) (auto dest!: set_mp[OF Aexp_edom]) have [simp]: "Aheap Δ e⋅a f|` (domA Δ ∪ domA Γ ∪ upds S) = Aheap Δ e⋅a " by (rule env_restr_useless) (auto dest!: set_mp[OF edom_Aheap]) have "((ABinds Γ)⋅ae ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" using assms(1) by (auto simp add: a_consistent.simps join_below_iff env_restr_join) moreover have" Aexp (Let Δ e)⋅a f|` (domA Γ ∪ upds S) ⊑ ae" using assms(1) by (auto simp add: a_consistent.simps join_below_iff env_restr_join) moreover have "ABinds Δ⋅(Aheap Δ e⋅a) ⊔ Aexp e⋅a ⊑ Aheap Δ e⋅a ⊔ Aexp (Let Δ e)⋅a" by (rule Aexp_Let) ultimately have "(ABinds (Δ @ Γ)⋅(Aheap Δ e⋅a ⊔ ae) ⊔ Aexp e⋅a ⊔ AEstack as S) f|` (domA (Δ@Γ) ∪ upds S) ⊑ Aheap Δ e⋅a ⊔ ae" by (auto 4 4 simp add: env_restr_join Abinds_append_disjoint[OF fresh_distinct[OF assms(2)]] join_below_iff simp del: join_comm elim: below_trans below_trans[OF env_restr_mono]) moreover note fresh_distinct[OF assms(2)] moreover from fresh_distinct_fv[OF assms(3)] have "domA Δ ∩ upds S = {}" by (auto dest!: set_mp[OF ups_fv_subset]) ultimately show ?thesis using assms(1) by (auto simp add: a_consistent.simps dest!: set_mp[OF edom_Aheap] intro: heap_upds_ok_append) qed lemma a_consistent_if⇩1: assumes "a_consistent (ae, a, as) (Γ, scrut ? e1 : e2, S)" shows "a_consistent (ae, 0, a#as) (Γ, scrut, Alts e1 e2 # S)" proof- from assms have "Aexp (scrut ? e1 : e2)⋅a f|` (domA Γ ∪ upds S) ⊑ ae" by (auto simp add: a_consistent.simps env_restr_join join_below_iff) hence "(Aexp scrut⋅0 ⊔ Aexp e1⋅a ⊔ Aexp e2⋅a) f|` (domA Γ ∪ upds S) ⊑ ae" by (rule below_trans[OF env_restr_mono[OF Aexp_IfThenElse]]) thus ?thesis using assms by (auto simp add: a_consistent.simps join_below_iff env_restr_join) qed lemma a_consistent_if⇩2: assumes "a_consistent (ae, a, a'#as') (Γ, Bool b, Alts e1 e2 # S)" shows "a_consistent (ae, a', as') (Γ, if b then e1 else e2, S)" using assms by (auto simp add: a_consistent.simps join_below_iff env_restr_join) lemma a_consistent_alts_on_stack: assumes "a_consistent (ae, a, as) (Γ, Bool b, Alts e1 e2 # S)" obtains a' as' where "as = a' # as'" "a = 0" using assms by (auto simp add: a_consistent.simps) lemma closed_a_consistent: "fv e = ({}::var set) ⟹ a_consistent (⊥, 0, []) ([], e, [])" by (auto simp add: edom_empty_iff_bot a_consistent.simps dest!: set_mp[OF Aexp_edom]) end end