Theory AOT_RestrictedVariables
1
2theory AOT_RestrictedVariables
3 imports AOT_PLM
4 keywords "AOT_register_rigid_restricted_type" :: thy_goal
5 and "AOT_register_restricted_type" :: thy_goal
6begin
7
8
9section‹Restricted Variables›
10
11locale AOT_restriction_condition =
12 fixes ψ :: ‹'a::AOT_Term_id_2 ⇒ 𝗈›
13 assumes "res-var:2"[AOT]: ‹[v ⊨ ∃α ψ{α}]›
14 assumes "res-var:3"[AOT]: ‹[v ⊨ ψ{τ} → τ↓]›
15
16ML‹
17fun register_restricted_type (name:string, restriction:string) thy =
18let
19val ctxt = thy
20val ctxt = setupStrictWorld ctxt
21val trm = Syntax.check_term ctxt (AOT_read_term @{nonterminal φ'} ctxt restriction)
22val free = case (Term.add_frees trm []) of [f] => f |
23 _ => raise Term.TERM ("Expected single free variable.", [trm])
24val trm = Term.absfree free trm
25val localeTerm = Const (\<^const_name>‹AOT_restriction_condition›, dummyT) $ trm
26val localeTerm = Syntax.check_term ctxt localeTerm
27fun after_qed thms thy = let
28val st = Interpretation.global_interpretation
29 (([(@{locale AOT_restriction_condition}, ((name, true),
30 (Expression.Named [("ψ", trm)], [])))], [])) [] thy
31val st = Proof.refine_insert (flat thms) st
32val thy = Proof.global_immediate_proof st
33
34val thy = Local_Theory.background_theory
35 (AOT_Constraints.map (Symtab.update
36 (name, (term_of (snd free), term_of (snd free))))) thy
37val thy = Local_Theory.background_theory
38 (AOT_Restriction.map (Symtab.update
39 (name, (trm, Const (\<^const_name>‹AOT_term_of_var›, dummyT))))) thy
40
41in thy end
42in
43Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop localeTerm, [])]] ctxt
44end
45
46val _ =
47 Outer_Syntax.command
48 \<^command_keyword>‹AOT_register_restricted_type›
49 "Register a restricted type."
50 (((Parse.short_ident --| Parse.$$$ ":") -- Parse.term) >>
51 (Toplevel.local_theory_to_proof NONE NONE o register_restricted_type));
52›
53
54locale AOT_rigid_restriction_condition = AOT_restriction_condition +
55 assumes rigid[AOT]: ‹[v ⊨ ∀α(ψ{α} → □ψ{α})]›
56begin
57lemma rigid_condition[AOT]: ‹[v ⊨ □(ψ{α} → □ψ{α})]›
58 using rigid[THEN "∀E"(2)] RN by simp
59lemma type_set_nonempty[AOT_no_atp, no_atp]: ‹∃x . x ∈ { α . [w⇩0 ⊨ ψ{α}]}›
60 by (metis "instantiation" mem_Collect_eq "res-var:2")
61end
62
63locale AOT_restricted_type = AOT_rigid_restriction_condition +
64 fixes Rep and Abs
65 assumes AOT_restricted_type_definition[AOT_no_atp]:
66 ‹type_definition Rep Abs { α . [w⇩0 ⊨ ψ{α}]}›
67begin
68
69AOT_theorem restricted_var_condition: ‹ψ{«AOT_term_of_var (Rep α)»}›
70proof -
71 interpret type_definition Rep Abs "{ α . [w⇩0 ⊨ ψ{α}]}"
72 using AOT_restricted_type_definition.
73 AOT_actually {
74 AOT_have ‹«AOT_term_of_var (Rep α)»↓› and ‹ψ{«AOT_term_of_var (Rep α)»}›
75 using AOT_sem_imp Rep "res-var:3" by auto
76 }
77 moreover AOT_actually {
78 AOT_have ‹ψ{α} → □ψ{α}› for α
79 using AOT_sem_box rigid_condition by presburger
80 AOT_hence ‹ψ{τ} → □ψ{τ}› if ‹τ↓› for τ
81 by (metis AOT_model.AOT_term_of_var_cases AOT_sem_denotes that)
82 }
83 ultimately AOT_show ‹ψ{«AOT_term_of_var (Rep α)»}›
84 using AOT_sem_box AOT_sem_imp by blast
85qed
86lemmas "ψ" = restricted_var_condition
87
88AOT_theorem GEN: assumes ‹for arbitrary α: φ{«AOT_term_of_var (Rep α)»}›
89 shows ‹∀α (ψ{α} → φ{α})›
90proof(rule GEN; rule "→I")
91 interpret type_definition Rep Abs "{ α . [w⇩0 ⊨ ψ{α}]}"
92 using AOT_restricted_type_definition.
93 fix α
94 AOT_assume ‹ψ{α}›
95 AOT_hence ‹❙𝒜ψ{α}›
96 by (metis AOT_model_axiom_def AOT_sem_box AOT_sem_imp act_closure rigid_condition)
97 hence 0: ‹[w⇩0 ⊨ ψ{α}]› by (metis AOT_sem_act)
98 {
99 fix τ
100 assume α_def: ‹α = Rep τ›
101 AOT_have ‹φ{α}›
102 unfolding α_def
103 using assms by blast
104 }
105 AOT_thus ‹φ{α}›
106 using Rep_cases[simplified, OF 0]
107 by blast
108qed
109lemmas "∀I" = GEN
110
111end
112
113
114lemma AOT_restricted_type_intro[AOT_no_atp, no_atp]:
115 assumes ‹type_definition Rep Abs { α . [w⇩0 ⊨ ψ{α}]}›
116 and ‹AOT_rigid_restriction_condition ψ›
117 shows ‹AOT_restricted_type ψ Rep Abs›
118 by (auto intro!: assms AOT_restricted_type_axioms.intro AOT_restricted_type.intro)
119
120
121
122ML‹
123fun register_rigid_restricted_type (name:string, restriction:string) thy =
124let
125val ctxt = thy
126val ctxt = setupStrictWorld ctxt
127val trm = Syntax.check_term ctxt (AOT_read_term @{nonterminal φ'} ctxt restriction)
128val free = case (Term.add_frees trm []) of [f] => f
129 | _ => raise Term.TERM ("Expected single free variable.", [trm])
130val trm = Term.absfree free trm
131val localeTerm = HOLogic.mk_Trueprop
132 (Const (\<^const_name>‹AOT_rigid_restriction_condition›, dummyT) $ trm)
133val localeTerm = Syntax.check_prop ctxt localeTerm
134val int_bnd = Binding.concealed (Binding.qualify true "internal" (Binding.name name))
135val bnds = {Rep_name = Binding.qualify true name (Binding.name "Rep"),
136 Abs_name = Binding.qualify true "Abs" int_bnd,
137 type_definition_name = Binding.qualify true "type_definition" int_bnd}
138
139fun after_qed witts thy = let
140 val thms = (map (Element.conclude_witness ctxt) (flat witts))
141
142 val typeset = HOLogic.mk_Collect ("α", dummyT,
143 \<^const>‹AOT_model_valid_in› $ \<^const>‹w⇩0› $
144 (trm $ (Const (\<^const_name>‹AOT_term_of_var›, dummyT) $ Bound 0)))
145 val typeset = Syntax.check_term thy typeset
146 val nonempty_thm = Drule.OF
147 (@{thm AOT_rigid_restriction_condition.type_set_nonempty}, thms)
148
149 val ((_,st),thy) = Typedef.add_typedef {overloaded=true}
150 (Binding.name name, [], Mixfix.NoSyn) typeset (SOME bnds)
151 (fn ctxt => (Tactic.resolve_tac ctxt ([nonempty_thm]) 1)) thy
152 val ({rep_type = _, abs_type = _, Rep_name = Rep_name, Abs_name = Abs_name,
153 axiom_name = _},
154 {inhabited = _, type_definition = type_definition, Rep = _,
155 Rep_inverse = _, Abs_inverse = _, Rep_inject = _, Abs_inject = _,
156 Rep_cases = _, Abs_cases = _, Rep_induct = _, Abs_induct = _}) = st
157
158 val locale_thm = Drule.OF (@{thm AOT_restricted_type_intro}, type_definition::thms)
159
160 val st = Interpretation.global_interpretation (([(@{locale AOT_restricted_type},
161 ((name, true), (Expression.Named [
162 ("ψ", trm),
163 ("Rep", Const (Rep_name, dummyT)),
164 ("Abs", Const (Abs_name, dummyT))], [])))
165 ], [])) [] thy
166
167 val st = Proof.refine_insert [locale_thm] st
168 val thy = Proof.global_immediate_proof st
169
170 val thy = Local_Theory.background_theory (AOT_Constraints.map (
171 Symtab.update (name, (term_of (snd free), term_of (snd free))))) thy
172 val thy = Local_Theory.background_theory (AOT_Restriction.map (
173 Symtab.update (name, (trm, Const (Rep_name, dummyT))))) thy
174
175 in thy end
176in
177Element.witness_proof after_qed [[localeTerm]] thy
178end
179
180val _ =
181 Outer_Syntax.command
182 \<^command_keyword>‹AOT_register_rigid_restricted_type›
183 "Register a restricted type."
184 (((Parse.short_ident --| Parse.$$$ ":") -- Parse.term) >>
185 (Toplevel.local_theory_to_proof NONE NONE o register_rigid_restricted_type));
186›
187
188
189ML‹
190fun get_instantiated_allI ctxt varname thm = let
191val trm = Thm.concl_of thm
192val trm = case trm of (@{const Trueprop} $ (@{const AOT_model_valid_in} $ _ $ x)) => x
193 | _ => raise Term.TERM ("Expected simple theorem.", [trm])
194fun extractVars (Const (\<^const_name>‹AOT_term_of_var›, t) $ (Const rep $ Var v)) =
195 (if fst (fst v) = fst varname
196 then [Const (\<^const_name>‹AOT_term_of_var›, t) $ (Const rep $ Var v)]
197 else [])
198 | extractVars (t1 $ t2) = extractVars t1 @ extractVars t2
199 | extractVars (Abs (_, _, t)) = extractVars t
200 | extractVars _ = []
201val vars = extractVars trm
202val vartrm = hd vars
203val vars = fold Term.add_vars vars []
204val var = hd vars
205val trmty = (case vartrm of (Const (_, Type ("fun", [_, ty])) $ _) => ty
206 | _ => raise Match)
207val varty = snd var
208val tyname = fst (Term.dest_Type varty)
209val b = tyname^".∀I"
210val thms = fst (Context.map_proof_result (fn ctxt => (Attrib.eval_thms ctxt
211 [(Facts.Named ((b,Position.none),NONE),[])], ctxt)) ctxt)
212val allthm = (case thms of (thm::_) => thm
213 | _ => raise Fail "Unknown restricted type.")
214val trm = Abs (Term.string_of_vname (fst var), trmty, Term.abstract_over (vartrm, trm))
215val trm = Thm.cterm_of (Context.proof_of ctxt) trm
216val phi = hd (Term.add_vars (Thm.prop_of allthm) [])
217val allthm = Drule.instantiate_normalize (TVars.empty, Vars.make [(phi,trm)]) allthm
218in
219allthm
220end
221›
222
223
224attribute_setup "unconstrain" =
225 ‹Scan.lift (Scan.repeat1 Args.var) >> (fn args => Thm.rule_attribute []
226 (fn ctxt => fn thm =>
227 let
228 val thm = fold (fn arg => fn thm => thm RS get_instantiated_allI ctxt arg thm)
229 args thm
230 val thm = fold (fn _ => fn thm => thm RS @{thm "∀E"(2)}) args thm
231 in
232 thm
233 end))›
234 "Generalize a statement about restricted variables to a statement about
235 unrestricted variables with explicit restriction condition."
236
237
238
239context AOT_restricted_type
240begin
241
242AOT_theorem "rule-ui":
243 assumes ‹∀α(ψ{α} → φ{α})›
244 shows ‹φ{«AOT_term_of_var (Rep α)»}›
245proof -
246 AOT_have ‹φ{α}› if ‹ψ{α}› for α using assms[THEN "∀E"(2), THEN "→E"] that by blast
247 moreover AOT_have ‹ψ{«AOT_term_of_var (Rep α)»}›
248 by (auto simp: ψ)
249 ultimately show ?thesis by blast
250qed
251lemmas "∀E" = "rule-ui"
252
253AOT_theorem "instantiation":
254 assumes ‹for arbitrary β: φ{«AOT_term_of_var (Rep β)»} ❙⊢ χ› and ‹∃α (ψ{α} & φ{α})›
255 shows ‹χ›
256proof -
257 AOT_have ‹φ{«AOT_term_of_var (Rep α)»} → χ› for α
258 using assms(1)
259 by (simp add: "deduction-theorem")
260 AOT_hence 0: ‹∀α (ψ{α} → (φ{α} → χ))›
261 using GEN by simp
262 moreover AOT_obtain α where ‹ψ{α} & φ{α}› using assms(2) "∃E"[rotated] by blast
263 ultimately AOT_show ‹χ› using "AOT_PLM.∀E"(2)[THEN "→E", THEN "→E"] "&E" by fast
264qed
265lemmas "∃E" = "instantiation"
266
267AOT_theorem existential: assumes ‹φ{«AOT_term_of_var (Rep β)»}›
268 shows ‹∃ α (ψ{α} & φ{α})›
269 by (meson AOT_restricted_type.ψ AOT_restricted_type_axioms assms
270 "&I" "existential:2[const_var]")
271lemmas "∃I" = existential
272end
273
274
275context AOT_rigid_restriction_condition
276begin
277
278AOT_theorem "res-var-bound-reas[1]":
279 ‹∀α(ψ{α} → ∀β φ{α, β}) ≡ ∀β∀α (ψ{α} → φ{α, β})›
280proof(safe intro!: "≡I" "→I" GEN)
281 fix β α
282 AOT_assume ‹∀α (ψ{α} → ∀β φ{α, β})›
283 AOT_hence ‹ψ{α} → ∀β φ{α, β}› using "∀E"(2) by blast
284 moreover AOT_assume ‹ψ{α}›
285 ultimately AOT_have ‹∀β φ{α, β}› using "→E" by blast
286 AOT_thus ‹φ{α, β}› using "∀E"(2) by blast
287next
288 fix α β
289 AOT_assume ‹∀β∀α(ψ{α} → φ{α, β})›
290 AOT_hence ‹∀α(ψ{α} → φ{α, β})› using "∀E"(2) by blast
291 AOT_hence ‹ψ{α} → φ{α, β}› using "∀E"(2) by blast
292 moreover AOT_assume ‹ψ{α}›
293 ultimately AOT_show ‹φ{α, β}› using "→E" by blast
294qed
295
296AOT_theorem "res-var-bound-reas[BF]":
297 ‹∀α(ψ{α} → □φ{α}) → □∀α(ψ{α} → φ{α})›
298proof(safe intro!: "→I")
299 AOT_assume ‹∀α(ψ{α} → □φ{α})›
300 AOT_hence ‹ψ{α} → □φ{α}› for α
301 using "∀E"(2) by blast
302 AOT_hence ‹□(ψ{α} → φ{α})› for α
303 by (metis "sc-eq-box-box:6" rigid_condition "vdash-properties:6")
304 AOT_hence ‹∀α □(ψ{α} → φ{α})›
305 by (rule GEN)
306 AOT_thus ‹□∀α (ψ{α} → φ{α})›
307 by (metis "BF" "vdash-properties:6")
308qed
309
310AOT_theorem "res-var-bound-reas[CBF]":
311‹□∀α(ψ{α} → φ{α}) → ∀α(ψ{α} → □φ{α})›
312proof(safe intro!: "→I" GEN)
313 fix α
314 AOT_assume ‹□∀α (ψ{α} → φ{α})›
315 AOT_hence ‹∀α □(ψ{α} → φ{α})›
316 by (metis "CBF" "vdash-properties:6")
317 AOT_hence 1: ‹□(ψ{α} → φ{α})›
318 using "∀E"(2) by blast
319 AOT_assume ‹ψ{α}›
320 AOT_hence ‹□ψ{α}›
321 by (metis "B◇" "T◇" rigid_condition "vdash-properties:6")
322 AOT_thus ‹□φ{α}›
323 using 1 "qml:1"[axiom_inst, THEN "→E", THEN "→E"] by blast
324qed
325
326AOT_theorem "res-var-bound-reas[2]":
327‹∀α (ψ{α} → ❙𝒜φ{α}) → ❙𝒜∀α (ψ{α} → φ{α})›
328proof(safe intro!: "→I")
329 AOT_assume ‹∀α (ψ{α} → ❙𝒜φ{α})›
330 AOT_hence ‹ψ{α} → ❙𝒜φ{α}› for α
331 using "∀E"(2) by blast
332 AOT_hence ‹❙𝒜(ψ{α} → φ{α})› for α
333 by (metis "sc-eq-box-box:7" rigid_condition "vdash-properties:6")
334 AOT_hence ‹∀α ❙𝒜(ψ{α} → φ{α})›
335 by (rule GEN)
336 AOT_thus ‹❙𝒜∀α(ψ{α} → φ{α})›
337 by (metis "≡E"(2) "logic-actual-nec:3"[axiom_inst])
338qed
339
340
341AOT_theorem "res-var-bound-reas[3]":
342 ‹❙𝒜∀α (ψ{α} → φ{α}) → ∀α (ψ{α} → ❙𝒜φ{α})›
343proof(safe intro!: "→I" GEN)
344 fix α
345 AOT_assume ‹❙𝒜∀α (ψ{α} → φ{α})›
346 AOT_hence ‹∀α ❙𝒜(ψ{α} → φ{α})›
347 by (metis "≡E"(1) "logic-actual-nec:3"[axiom_inst])
348 AOT_hence 1: ‹❙𝒜(ψ{α} → φ{α})› by (metis "rule-ui:3")
349 AOT_assume ‹ψ{α}›
350 AOT_hence ‹❙𝒜ψ{α}›
351 by (metis "nec-imp-act" "qml:2"[axiom_inst] rigid_condition "→E")
352 AOT_thus ‹❙𝒜φ{α}›
353 using 1 by (metis "act-cond" "→E")
354qed
355
356AOT_theorem "res-var-bound-reas[Buridan]":
357 ‹∃α (ψ{α} & □φ{α}) → □∃α (ψ{α} & φ{α})›
358proof (rule "→I")
359 AOT_assume ‹∃α (ψ{α} & □φ{α})›
360 then AOT_obtain α where ‹ψ{α} & □φ{α}›
361 using "∃E"[rotated] by blast
362 AOT_hence ‹□(ψ{α} & φ{α})›
363 by (metis "KBasic:11" "KBasic:3" "T◇" "&I" "&E"(1) "&E"(2)
364 "≡E"(2) "reductio-aa:1" rigid_condition "vdash-properties:6")
365 AOT_hence ‹∃α □(ψ{α} & φ{α})›
366 by (rule "∃I")
367 AOT_thus ‹□∃α (ψ{α} & φ{α})›
368 by (rule Buridan[THEN "→E"])
369qed
370
371AOT_theorem "res-var-bound-reas[BF◇]":
372 ‹◇∃α (ψ{α} & φ{α}) → ∃α (ψ{α} & ◇φ{α})›
373proof(rule "→I")
374 AOT_assume ‹◇∃α (ψ{α} & φ{α})›
375 AOT_hence ‹∃α ◇(ψ{α} & φ{α})›
376 using "BF◇"[THEN "→E"] by blast
377 then AOT_obtain α where ‹◇(ψ{α} & φ{α})›
378 using "∃E"[rotated] by blast
379 AOT_hence ‹◇ψ{α}› and ‹◇φ{α}›
380 using "KBasic2:3" "&E" "→E" by blast+
381 moreover AOT_have ‹ψ{α}›
382 using calculation rigid_condition by (metis "B◇" "K◇" "→E")
383 ultimately AOT_have ‹ψ{α} & ◇φ{α}›
384 using "&I" by blast
385 AOT_thus ‹∃α (ψ{α} & ◇φ{α})›
386 by (rule "∃I")
387qed
388
389AOT_theorem "res-var-bound-reas[CBF◇]":
390 ‹∃α (ψ{α} & ◇φ{α}) → ◇∃α (ψ{α} & φ{α})›
391proof(rule "→I")
392 AOT_assume ‹∃α (ψ{α} & ◇φ{α})›
393 then AOT_obtain α where ‹ψ{α} & ◇φ{α}›
394 using "∃E"[rotated] by blast
395 AOT_hence ‹□ψ{α}› and ‹◇φ{α}›
396 using rigid_condition[THEN "qml:2"[axiom_inst, THEN "→E"], THEN "→E"] "&E" by blast+
397 AOT_hence ‹◇(ψ{α} & φ{α})›
398 by (metis "KBasic:16" "con-dis-taut:5" "→E")
399 AOT_hence ‹∃α ◇(ψ{α} & φ{α})›
400 by (rule "∃I")
401 AOT_thus ‹◇∃α (ψ{α} & φ{α})›
402 using "CBF◇"[THEN "→E"] by fast
403qed
404
405AOT_theorem "res-var-bound-reas[A-Exists:1]":
406 ‹❙𝒜∃!α (ψ{α} & φ{α}) ≡ ∃!α (ψ{α} & ❙𝒜φ{α})›
407proof(safe intro!: "≡I" "→I")
408 AOT_assume ‹❙𝒜∃!α (ψ{α} & φ{α})›
409 AOT_hence ‹∃!α ❙𝒜(ψ{α} & φ{α})›
410 using "A-Exists:1"[THEN "≡E"(1)] by blast
411 AOT_hence ‹∃!α (❙𝒜ψ{α} & ❙𝒜φ{α})›
412 apply(AOT_subst ‹❙𝒜ψ{α} & ❙𝒜φ{α}› ‹❙𝒜(ψ{α} & φ{α})› for: α)
413 apply (meson "Act-Basic:2" "intro-elim:3:f" "oth-class-taut:3:a")
414 by simp
415 AOT_thus ‹∃!α (ψ{α} & ❙𝒜φ{α})›
416 apply (AOT_subst ‹ψ{α}› ‹❙𝒜ψ{α}› for: α)
417 using "Commutativity of ≡" "intro-elim:3:b" "sc-eq-fur:2"
418 "→E" rigid_condition by blast
419next
420 AOT_assume ‹∃!α (ψ{α} & ❙𝒜φ{α})›
421 AOT_hence ‹∃!α (❙𝒜ψ{α} & ❙𝒜φ{α})›
422 apply (AOT_subst ‹❙𝒜ψ{α}› ‹ψ{α}› for: α)
423 apply (meson "sc-eq-fur:2" "→E" rigid_condition)
424 by simp
425 AOT_hence ‹∃!α ❙𝒜(ψ{α} & φ{α})›
426 apply (AOT_subst ‹❙𝒜(ψ{α} & φ{α})› ‹❙𝒜ψ{α} & ❙𝒜φ{α}› for: α)
427 using "Act-Basic:2" apply presburger
428 by simp
429 AOT_thus ‹❙𝒜∃!α (ψ{α} & φ{α})›
430 by (metis "A-Exists:1" "intro-elim:3:b")
431qed
432
433end
434
435
436end
437