|
1 theory Lambda |
|
2 imports "../Nominal2" Quotient_Option |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 declare [[STEPS = 100]] |
|
7 |
|
8 nominal_datatype lam = |
|
9 Var "name" |
|
10 | App "lam" "lam" |
|
11 | Lam x::"name" l::"lam" bind x in l |
|
12 |
|
13 thm lam.distinct |
|
14 thm lam.induct |
|
15 thm lam.exhaust |
|
16 thm lam.fv_defs |
|
17 thm lam.bn_defs |
|
18 thm lam.perm_simps |
|
19 thm lam.eq_iff |
|
20 thm lam.fv_bn_eqvt |
|
21 thm lam.size_eqvt |
|
22 thm lam.size |
|
23 thm lam_raw.size |
|
24 thm lam.fresh |
|
25 |
|
26 primrec match_Var_raw where |
|
27 "match_Var_raw (Var_raw x) = Some x" |
|
28 | "match_Var_raw (App_raw x y) = None" |
|
29 | "match_Var_raw (Lam_raw n t) = None" |
|
30 |
|
31 quotient_definition |
|
32 "match_Var :: lam \<Rightarrow> name option" |
|
33 is match_Var_raw |
|
34 |
|
35 lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw" |
|
36 by (rule, induct_tac a b rule: alpha_lam_raw.induct, simp_all) |
|
37 |
|
38 lemmas match_Var_simps = match_Var_raw.simps[quot_lifted] |
|
39 |
|
40 primrec match_App_raw where |
|
41 "match_App_raw (Var_raw x) = None" |
|
42 | "match_App_raw (App_raw x y) = Some (x, y)" |
|
43 | "match_App_raw (Lam_raw n t) = None" |
|
44 |
|
45 quotient_definition |
|
46 "match_App :: lam \<Rightarrow> (lam \<times> lam) option" |
|
47 is match_App_raw |
|
48 |
|
49 lemma [quot_respect]: |
|
50 "(alpha_lam_raw ===> option_rel (prod_rel alpha_lam_raw alpha_lam_raw)) match_App_raw match_App_raw" |
|
51 by (intro fun_relI, induct_tac a b rule: alpha_lam_raw.induct, simp_all) |
|
52 |
|
53 lemmas match_App_simps = match_App_raw.simps[quot_lifted] |
|
54 |
|
55 definition next_name where |
|
56 "next_name (s :: 'a :: fs) = (THE x. \<forall>a \<in> supp s. atom x \<noteq> a)" |
|
57 |
|
58 lemma lam_eq: "Lam a t = Lam b s \<longleftrightarrow> (a \<leftrightarrow> b) \<bullet> t = s" |
|
59 apply (simp add: lam.eq_iff Abs_eq_iff alphas) |
|
60 sorry |
|
61 |
|
62 lemma lam_half_inj: "(Lam z s = Lam z sa) = (s = sa)" |
|
63 by (auto simp add: lam_eq) |
|
64 |
|
65 definition |
|
66 "match_Lam (S :: 'a :: fs) t = (if (\<exists>n s. (t = Lam n s)) then |
|
67 (let z = next_name (S, t) in Some (z, THE s. t = Lam z s)) else None)" |
|
68 |
|
69 lemma match_Lam_simps: |
|
70 "match_Lam S (Var n) = None" |
|
71 "match_Lam S (App l r) = None" |
|
72 "match_Lam S (Lam z s) = (let n = next_name (S, (Lam z s)) in Some (n, (z \<leftrightarrow> n) \<bullet> s))" |
|
73 apply (simp_all add: match_Lam_def lam.distinct) |
|
74 apply (auto simp add: lam_eq) |
|
75 done |
|
76 |
|
77 lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b" |
|
78 by (induct x rule: lam.induct) (simp_all add: match_App_simps) |
|
79 |
|
80 |
|
81 lemma lam_some: "match_Lam S x = Some (n, t) \<Longrightarrow> x = Lam n t" |
|
82 apply (induct x rule: lam.induct) |
|
83 apply (simp add: match_Lam_simps) |
|
84 apply (simp add: match_Lam_simps) |
|
85 apply (simp add: match_Lam_simps Let_def lam_eq) |
|
86 apply clarify |
|
87 done |
|
88 |
|
89 function subst where |
|
90 "subst v s t = ( |
|
91 case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow> |
|
92 case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow> |
|
93 case match_Lam (v, s) t of Some (n, s') \<Rightarrow> Lam n (subst v s s') | None \<Rightarrow> undefined)" |
|
94 print_theorems |
|
95 thm subst_rel.intros[no_vars] |
|
96 by pat_completeness auto |
|
97 |
|
98 termination apply (relation "measure (\<lambda>(_, _, t). size t)") |
|
99 apply auto[1] |
|
100 apply (case_tac a) apply simp |
|
101 apply (frule lam_some) apply (simp add: lam.size) |
|
102 apply (case_tac a) apply simp |
|
103 apply (frule app_some) apply (simp add: lam.size) |
|
104 apply (case_tac a) apply simp |
|
105 apply (frule app_some) apply (simp add: lam.size) |
|
106 done |
|
107 |
|
108 lemma subst_eqs: |
|
109 "subst y s (Var x) = (if x = y then s else (Var x))" |
|
110 "subst y s (App l r) = App (subst y s l) (subst y s r)" |
|
111 "subst y s (Lam x t) = |
|
112 (let n = next_name ((y, s), Lam x t) in Lam n (subst y s ((x \<leftrightarrow> n) \<bullet> t)))" |
|
113 apply (subst subst.simps) |
|
114 apply (simp only: match_Var_simps option.simps) |
|
115 apply (subst subst.simps) |
|
116 apply (simp only: match_App_simps option.simps prod.simps match_Var_simps) |
|
117 apply (subst subst.simps) |
|
118 apply (simp only: match_App_simps option.simps prod.simps match_Var_simps match_Lam_simps Let_def) |
|
119 done |
|
120 |
|
121 lemma subst_eqvt: |
|
122 "p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)" |
|
123 proof (induct v s t rule: subst.induct) |
|
124 case (1 v s t) |
|
125 show ?case proof (cases t rule: lam.exhaust) |
|
126 fix n |
|
127 assume "t = Var n" |
|
128 then show ?thesis by (simp add: match_Var_simps) |
|
129 next |
|
130 fix l r |
|
131 assume "t = App l r" |
|
132 then show ?thesis |
|
133 apply (simp only: subst_eqs lam.perm_simps) |
|
134 apply (subst 1(2)[of "(l, r)" "l" "r"]) |
|
135 apply (simp add: match_Var_simps) |
|
136 apply (simp add: match_App_simps) |
|
137 apply (rule refl) |
|
138 apply (subst 1(3)[of "(l, r)" "l" "r"]) |
|
139 apply (simp add: match_Var_simps) |
|
140 apply (simp add: match_App_simps) |
|
141 apply (rule refl) |
|
142 apply (rule refl) |
|
143 done |
|
144 next |
|
145 fix n t' |
|
146 assume "t = Lam n t'" |
|
147 then show ?thesis |
|
148 apply (simp only: subst_eqs lam.perm_simps Let_def) |
|
149 apply (subst 1(1)) |
|
150 apply (simp add: match_Var_simps) |
|
151 apply (simp add: match_App_simps) |
|
152 apply (simp add: match_Lam_simps Let_def) |
|
153 apply (rule refl) |
|
154 (* next_name is not equivariant :( *) |
|
155 apply (simp only: lam_eq) |
|
156 sorry |
|
157 qed |
|
158 qed |
|
159 |
|
160 lemma subst_eqvt': |
|
161 "p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)" |
|
162 apply (induct t arbitrary: v s rule: lam.induct) |
|
163 apply (simp only: subst_eqs lam.perm_simps eqvts) |
|
164 apply (simp only: subst_eqs lam.perm_simps) |
|
165 apply (simp only: subst_eqs lam.perm_simps Let_def) |
|
166 apply (simp only: lam_eq) |
|
167 sorry |
|
168 |
|
169 lemma subst_eq3: |
|
170 "atom x \<sharp> (y, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)" |
|
171 apply (simp only: subst_eqs Let_def) |
|
172 apply (simp only: lam_eq) |
|
173 (* p # y p # s subst_eqvt *) |
|
174 (* p \<bullet> -p \<bullet> (subst y s t) = subst y s t *) |
|
175 sorry |
|
176 |
|
177 end |
|
178 |
|
179 |
|
180 |