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
9sectionRestricted 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_nameAOT_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_nameAOT_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_keywordAOT_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  { α . [w0  ψ{α}]}
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 { α . [w0  ψ{α}]}
67begin
68
69AOT_theorem restricted_var_condition: ψ{«AOT_term_of_var (Rep α)»}
70proof -
71  interpret type_definition Rep Abs "{ α . [w0  ψ{α}]}"
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 "{ α . [w0  ψ{α}]}"
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: [w0  ψ{α}] 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 { α . [w0  ψ{α}]}
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_nameAOT_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    constAOT_model_valid_in $ constw0 $
144    (trm $ (Const (const_nameAOT_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_keywordAOT_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(* Generalized mechanism for "AOT_restricted_type.∀I" followed by ∀E *)
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_nameAOT_term_of_var, t) $ (Const rep $ Var v)) =
195    (if fst (fst v) = fst varname
196     then [Const (const_nameAOT_term_of_var, t) $ (Const rep $ Var v)]
197     else []) (* TODO: care about the index *)
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" (* TODO: better way to find the theorem *)
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(* TODO: unconstraining multiple variables does not work yet *)
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(*>*)