equal
deleted
inserted
replaced
20 | A "neu" "sem" |
20 | A "neu" "sem" |
21 and env = |
21 and env = |
22 ENil |
22 ENil |
23 | ECons "env" "name" "sem" |
23 | ECons "env" "name" "sem" |
24 |
24 |
25 nominal_primrec |
25 nominal_primrec |
26 evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and |
26 evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and |
27 evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem" |
27 evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem" |
28 where |
28 where |
29 "evals ENil (Var x) = N (V x)" |
29 "evals ENil (Var x) = N (V x)" |
30 | "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" |
30 | "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" |
31 | "evals env (Lam [x]. t) = L env x t" |
31 | "evals env (Lam [x]. t) = L env x t" |
32 | "evals env (App t1 t2) = evals_aux (evals env t1) t2 env" |
32 | "evals env (App t1 t2) = evals_aux (evals env t1) t2 env" |
33 | "evals_aux (L cenv x t) t2 env = evals (ECons cenv x (evals env t2)) t" |
33 | "evals_aux (L cenv x t) t2 env = evals (ECons cenv x (evals env t2)) t" |
34 | "evals_aux (N n) t2 env = N (A n (evals env t2))" |
34 | "evals_aux (N n) t2 env = N (A n (evals env t2))" |
35 defer |
35 defer |
36 defer |
36 apply (rule TrueI) |
37 --"completeness" |
37 --"completeness" |
38 apply(case_tac x) |
38 apply(case_tac x) |
39 apply(simp) |
39 apply(simp) |
40 apply(case_tac a) |
40 apply(case_tac a) |
41 apply(simp) |
41 apply(simp) |
54 apply(all_trivials) |
54 apply(all_trivials) |
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]) |
|
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)") |
|
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))") |
|
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))") |
59 defer |
66 defer |
60 apply(simp) |
67 apply (simp_all add: eqvt_at_def evals_def)[3] |
61 sorry |
68 sorry |
62 |
69 |
63 (* can probably not proved by a trivial size argument *) |
70 (* can probably not proved by a trivial size argument *) |
64 termination sorry |
71 termination sorry |
65 |
72 |