69 | "CPS (Var x) = CFun Hole (x~)" |
69 | "CPS (Var x) = CFun Hole (x~)" |
70 | "atom b \<sharp> M \<Longrightarrow> CPSv (Abs y M) = Abs y (Abs b ((CPS M)<Var b>))" |
70 | "atom b \<sharp> M \<Longrightarrow> CPSv (Abs y M) = Abs y (Abs b ((CPS M)<Var b>))" |
71 | "atom b \<sharp> M \<Longrightarrow> CPS (Abs y M) = CFun Hole (Abs y (Abs b ((CPS M)<Var b>)))" |
71 | "atom b \<sharp> M \<Longrightarrow> CPS (Abs y M) = CFun Hole (Abs y (Abs b ((CPS M)<Var b>)))" |
72 | "CPSv (M $ N) = Abs x (Var x)" |
72 | "CPSv (M $ N) = Abs x (Var x)" |
73 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole" |
73 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole" |
74 | "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) = |
74 | "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> M \<Longrightarrow> CPS (M $ N) = |
75 ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))" |
75 ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))" |
76 | "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) = |
76 | "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) = |
77 ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))" |
77 ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))" |
78 | "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $ N) = |
78 | "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $ N) = |
79 ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $ Var b) Hole))))" |
79 ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $ Var b) Hole))))" |
80 apply auto |
80 apply auto |
|
81 defer |
|
82 apply (case_tac x) |
|
83 apply (rule_tac y="a" in lt.exhaust) |
|
84 apply auto |
|
85 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
|
86 apply (simp add: Abs1_eq_iff) |
|
87 apply blast+ |
|
88 apply (rule_tac y="b" in lt.exhaust) |
|
89 apply auto |
|
90 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
|
91 apply (simp add: Abs1_eq_iff) |
|
92 apply blast |
|
93 apply (rule_tac ?'a="name" in obtain_fresh) |
|
94 apply (rule_tac x="(lt1, lt2, a)" and ?'a="name" in obtain_fresh) |
|
95 apply (simp add: fresh_Pair_elim) |
|
96 apply (case_tac "isValue lt1", case_tac [!] "isValue lt2")[1] |
|
97 apply (simp_all add: fresh_Pair)[4] |
|
98 --"" |
|
99 apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh) |
|
100 apply (subgoal_tac "Abs b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Abs a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)") |
|
101 apply (subgoal_tac "Abs ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Abs a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)") |
|
102 apply (simp only:) |
|
103 apply (erule Abs_lst1_fcb) |
|
104 apply (simp add: Abs_fresh_iff) |
|
105 apply (simp_all add: Abs_fresh_iff lt.fresh fresh_Pair_elim fresh_at_base swap_fresh_fresh)[2] |
|
106 (* need an invariant to get eqvt_at (Proj) *) |
|
107 defer defer |
|
108 apply simp |
|
109 apply (simp_all add: Abs1_eq_iff fresh_Pair_elim fresh_at_base)[2] |
|
110 defer defer |
|
111 defer |
|
112 apply (simp add: Abs1_eq_iff fresh_at_base lt.fresh) |
|
113 apply (rule arg_cong) back |
|
114 defer |
|
115 apply (rule arg_cong) back |
|
116 defer |
|
117 apply (rule arg_cong) back |
|
118 defer |
81 oops --"The goals seem reasonable" |
119 oops --"The goals seem reasonable" |
82 |
120 |
83 end |
121 end |