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