author | wenzelm |
Sat, 22 Mar 2014 20:42:16 +0100 | |
changeset 56256 | 1e01c159e7d9 |
parent 55382 | 9218fa411c15 |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
35108 | 1 |
(* Title: HOL/TLA/Intensional.thy |
2 |
Author: Stephan Merz |
|
3 |
Copyright: 1998 University of Munich |
|
21624 | 4 |
*) |
3807 | 5 |
|
21624 | 6 |
header {* A framework for "intensional" (possible-world based) logics |
7 |
on top of HOL, with lifting of constants and functions *} |
|
3807 | 8 |
|
17309 | 9 |
theory Intensional |
10 |
imports Main |
|
11 |
begin |
|
3807 | 12 |
|
55382
9218fa411c15
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
54742
diff
changeset
|
13 |
class world |
6255 | 14 |
|
15 |
(** abstract syntax **) |
|
3807 | 16 |
|
42018 | 17 |
type_synonym ('w,'a) expr = "'w => 'a" (* intention: 'w::world, 'a::type *) |
18 |
type_synonym 'w form = "('w, bool) expr" |
|
3807 | 19 |
|
20 |
consts |
|
17309 | 21 |
Valid :: "('w::world) form => bool" |
22 |
const :: "'a => ('w::world, 'a) expr" |
|
23 |
lift :: "['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr" |
|
24 |
lift2 :: "['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr" |
|
25 |
lift3 :: "['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr" |
|
3807 | 26 |
|
6255 | 27 |
(* "Rigid" quantification (logic level) *) |
28 |
RAll :: "('a => ('w::world) form) => 'w form" (binder "Rall " 10) |
|
29 |
REx :: "('a => ('w::world) form) => 'w form" (binder "Rex " 10) |
|
30 |
REx1 :: "('a => ('w::world) form) => 'w form" (binder "Rex! " 10) |
|
3807 | 31 |
|
6255 | 32 |
(** concrete syntax **) |
3807 | 33 |
|
41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
38786
diff
changeset
|
34 |
nonterminal lift and liftargs |
3807 | 35 |
|
36 |
syntax |
|
17309 | 37 |
"" :: "id => lift" ("_") |
38 |
"" :: "longid => lift" ("_") |
|
39 |
"" :: "var => lift" ("_") |
|
40 |
"_applC" :: "[lift, cargs] => lift" ("(1_/ _)" [1000, 1000] 999) |
|
41 |
"" :: "lift => lift" ("'(_')") |
|
42 |
"_lambda" :: "[idts, 'a] => lift" ("(3%_./ _)" [0, 3] 3) |
|
43 |
"_constrain" :: "[lift, type] => lift" ("(_::_)" [4, 0] 3) |
|
44 |
"" :: "lift => liftargs" ("_") |
|
45 |
"_liftargs" :: "[lift, liftargs] => liftargs" ("_,/ _") |
|
46 |
"_Valid" :: "lift => bool" ("(|- _)" 5) |
|
47 |
"_holdsAt" :: "['a, lift] => bool" ("(_ |= _)" [100,10] 10) |
|
6255 | 48 |
|
49 |
(* Syntax for lifted expressions outside the scope of |- or |= *) |
|
35354 | 50 |
"_LIFT" :: "lift => 'a" ("LIFT _") |
6255 | 51 |
|
52 |
(* generic syntax for lifted constants and functions *) |
|
17309 | 53 |
"_const" :: "'a => lift" ("(#_)" [1000] 999) |
54 |
"_lift" :: "['a, lift] => lift" ("(_<_>)" [1000] 999) |
|
55 |
"_lift2" :: "['a, lift, lift] => lift" ("(_<_,/ _>)" [1000] 999) |
|
56 |
"_lift3" :: "['a, lift, lift, lift] => lift" ("(_<_,/ _,/ _>)" [1000] 999) |
|
6255 | 57 |
|
58 |
(* concrete syntax for common infix functions: reuse same symbol *) |
|
17309 | 59 |
"_liftEqu" :: "[lift, lift] => lift" ("(_ =/ _)" [50,51] 50) |
60 |
"_liftNeq" :: "[lift, lift] => lift" ("(_ ~=/ _)" [50,51] 50) |
|
61 |
"_liftNot" :: "lift => lift" ("(~ _)" [40] 40) |
|
62 |
"_liftAnd" :: "[lift, lift] => lift" ("(_ &/ _)" [36,35] 35) |
|
63 |
"_liftOr" :: "[lift, lift] => lift" ("(_ |/ _)" [31,30] 30) |
|
64 |
"_liftImp" :: "[lift, lift] => lift" ("(_ -->/ _)" [26,25] 25) |
|
65 |
"_liftIf" :: "[lift, lift, lift] => lift" ("(if (_)/ then (_)/ else (_))" 10) |
|
66 |
"_liftPlus" :: "[lift, lift] => lift" ("(_ +/ _)" [66,65] 65) |
|
67 |
"_liftMinus" :: "[lift, lift] => lift" ("(_ -/ _)" [66,65] 65) |
|
68 |
"_liftTimes" :: "[lift, lift] => lift" ("(_ */ _)" [71,70] 70) |
|
69 |
"_liftDiv" :: "[lift, lift] => lift" ("(_ div _)" [71,70] 70) |
|
70 |
"_liftMod" :: "[lift, lift] => lift" ("(_ mod _)" [71,70] 70) |
|
71 |
"_liftLess" :: "[lift, lift] => lift" ("(_/ < _)" [50, 51] 50) |
|
72 |
"_liftLeq" :: "[lift, lift] => lift" ("(_/ <= _)" [50, 51] 50) |
|
73 |
"_liftMem" :: "[lift, lift] => lift" ("(_/ : _)" [50, 51] 50) |
|
74 |
"_liftNotMem" :: "[lift, lift] => lift" ("(_/ ~: _)" [50, 51] 50) |
|
75 |
"_liftFinset" :: "liftargs => lift" ("{(_)}") |
|
6255 | 76 |
(** TODO: syntax for lifted collection / comprehension **) |
17309 | 77 |
"_liftPair" :: "[lift,liftargs] => lift" ("(1'(_,/ _'))") |
6255 | 78 |
(* infix syntax for list operations *) |
17309 | 79 |
"_liftCons" :: "[lift, lift] => lift" ("(_ #/ _)" [65,66] 65) |
80 |
"_liftApp" :: "[lift, lift] => lift" ("(_ @/ _)" [65,66] 65) |
|
81 |
"_liftList" :: "liftargs => lift" ("[(_)]") |
|
6255 | 82 |
|
83 |
(* Rigid quantification (syntax level) *) |
|
17309 | 84 |
"_ARAll" :: "[idts, lift] => lift" ("(3! _./ _)" [0, 10] 10) |
85 |
"_AREx" :: "[idts, lift] => lift" ("(3? _./ _)" [0, 10] 10) |
|
86 |
"_AREx1" :: "[idts, lift] => lift" ("(3?! _./ _)" [0, 10] 10) |
|
87 |
"_RAll" :: "[idts, lift] => lift" ("(3ALL _./ _)" [0, 10] 10) |
|
88 |
"_REx" :: "[idts, lift] => lift" ("(3EX _./ _)" [0, 10] 10) |
|
89 |
"_REx1" :: "[idts, lift] => lift" ("(3EX! _./ _)" [0, 10] 10) |
|
3807 | 90 |
|
91 |
translations |
|
35108 | 92 |
"_const" == "CONST const" |
93 |
"_lift" == "CONST lift" |
|
94 |
"_lift2" == "CONST lift2" |
|
95 |
"_lift3" == "CONST lift3" |
|
96 |
"_Valid" == "CONST Valid" |
|
6255 | 97 |
"_RAll x A" == "Rall x. A" |
98 |
"_REx x A" == "Rex x. A" |
|
99 |
"_REx1 x A" == "Rex! x. A" |
|
100 |
"_ARAll" => "_RAll" |
|
101 |
"_AREx" => "_REx" |
|
102 |
"_AREx1" => "_REx1" |
|
3807 | 103 |
|
6255 | 104 |
"w |= A" => "A w" |
105 |
"LIFT A" => "A::_=>_" |
|
3807 | 106 |
|
6255 | 107 |
"_liftEqu" == "_lift2 (op =)" |
108 |
"_liftNeq u v" == "_liftNot (_liftEqu u v)" |
|
35108 | 109 |
"_liftNot" == "_lift (CONST Not)" |
6255 | 110 |
"_liftAnd" == "_lift2 (op &)" |
111 |
"_liftOr" == "_lift2 (op | )" |
|
112 |
"_liftImp" == "_lift2 (op -->)" |
|
35108 | 113 |
"_liftIf" == "_lift3 (CONST If)" |
6255 | 114 |
"_liftPlus" == "_lift2 (op +)" |
115 |
"_liftMinus" == "_lift2 (op -)" |
|
116 |
"_liftTimes" == "_lift2 (op *)" |
|
117 |
"_liftDiv" == "_lift2 (op div)" |
|
118 |
"_liftMod" == "_lift2 (op mod)" |
|
119 |
"_liftLess" == "_lift2 (op <)" |
|
120 |
"_liftLeq" == "_lift2 (op <=)" |
|
121 |
"_liftMem" == "_lift2 (op :)" |
|
122 |
"_liftNotMem x xs" == "_liftNot (_liftMem x xs)" |
|
35108 | 123 |
"_liftFinset (_liftargs x xs)" == "_lift2 (CONST insert) x (_liftFinset xs)" |
124 |
"_liftFinset x" == "_lift2 (CONST insert) x (_const {})" |
|
6255 | 125 |
"_liftPair x (_liftargs y z)" == "_liftPair x (_liftPair y z)" |
35108 | 126 |
"_liftPair" == "_lift2 (CONST Pair)" |
127 |
"_liftCons" == "CONST lift2 (CONST Cons)" |
|
128 |
"_liftApp" == "CONST lift2 (op @)" |
|
6255 | 129 |
"_liftList (_liftargs x xs)" == "_liftCons x (_liftList xs)" |
130 |
"_liftList x" == "_liftCons x (_const [])" |
|
3807 | 131 |
|
17309 | 132 |
|
3807 | 133 |
|
6255 | 134 |
"w |= ~A" <= "_liftNot A w" |
135 |
"w |= A & B" <= "_liftAnd A B w" |
|
136 |
"w |= A | B" <= "_liftOr A B w" |
|
137 |
"w |= A --> B" <= "_liftImp A B w" |
|
138 |
"w |= u = v" <= "_liftEqu u v w" |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
139 |
"w |= ALL x. A" <= "_RAll x A w" |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
140 |
"w |= EX x. A" <= "_REx x A w" |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset
|
141 |
"w |= EX! x. A" <= "_REx1 x A w" |
3807 | 142 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
9517
diff
changeset
|
143 |
syntax (xsymbols) |
17309 | 144 |
"_Valid" :: "lift => bool" ("(\<turnstile> _)" 5) |
145 |
"_holdsAt" :: "['a, lift] => bool" ("(_ \<Turnstile> _)" [100,10] 10) |
|
146 |
"_liftNeq" :: "[lift, lift] => lift" (infixl "\<noteq>" 50) |
|
147 |
"_liftNot" :: "lift => lift" ("\<not> _" [40] 40) |
|
148 |
"_liftAnd" :: "[lift, lift] => lift" (infixr "\<and>" 35) |
|
149 |
"_liftOr" :: "[lift, lift] => lift" (infixr "\<or>" 30) |
|
150 |
"_liftImp" :: "[lift, lift] => lift" (infixr "\<longrightarrow>" 25) |
|
151 |
"_RAll" :: "[idts, lift] => lift" ("(3\<forall>_./ _)" [0, 10] 10) |
|
152 |
"_REx" :: "[idts, lift] => lift" ("(3\<exists>_./ _)" [0, 10] 10) |
|
153 |
"_REx1" :: "[idts, lift] => lift" ("(3\<exists>!_./ _)" [0, 10] 10) |
|
154 |
"_liftLeq" :: "[lift, lift] => lift" ("(_/ \<le> _)" [50, 51] 50) |
|
155 |
"_liftMem" :: "[lift, lift] => lift" ("(_/ \<in> _)" [50, 51] 50) |
|
156 |
"_liftNotMem" :: "[lift, lift] => lift" ("(_/ \<notin> _)" [50, 51] 50) |
|
3808 | 157 |
|
6340 | 158 |
syntax (HTML output) |
17309 | 159 |
"_liftNeq" :: "[lift, lift] => lift" (infixl "\<noteq>" 50) |
160 |
"_liftNot" :: "lift => lift" ("\<not> _" [40] 40) |
|
161 |
"_liftAnd" :: "[lift, lift] => lift" (infixr "\<and>" 35) |
|
162 |
"_liftOr" :: "[lift, lift] => lift" (infixr "\<or>" 30) |
|
163 |
"_RAll" :: "[idts, lift] => lift" ("(3\<forall>_./ _)" [0, 10] 10) |
|
164 |
"_REx" :: "[idts, lift] => lift" ("(3\<exists>_./ _)" [0, 10] 10) |
|
165 |
"_REx1" :: "[idts, lift] => lift" ("(3\<exists>!_./ _)" [0, 10] 10) |
|
166 |
"_liftLeq" :: "[lift, lift] => lift" ("(_/ \<le> _)" [50, 51] 50) |
|
167 |
"_liftMem" :: "[lift, lift] => lift" ("(_/ \<in> _)" [50, 51] 50) |
|
168 |
"_liftNotMem" :: "[lift, lift] => lift" ("(_/ \<notin> _)" [50, 51] 50) |
|
6340 | 169 |
|
35318
e1b61c5fd494
dropped axclass, going back to purely syntactic type classes
haftmann
parents:
35108
diff
changeset
|
170 |
defs |
17309 | 171 |
Valid_def: "|- A == ALL w. w |= A" |
172 |
||
173 |
unl_con: "LIFT #c w == c" |
|
21020 | 174 |
unl_lift: "lift f x w == f (x w)" |
17309 | 175 |
unl_lift2: "LIFT f<x, y> w == f (x w) (y w)" |
176 |
unl_lift3: "LIFT f<x, y, z> w == f (x w) (y w) (z w)" |
|
3807 | 177 |
|
17309 | 178 |
unl_Rall: "w |= ALL x. A x == ALL x. (w |= A x)" |
179 |
unl_Rex: "w |= EX x. A x == EX x. (w |= A x)" |
|
180 |
unl_Rex1: "w |= EX! x. A x == EX! x. (w |= A x)" |
|
3807 | 181 |
|
21624 | 182 |
|
183 |
subsection {* Lemmas and tactics for "intensional" logics. *} |
|
184 |
||
185 |
lemmas intensional_rews [simp] = |
|
186 |
unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1 |
|
187 |
||
188 |
lemma inteq_reflection: "|- x=y ==> (x==y)" |
|
189 |
apply (unfold Valid_def unl_lift2) |
|
190 |
apply (rule eq_reflection) |
|
191 |
apply (rule ext) |
|
192 |
apply (erule spec) |
|
193 |
done |
|
194 |
||
195 |
lemma intI [intro!]: "(!!w. w |= A) ==> |- A" |
|
196 |
apply (unfold Valid_def) |
|
197 |
apply (rule allI) |
|
198 |
apply (erule meta_spec) |
|
199 |
done |
|
200 |
||
201 |
lemma intD [dest]: "|- A ==> w |= A" |
|
202 |
apply (unfold Valid_def) |
|
203 |
apply (erule spec) |
|
204 |
done |
|
205 |
||
206 |
(** Lift usual HOL simplifications to "intensional" level. **) |
|
207 |
||
208 |
lemma int_simps: |
|
209 |
"|- (x=x) = #True" |
|
210 |
"|- (~#True) = #False" "|- (~#False) = #True" "|- (~~ P) = P" |
|
211 |
"|- ((~P) = P) = #False" "|- (P = (~P)) = #False" |
|
212 |
"|- (P ~= Q) = (P = (~Q))" |
|
213 |
"|- (#True=P) = P" "|- (P=#True) = P" |
|
214 |
"|- (#True --> P) = P" "|- (#False --> P) = #True" |
|
215 |
"|- (P --> #True) = #True" "|- (P --> P) = #True" |
|
216 |
"|- (P --> #False) = (~P)" "|- (P --> ~P) = (~P)" |
|
217 |
"|- (P & #True) = P" "|- (#True & P) = P" |
|
218 |
"|- (P & #False) = #False" "|- (#False & P) = #False" |
|
219 |
"|- (P & P) = P" "|- (P & ~P) = #False" "|- (~P & P) = #False" |
|
220 |
"|- (P | #True) = #True" "|- (#True | P) = #True" |
|
221 |
"|- (P | #False) = P" "|- (#False | P) = P" |
|
222 |
"|- (P | P) = P" "|- (P | ~P) = #True" "|- (~P | P) = #True" |
|
223 |
"|- (! x. P) = P" "|- (? x. P) = P" |
|
224 |
"|- (~Q --> ~P) = (P --> Q)" |
|
225 |
"|- (P|Q --> R) = ((P-->R)&(Q-->R))" |
|
226 |
apply (unfold Valid_def intensional_rews) |
|
227 |
apply blast+ |
|
228 |
done |
|
229 |
||
230 |
declare int_simps [THEN inteq_reflection, simp] |
|
231 |
||
232 |
lemma TrueW [simp]: "|- #True" |
|
233 |
by (simp add: Valid_def unl_con) |
|
234 |
||
235 |
||
236 |
||
237 |
(* ======== Functions to "unlift" intensional implications into HOL rules ====== *) |
|
238 |
||
239 |
ML {* |
|
240 |
(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g. |
|
241 |
|- F = G becomes F w = G w |
|
242 |
|- F --> G becomes F w --> G w |
|
243 |
*) |
|
244 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
245 |
fun int_unlift ctxt th = |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
246 |
rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th); |
21624 | 247 |
|
248 |
(* Turn |- F = G into meta-level rewrite rule F == G *) |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
249 |
fun int_rewrite ctxt th = |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
250 |
zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection})) |
21624 | 251 |
|
252 |
(* flattening turns "-->" into "==>" and eliminates conjunctions in the |
|
253 |
antecedent. For example, |
|
254 |
||
255 |
P & Q --> (R | S --> T) becomes [| P; Q; R | S |] ==> T |
|
256 |
||
257 |
Flattening can be useful with "intensional" lemmas (after unlifting). |
|
258 |
Naive resolution with mp and conjI may run away because of higher-order |
|
259 |
unification, therefore the code is a little awkward. |
|
260 |
*) |
|
261 |
fun flatten t = |
|
262 |
let |
|
263 |
(* analogous to RS, but using matching instead of resolution *) |
|
264 |
fun matchres tha i thb = |
|
31945 | 265 |
case Seq.chop 2 (Thm.biresolution true [(false,tha)] i thb) of |
21624 | 266 |
([th],_) => th |
267 |
| ([],_) => raise THM("matchres: no match", i, [tha,thb]) |
|
268 |
| _ => raise THM("matchres: multiple unifiers", i, [tha,thb]) |
|
269 |
||
270 |
(* match tha with some premise of thb *) |
|
271 |
fun matchsome tha thb = |
|
272 |
let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb]) |
|
273 |
| hmatch n = matchres tha n thb handle THM _ => hmatch (n-1) |
|
274 |
in hmatch (nprems_of thb) end |
|
275 |
||
276 |
fun hflatten t = |
|
277 |
case (concl_of t) of |
|
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38549
diff
changeset
|
278 |
Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp) |
21624 | 279 |
| _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t |
280 |
in |
|
281 |
hflatten t |
|
282 |
end |
|
283 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
284 |
fun int_use ctxt th = |
21624 | 285 |
case (concl_of th) of |
56256 | 286 |
Const _ $ (Const (@{const_name Valid}, _) $ _) => |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
287 |
(flatten (int_unlift ctxt th) handle THM _ => th) |
21624 | 288 |
| _ => th |
289 |
*} |
|
290 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
291 |
attribute_setup int_unlift = |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
292 |
{* Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of)) *} |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
293 |
attribute_setup int_rewrite = |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
294 |
{* Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of)) *} |
42814 | 295 |
attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *} |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
296 |
attribute_setup int_use = |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
297 |
{* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *} |
21624 | 298 |
|
299 |
lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)" |
|
300 |
by (simp add: Valid_def) |
|
301 |
||
302 |
lemma Not_Rex: "|- (~ (? x. F x)) = (! x. ~ F x)" |
|
303 |
by (simp add: Valid_def) |
|
304 |
||
305 |
end |