More module splitting
[darcs-mirror-isa-launchbury.git] / Launchbury / NoCardinalityAnalysis.thy
1 theory NoCardinalityAnalysis
2 imports CardinalityAnalysisSpec
3 begin
4
5 locale NoCardinalityAnalysis = CorrectArityAnalysisLet +
6   assumes Aheap_thunk: "x \<in> thunks \<Gamma> \<Longrightarrow> (Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
7 begin
8
9 definition a2c :: "Arity\<^sub>\<bottom> \<rightarrow> two" where "a2c = (\<Lambda> a. if a \<sqsubseteq> \<bottom> then \<bottom> else many)"
10 lemma a2c_simp: "a2c\<cdot>a = (if a \<sqsubseteq> \<bottom> then \<bottom> else many)"
11   unfolding a2c_def by (rule beta_cfun[OF cont_if_else_above]) auto
12
13
14 lemma a2c_eqvt[eqvt]: "\<pi> \<bullet> a2c = a2c"
15   unfolding a2c_def
16   apply perm_simp
17   apply (rule Abs_cfun_eqvt)
18   apply (rule cont_if_else_above)
19   apply auto
20   done
21
22 definition ae2ce :: "AEnv \<Rightarrow> (var \<Rightarrow> two)" where "ae2ce ae x = a2c\<cdot>(ae x)"
23
24 lemma ae2ce_cont: "cont ae2ce"
25   by (auto simp add: ae2ce_def) 
26 lemmas cont_compose[OF ae2ce_cont, cont2cont, simp]
27
28 lemma ae2ce_eqvt[eqvt]: "\<pi> \<bullet> ae2ce ae x = ae2ce (\<pi> \<bullet> ae) (\<pi> \<bullet> x)"
29   unfolding ae2ce_def by perm_simp rule
30
31 lemma ae2ce_to_env_restr: "ae2ce ae = (\<lambda>_ . many) f|` edom ae"
32   by (auto simp add: ae2ce_def lookup_env_restr_eq edom_def a2c_simp)
33
34 lemma edom_ae2ce[simp]: "edom (ae2ce ae) = edom ae"
35   unfolding edom_def
36   by (auto simp add: ae2ce_def  a2c_simp)
37
38
39 definition cHeap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> (var \<Rightarrow> two)"
40   where "cHeap \<Gamma> e = (\<Lambda> a. ae2ce (Aheap \<Gamma> e\<cdot>a))"
41 lemma cHeap_simp[simp]: "cHeap \<Gamma> e\<cdot>a = ae2ce (Aheap \<Gamma> e\<cdot>a)"
42   unfolding cHeap_def by simp
43
44 sublocale CardinalityHeap cHeap.
45
46 sublocale CardinalityHeapCorrect cHeap Aheap
47   apply default
48   apply (erule Aheap_thunk)
49   apply simp
50   done
51
52 fun prognosis where 
53   "prognosis ae a (\<Gamma>, e, S) = ((\<lambda>_. many) f|` (edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp e\<cdot>a) \<union> ap S))"
54
55 lemma record_all_noop[simp]:
56   "record_call x\<cdot>((\<lambda>_. many) f|` S) = (\<lambda>_. many) f|` S"
57   by (auto simp add: record_call_def lookup_env_restr_eq)
58
59 sublocale CardinalityPrognosis prognosis.
60
61 sublocale CardinalityPrognosisShape prognosis
62 proof
63   case goal1 thus ?case by (simp cong: Abinds_env_restr_cong)
64 next
65   case goal2 thus ?case by (simp cong: Abinds_reorder)
66 next
67   case goal3 thus ?case by (auto intro!: env_restr_mono2 dest: set_mp[OF edom_mono[OF ABinds_delete_below]])
68 next
69   case goal4 thus ?case by auto
70 next
71   case goal5
72   show ?case by (auto intro: env_restr_mono2 )
73 next
74   case goal6
75   from `ae x = \<bottom>`
76   have "ABinds (delete x \<Gamma>)\<cdot>ae = ABinds \<Gamma>\<cdot>ae" by (rule ABinds_delete_bot)
77   thus ?case by simp
78 next
79   case goal7
80   from Aexp_Var[where n = a and x = x]
81   have "(Aexp (Var x)\<cdot>a) x \<noteq> \<bottom>" by auto
82   hence "x \<in> edom (Aexp (Var x)\<cdot>a)" by (simp add: edomIff)
83   thus ?case by simp
84 qed
85
86 sublocale CardinalityPrognosisApp prognosis
87 proof
88   case goal1 thus ?case
89     using edom_mono[OF Aexp_App] by (auto intro!: env_restr_mono2)
90 qed
91
92 sublocale CardinalityPrognosisLam prognosis
93 proof
94   case goal1
95   have "edom (Aexp e[y::=x]\<cdot>(pred\<cdot>a)) \<subseteq> insert x (edom (env_delete y (Aexp e\<cdot>(pred\<cdot>a))))"
96     by (auto dest: set_mp[OF edom_mono[OF Aexp_subst]] )
97   also have "\<dots> \<subseteq> insert x (edom (Aexp (Lam [y]. e)\<cdot>a))"
98     using edom_mono[OF Aexp_Lam] by auto
99   finally show ?case by (auto intro!: env_restr_mono2)
100 qed
101
102 sublocale CardinalityPrognosisVar prognosis
103 proof
104   case goal1
105   thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF goal1(1)])
106 next
107   case goal2
108   thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF goal2(1)])
109 next
110   case goal3
111   have "fup\<cdot>(Aexp e)\<cdot>(ae x) \<sqsubseteq> Aexp e\<cdot>0" by (cases "ae x") (auto intro: monofun_cfun_arg)
112   from edom_mono[OF this]
113   show ?case by (auto intro!: env_restr_mono2 dest: set_mp[OF edom_mono[OF ABinds_delete_below]])
114 qed
115   
116 sublocale CardinalityPrognosisLet prognosis  cHeap Aheap
117 proof
118   case goal1
119
120   from set_mp[OF goal1(3)] fresh_distinct[OF goal1(1)] fresh_distinct_fv[OF goal1(2)]
121   have  "ae f|` domA \<Delta> = \<bottom>"
122     by (auto dest: set_mp[OF ups_fv_subset])
123   hence [simp]: "ABinds \<Delta>\<cdot>(ae \<squnion> Aheap \<Delta> e\<cdot>a) = ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)" by (simp cong: Abinds_env_restr_cong add: env_restr_join)
124
125   from  fresh_distinct[OF goal1(1)]
126   have "Aheap \<Delta> e\<cdot>a f|` domA \<Gamma> = \<bottom>" by (auto dest!: set_mp[OF edom_Aheap])
127   hence [simp]: "ABinds \<Gamma>\<cdot>(ae \<squnion> Aheap \<Delta> e\<cdot>a) = ABinds \<Gamma>\<cdot>ae" by (simp cong: Abinds_env_restr_cong add: env_restr_join)
128   
129   have "edom (ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) \<union> edom (Aexp e\<cdot>a)  = edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union>  edom (Aexp e\<cdot>a) "
130     by (simp add: Abinds_append_disjoint[OF fresh_distinct[OF goal1(1)]] Un_commute)
131   also have "\<dots> = edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)"
132     by force
133   also have "\<dots> \<subseteq> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Let \<Delta> e)\<cdot>a)"
134     using  edom_mono[OF Aexp_Let] by force
135   also have "\<dots> = edom (Aheap \<Delta> e\<cdot>a) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)"
136     by auto
137   finally
138   have "edom (ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) \<union> edom (Aexp e\<cdot>a) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp (Terms.Let \<Delta> e)\<cdot>a)".
139   hence "edom (ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) \<union> edom (Aexp e\<cdot>a) \<union> ap S \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp (Terms.Let \<Delta> e)\<cdot>a) \<union> ap S" by auto
140   thus ?case by (simp add: ae2ce_to_env_restr env_restr_join2 Un_assoc[symmetric] env_restr_mono2)
141 qed
142
143 sublocale CardinalityPrognosisEdom prognosis
144   by default (auto dest: set_mp[OF Aexp_edom] set_mp[OF ap_fv_subset] set_mp[OF edom_AnalBinds])
145
146
147 sublocale CardinalityPrognosisCorrect prognosis cHeap Aheap Aexp..
148 end
149
150 end