Demand more in FutureAnalysisCarrier
authorJoachim Breitner <mail@joachim-breitner.de>
Fri, 19 Dec 2014 15:29:47 +0000 (15:29 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Fri, 19 Dec 2014 15:29:47 +0000 (15:29 +0000)
Launchbury/CoCallCardinality.thy
Launchbury/FTreeCardinality.thy

index dd8db08..2f53232 100644 (file)
@@ -41,7 +41,7 @@ by (auto simp add: Fexp.AnalBinds_lookup Fexp_def split: option.splits
          elim!: set_mp[OF edom_mono[OF monofun_cfun_fun[OF ABind_below_ABinds]]])
 
 sublocale FutureAnalysisCarrier Fexp
-  by default (rule carrier_Fexp')
+  apply default unfolding Fexp_simp carrier_ccFTree..
 
 sublocale FutureAnalysisCorrect Fexp
 proof default
@@ -260,7 +260,7 @@ next
       next
         case (up a')
         have subset: "(carrier (fup\<cdot>(Fexp e')\<cdot>((Aheap \<Delta> e\<cdot>a) x))) \<subseteq> fv e'"
-          using up e' by (simp add: Fexp.AnalBinds_lookup carrier_Fexp)
+          using up e' by (auto simp add: Fexp.AnalBinds_lookup carrier_Fexp dest!: set_mp[OF Aexp_edom])
         
         from e' up
         have "ccProd (fv e') (ccNeighbors (domA \<Delta>) (ccHeap \<Delta> e\<cdot>a)) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"  
index c551e5e..3e4bccc 100644 (file)
@@ -9,8 +9,8 @@ begin
   abbreviation "FBinds == Fexp.AnalBinds"
 end
 
-locale FutureAnalysisCarrier = FutureAnalysis +
-  assumes carrier_Fexp: "carrier (Fexp e\<cdot>a) \<subseteq> fv e"
+locale FutureAnalysisCarrier = FutureAnalysis + EdomArityAnalysis +
+  assumes carrier_Fexp: "carrier (Fexp e\<cdot>a) = edom (Aexp e\<cdot>a)"
 
 locale FutureAnalysisCorrect = FutureAnalysisCarrier +
   assumes Fexp_App: "many_calls x \<otimes>\<otimes> (Fexp e)\<cdot>(inc\<cdot>a) \<sqsubseteq> Fexp (App e x)\<cdot>a"
@@ -71,9 +71,8 @@ begin
   apply (simp add: Fexp.AnalBinds_lookup)
   apply (auto split: option.split simp add: empty_is_bottom[symmetric] )
   apply (case_tac "ae x")
-  apply (auto simp add: empty_is_bottom[symmetric] dest!: set_mp[OF carrier_Fexp])
+  apply (auto simp add: empty_is_bottom[symmetric] carrier_Fexp dest!: set_mp[OF Aexp_edom])
   by (metis (poly_guards_query) contra_subsetD domA_from_set map_of_fv_subset map_of_is_SomeD option.sel)
-
 end