No need for heap_upds_ok in EtaExpandCorrect
authorJoachim Breitner <mail@joachim-breitner.de>
Tue, 20 Jan 2015 14:36:02 +0000 (14:36 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Tue, 20 Jan 2015 14:36:02 +0000 (14:36 +0000)
Launchbury/ArityConsistent.thy
Launchbury/ArityEtaExpandCorrect.thy
Launchbury/CardinalityEtaExpandCorrect.thy

index e14d025..7d3919e 100644 (file)
@@ -49,6 +49,10 @@ lemma a_consistent_stackD:
   "a_consistent (ae, a, as) (\<Gamma>, e, S) \<Longrightarrow> Astack S \<sqsubseteq> a"
   by (rule a_consistentE)
 
+lemma a_consistent_heap_upds_okD:
+  "a_consistent (ae, a, as) (\<Gamma>, e, S) \<Longrightarrow> heap_upds_ok (\<Gamma>, S)"
+  by (rule a_consistentE)
+
 lemma a_consistent_app\<^sub>1:
   "a_consistent (ae, a, as) (\<Gamma>, App e x, S) \<Longrightarrow> a_consistent (ae, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
   by (auto simp add: join_below_iff env_restr_join a_consistent.simps
index 66a3e18..7015e82 100644 (file)
@@ -54,7 +54,6 @@ begin
   inductive consistent :: "astate \<Rightarrow> conf \<Rightarrow> bool" where
     consistentI[intro!]: 
     "a_consistent (ae, a, as) (\<Gamma>, e, S)
-    \<Longrightarrow> heap_upds_ok (\<Gamma>, S)
     \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow>  ae x = up\<cdot>0)
     \<Longrightarrow> consistent (ae, a, as) (\<Gamma>, e, S)"  
   inductive_cases consistentE[elim!]: "consistent (ae, a, as) (\<Gamma>, e, S)"
@@ -90,10 +89,10 @@ begin
   case (thunk \<Gamma> x e S)
     hence "x \<in> thunks \<Gamma>" by auto
     hence [simp]: "x \<in> domA \<Gamma>" by (rule set_mp[OF thunks_domA])
-    hence "x \<notin> upds S" using thunk by (auto elim!: heap_upds_okE)
+
+    have "x \<notin> upds S" using thunk by (auto dest!: a_consistent_heap_upds_okD  heap_upds_okE)
     
     have "x \<in> edom ae" using thunk by auto
-  
     have "ae x = up\<cdot>0" using thunk `x \<in> thunks \<Gamma>` by (auto)
 
     have "a_consistent (ae, 0, as) (delete x \<Gamma>, e, Upd x # S)" using thunk `ae x = up\<cdot>0`
@@ -195,10 +194,6 @@ begin
       hence "(?ae \<squnion> ae) x = up\<cdot>0" by (auto simp add: Aheap_heap3)
     }
     moreover
-    have "heap_upds_ok (\<Gamma>, S)" using let\<^sub>1 by auto
-    with fresh_distinct[OF let\<^sub>1(1)]  `domA \<Delta> \<inter> upds S = {}`
-    have "heap_upds_ok (\<Delta> @ \<Gamma>, S)" by (rule heap_upds_ok_append)
-    moreover
     
     have "a_consistent (ae, a, as) (\<Gamma>, Let \<Delta> e, S)"
       using let\<^sub>1 by auto
index 2300068..30077d5 100644 (file)
@@ -60,7 +60,6 @@ begin
   inductive consistent :: "tstate \<Rightarrow> conf \<Rightarrow> bool" where
     consistentI[intro!]: 
     "a_consistent (ae, a, as) (restr_conf (edom ce) (\<Gamma>, e, S))
-    \<Longrightarrow> heap_upds_ok (\<Gamma>, S)
     \<Longrightarrow> edom ae = edom ce
     \<Longrightarrow> prognosis ae as a (\<Gamma>, e, S) \<sqsubseteq> ce
     \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
@@ -108,12 +107,13 @@ begin
   case (thunk \<Gamma> x e S)
     hence "x \<in> thunks \<Gamma>" by auto
     hence [simp]: "x \<in> domA \<Gamma>" by (rule set_mp[OF thunks_domA])
-    hence "x \<notin> upds S" using thunk by (auto elim!: heap_upds_okE)
 
     from thunk have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
     from below_trans[OF prognosis_called fun_belowD[OF this] ]
     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
 
+    have "x \<notin> upds S" using thunk by (auto dest!: a_consistent_heap_upds_okD  heap_upds_okE)
+
     have "x \<in> edom ae" using thunk by auto
     then obtain u where "ae x = up\<cdot>u" by (cases "ae x") (auto simp add: edom_def)
   
@@ -380,10 +380,6 @@ begin
     finally have "prognosis (?ae \<squnion> ae) as a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> ce" by this simp
     }
     moreover
-    have "heap_upds_ok (\<Gamma>, S)" using let\<^sub>1 by auto
-    with fresh_distinct[OF let\<^sub>1(1)]  `domA \<Delta> \<inter> upds S = {}`
-    have "heap_upds_ok (\<Delta> @ \<Gamma>, S)" by (rule heap_upds_ok_append)
-    moreover
     
     have "a_consistent (ae, a, as) (restrictA (edom ce) \<Gamma>, Let \<Delta> e, restr_stack (edom ce) S)"
       using let\<^sub>1 by auto