Avoid theory-level interpretation
[darcs-mirror-isa-launchbury.git] / Launchbury / CallArityCorrectEnd2End.thy
1 theory CallArityCorrectEnd2End
2 imports CardinalityEtaExpand CoCallImplCorrect CoCallImplFTreeCorrect FTreeCardinality "~~/src/Tools/Permanent_Interpretation" 
3 begin
4
5 interpretation CoCallImplCorrect.
6
7 thm CardinalityArityTransformation.foo
8
9 print_locales
10 print_interps FTreeAnalysisCarrier
11 print_interps CardinalityPrognosisCorrectLet
12 print_interps CardinalityArityTransformation
13
14
15 permanent_interpretation CardinalityArityTransformation prognosis Aexp Aheap cHeap
16   defining final_consistent = consistent
17   and final_conf_transform = conf_transform
18   and final_transform = "AbstractTransform.transform (Rep_cfun inc) (Rep_cfun pred) (\<lambda>\<Delta> e a. (a, Aheap \<Delta> e\<cdot>a)) fst snd (\<lambda>a. Var) (\<lambda>a. Var1) (\<lambda>a. App) (\<lambda>a v e . Lam [v]. e)
19   (\<lambda>b \<Gamma>. Terms.Let (map_transform Aeta_expand (snd b) \<Gamma>))"
20    by default
21
22 lemma end2end:
23   "c \<Rightarrow>\<^sup>* c' \<Longrightarrow>
24   \<not> boring_step c' \<Longrightarrow>
25   consistent (ae, ce, a) c \<Longrightarrow>
26   \<exists>ae' ce' a'. consistent  (ae', ce', a') c' \<and> final_conf_transform  (ae, ce, a) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform  (ae', ce', a') c'"
27   by (rule foo)
28
29 lemma end2end_closed:
30   assumes closed: "fv e = ({} :: var set)"
31   assumes "([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>,v,[])"
32   assumes "isLam v"
33   shows "\<exists> \<Gamma>' v'. length \<Gamma>' \<le> length \<Gamma> \<and> isLam v' \<and> ([], final_transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (\<Gamma>',v',[])"
34 proof-
35   note assms(2)
36   moreover
37   have "\<not> boring_step (\<Gamma>,v,[])" by (simp add: boring_step.simps)
38   moreover
39   have "consistent (\<bottom>,\<bottom>,0) ([], e, [])" using closed by (rule closed_consistent)
40   ultimately
41   obtain ae ce a where
42     *: "consistent  (ae, ce, a) (\<Gamma>,v,[])" and
43     **: "final_conf_transform  (\<bottom>, \<bottom>, 0) ([],e,[]) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, a) (\<Gamma>,v,[])"
44     by (metis end2end)
45
46   let ?\<Gamma> = "restrictA (edom ce) (map_transform Aeta_expand ae (map_transform final_transform ae \<Gamma>))"
47   let ?v = "final_transform a v"
48
49   show ?thesis
50   proof(intro exI conjI)
51     show "length (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform final_transform ae \<Gamma>))) \<le> length \<Gamma>"
52       by (rule order_trans[OF length_restrictA_le]) simp
53
54     have "final_conf_transform  (\<bottom>, \<bottom>, 0) ([],e,[]) = ([],final_transform 0 e,[])" by simp
55     with **
56     show "([], final_transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (?\<Gamma>, ?v, [])" by simp
57
58     show "isLam (transform a v)" using `isLam v` by simp
59   qed
60 qed
61
62 lemma fresh_var_eqE[elim_format]: "fresh_var e = x \<Longrightarrow> x \<notin>  fv e"
63   by (metis fresh_var_not_free)
64
65 lemma example1:
66   fixes e :: exp
67   fixes f g x y z :: var
68   assumes Aexp_e: "\<And>a. Aexp e\<cdot>a = esing x\<cdot>(up\<cdot>a) \<squnion> esing y\<cdot>(up\<cdot>a)"
69   assumes ccExp_e: "\<And>a. CCexp e\<cdot>a = \<bottom>"
70   assumes [simp]: "final_transform 1 e = e"
71   assumes "isLam e"
72   assumes disj: "y \<noteq> f" "y \<noteq> g" "x \<noteq> y" "z \<noteq> f" "z \<noteq> g" "y \<noteq> x"
73   assumes fresh: "atom z \<sharp> e"
74   shows "final_transform 1 (let y be  App (Var f) g in (let x be e in (Var x))) = 
75          let y be (Lam [z]. App (App (Var f) g) z) in (let x be (Lam [z]. App e z) in (Var x))"
76 proof-
77   from arg_cong[where f = edom, OF Aexp_e]
78   have "x \<in> fv e" by simp (metis Aexp_edom' insert_subset)
79   hence "\<not> atom x \<sharp> e" by (simp add:fresh_def fv_def)
80   hence [simp]: "\<not> nonrec [(x,e)]"
81     by (simp add: nonrec_def)
82  
83   from `isLam e`
84   have [simp]: "thunks [(x, e)] = {}"
85     by (simp add: thunks_Cons)
86
87   have [simp]: "CCfix [(x, e)]\<cdot>(esing x\<cdot>(up\<cdot>1) \<squnion> esing y\<cdot>(up\<cdot>1), \<bottom>) = \<bottom>"
88     unfolding CCfix_def
89     apply (simp add: fix_bottom_iff ccBindsExtra_simp)
90     apply (simp add: ccBind_eq disj ccExp_e)
91     done
92
93   have [simp]: "Afix [(x, e)]\<cdot>(esing x\<cdot>(up\<cdot>1)) = esing x\<cdot>(up\<cdot>1) \<squnion> esing y\<cdot>(up\<cdot>1)"
94     unfolding Afix_def
95     apply simp
96     apply (rule fix_eqI)
97     apply (simp add: disj Aexp_e)
98     apply (case_tac "z x")
99     apply (auto simp add: disj Aexp_e)
100     done
101
102   have [simp]: "Aheap [(y, App (Var f) g)] (let x be e in Var x)\<cdot>1 = esing y\<cdot>((Aexp (let x be e in Var x )\<cdot>1) y)"
103     by (auto simp add:  Aheap_nonrec_simp ABind_nonrec_eq pure_fresh fresh_at_base disj)
104
105   have [simp]: "(Aexp (let x be e in Var x)\<cdot>1) = esing y\<cdot>(up\<cdot>1)"
106     by (simp add: env_restr_join disj)
107     
108   have [simp]: "Aheap [(x, e)] (Var x)\<cdot>1 = esing x\<cdot>(up\<cdot>1)"
109     by (simp add: env_restr_join disj)
110
111   have 1: "1 = inc\<cdot>0" apply (simp add: inc_def) apply transfer apply simp done
112   
113   have [simp]: "Aeta_expand 1 (App (Var f) g) = (Lam [z]. App (App (Var f) g) z)"
114     apply (simp add: 1 del: exp_assn.eq_iff)
115     apply (subst change_Lam_Variable[of z "fresh_var (App (Var f) g)"])
116     apply (auto simp add: fresh_Pair fresh_at_base pure_fresh disj intro!: flip_fresh_fresh  elim!: fresh_var_eqE)
117     done
118
119   have [simp]: "Aeta_expand 1 e = (Lam [z]. App e z)"
120     apply (simp add: 1 del: exp_assn.eq_iff)
121     apply (subst change_Lam_Variable[of z "fresh_var e"])
122     apply (auto simp add: fresh_Pair fresh_at_base pure_fresh disj fresh intro!: flip_fresh_fresh  elim!: fresh_var_eqE)
123     done
124
125
126   show ?thesis
127     by (simp del: Let_eq_iff add: map_transform_Cons map_transform_Nil disj[symmetric])
128 qed
129
130
131 end