| author | Christian Urban <urbanc@in.tum.de> |
| Wed, 06 Jul 2011 01:04:09 +0200 | |
| changeset 2954 | dc6007dd9c30 |
| parent 2953 | 80f01215d1a6 |
| child 2955 | 4049a2651dd9 |
| permissions | -rw-r--r-- |
| 2952 | 1 |
theory Lambda |
2 |
imports |
|
3 |
"../Nominal2" |
|
4 |
begin |
|
5 |
||
6 |
||
7 |
atom_decl name |
|
8 |
||
9 |
nominal_datatype lam = |
|
10 |
Var "name" |
|
11 |
| App "lam" "lam" |
|
12 |
| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
|
|
13 |
||
14 |
||
15 |
nominal_datatype sem = |
|
16 |
L "env" x::"name" l::"lam" binds x in l |
|
17 |
| N "neu" |
|
18 |
and neu = |
|
19 |
V "name" |
|
20 |
| A "neu" "sem" |
|
21 |
and env = |
|
22 |
ENil |
|
23 |
| ECons "env" "name" "sem" |
|
24 |
||
|
2953
80f01215d1a6
Setup eqvt_at for first goal
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2952
diff
changeset
|
25 |
nominal_primrec |
| 2952 | 26 |
evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and |
27 |
evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem" |
|
28 |
where |
|
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))" |
|
31 |
| "evals env (Lam [x]. t) = L env x t" |
|
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" |
|
34 |
| "evals_aux (N n) t2 env = N (A n (evals env t2))" |
|
35 |
defer |
|
|
2953
80f01215d1a6
Setup eqvt_at for first goal
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2952
diff
changeset
|
36 |
apply (rule TrueI) |
| 2952 | 37 |
--"completeness" |
38 |
apply(case_tac x) |
|
39 |
apply(simp) |
|
40 |
apply(case_tac a) |
|
41 |
apply(simp) |
|
42 |
apply(case_tac aa rule: sem_neu_env.exhaust(3)) |
|
43 |
apply(simp) |
|
44 |
apply(case_tac b rule: lam.exhaust) |
|
45 |
apply(metis)+ |
|
46 |
apply(case_tac b rule: lam.exhaust) |
|
47 |
apply(metis)+ |
|
48 |
apply(simp) |
|
49 |
apply(case_tac b) |
|
50 |
apply(simp) |
|
51 |
apply(case_tac a rule: sem_neu_env.exhaust(1)) |
|
52 |
apply(metis)+ |
|
53 |
--"compatibility" |
|
54 |
apply(all_trivials) |
|
55 |
apply(simp) |
|
56 |
apply(simp) |
|
57 |
apply(simp) |
|
58 |
apply(simp) |
|
|
2953
80f01215d1a6
Setup eqvt_at for first goal
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2952
diff
changeset
|
59 |
apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff]) |
|
2954
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
60 |
apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva x (evals enva t2a), t)") |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
61 |
apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (enva, t2a)") |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
62 |
apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa (evals enva t2a), ta)") |
|
2953
80f01215d1a6
Setup eqvt_at for first goal
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2952
diff
changeset
|
63 |
apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva x (evals enva t2a), t))") |
|
80f01215d1a6
Setup eqvt_at for first goal
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2952
diff
changeset
|
64 |
apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))") |
|
80f01215d1a6
Setup eqvt_at for first goal
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2952
diff
changeset
|
65 |
apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))") |
|
2954
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
66 |
apply(erule conjE)+ |
| 2952 | 67 |
defer |
|
2953
80f01215d1a6
Setup eqvt_at for first goal
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2952
diff
changeset
|
68 |
apply (simp_all add: eqvt_at_def evals_def)[3] |
|
2954
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
69 |
apply(simp) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
70 |
defer |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
71 |
apply(erule_tac c="(cenv, env)" in Abs_lst1_fcb2') |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
72 |
apply(rule fresh_eqvt_at) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
73 |
back |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
74 |
apply(simp add: eqvt_at_def) |
| 2952 | 75 |
sorry |
76 |
||
77 |
(* can probably not proved by a trivial size argument *) |
|
78 |
termination sorry |
|
79 |
||
|
2954
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
80 |
nominal_primrec |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
81 |
reify :: "sem \<Rightarrow> lam" and |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
82 |
reifyn :: "neu \<Rightarrow> lam" |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
83 |
where |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
84 |
"reify (L env y t) = (fresh_fun (\<lambda>x::name. Lam [x]. (reify (evals (ECons env y (N (V x))) t))))" |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
85 |
| "reify (N n) = reifyn n" |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
86 |
| "reifyn (V x) = Var x" |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
87 |
| "reifyn (A n d) = App (reifyn n) (reify d)" |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
88 |
defer |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
89 |
defer |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
90 |
--"completeness" |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
91 |
apply(case_tac x) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
92 |
apply(simp) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
93 |
apply(case_tac a rule: sem_neu_env.exhaust(1)) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
94 |
apply(metis)+ |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
95 |
apply(case_tac b rule: sem_neu_env.exhaust(2)) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
96 |
apply(simp) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
97 |
apply(simp) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
98 |
apply(metis) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
99 |
--"compatibility" |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
100 |
apply(all_trivials) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
101 |
defer |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
102 |
apply(simp) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
103 |
apply(simp) |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
104 |
sorry |
| 2952 | 105 |
|
|
2954
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
106 |
termination sorry |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
107 |
|
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
108 |
definition |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
109 |
eval :: "lam \<Rightarrow> sem" |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
110 |
where |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
111 |
"eval t = evals ENil t" |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
112 |
|
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
113 |
definition |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
114 |
normalize :: "lam \<Rightarrow> lam" |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
115 |
where |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
116 |
"normalize t = reify (eval t)" |
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
117 |
|
|
dc6007dd9c30
a little further with NBE
Christian Urban <urbanc@in.tum.de>
parents:
2953
diff
changeset
|
118 |
end |