author | wenzelm |
Wed, 16 Dec 2015 16:31:36 +0100 | |
changeset 61853 | fb7756087101 |
parent 60592 | c9bd1d902f04 |
child 62150 | 33ce5f41a9e1 |
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 |
|
60592 | 6 |
section \<open>A framework for "intensional" (possible-world based) logics |
7 |
on top of HOL, with lifting of constants and functions\<close> |
|
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 |
|
60588 | 17 |
type_synonym ('w,'a) expr = "'w \<Rightarrow> 'a" (* intention: 'w::world, 'a::type *) |
42018 | 18 |
type_synonym 'w form = "('w, bool) expr" |
3807 | 19 |
|
20 |
consts |
|
60588 | 21 |
Valid :: "('w::world) form \<Rightarrow> bool" |
22 |
const :: "'a \<Rightarrow> ('w::world, 'a) expr" |
|
23 |
lift :: "['a \<Rightarrow> 'b, ('w::world, 'a) expr] \<Rightarrow> ('w,'b) expr" |
|
24 |
lift2 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c, ('w::world,'a) expr, ('w,'b) expr] \<Rightarrow> ('w,'c) expr" |
|
25 |
lift3 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] \<Rightarrow> ('w,'d) expr" |
|
3807 | 26 |
|
6255 | 27 |
(* "Rigid" quantification (logic level) *) |
60588 | 28 |
RAll :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rall " 10) |
29 |
REx :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rex " 10) |
|
30 |
REx1 :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> '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 |
|
60588 | 37 |
"" :: "id \<Rightarrow> lift" ("_") |
38 |
"" :: "longid \<Rightarrow> lift" ("_") |
|
39 |
"" :: "var \<Rightarrow> lift" ("_") |
|
40 |
"_applC" :: "[lift, cargs] \<Rightarrow> lift" ("(1_/ _)" [1000, 1000] 999) |
|
41 |
"" :: "lift \<Rightarrow> lift" ("'(_')") |
|
42 |
"_lambda" :: "[idts, 'a] \<Rightarrow> lift" ("(3\<lambda>_./ _)" [0, 3] 3) |
|
43 |
"_constrain" :: "[lift, type] \<Rightarrow> lift" ("(_::_)" [4, 0] 3) |
|
44 |
"" :: "lift \<Rightarrow> liftargs" ("_") |
|
45 |
"_liftargs" :: "[lift, liftargs] \<Rightarrow> liftargs" ("_,/ _") |
|
60591 | 46 |
"_Valid" :: "lift \<Rightarrow> bool" ("(\<turnstile> _)" 5) |
47 |
"_holdsAt" :: "['a, lift] \<Rightarrow> bool" ("(_ \<Turnstile> _)" [100,10] 10) |
|
6255 | 48 |
|
60588 | 49 |
(* Syntax for lifted expressions outside the scope of \<turnstile> or |= *) |
50 |
"_LIFT" :: "lift \<Rightarrow> 'a" ("LIFT _") |
|
6255 | 51 |
|
52 |
(* generic syntax for lifted constants and functions *) |
|
60588 | 53 |
"_const" :: "'a \<Rightarrow> lift" ("(#_)" [1000] 999) |
54 |
"_lift" :: "['a, lift] \<Rightarrow> lift" ("(_<_>)" [1000] 999) |
|
55 |
"_lift2" :: "['a, lift, lift] \<Rightarrow> lift" ("(_<_,/ _>)" [1000] 999) |
|
56 |
"_lift3" :: "['a, lift, lift, lift] \<Rightarrow> lift" ("(_<_,/ _,/ _>)" [1000] 999) |
|
6255 | 57 |
|
58 |
(* concrete syntax for common infix functions: reuse same symbol *) |
|
60588 | 59 |
"_liftEqu" :: "[lift, lift] \<Rightarrow> lift" ("(_ =/ _)" [50,51] 50) |
60591 | 60 |
"_liftNeq" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<noteq>/ _)" [50,51] 50) |
61 |
"_liftNot" :: "lift \<Rightarrow> lift" ("(\<not> _)" [40] 40) |
|
62 |
"_liftAnd" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<and>/ _)" [36,35] 35) |
|
63 |
"_liftOr" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<or>/ _)" [31,30] 30) |
|
64 |
"_liftImp" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<longrightarrow>/ _)" [26,25] 25) |
|
60588 | 65 |
"_liftIf" :: "[lift, lift, lift] \<Rightarrow> lift" ("(if (_)/ then (_)/ else (_))" 10) |
66 |
"_liftPlus" :: "[lift, lift] \<Rightarrow> lift" ("(_ +/ _)" [66,65] 65) |
|
67 |
"_liftMinus" :: "[lift, lift] \<Rightarrow> lift" ("(_ -/ _)" [66,65] 65) |
|
68 |
"_liftTimes" :: "[lift, lift] \<Rightarrow> lift" ("(_ */ _)" [71,70] 70) |
|
69 |
"_liftDiv" :: "[lift, lift] \<Rightarrow> lift" ("(_ div _)" [71,70] 70) |
|
70 |
"_liftMod" :: "[lift, lift] \<Rightarrow> lift" ("(_ mod _)" [71,70] 70) |
|
71 |
"_liftLess" :: "[lift, lift] \<Rightarrow> lift" ("(_/ < _)" [50, 51] 50) |
|
60591 | 72 |
"_liftLeq" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<le> _)" [50, 51] 50) |
73 |
"_liftMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<in> _)" [50, 51] 50) |
|
74 |
"_liftNotMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<notin> _)" [50, 51] 50) |
|
60588 | 75 |
"_liftFinset" :: "liftargs \<Rightarrow> lift" ("{(_)}") |
6255 | 76 |
(** TODO: syntax for lifted collection / comprehension **) |
60588 | 77 |
"_liftPair" :: "[lift,liftargs] \<Rightarrow> lift" ("(1'(_,/ _'))") |
6255 | 78 |
(* infix syntax for list operations *) |
60588 | 79 |
"_liftCons" :: "[lift, lift] \<Rightarrow> lift" ("(_ #/ _)" [65,66] 65) |
80 |
"_liftApp" :: "[lift, lift] \<Rightarrow> lift" ("(_ @/ _)" [65,66] 65) |
|
81 |
"_liftList" :: "liftargs \<Rightarrow> lift" ("[(_)]") |
|
6255 | 82 |
|
83 |
(* Rigid quantification (syntax level) *) |
|
60591 | 84 |
"_RAll" :: "[idts, lift] \<Rightarrow> lift" ("(3\<forall>_./ _)" [0, 10] 10) |
85 |
"_REx" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>_./ _)" [0, 10] 10) |
|
86 |
"_REx1" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>!_./ _)" [0, 10] 10) |
|
3807 | 87 |
|
88 |
translations |
|
35108 | 89 |
"_const" == "CONST const" |
90 |
"_lift" == "CONST lift" |
|
91 |
"_lift2" == "CONST lift2" |
|
92 |
"_lift3" == "CONST lift3" |
|
93 |
"_Valid" == "CONST Valid" |
|
6255 | 94 |
"_RAll x A" == "Rall x. A" |
95 |
"_REx x A" == "Rex x. A" |
|
96 |
"_REx1 x A" == "Rex! x. A" |
|
3807 | 97 |
|
60591 | 98 |
"w \<Turnstile> A" => "A w" |
99 |
"LIFT A" => "A::_\<Rightarrow>_" |
|
3807 | 100 |
|
6255 | 101 |
"_liftEqu" == "_lift2 (op =)" |
102 |
"_liftNeq u v" == "_liftNot (_liftEqu u v)" |
|
35108 | 103 |
"_liftNot" == "_lift (CONST Not)" |
60591 | 104 |
"_liftAnd" == "_lift2 (op \<and>)" |
105 |
"_liftOr" == "_lift2 (op \<or>)" |
|
106 |
"_liftImp" == "_lift2 (op \<longrightarrow>)" |
|
35108 | 107 |
"_liftIf" == "_lift3 (CONST If)" |
6255 | 108 |
"_liftPlus" == "_lift2 (op +)" |
109 |
"_liftMinus" == "_lift2 (op -)" |
|
110 |
"_liftTimes" == "_lift2 (op *)" |
|
111 |
"_liftDiv" == "_lift2 (op div)" |
|
112 |
"_liftMod" == "_lift2 (op mod)" |
|
113 |
"_liftLess" == "_lift2 (op <)" |
|
60591 | 114 |
"_liftLeq" == "_lift2 (op \<le>)" |
115 |
"_liftMem" == "_lift2 (op \<in>)" |
|
6255 | 116 |
"_liftNotMem x xs" == "_liftNot (_liftMem x xs)" |
35108 | 117 |
"_liftFinset (_liftargs x xs)" == "_lift2 (CONST insert) x (_liftFinset xs)" |
118 |
"_liftFinset x" == "_lift2 (CONST insert) x (_const {})" |
|
6255 | 119 |
"_liftPair x (_liftargs y z)" == "_liftPair x (_liftPair y z)" |
35108 | 120 |
"_liftPair" == "_lift2 (CONST Pair)" |
121 |
"_liftCons" == "CONST lift2 (CONST Cons)" |
|
122 |
"_liftApp" == "CONST lift2 (op @)" |
|
6255 | 123 |
"_liftList (_liftargs x xs)" == "_liftCons x (_liftList xs)" |
124 |
"_liftList x" == "_liftCons x (_const [])" |
|
3807 | 125 |
|
17309 | 126 |
|
3807 | 127 |
|
60591 | 128 |
"w \<Turnstile> \<not>A" <= "_liftNot A w" |
129 |
"w \<Turnstile> A \<and> B" <= "_liftAnd A B w" |
|
130 |
"w \<Turnstile> A \<or> B" <= "_liftOr A B w" |
|
131 |
"w \<Turnstile> A \<longrightarrow> B" <= "_liftImp A B w" |
|
132 |
"w \<Turnstile> u = v" <= "_liftEqu u v w" |
|
133 |
"w \<Turnstile> \<forall>x. A" <= "_RAll x A w" |
|
134 |
"w \<Turnstile> \<exists>x. A" <= "_REx x A w" |
|
135 |
"w \<Turnstile> \<exists>!x. A" <= "_REx1 x A w" |
|
3808 | 136 |
|
35318
e1b61c5fd494
dropped axclass, going back to purely syntactic type classes
haftmann
parents:
35108
diff
changeset
|
137 |
defs |
60588 | 138 |
Valid_def: "\<turnstile> A == \<forall>w. w \<Turnstile> A" |
17309 | 139 |
|
140 |
unl_con: "LIFT #c w == c" |
|
21020 | 141 |
unl_lift: "lift f x w == f (x w)" |
17309 | 142 |
unl_lift2: "LIFT f<x, y> w == f (x w) (y w)" |
143 |
unl_lift3: "LIFT f<x, y, z> w == f (x w) (y w) (z w)" |
|
3807 | 144 |
|
60588 | 145 |
unl_Rall: "w \<Turnstile> \<forall>x. A x == \<forall>x. (w \<Turnstile> A x)" |
60591 | 146 |
unl_Rex: "w \<Turnstile> \<exists>x. A x == \<exists>x. (w \<Turnstile> A x)" |
60588 | 147 |
unl_Rex1: "w \<Turnstile> \<exists>!x. A x == \<exists>!x. (w \<Turnstile> A x)" |
3807 | 148 |
|
21624 | 149 |
|
60592 | 150 |
subsection \<open>Lemmas and tactics for "intensional" logics.\<close> |
21624 | 151 |
|
152 |
lemmas intensional_rews [simp] = |
|
153 |
unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1 |
|
154 |
||
60588 | 155 |
lemma inteq_reflection: "\<turnstile> x=y \<Longrightarrow> (x==y)" |
21624 | 156 |
apply (unfold Valid_def unl_lift2) |
157 |
apply (rule eq_reflection) |
|
158 |
apply (rule ext) |
|
159 |
apply (erule spec) |
|
160 |
done |
|
161 |
||
60588 | 162 |
lemma intI [intro!]: "(\<And>w. w \<Turnstile> A) \<Longrightarrow> \<turnstile> A" |
21624 | 163 |
apply (unfold Valid_def) |
164 |
apply (rule allI) |
|
165 |
apply (erule meta_spec) |
|
166 |
done |
|
167 |
||
60588 | 168 |
lemma intD [dest]: "\<turnstile> A \<Longrightarrow> w \<Turnstile> A" |
21624 | 169 |
apply (unfold Valid_def) |
170 |
apply (erule spec) |
|
171 |
done |
|
172 |
||
173 |
(** Lift usual HOL simplifications to "intensional" level. **) |
|
174 |
||
175 |
lemma int_simps: |
|
60588 | 176 |
"\<turnstile> (x=x) = #True" |
177 |
"\<turnstile> (\<not>#True) = #False" "\<turnstile> (\<not>#False) = #True" "\<turnstile> (\<not>\<not> P) = P" |
|
178 |
"\<turnstile> ((\<not>P) = P) = #False" "\<turnstile> (P = (\<not>P)) = #False" |
|
179 |
"\<turnstile> (P \<noteq> Q) = (P = (\<not>Q))" |
|
180 |
"\<turnstile> (#True=P) = P" "\<turnstile> (P=#True) = P" |
|
181 |
"\<turnstile> (#True \<longrightarrow> P) = P" "\<turnstile> (#False \<longrightarrow> P) = #True" |
|
182 |
"\<turnstile> (P \<longrightarrow> #True) = #True" "\<turnstile> (P \<longrightarrow> P) = #True" |
|
183 |
"\<turnstile> (P \<longrightarrow> #False) = (\<not>P)" "\<turnstile> (P \<longrightarrow> \<not>P) = (\<not>P)" |
|
60591 | 184 |
"\<turnstile> (P \<and> #True) = P" "\<turnstile> (#True \<and> P) = P" |
185 |
"\<turnstile> (P \<and> #False) = #False" "\<turnstile> (#False \<and> P) = #False" |
|
186 |
"\<turnstile> (P \<and> P) = P" "\<turnstile> (P \<and> \<not>P) = #False" "\<turnstile> (\<not>P \<and> P) = #False" |
|
187 |
"\<turnstile> (P \<or> #True) = #True" "\<turnstile> (#True \<or> P) = #True" |
|
188 |
"\<turnstile> (P \<or> #False) = P" "\<turnstile> (#False \<or> P) = P" |
|
189 |
"\<turnstile> (P \<or> P) = P" "\<turnstile> (P \<or> \<not>P) = #True" "\<turnstile> (\<not>P \<or> P) = #True" |
|
60588 | 190 |
"\<turnstile> (\<forall>x. P) = P" "\<turnstile> (\<exists>x. P) = P" |
191 |
"\<turnstile> (\<not>Q \<longrightarrow> \<not>P) = (P \<longrightarrow> Q)" |
|
60591 | 192 |
"\<turnstile> (P\<or>Q \<longrightarrow> R) = ((P\<longrightarrow>R)\<and>(Q\<longrightarrow>R))" |
21624 | 193 |
apply (unfold Valid_def intensional_rews) |
194 |
apply blast+ |
|
195 |
done |
|
196 |
||
197 |
declare int_simps [THEN inteq_reflection, simp] |
|
198 |
||
60588 | 199 |
lemma TrueW [simp]: "\<turnstile> #True" |
21624 | 200 |
by (simp add: Valid_def unl_con) |
201 |
||
202 |
||
203 |
||
204 |
(* ======== Functions to "unlift" intensional implications into HOL rules ====== *) |
|
205 |
||
60592 | 206 |
ML \<open> |
21624 | 207 |
(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g. |
60588 | 208 |
\<turnstile> F = G becomes F w = G w |
209 |
\<turnstile> F \<longrightarrow> G becomes F w \<longrightarrow> G w |
|
21624 | 210 |
*) |
211 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
212 |
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
|
213 |
rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th); |
21624 | 214 |
|
60588 | 215 |
(* Turn \<turnstile> 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
|
216 |
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
|
217 |
zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection})) |
21624 | 218 |
|
60588 | 219 |
(* flattening turns "\<longrightarrow>" into "\<Longrightarrow>" and eliminates conjunctions in the |
21624 | 220 |
antecedent. For example, |
221 |
||
60588 | 222 |
P & Q \<longrightarrow> (R | S \<longrightarrow> T) becomes \<lbrakk> P; Q; R | S \<rbrakk> \<Longrightarrow> T |
21624 | 223 |
|
224 |
Flattening can be useful with "intensional" lemmas (after unlifting). |
|
225 |
Naive resolution with mp and conjI may run away because of higher-order |
|
226 |
unification, therefore the code is a little awkward. |
|
227 |
*) |
|
228 |
fun flatten t = |
|
229 |
let |
|
230 |
(* analogous to RS, but using matching instead of resolution *) |
|
231 |
fun matchres tha i thb = |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58889
diff
changeset
|
232 |
case Seq.chop 2 (Thm.biresolution NONE true [(false,tha)] i thb) of |
21624 | 233 |
([th],_) => th |
234 |
| ([],_) => raise THM("matchres: no match", i, [tha,thb]) |
|
235 |
| _ => raise THM("matchres: multiple unifiers", i, [tha,thb]) |
|
236 |
||
237 |
(* match tha with some premise of thb *) |
|
238 |
fun matchsome tha thb = |
|
239 |
let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb]) |
|
240 |
| hmatch n = matchres tha n thb handle THM _ => hmatch (n-1) |
|
59582 | 241 |
in hmatch (Thm.nprems_of thb) end |
21624 | 242 |
|
243 |
fun hflatten t = |
|
59582 | 244 |
case Thm.concl_of t of |
245 |
Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp) |
|
246 |
| _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t |
|
21624 | 247 |
in |
248 |
hflatten t |
|
249 |
end |
|
250 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
251 |
fun int_use ctxt th = |
59582 | 252 |
case Thm.concl_of th of |
56256 | 253 |
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
|
254 |
(flatten (int_unlift ctxt th) handle THM _ => th) |
21624 | 255 |
| _ => th |
60592 | 256 |
\<close> |
21624 | 257 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
258 |
attribute_setup int_unlift = |
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
60592
diff
changeset
|
259 |
\<open>Scan.succeed (Thm.rule_attribute [] (int_unlift o Context.proof_of))\<close> |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
260 |
attribute_setup int_rewrite = |
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
60592
diff
changeset
|
261 |
\<open>Scan.succeed (Thm.rule_attribute [] (int_rewrite o Context.proof_of))\<close> |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
60592
diff
changeset
|
262 |
attribute_setup flatten = |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
60592
diff
changeset
|
263 |
\<open>Scan.succeed (Thm.rule_attribute [] (K flatten))\<close> |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
42814
diff
changeset
|
264 |
attribute_setup int_use = |
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
60592
diff
changeset
|
265 |
\<open>Scan.succeed (Thm.rule_attribute [] (int_use o Context.proof_of))\<close> |
21624 | 266 |
|
60588 | 267 |
lemma Not_Rall: "\<turnstile> (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)" |
21624 | 268 |
by (simp add: Valid_def) |
269 |
||
60588 | 270 |
lemma Not_Rex: "\<turnstile> (\<not> (\<exists>x. F x)) = (\<forall>x. \<not> F x)" |
21624 | 271 |
by (simp add: Valid_def) |
272 |
||
273 |
end |