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