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