Add Null and (e ? e : e)
[darcs-mirror-isa-launchbury.git] / Launchbury / AbstractTransform.thy
1 theory AbstractTransform
2 imports Terms TransformTools
3 begin
4
5 locale AbstractAnalProp =
6   fixes PropApp :: "'a \<Rightarrow> 'a::cont_pt"
7   fixes PropLam :: "'a \<Rightarrow> 'a"
8   fixes AnalLet :: "heap \<Rightarrow> exp \<Rightarrow> 'a \<Rightarrow> 'b::cont_pt"
9   fixes PropLetBody :: "'b \<Rightarrow> 'a"
10   fixes PropLetHeap :: "'b\<Rightarrow> var \<Rightarrow> 'a\<^sub>\<bottom>"
11   assumes PropApp_eqvt: "\<pi> \<bullet> PropApp \<equiv> PropApp"
12   assumes PropLam_eqvt: "\<pi> \<bullet> PropLam \<equiv> PropLam"
13   assumes AnalLet_eqvt: "\<pi> \<bullet> AnalLet \<equiv> AnalLet"
14   assumes PropLetBody_eqvt: "\<pi> \<bullet> PropLetBody \<equiv> PropLetBody"
15   assumes PropLetHeap_eqvt: "\<pi> \<bullet> PropLetHeap \<equiv> PropLetHeap"
16
17 locale AbstractAnalPropSubst = AbstractAnalProp +
18   assumes AnalLet_subst:  "x \<notin> domA \<Gamma> \<Longrightarrow> y \<notin> domA \<Gamma> \<Longrightarrow> AnalLet (\<Gamma>[x::h=y]) (e[x::=y]) a = AnalLet \<Gamma> e a"
19
20 locale AbstractTransform = AbstractAnalProp +
21   constrains AnalLet :: "heap \<Rightarrow> exp \<Rightarrow> 'a::pure_cont_pt \<Rightarrow> 'b::cont_pt"
22   fixes TransVar :: "'a \<Rightarrow> var \<Rightarrow> exp"
23   fixes TransApp :: "'a \<Rightarrow> exp \<Rightarrow> var \<Rightarrow> exp"
24   fixes TransLam :: "'a \<Rightarrow> var \<Rightarrow> exp \<Rightarrow> exp"
25   fixes TransLet :: "'b \<Rightarrow> heap \<Rightarrow> exp \<Rightarrow> exp"
26   assumes TransVar_eqvt: "\<pi> \<bullet> TransVar = TransVar"
27   assumes TransApp_eqvt: "\<pi> \<bullet> TransApp = TransApp"
28   assumes TransLam_eqvt: "\<pi> \<bullet> TransLam = TransLam"
29   assumes TransLet_eqvt: "\<pi> \<bullet> TransLet = TransLet"
30   assumes SuppTransLam: "supp (TransLam a v e) \<subseteq> supp e - supp v"
31   assumes SuppTransLet: "supp (TransLet b \<Gamma> e) \<subseteq> supp (\<Gamma>, e) - atom ` domA \<Gamma>"
32 begin
33   nominal_function transform where
34     "transform a (App e x) = TransApp a (transform (PropApp a) e) x"
35   | "transform a (Lam [x]. e) = TransLam a x (transform (PropLam a) e)"
36   | "transform a (Var x) = TransVar a x"
37   | "transform a (Let \<Gamma> e) = TransLet (AnalLet \<Gamma> e a)
38         (map_transform transform (PropLetHeap (AnalLet \<Gamma> e a)) \<Gamma>)
39         (transform (PropLetBody (AnalLet \<Gamma> e a)) e)"
40   | "transform a Null = Null"
41   | "transform a (scrut ? e1 : e2)  = (transform a scrut ? transform a e1 : transform a e2)"
42 proof-
43 case goal1
44   note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] AnalLet_eqvt[eqvt_raw] TransVar_eqvt[eqvt]  TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
45   show ?case
46   unfolding eqvt_def transform_graph_aux_def
47     apply rule
48     apply perm_simp
49     apply (rule refl)
50     done
51   case (goal3 P x)
52     show ?case
53     proof (cases x)
54       fix a b
55       assume "x = (a, b)"
56       thus ?case
57       using goal3
58       apply (cases b rule:Terms.exp_strong_exhaust)
59       apply auto
60       done
61     qed
62   next
63 case (goal10 a x e a' x' e')
64   from goal10(5)
65   have "a' = a" and  "Lam [x]. e = Lam [x']. e'" by simp_all
66   from this(2)
67   show ?case
68   unfolding `a' = a`
69   proof(rule eqvt_lam_case)
70     fix \<pi> :: perm
71
72     have "supp (TransLam a x (transform_sumC (PropLam a, e))) \<subseteq> supp (Lam [x]. e)"
73       apply (rule subset_trans[OF SuppTransLam])
74       apply (auto simp add:  exp_assn.supp supp_Pair supp_at_base pure_supp exp_assn.fsupp dest!: set_mp[OF supp_eqvt_at[OF goal10(1)], rotated])
75       done
76     moreover
77     assume "supp \<pi> \<sharp>* (Lam [x]. e)" 
78     ultimately
79     have *: "supp \<pi> \<sharp>* TransLam a x (transform_sumC (PropLam a, e))" by (auto simp add: fresh_star_def fresh_def)
80
81     note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransVar_eqvt[eqvt] TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
82
83     have "TransLam a (\<pi> \<bullet> x) (transform_sumC (PropLam a, \<pi> \<bullet> e))
84         = TransLam a (\<pi> \<bullet> x) (transform_sumC (\<pi> \<bullet>  (PropLam a, e)))"
85       by perm_simp rule
86     also have "\<dots> = TransLam a (\<pi> \<bullet> x) (\<pi> \<bullet> transform_sumC (PropLam a, e))"
87       unfolding eqvt_at_apply'[OF goal10(1)]..
88     also have "\<dots> = \<pi> \<bullet> (TransLam a x (transform_sumC (PropLam a, e)))"
89       by simp
90     also have "\<dots> = TransLam a x (transform_sumC (PropLam a, e))"
91       by (rule perm_supp_eq[OF *])
92     finally show "TransLam a (\<pi> \<bullet> x) (transform_sumC (PropLam a, \<pi> \<bullet> e)) = TransLam a x (transform_sumC (PropLam a, e))" by simp
93   qed
94 next
95 case (goal19 a as body a' as' body')
96   note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw]  AnalLet_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransVar_eqvt[eqvt]  TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
97
98   from supp_eqvt_at[OF goal19(1)]
99   have "\<And> x e a. (x, e) \<in> set as \<Longrightarrow> supp (transform_sumC (a, e)) \<subseteq> supp e"
100     by (auto simp add: exp_assn.fsupp supp_Pair pure_supp)
101   hence supp_map: "\<And>ae. supp (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) ae as) \<subseteq> supp as"
102     by (rule supp_map_transform_step)
103
104   from goal19(9)
105   have "a' = a" and  "Terms.Let as body = Terms.Let as' body'" by simp_all
106   from this(2)
107   show ?case
108   unfolding `a' = a`
109   proof (rule eqvt_let_case)
110     have "supp (TransLet (AnalLet as body a) (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))) \<subseteq> supp (Let as body)"
111       by (auto simp add: Let_supp supp_Pair pure_supp exp_assn.fsupp
112                dest!: set_mp[OF supp_eqvt_at[OF goal19(2)], rotated] set_mp[OF SuppTransLet] set_mp[OF supp_map])
113     moreover
114     fix \<pi> :: perm
115     assume "supp \<pi> \<sharp>* Terms.Let as body"
116     ultimately
117     have *: "supp \<pi> \<sharp>* TransLet (AnalLet as body a) (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))"
118       by (auto simp add: fresh_star_def fresh_def)
119
120     have "TransLet (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a) (map_transform (\<lambda>x0 x1. (\<pi> \<bullet> transform_sumC) (x0, x1)) (PropLetHeap (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a)) (\<pi> \<bullet> as)) ((\<pi> \<bullet> transform_sumC) (PropLetBody (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a), \<pi> \<bullet> body)) = 
121         \<pi> \<bullet> TransLet (AnalLet as body a) (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))"
122        by (simp del: Let_eq_iff Pair_eqvt add:  eqvt_at_apply[OF goal19(2)])
123     also have "\<dots> = TransLet (AnalLet as body a) (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))"
124       by (rule perm_supp_eq[OF *])
125     also
126     have "map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a)) (\<pi> \<bullet> as)
127         = map_transform (\<lambda>x xa. (\<pi> \<bullet> transform_sumC) (x, xa)) (PropLetHeap (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a)) (\<pi> \<bullet> as)"
128         apply (rule map_transform_fundef_cong[OF _ refl refl])
129         apply (subst (asm) set_eqvt[symmetric])
130         apply (subst (asm) mem_permute_set)
131         apply (auto simp add: permute_self  dest: eqvt_at_apply''[OF goal19(1)[where aa = "(- \<pi> \<bullet> a)" for a], where p = \<pi>, symmetric])
132         done
133     moreover
134     have "(\<pi> \<bullet> transform_sumC) (PropLetBody (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a), \<pi> \<bullet> body) = transform_sumC (PropLetBody (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a), \<pi> \<bullet> body)"
135       using eqvt_at_apply''[OF goal19(2), where p = \<pi>] by perm_simp
136     ultimately
137     show "TransLet (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a) (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a)) (\<pi> \<bullet> as)) (transform_sumC (PropLetBody (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a), \<pi> \<bullet> body)) =
138           TransLet (AnalLet as body a) (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))" by metis
139     qed
140   qed auto
141   nominal_termination by lexicographic_order
142 end
143
144 locale AbstractTransformSubst = AbstractTransform + AbstractAnalPropSubst +
145   assumes TransVar_subst: "(TransVar a v)[x ::= y] = (TransVar a v[x ::v= y])"
146   assumes TransApp_subst: "(TransApp a e v)[x ::= y] = (TransApp a e[x ::= y] v[x ::v= y])"
147   assumes TransLam_subst: "atom v \<sharp> (x,y) \<Longrightarrow> (TransLam a v e)[x ::= y] = (TransLam a v[x ::v= y] e[x ::= y])"
148   assumes TransLet_subst: "atom ` domA \<Gamma> \<sharp>* (x,y) \<Longrightarrow> (TransLet b \<Gamma> e)[x ::= y] = (TransLet b \<Gamma>[x ::h= y] e[x ::= y])"
149 begin
150   lemma subst_transform: "(transform a e)[x ::= y] = transform a e[x ::= y]"
151   proof (nominal_induct e avoiding: x y arbitrary: a  rule: exp_strong_induct_set)
152   case (Let \<Delta> body x y)
153     hence *: "x \<notin> domA \<Delta>" "y \<notin> domA \<Delta>" by (auto simp add: fresh_star_def fresh_at_base)
154     hence "AnalLet \<Delta>[x::h=y] body[x::=y] a = AnalLet \<Delta> body a" by (rule AnalLet_subst)
155     with Let
156     show ?case
157     apply (auto simp add: fresh_star_Pair TransLet_subst simp del: Let_eq_iff)
158     apply (rule fun_cong[OF arg_cong[where f = "TransLet b" for b]])
159     apply (rule subst_map_transform)
160     apply simp
161     done
162   qed (simp_all add: TransVar_subst TransApp_subst TransLam_subst)
163 end
164
165
166 locale AbstractTransformBound = AbstractAnalProp + supp_bounded_transform  +
167   constrains PropApp :: "'a \<Rightarrow> 'a::pure_cont_pt"
168   constrains PropLetHeap :: "'b::cont_pt \<Rightarrow> var \<Rightarrow> 'a\<^sub>\<bottom>"
169   constrains trans :: "'c::cont_pt \<Rightarrow> exp \<Rightarrow> exp"
170   fixes PropLetHeapTrans :: "'b\<Rightarrow> var \<Rightarrow> 'c\<^sub>\<bottom>"
171   assumes PropLetHeapTrans_eqvt: "\<pi> \<bullet> PropLetHeapTrans = PropLetHeapTrans"
172   assumes TransBound_eqvt: "\<pi> \<bullet> trans = trans"
173 begin
174   sublocale AbstractTransform PropApp PropLam AnalLet PropLetBody PropLetHeap
175       "(\<lambda> a. Var)"
176       "(\<lambda> a. App)"
177       "(\<lambda> a. Terms.Lam)"
178       "(\<lambda> b \<Gamma> e . Let (map_transform trans (PropLetHeapTrans b) \<Gamma>) e)"
179   proof-
180   note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] AnalLet_eqvt[eqvt_raw] PropLetHeapTrans_eqvt[eqvt] TransBound_eqvt[eqvt]
181   case goal1
182   show ?case
183   apply default
184   apply ((perm_simp, rule)+)[4]
185   apply (auto simp add: exp_assn.supp supp_at_base)[1]
186   apply (auto simp add: Let_supp supp_Pair supp_at_base dest: set_mp[OF supp_map_transform])[1]
187   done
188   qed
189
190   lemma isLam_transform[simp]:
191     "isLam (transform a e) \<longleftrightarrow> isLam e"
192     by (induction e rule:isLam.induct) auto
193 end
194
195 locale AbstractTransformBoundSubst = AbstractAnalPropSubst + AbstractTransformBound + 
196   assumes TransBound_subst: "(trans a e)[x::=y] = trans a e[x::=y]"
197 begin
198   sublocale AbstractTransformSubst PropApp PropLam AnalLet PropLetBody PropLetHeap
199       "(\<lambda> a. Var)"
200       "(\<lambda> a. App)"
201       "(\<lambda> a. Terms.Lam)"
202       "(\<lambda> b \<Gamma> e . Let (map_transform trans (PropLetHeapTrans b) \<Gamma>) e)"
203   proof-
204   note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransBound_eqvt[eqvt]
205   case goal1
206   show ?case
207   apply default
208   apply simp_all[3]
209   apply (simp del: Let_eq_iff)
210   apply (rule arg_cong[where f = "\<lambda> x. Let x y" for y])
211   apply (rule subst_map_transform)
212   apply (simp add: TransBound_subst)
213   done
214   qed
215 end
216
217
218 end