55 apply(simp) |
55 apply(simp) |
56 apply(simp) |
56 apply(simp) |
57 apply(simp) |
57 apply(simp) |
58 apply(simp) |
58 apply(simp) |
59 apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff]) |
59 apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff]) |
60 apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (ECons cenva x (evals enva t2a), t)") |
60 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva x (evals enva t2a), t)") |
61 apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (enva, t2a)") |
61 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (enva, t2a)") |
62 apply (subgoal_tac "eqvt_at (\<lambda>(a,b). evals a b) (ECons cenva xa (evals enva t2a), ta)") |
62 apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa (evals enva t2a), ta)") |
63 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva x (evals enva t2a), t))") |
63 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva x (evals enva t2a), t))") |
64 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))") |
64 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))") |
65 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))") |
65 apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))") |
|
66 apply(erule conjE)+ |
66 defer |
67 defer |
67 apply (simp_all add: eqvt_at_def evals_def)[3] |
68 apply (simp_all add: eqvt_at_def evals_def)[3] |
|
69 apply(simp) |
|
70 defer |
|
71 apply(erule_tac c="(cenv, env)" in Abs_lst1_fcb2') |
|
72 apply(rule fresh_eqvt_at) |
|
73 back |
|
74 apply(simp add: eqvt_at_def) |
68 sorry |
75 sorry |
69 |
76 |
70 (* can probably not proved by a trivial size argument *) |
77 (* can probably not proved by a trivial size argument *) |
71 termination sorry |
78 termination sorry |
72 |
79 |
|
80 nominal_primrec |
|
81 reify :: "sem \<Rightarrow> lam" and |
|
82 reifyn :: "neu \<Rightarrow> lam" |
|
83 where |
|
84 "reify (L env y t) = (fresh_fun (\<lambda>x::name. Lam [x]. (reify (evals (ECons env y (N (V x))) t))))" |
|
85 | "reify (N n) = reifyn n" |
|
86 | "reifyn (V x) = Var x" |
|
87 | "reifyn (A n d) = App (reifyn n) (reify d)" |
|
88 defer |
|
89 defer |
|
90 --"completeness" |
|
91 apply(case_tac x) |
|
92 apply(simp) |
|
93 apply(case_tac a rule: sem_neu_env.exhaust(1)) |
|
94 apply(metis)+ |
|
95 apply(case_tac b rule: sem_neu_env.exhaust(2)) |
|
96 apply(simp) |
|
97 apply(simp) |
|
98 apply(metis) |
|
99 --"compatibility" |
|
100 apply(all_trivials) |
|
101 defer |
|
102 apply(simp) |
|
103 apply(simp) |
|
104 sorry |
73 |
105 |
|
106 termination sorry |
|
107 |
|
108 definition |
|
109 eval :: "lam \<Rightarrow> sem" |
|
110 where |
|
111 "eval t = evals ENil t" |
|
112 |
|
113 definition |
|
114 normalize :: "lam \<Rightarrow> lam" |
|
115 where |
|
116 "normalize t = reify (eval t)" |
|
117 |
|
118 end |