2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 1
header {* CPS conversion *}
2895
+ − 2
theory CPS1_Plotkin
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 3
imports Lt
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 4
begin
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 5
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 6
nominal_primrec
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 7
CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 8
where
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 9
"atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $ (x~)))"
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 10
| "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $ Lam x (M*))"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 11
| "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow>
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 12
(M $ N)* = Lam k (M* $ Lam m (N* $ Lam n (m~ $ n~ $ k~)))"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 13
unfolding eqvt_def CPS_graph_def
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 14
apply (rule, perm_simp, rule, rule)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 15
apply (simp_all add: fresh_Pair_elim)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 16
apply (rule_tac y="x" in lt.exhaust)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 17
apply (auto)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 18
apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 19
apply (simp_all add: fresh_at_base)[3]
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 20
apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 21
apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 22
apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 23
apply (simp add: fresh_Pair_elim fresh_at_base)
3089
+ − 24
apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
+ − 25
apply (simp add: fresh_Pair_elim fresh_at_base)[2]
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 26
apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 27
--"-"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 28
apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans)
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 29
apply (case_tac "k = ka")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 30
apply simp
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 31
apply(simp (no_asm) add: Abs1_eq_iff del:eqvts)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 32
apply (simp del: eqvts add: lt.fresh fresh_at_base)
3089
+ − 33
apply (simp only: lt.perm_simps(1) lt.perm_simps(2) flip_def[symmetric] lt.eq_iff)
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 34
apply (subst flip_at_base_simps(2))
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 35
apply simp
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 36
apply (intro conjI refl)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 37
apply (rule flip_fresh_fresh[symmetric])
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 38
apply (simp_all add: lt.fresh)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 39
apply (metis fresh_eqvt_at lt.fsupp)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 40
apply (case_tac "ka = x")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 41
apply simp_all[2]
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 42
apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 43
apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 44
--"-"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 45
apply (simp add: Abs1_eq(3))
2933
+ − 46
apply (erule Abs_lst1_fcb2)
+ − 47
apply (simp_all add: Abs_fresh_iff fresh_Nil fresh_star_def eqvt_at_def)[4]
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 48
--"-"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 49
apply (rename_tac k' M N m' n')
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 50
apply (subgoal_tac "atom k \<sharp> CPS_sumC M \<and> atom k' \<sharp> CPS_sumC M \<and> atom k \<sharp> CPS_sumC N \<and> atom k' \<sharp> CPS_sumC N \<and>
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 51
atom m \<sharp> CPS_sumC N \<and> atom m' \<sharp> CPS_sumC N")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 52
prefer 2
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 53
apply (intro conjI)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 54
apply (erule fresh_eqvt_at, simp add: finite_supp, assumption)+
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 55
apply clarify
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 56
apply (case_tac "k = k'", case_tac [!] "m' = k",case_tac [!]"m = k'",case_tac[!] "m = m'")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 57
apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 58
by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 59
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 60
termination (eqvt) by lexicographic_order
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 61
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 62
lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim]
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 63
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 64
lemma [simp]: "supp (M*) = supp M"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 65
by (induct rule: CPS.induct, simp_all add: lt.supp supp_at_base fresh_at_base fresh_def supp_Pair)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 66
(simp_all only: atom_eq_iff[symmetric], blast+)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 67
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 68
lemma [simp]: "x \<sharp> M* = x \<sharp> M"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 69
unfolding fresh_def by simp
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 70
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 71
nominal_primrec
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 72
convert:: "lt => lt" ("_+" [250] 250)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 73
where
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 74
"(Var x)+ = Var x"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 75
| "(Lam x M)+ = Lam x (M*)"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 76
| "(M $ N)+ = M $ N"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 77
unfolding convert_graph_def eqvt_def
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 78
apply (rule, perm_simp, rule, rule)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 79
apply (erule lt.exhaust)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 80
apply (simp_all)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 81
apply blast
2984
+ − 82
apply (simp add: Abs1_eq_iff CPS.eqvt)
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 83
by blast
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 84
2984
+ − 85
termination (eqvt)
+ − 86
by (relation "measure size") (simp_all)
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 87
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 88
lemma convert_supp[simp]:
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 89
shows "supp (M+) = supp M"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 90
by (induct M rule: lt.induct, simp_all add: lt.supp)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 91
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 92
lemma convert_fresh[simp]:
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 93
shows "x \<sharp> (M+) = x \<sharp> M"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 94
unfolding fresh_def by simp
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 95
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 96
lemma [simp]:
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 97
shows "isValue (p \<bullet> (M::lt)) = isValue M"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 98
by (nominal_induct M rule: lt.strong_induct) auto
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 99
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 100
nominal_primrec
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 101
Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt" (infixl ";" 100)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 102
where
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 103
"Kapply (Lam x M) K = K $ (Lam x M)+"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 104
| "Kapply (Var x) K = K $ Var x"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 105
| "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $ N) K = M+ $ N+ $ K"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 106
| "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 107
Kapply (M $ N) K = N; (Lam n (M+ $ Var n $ K))"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 108
| "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 109
Kapply (M $ N) K = M; (Lam m (N* $ (Lam n (Var m $ Var n $ K))))"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 110
unfolding Kapply_graph_def eqvt_def
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 111
apply (rule, perm_simp, rule, rule)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 112
apply (simp_all)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 113
apply (case_tac x)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 114
apply (rule_tac y="a" in lt.exhaust)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 115
apply (auto)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 116
apply (case_tac "isValue lt1")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 117
apply (case_tac "isValue lt2")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 118
apply (auto)[1]
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 119
apply (rule_tac x="(lt1, ba)" and ?'a="name" in obtain_fresh)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 120
apply (simp add: fresh_Pair_elim fresh_at_base)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 121
apply (rule_tac x="(lt2, ba)" and ?'a="name" in obtain_fresh)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 122
apply (rule_tac x="(a, ba)" and ?'a="name" in obtain_fresh)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 123
apply (simp add: fresh_Pair_elim fresh_at_base)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 124
apply (auto simp add: Abs1_eq_iff eqvts)[1]
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 125
apply (rename_tac M N u K)
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 126
apply (subgoal_tac "Lam n (M+ $ n~ $ K) = Lam u (M+ $ u~ $ K)")
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 127
apply (simp only:)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 128
apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1]
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 129
apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))")
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 130
apply (simp only:)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 131
apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 132
apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 133
apply (subgoal_tac "Ka = (m \<leftrightarrow> ma) \<bullet> Ka")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 134
apply (subgoal_tac "Ka = (n \<leftrightarrow> (m \<leftrightarrow> ma) \<bullet> na) \<bullet> Ka")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 135
apply (case_tac "m = ma")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 136
apply simp_all
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 137
apply rule
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 138
apply (auto simp add: flip_fresh_fresh[symmetric])
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 139
apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 140
done
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 141
2984
+ − 142
termination (eqvt)
+ − 143
by (relation "measure (\<lambda>(t, _). size t)") (simp_all)
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 144
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 145
section{* lemma related to Kapply *}
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 146
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 147
lemma [simp]: "isValue V \<Longrightarrow> V; K = K $ (V+)"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 148
by (nominal_induct V rule: lt.strong_induct) auto
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 149
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 150
section{* lemma related to CPS conversion *}
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 151
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 152
lemma value_CPS:
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 153
assumes "isValue V"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 154
and "atom a \<sharp> V"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 155
shows "V* = Lam a (a~ $ V+)"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 156
using assms
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 157
proof (nominal_induct V avoiding: a rule: lt.strong_induct, simp_all add: lt.fresh)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 158
fix name :: name and lt aa
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 159
assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Lam b (b~ $ lt+)"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 160
"atom aa \<sharp> lt \<or> aa = name"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 161
obtain ab :: name where b: "atom ab \<sharp> (name, lt, a)" using obtain_fresh by blast
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 162
show "Lam name lt* = Lam aa (aa~ $ Lam name (lt*))" using a b
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 163
by (simp add: Abs1_eq_iff fresh_at_base lt.fresh)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 164
qed
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 165
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 166
section{* first lemma CPS subst *}
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 167
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 168
lemma CPS_subst_fv:
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 169
assumes *:"isValue V"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 170
shows "((M[x ::= V])* = (M*)[x ::= V+])"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 171
using * proof (nominal_induct M avoiding: V x rule: lt.strong_induct)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 172
case (Var name)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 173
assume *: "isValue V"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 174
obtain a :: name where a: "atom a \<sharp> (x, name, V)" using obtain_fresh by blast
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 175
show "((name~)[x ::= V])* = (name~)*[x ::= V+]" using a
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 176
by (simp add: fresh_at_base * value_CPS)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 177
next
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 178
case (Lam name lt V x)
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 179
assume *: "atom name \<sharp> V" "atom name \<sharp> x" "\<And>b ba. isValue b \<Longrightarrow> (lt[ba ::= b])* = lt*[ba ::= b+]"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 180
"isValue V"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 181
obtain a :: name where a: "atom a \<sharp> (name, lt, lt[x ::= V], x, V)" using obtain_fresh by blast
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 182
show "(Lam name lt[x ::= V])* = Lam name lt*[x ::= V+]" using * a
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 183
by (simp add: fresh_at_base)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 184
next
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 185
case (App lt1 lt2 V x)
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 186
assume *: "\<And>b ba. isValue b \<Longrightarrow> (lt1[ba ::= b])* = lt1*[ba ::= b+]" "\<And>b ba. isValue b \<Longrightarrow> (lt2[ba ::= b])* = lt2*[ba ::= b+]"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 187
"isValue V"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 188
obtain a :: name where a: "atom a \<sharp> (lt1[x ::= V], lt1, lt2[x ::= V], lt2, V, x)" using obtain_fresh by blast
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 189
obtain b :: name where b: "atom b \<sharp> (lt2[x ::= V], lt2, a, V, x)" using obtain_fresh by blast
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 190
obtain c :: name where c: "atom c \<sharp> (a, b, V, x)" using obtain_fresh by blast
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 191
show "((lt1 $ lt2)[x ::= V])* = (lt1 $ lt2)*[x ::= V+]" using * a b c
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 192
by (simp add: fresh_at_base)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 193
qed
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 194
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 195
lemma [simp]: "isValue V \<Longrightarrow> isValue (V+)"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 196
by (nominal_induct V rule: lt.strong_induct, auto)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 197
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 198
lemma CPS_eval_Kapply:
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 199
assumes a: "isValue K"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 200
shows "(M* $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (M ; K)"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 201
using a
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 202
proof (nominal_induct M avoiding: K rule: lt.strong_induct, simp_all)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 203
case (Var name K)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 204
assume *: "isValue K"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 205
obtain a :: name where a: "atom a \<sharp> (name, K)" using obtain_fresh by blast
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 206
show "(name~)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ name~" using * a
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 207
by simp (rule evbeta', simp_all add: fresh_at_base)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 208
next
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 209
fix name :: name and lt K
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 210
assume *: "atom name \<sharp> K" "\<And>b. isValue b \<Longrightarrow> lt* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt ; b" "isValue K"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 211
obtain a :: name where a: "atom a \<sharp> (name, K, lt)" using obtain_fresh by blast
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 212
then have b: "atom name \<sharp> a" using fresh_PairD(1) fresh_at_base atom_eq_iff by metis
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 213
show "Lam name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Lam name (lt*)" using * a b
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 214
by simp (rule evbeta', simp_all)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 215
next
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 216
fix lt1 lt2 K
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 217
assume *: "\<And>b. isValue b \<Longrightarrow> lt1* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 ; b" "\<And>b. isValue b \<Longrightarrow> lt2* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; b" "isValue K"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 218
obtain a :: name where a: "atom a \<sharp> (lt1, lt2, K)" using obtain_fresh by blast
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 219
obtain b :: name where b: "atom b \<sharp> (lt1, lt2, K, a)" using obtain_fresh by blast
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 220
obtain c :: name where c: "atom c \<sharp> (lt1, lt2, K, a, b)" using obtain_fresh by blast
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 221
have d: "atom a \<sharp> lt1" "atom a \<sharp> lt2" "atom a \<sharp> K" "atom b \<sharp> lt1" "atom b \<sharp> lt2" "atom b \<sharp> K" "atom b \<sharp> a"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 222
"atom c \<sharp> lt1" "atom c \<sharp> lt2" "atom c \<sharp> K" "atom c \<sharp> a" "atom c \<sharp> b" using fresh_Pair a b c by simp_all
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 223
have "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K))" using * d
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 224
by (simp add: fresh_at_base) (rule evbeta', simp_all add: fresh_at_base)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 225
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 226
assume e: "isValue lt1"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 227
have "lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $ Lam c (b~ $ c~ $ K)) $ lt1+"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 228
using * d e by simp
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 229
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 230
by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 231
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 232
assume f: "isValue lt2"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 233
have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 234
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 235
by (rule evbeta', simp_all add: d e f)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 236
finally show ?thesis using * d e f by simp
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 237
next
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 238
assume f: "\<not> isValue lt2"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 239
have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam c (lt1+ $ c~ $ K)" using * d e f by simp
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 240
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 241
finally show ?thesis using * d e f by simp
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 242
qed
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 243
finally show ?thesis .
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 244
qed (metis Kapply.simps(5) isValue.simps(2) * d)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 245
finally show "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" .
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 246
qed
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 247
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 248
lemma Kapply_eval:
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 249
assumes a: "M \<longrightarrow>\<^isub>\<beta> N" "isValue K"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 250
shows "(M; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (N; K)"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 251
using assms
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 252
proof (induct arbitrary: K rule: eval.induct)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 253
case (evbeta x V M)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 254
fix K
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 255
assume a: "isValue K" "isValue V" "atom x \<sharp> V"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 256
have "Lam x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* (((M*)[x ::= V+]) $ K)"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 257
by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1)
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 258
also have "... = ((M[x ::= V])* $ K)" by (simp add: CPS_subst_fv a)
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 259
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" by (rule CPS_eval_Kapply, simp_all add: a)
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 260
finally show "(Lam x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" using a by simp
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 261
next
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 262
case (ev1 V M N)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 263
fix V M N K
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 264
assume a: "isValue V" "M \<longrightarrow>\<^isub>\<beta> N" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* N ; K" "isValue K"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 265
obtain a :: name where b: "atom a \<sharp> (V, K, M, N)" using obtain_fresh by blast
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 266
show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" proof (cases "isValue N")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 267
assume "\<not> isValue N"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 268
then show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by simp
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 269
next
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 270
assume n: "isValue N"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 271
have c: "M; Lam a (V+ $ a~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam a (V+ $ a~ $ K) $ N+" using a b by (simp add: n)
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 272
also have d: "... \<longrightarrow>\<^isub>\<beta>\<^sup>* V+ $ N+ $ K" by (rule evbeta') (simp_all add: a b n)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 273
finally show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by (simp add: n)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 274
qed
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 275
next
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 276
case (ev2 M M' N)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 277
assume *: "M \<longrightarrow>\<^isub>\<beta> M'" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; K" "isValue K"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 278
obtain a :: name where a: "atom a \<sharp> (K, M, N, M')" using obtain_fresh by blast
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 279
obtain b :: name where b: "atom b \<sharp> (a, K, M, N, M', N+)" using obtain_fresh by blast
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 280
have d: "atom a \<sharp> K" "atom a \<sharp> M" "atom a \<sharp> N" "atom a \<sharp> M'" "atom b \<sharp> a" "atom b \<sharp> K"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 281
"atom b \<sharp> M" "atom b \<sharp> N" "atom b \<sharp> M'" using a b fresh_Pair by simp_all
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 282
have "M $ N ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Lam a (N* $ Lam b (a~ $ b~ $ K))" using * d by simp
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 283
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue M'")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 284
assume "\<not> isValue M'"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 285
then show ?thesis using * d by (simp_all add: evs1)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 286
next
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 287
assume e: "isValue M'"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 288
then have "M' ; Lam a (N* $ Lam b (a~ $ b~ $ K)) = Lam a (N* $ Lam b (a~ $ b~ $ K)) $ M'+" by simp
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 289
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Lam b (a~ $ b~ $ K))[a ::= M'+]"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 290
by (rule evbeta') (simp_all add: fresh_at_base e d)
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 291
also have "... = N* $ Lam b (M'+ $ b~ $ K)" using * d by (simp add: fresh_at_base)
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 292
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue N")
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 293
assume f: "isValue N"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 294
have "N* $ Lam b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (M'+ $ b~ $ K) $ N+"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 295
by (rule eval_trans, rule CPS_eval_Kapply) (simp_all add: d e f * evs1)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 296
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" by (rule evbeta') (simp_all add: d e f evs1)
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 297
finally show ?thesis .
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 298
next
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 299
assume "\<not> isValue N"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 300
then show ?thesis using d e
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 301
by (metis CPS_eval_Kapply Kapply.simps(4) isValue.simps(2))
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 302
qed
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 303
finally show ?thesis .
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 304
qed
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 305
finally show ?case .
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 306
qed
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 307
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 308
lemma Kapply_eval_rtrancl:
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 309
assumes H: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* N" and "isValue K"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 310
shows "(M;K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (N;K)"
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 311
using H
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 312
by (induct) (metis Kapply_eval assms(2) eval_trans evs1)+
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 313
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 314
lemma
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 315
assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V"
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 316
shows "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 317
proof-
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 318
obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 319
have e: "Lam x (x~) = Lam y (y~)"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 320
by (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 321
have "M* $ Lam x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Lam x (x~)"
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 322
by(rule CPS_eval_Kapply,simp_all add: assms)
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 323
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Lam x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms)
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 324
also have "... = V ; Lam y (y~)" using e by (simp only:)
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 325
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" by (simp add: assms, rule evbeta') (simp_all add: assms *)
2998
f0fab367453a
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 326
finally show "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" .
2861
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 327
qed
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 328
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 329
end
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 330
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 331
5635a968fd3f
Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 332