20319
|
1 |
(*
|
|
2 |
ID: $Id$
|
|
3 |
Author: Amine Chaieb, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Examples for generic reflection and reification *}
|
|
7 |
|
|
8 |
theory ReflectionEx
|
|
9 |
imports Reflection
|
|
10 |
begin
|
|
11 |
|
20337
|
12 |
text{* This theory presents two methods: reify and reflection *}
|
20319
|
13 |
|
20337
|
14 |
text{*
|
|
15 |
Consider an HOL type 'a, the structure of which is not recongnisable on the theory level. This is the case of bool, arithmetical terms such as int, real etc\<dots>
|
|
16 |
In order to implement a simplification on terms of type 'a we often need its structure.
|
|
17 |
Traditionnaly such simplifications are written in ML, proofs are synthesized.
|
|
18 |
An other strategy is to declare an HOL-datatype tau and an HOL function (the interpretation) that maps elements of tau to elements of 'a. The functionality of @{text reify} is to compute a term s::tau, which is the representant of t. For this it needs equations for the interpretation.
|
|
19 |
|
|
20 |
NB: All the interpretations supported by @{text reify} must have the type @{text "'b list \<Rightarrow> tau \<Rightarrow> 'a"}.
|
|
21 |
The method @{text reify} can also be told which subterm of the current subgoal should be reified. The general call for @{text reify} is: @{text "reify eqs (t)"}, where @{text eqs} are the defining equations of the interpretation and @{text "(t)"} is an optional parameter which specifies the subterm to which reification should be applied to. If @{text "(t)"} is abscent, @{text reify} tries to reify the whole subgoal.
|
|
22 |
|
|
23 |
The method reflection uses @{text reify} and has a very similar signature: @{text "reflection corr_thm eqs (t)"}. Here again @{text eqs} and @{text "(t)"} are as described above and @{text corr_thm} is a thorem proving @{term "I vs (f t) = I vs t"}. We assume that @{text I} is the interpretation and @{text f} is some useful and executable simplification of type @{text "tau \<Rightarrow> tau"}. The method @{text reflection} applies reification and hence the theorem @{term "t = I xs s"} and hence using @{text corr_thm} derives @{term "t = I xs (f s)"}. It then uses normalization by evaluation to prove @{term "f s = s'"} which almost finishes the proof of @{term "t = t'"} where @{term "I xs s' = t'"}.
|
|
24 |
*}
|
|
25 |
|
|
26 |
text{* Example 1 : Propositional formulae and NNF.*}
|
|
27 |
text{* The type @{text fm} represents simple propositional formulae: *}
|
|
28 |
|
20319
|
29 |
datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
|
|
30 |
|
|
31 |
consts Ifm :: "bool list \<Rightarrow> fm \<Rightarrow> bool"
|
|
32 |
primrec
|
|
33 |
"Ifm vs (At n) = vs!n"
|
|
34 |
"Ifm bs (And p q) = (Ifm bs p \<and> Ifm bs q)"
|
|
35 |
"Ifm vs (Or p q) = (Ifm vs p \<or> Ifm vs q)"
|
|
36 |
"Ifm vs (Imp p q) = (Ifm vs p \<longrightarrow> Ifm vs q)"
|
|
37 |
"Ifm vs (Iff p q) = (Ifm vs p = Ifm vs q)"
|
|
38 |
"Ifm vs (NOT p) = (\<not> (Ifm vs p))"
|
|
39 |
|
|
40 |
consts fmsize :: "fm \<Rightarrow> nat"
|
|
41 |
primrec
|
|
42 |
"fmsize (At n) = 1"
|
|
43 |
"fmsize (NOT p) = 1 + fmsize p"
|
|
44 |
"fmsize (And p q) = 1 + fmsize p + fmsize q"
|
|
45 |
"fmsize (Or p q) = 1 + fmsize p + fmsize q"
|
|
46 |
"fmsize (Imp p q) = 2 + fmsize p + fmsize q"
|
|
47 |
"fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
|
|
48 |
|
|
49 |
|
|
50 |
|
20337
|
51 |
text{* Method @{text reify} maps a bool to an fm. For this it needs the
|
|
52 |
semantics of fm, i.e.\ the rewrite rules in @{text Ifm.simps}. *}
|
20319
|
53 |
lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
|
|
54 |
apply (reify Ifm.simps)
|
|
55 |
oops
|
|
56 |
|
|
57 |
(* You can also just pick up a subterm to reify \<dots> *)
|
|
58 |
lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
|
|
59 |
apply (reify Ifm.simps ("((~ D) & (~ F))"))
|
|
60 |
oops
|
|
61 |
|
20337
|
62 |
text{* Let's perform NNF. This is a version that tends to generate disjunctions *}
|
20319
|
63 |
consts nnf :: "fm \<Rightarrow> fm"
|
|
64 |
recdef nnf "measure fmsize"
|
|
65 |
"nnf (At n) = At n"
|
|
66 |
"nnf (And p q) = And (nnf p) (nnf q)"
|
|
67 |
"nnf (Or p q) = Or (nnf p) (nnf q)"
|
|
68 |
"nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
|
|
69 |
"nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
|
|
70 |
"nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
|
|
71 |
"nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
|
|
72 |
"nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
|
|
73 |
"nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
|
|
74 |
"nnf (NOT (NOT p)) = nnf p"
|
|
75 |
"nnf (NOT p) = NOT p"
|
|
76 |
|
20337
|
77 |
text{* The correctness theorem of nnf: it preserves the semantics of fm *}
|
20319
|
78 |
lemma nnf: "Ifm vs (nnf p) = Ifm vs p"
|
|
79 |
by (induct p rule: nnf.induct) auto
|
|
80 |
|
20337
|
81 |
text{* Now let's perform NNF using our @{term nnf} function defined above. First to the whole subgoal. *}
|
20319
|
82 |
lemma "(\<not> (A = B)) \<and> (B \<longrightarrow> (A \<noteq> (B | C \<and> (B \<longrightarrow> A | D)))) \<longrightarrow> A \<or> B \<and> D"
|
|
83 |
apply (reflection nnf Ifm.simps)
|
|
84 |
oops
|
|
85 |
|
20337
|
86 |
text{* Now we specify on which subterm it should be applied*}
|
20319
|
87 |
lemma "(\<not> (A = B)) \<and> (B \<longrightarrow> (A \<noteq> (B | C \<and> (B \<longrightarrow> A | D)))) \<longrightarrow> A \<or> B \<and> D"
|
|
88 |
apply (reflection nnf Ifm.simps ("(B | C \<and> (B \<longrightarrow> A | D))"))
|
|
89 |
oops
|
|
90 |
|
|
91 |
|
20337
|
92 |
(* Example 2 : Simple arithmetic formulae *)
|
20319
|
93 |
|
20337
|
94 |
text{* The type @{text num} reflects linear expressions over natural number *}
|
20319
|
95 |
datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
|
|
96 |
|
20337
|
97 |
text{* This is just technical to make recursive definitions easier. *}
|
20319
|
98 |
consts num_size :: "num \<Rightarrow> nat"
|
|
99 |
primrec
|
|
100 |
"num_size (C c) = 1"
|
|
101 |
"num_size (Var n) = 1"
|
|
102 |
"num_size (Add a b) = 1 + num_size a + num_size b"
|
|
103 |
"num_size (Mul c a) = 1 + num_size a"
|
|
104 |
"num_size (CN n c a) = 4 + num_size a "
|
|
105 |
|
20337
|
106 |
text{* The semantics of num *}
|
20319
|
107 |
consts Inum:: "nat list \<Rightarrow> num \<Rightarrow> nat"
|
|
108 |
primrec
|
|
109 |
Inum_C : "Inum vs (C i) = i"
|
|
110 |
Inum_Var: "Inum vs (Var n) = vs!n"
|
|
111 |
Inum_Add: "Inum vs (Add s t) = Inum vs s + Inum vs t"
|
|
112 |
Inum_Mul: "Inum vs (Mul c t) = c * Inum vs t"
|
|
113 |
Inum_CN : "Inum vs (CN n c t) = c*(vs!n) + Inum vs t"
|
|
114 |
|
20337
|
115 |
text{* Let's reify some nat expressions \<dots> *}
|
20319
|
116 |
lemma "4 * (2*x + (y::nat)) \<noteq> 0"
|
|
117 |
apply (reify Inum.simps ("4 * (2*x + (y::nat))"))
|
|
118 |
oops
|
20337
|
119 |
text{* We're in a bad situation!! The term above has been recongnized as a constant, which is correct but does not correspond to our intuition of the constructor C. It should encapsulate constants, i.e. numbers, i.e. numerals.*}
|
|
120 |
|
|
121 |
text{* So let's leave the Inum_C equation at the end and see what happens \<dots>*}
|
20319
|
122 |
lemma "4 * (2*x + (y::nat)) \<noteq> 0"
|
|
123 |
apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2*x + (y::nat))"))
|
|
124 |
oops
|
20337
|
125 |
text{* Better, but it still reifies @{term x} to @{term "C x"}. Note that the reification depends on the order of the equations. The problem is that the right hand side of @{thm Inum_C} matches any term of type nat, which makes things bad. We want only numerals to match\<dots> So let's specialize @{text Inum_C} with numerals.*}
|
20319
|
126 |
|
|
127 |
lemma Inum_number: "Inum vs (C (number_of t)) = number_of t" by simp
|
|
128 |
lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number
|
|
129 |
|
20337
|
130 |
text{* Second attempt *}
|
20319
|
131 |
lemma "1 * (2*x + (y::nat)) \<noteq> 0"
|
|
132 |
apply (reify Inum_eqs ("1 * (2*x + (y::nat))"))
|
|
133 |
oops
|
20337
|
134 |
text{* That was fine, so let's try an other one\<dots> *}
|
20319
|
135 |
|
20337
|
136 |
lemma "1 * (2* x + (y::nat) + 0 + 1) \<noteq> 0"
|
20319
|
137 |
apply (reify Inum_eqs ("1 * (2*x + (y::nat) + 0 + 1)"))
|
|
138 |
oops
|
20337
|
139 |
text{* Oh!! 0 is not a variable \<dots> Oh! 0 is not a number_of .. thing. The same for 1. So let's add those equations too *}
|
20319
|
140 |
|
|
141 |
lemma Inum_01: "Inum vs (C 0) = 0" "Inum vs (C 1) = 1" "Inum vs (C(Suc n)) = Suc n"
|
|
142 |
by simp+
|
20337
|
143 |
|
20319
|
144 |
lemmas Inum_eqs'= Inum_eqs Inum_01
|
20337
|
145 |
|
|
146 |
text{* Third attempt: *}
|
20319
|
147 |
|
|
148 |
lemma "1 * (2*x + (y::nat) + 0 + 1) \<noteq> 0"
|
|
149 |
apply (reify Inum_eqs' ("1 * (2*x + (y::nat) + 0 + 1)"))
|
|
150 |
oops
|
20337
|
151 |
text{* Okay, let's try reflection. Some simplifications on num follow. You can skim until the main theorem @{text linum} *}
|
20319
|
152 |
consts lin_add :: "num \<times> num \<Rightarrow> num"
|
|
153 |
recdef lin_add "measure (\<lambda>(x,y). ((size x) + (size y)))"
|
|
154 |
"lin_add (CN n1 c1 r1,CN n2 c2 r2) =
|
|
155 |
(if n1=n2 then
|
|
156 |
(let c = c1 + c2
|
|
157 |
in (if c=0 then lin_add(r1,r2) else CN n1 c (lin_add (r1,r2))))
|
|
158 |
else if n1 \<le> n2 then (CN n1 c1 (lin_add (r1,CN n2 c2 r2)))
|
|
159 |
else (CN n2 c2 (lin_add (CN n1 c1 r1,r2))))"
|
|
160 |
"lin_add (CN n1 c1 r1,t) = CN n1 c1 (lin_add (r1, t))"
|
|
161 |
"lin_add (t,CN n2 c2 r2) = CN n2 c2 (lin_add (t,r2))"
|
|
162 |
"lin_add (C b1, C b2) = C (b1+b2)"
|
|
163 |
"lin_add (a,b) = Add a b"
|
|
164 |
lemma lin_add: "Inum bs (lin_add (t,s)) = Inum bs (Add t s)"
|
|
165 |
apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
|
|
166 |
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
|
|
167 |
by (case_tac "n1 = n2", simp_all add: ring_eq_simps)
|
|
168 |
|
|
169 |
consts lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
|
|
170 |
recdef lin_mul "measure size "
|
|
171 |
"lin_mul (C j) = (\<lambda> i. C (i*j))"
|
|
172 |
"lin_mul (CN n c a) = (\<lambda> i. if i=0 then (C 0) else CN n (i*c) (lin_mul a i))"
|
|
173 |
"lin_mul t = (\<lambda> i. Mul i t)"
|
|
174 |
|
20337
|
175 |
lemma lin_mul: "Inum bs (lin_mul t i) = Inum bs (Mul i t)"
|
20503
|
176 |
by (induct t arbitrary: i rule: lin_mul.induct) (auto simp add: ring_eq_simps)
|
20319
|
177 |
|
|
178 |
consts linum:: "num \<Rightarrow> num"
|
|
179 |
recdef linum "measure num_size"
|
|
180 |
"linum (C b) = C b"
|
|
181 |
"linum (Var n) = CN n 1 (C 0)"
|
|
182 |
"linum (Add t s) = lin_add (linum t, linum s)"
|
|
183 |
"linum (Mul c t) = lin_mul (linum t) c"
|
|
184 |
"linum (CN n c t) = lin_add (linum (Mul c (Var n)),linum t)"
|
|
185 |
|
|
186 |
lemma linum : "Inum vs (linum t) = Inum vs t"
|
|
187 |
by (induct t rule: linum.induct, simp_all add: lin_mul lin_add)
|
|
188 |
|
20337
|
189 |
text{* Now we can use linum to simplify nat terms using reflection *}
|
|
190 |
lemma "(Suc (Suc 1)) * (x + (Suc 1)*y) = 3*x + 6*y"
|
|
191 |
apply (reflection linum Inum_eqs' ("(Suc (Suc 1)) * (x + (Suc 1)*y)"))
|
20319
|
192 |
oops
|
|
193 |
|
20337
|
194 |
text{* Let's lift this to formulae and see what happens *}
|
20319
|
195 |
|
|
196 |
datatype aform = Lt num num | Eq num num | Ge num num | NEq num num |
|
|
197 |
Conj aform aform | Disj aform aform | NEG aform | T | F
|
|
198 |
consts linaformsize:: "aform \<Rightarrow> nat"
|
|
199 |
recdef linaformsize "measure size"
|
|
200 |
"linaformsize T = 1"
|
|
201 |
"linaformsize F = 1"
|
|
202 |
"linaformsize (Lt a b) = 1"
|
|
203 |
"linaformsize (Ge a b) = 1"
|
|
204 |
"linaformsize (Eq a b) = 1"
|
|
205 |
"linaformsize (NEq a b) = 1"
|
|
206 |
"linaformsize (NEG p) = 2 + linaformsize p"
|
|
207 |
"linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
|
|
208 |
"linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
|
|
209 |
|
|
210 |
|
|
211 |
consts aform :: "nat list => aform => bool"
|
|
212 |
primrec
|
|
213 |
"aform vs T = True"
|
|
214 |
"aform vs F = False"
|
|
215 |
"aform vs (Lt a b) = (Inum vs a < Inum vs b)"
|
|
216 |
"aform vs (Eq a b) = (Inum vs a = Inum vs b)"
|
|
217 |
"aform vs (Ge a b) = (Inum vs a \<ge> Inum vs b)"
|
|
218 |
"aform vs (NEq a b) = (Inum vs a \<noteq> Inum vs b)"
|
|
219 |
"aform vs (NEG p) = (\<not> (aform vs p))"
|
|
220 |
"aform vs (Conj p q) = (aform vs p \<and> aform vs q)"
|
|
221 |
"aform vs (Disj p q) = (aform vs p \<or> aform vs q)"
|
|
222 |
|
20337
|
223 |
text{* Let's reify and do reflection. *}
|
20319
|
224 |
lemma "(3::nat)*x + t < 0 \<and> (2 * x + y \<noteq> 17)"
|
|
225 |
apply (reify Inum_eqs' aform.simps)
|
|
226 |
oops
|
|
227 |
|
20337
|
228 |
text{* Note that reification handles several interpretations at the same time*}
|
20319
|
229 |
lemma "(3::nat)*x + t < 0 & x*x + t*x + 3 + 1 = z*t*4*z | x + x + 1 < 0"
|
|
230 |
apply (reflection linum Inum_eqs' aform.simps ("x + x + 1"))
|
|
231 |
oops
|
|
232 |
|
20337
|
233 |
text{* For reflection we now define a simple transformation on aform: NNF + linum on atoms *}
|
20319
|
234 |
consts linaform:: "aform \<Rightarrow> aform"
|
|
235 |
recdef linaform "measure linaformsize"
|
|
236 |
"linaform (Lt s t) = Lt (linum s) (linum t)"
|
|
237 |
"linaform (Eq s t) = Eq (linum s) (linum t)"
|
|
238 |
"linaform (Ge s t) = Ge (linum s) (linum t)"
|
|
239 |
"linaform (NEq s t) = NEq (linum s) (linum t)"
|
|
240 |
"linaform (Conj p q) = Conj (linaform p) (linaform q)"
|
|
241 |
"linaform (Disj p q) = Disj (linaform p) (linaform q)"
|
|
242 |
"linaform (NEG T) = F"
|
|
243 |
"linaform (NEG F) = T"
|
|
244 |
"linaform (NEG (Lt a b)) = Ge a b"
|
|
245 |
"linaform (NEG (Ge a b)) = Lt a b"
|
|
246 |
"linaform (NEG (Eq a b)) = NEq a b"
|
|
247 |
"linaform (NEG (NEq a b)) = Eq a b"
|
|
248 |
"linaform (NEG (NEG p)) = linaform p"
|
|
249 |
"linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
|
|
250 |
"linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
|
|
251 |
"linaform p = p"
|
|
252 |
|
|
253 |
lemma linaform: "aform vs (linaform p) = aform vs p"
|
|
254 |
by (induct p rule: linaform.induct, auto simp add: linum)
|
|
255 |
|
|
256 |
lemma "(((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0)))) + (Suc (Suc (Suc 0))) * ((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0))))< 0) \<and> (Suc 0 + Suc 0< 0)"
|
20337
|
257 |
apply (reflection linaform Inum_eqs' aform.simps)
|
20319
|
258 |
oops
|
|
259 |
|
20374
|
260 |
|
|
261 |
text{* And finally an example for binders. Here we have an existential quantifier. Binding is trough de Bruijn indices, the index of the varibles. *}
|
|
262 |
|
|
263 |
datatype afm = LT num num | EQ num | AND afm afm | OR afm afm | E afm | A afm
|
|
264 |
|
|
265 |
consts Iafm:: "nat list \<Rightarrow> afm \<Rightarrow> bool"
|
|
266 |
|
|
267 |
primrec
|
|
268 |
"Iafm vs (LT s t) = (Inum vs s < Inum vs t)"
|
|
269 |
"Iafm vs (EQ t) = (Inum vs t = 0)"
|
|
270 |
"Iafm vs (AND p q) = (Iafm vs p \<and> Iafm vs q)"
|
|
271 |
"Iafm vs (OR p q) = (Iafm vs p \<or> Iafm vs q)"
|
|
272 |
"Iafm vs (E p) = (\<exists>x. Iafm (x#vs) p)"
|
|
273 |
"Iafm vs (A p) = (\<forall>x. Iafm (x#vs) p)"
|
|
274 |
|
|
275 |
lemma " \<forall>(x::nat) y. \<exists> z. z < x + 3*y \<and> x + y = 0"
|
|
276 |
apply (reify Inum_eqs' Iafm.simps)
|
|
277 |
oops
|
|
278 |
|
|
279 |
|
|
280 |
|
20319
|
281 |
end
|