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