1.1 --- a/NEWS Fri Apr 02 12:25:48 2004 +0200
1.2 +++ b/NEWS Fri Apr 02 14:08:30 2004 +0200
1.3 @@ -52,7 +52,8 @@
1.4
1.5 *** Isar ***
1.6
1.7 -* Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
1.8 +* Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac,
1.9 + cut_tac, subgoal_tac and thin_tac:
1.10 - Now understand static (Isar) contexts. As a consequence, users of Isar
1.11 locales are no longer forced to write Isar proof scripts.
1.12 For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
1.13 @@ -79,6 +80,14 @@
1.14 specification and "includes" elements in goal statement.
1.15 - Rule sets <locale>.intro and <locale>.axioms no longer declared as
1.16 [intro?] and [elim?] (respectively) by default.
1.17 + - Experimental command for instantiation of locales in proof contexts:
1.18 + instantiate <label>: <loc>
1.19 + Instantiates locale <loc> and adds all its theorems to the current context
1.20 + taking into account their attributes, and qualifying their names with
1.21 + <label>. If the locale has assumptions, a chained fact of the form
1.22 + "<loc> t1 ... tn" is expected from which instantiations of the parameters
1.23 + are derived.
1.24 + A few (very simple) examples can be found in FOL/ex/LocaleInst.thy.
1.25
1.26 * HOL: Tactic emulation methods induct_tac and case_tac understand static
1.27 (Isar) contexts.
2.1 --- a/etc/isar-keywords-ZF.el Fri Apr 02 12:25:48 2004 +0200
2.2 +++ b/etc/isar-keywords-ZF.el Fri Apr 02 14:08:30 2004 +0200
2.3 @@ -55,6 +55,7 @@
2.4 "exit"
2.5 "extract"
2.6 "extract_type"
2.7 + "finalconsts"
2.8 "finally"
2.9 "fix"
2.10 "from"
2.11 @@ -69,6 +70,7 @@
2.12 "inductive_cases"
2.13 "init_toplevel"
2.14 "instance"
2.15 + "instantiate"
2.16 "judgment"
2.17 "kill"
2.18 "kill_thy"
2.19 @@ -308,6 +310,7 @@
2.20 "defs"
2.21 "extract"
2.22 "extract_type"
2.23 + "finalconsts"
2.24 "generate_code"
2.25 "global"
2.26 "hide"
2.27 @@ -393,6 +396,7 @@
2.28
2.29 (defconst isar-keywords-proof-decl
2.30 '("also"
2.31 + "instantiate"
2.32 "let"
2.33 "moreover"
2.34 "note"
3.1 --- a/etc/isar-keywords.el Fri Apr 02 12:25:48 2004 +0200
3.2 +++ b/etc/isar-keywords.el Fri Apr 02 14:08:30 2004 +0200
3.3 @@ -73,6 +73,7 @@
3.4 "inductive_cases"
3.5 "init_toplevel"
3.6 "instance"
3.7 + "instantiate"
3.8 "judgment"
3.9 "kill"
3.10 "kill_thy"
3.11 @@ -429,6 +430,7 @@
3.12
3.13 (defconst isar-keywords-proof-decl
3.14 '("also"
3.15 + "instantiate"
3.16 "let"
3.17 "moreover"
3.18 "note"
4.1 --- a/src/FOL/IsaMakefile Fri Apr 02 12:25:48 2004 +0200
4.2 +++ b/src/FOL/IsaMakefile Fri Apr 02 14:08:30 2004 +0200
4.3 @@ -44,6 +44,7 @@
4.4
4.5 $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy \
4.6 ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy \
4.7 + ex/LocaleInst.thy \
4.8 ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy \
4.9 ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\
4.10 ex/foundn.ML ex/Intuitionistic.thy ex/intro.ML ex/prop.ML ex/quant.ML
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/FOL/ex/LocaleInst.thy Fri Apr 02 14:08:30 2004 +0200
5.3 @@ -0,0 +1,114 @@
5.4 +(* Title: FOL/ex/LocaleInst.thy
5.5 + ID: $Id$
5.6 + Author: Clemens Ballarin
5.7 + Copyright (c) 2004 by Clemens Ballarin
5.8 +
5.9 +Test of locale instantiation mechanism, also provides a few examples.
5.10 +*)
5.11 +
5.12 +header {* Test of Locale instantiation *}
5.13 +
5.14 +theory LocaleInst = FOL:
5.15 +
5.16 +ML {* set show_hyps *}
5.17 +
5.18 +section {* Locale without assumptions *}
5.19 +
5.20 +locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
5.21 +
5.22 +lemma "[| A; B |] ==> A & B"
5.23 +proof -
5.24 + instantiate my: L1 txt {* No chained fact required. *}
5.25 + assume B and A txt {* order reversed *}
5.26 + then show "A & B" ..
5.27 + txt {* Applies @{thm my.rev_conjI}. *}
5.28 +qed
5.29 +
5.30 +section {* Simple locale with assumptions *}
5.31 +
5.32 +typedecl i
5.33 +arities i :: "term"
5.34 +
5.35 +consts bin :: "[i, i] => i" (infixl "#" 60)
5.36 +
5.37 +axioms i_assoc: "(x # y) # z = x # (y # z)"
5.38 + i_comm: "x # y = y # x"
5.39 +
5.40 +locale L2 =
5.41 + fixes OP (infixl "+" 60)
5.42 + assumes assoc: "(x + y) + z = x + (y + z)"
5.43 + and comm: "x + y = y + x"
5.44 +
5.45 +lemma (in L2) lcomm: "x + (y + z) = y + (x + z)"
5.46 +proof -
5.47 + have "x + (y + z) = (x + y) + z" by (simp add: assoc)
5.48 + also have "... = (y + x) + z" by (simp add: comm)
5.49 + also have "... = y + (x + z)" by (simp add: assoc)
5.50 + finally show ?thesis .
5.51 +qed
5.52 +
5.53 +lemmas (in L2) AC = comm assoc lcomm
5.54 +
5.55 +lemma "(x::i) # y # z # w = y # x # w # z"
5.56 +proof -
5.57 + have "L2 (op #)" by (rule L2.intro [of "op #", OF i_assoc i_comm])
5.58 + then instantiate my: L2
5.59 + txt {* Chained fact required to discharge assumptions of @{text L2}
5.60 + and instantiate parameters. *}
5.61 + show ?thesis by (simp only: my.OP.AC) (* or simply AC *)
5.62 +qed
5.63 +
5.64 +section {* Nested locale with assumptions *}
5.65 +
5.66 +locale L3 =
5.67 + fixes OP (infixl "+" 60)
5.68 + assumes assoc: "(x + y) + z = x + (y + z)"
5.69 +
5.70 +locale L4 = L3 +
5.71 + assumes comm: "x + y = y + x"
5.72 +
5.73 +lemma (in L4) lcomm: "x + (y + z) = y + (x + z)"
5.74 +proof -
5.75 + have "x + (y + z) = (x + y) + z" by (simp add: assoc)
5.76 + also have "... = (y + x) + z" by (simp add: comm)
5.77 + also have "... = y + (x + z)" by (simp add: assoc)
5.78 + finally show ?thesis .
5.79 +qed
5.80 +
5.81 +lemmas (in L4) AC = comm assoc lcomm
5.82 +
5.83 +text {* Conceptually difficult locale:
5.84 + 2nd context fragment contains facts with differing metahyps. *}
5.85 +
5.86 +lemma L4_intro:
5.87 + fixes OP (infixl "+" 60)
5.88 + assumes assoc: "!!x y z. (x + y) + z = x + (y + z)"
5.89 + and comm: "!!x y. x + y = y + x"
5.90 + shows "L4 (op+)"
5.91 + by (blast intro: L4.intro L3.intro assoc L4_axioms.intro comm)
5.92 +
5.93 +lemma "(x::i) # y # z # w = y # x # w # z"
5.94 +proof -
5.95 + have "L4 (op #)" by (rule L4_intro [of "op #", OF i_assoc i_comm])
5.96 + then instantiate my: L4
5.97 + show ?thesis by (simp only: my.OP.AC) (* or simply AC *)
5.98 +qed
5.99 +
5.100 +section {* Locale with definition *}
5.101 +
5.102 +text {* This example is admittedly not very creative :-) *}
5.103 +
5.104 +locale L5 = L4 + var A +
5.105 + defines A_def: "A == True"
5.106 +
5.107 +lemma (in L5) lem: A
5.108 + by (unfold A_def) rule
5.109 +
5.110 +lemma "L5(op #) ==> True"
5.111 +proof -
5.112 + assume "L5(op #)"
5.113 + then instantiate my: L5
5.114 + show ?thesis by (rule lem) (* lem instantiated to True *)
5.115 +qed
5.116 +
5.117 +end
6.1 --- a/src/Pure/Isar/isar_syn.ML Fri Apr 02 12:25:48 2004 +0200
6.2 +++ b/src/Pure/Isar/isar_syn.ML Fri Apr 02 14:08:30 2004 +0200
6.3 @@ -357,6 +357,12 @@
6.4 OuterSyntax.command "using" "augment goal facts" K.prf_decl
6.5 (facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.using_facts)));
6.6
6.7 +val instantiateP =
6.8 + OuterSyntax.command "instantiate" "instantiate locale" K.prf_decl
6.9 + (P.name --| P.$$$ ":" -- P.xname
6.10 +(* (P.xname -- (P.$$$ "[" |-- P.name --| P.$$$ "]") *)
6.11 + >> (Toplevel.print oo (Toplevel.proof o IsarThy.instantiate_locale)));
6.12 +
6.13
6.14 (* proof context *)
6.15
6.16 @@ -756,7 +762,7 @@
6.17 default_proofP, immediate_proofP, done_proofP, skip_proofP,
6.18 forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
6.19 finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
6.20 - redoP, undos_proofP, undoP, killP,
6.21 + redoP, undos_proofP, undoP, killP, instantiateP,
6.22 (*diagnostic commands*)
6.23 pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
6.24 print_syntaxP, print_theoremsP, print_localesP, print_localeP,
7.1 --- a/src/Pure/Isar/isar_thy.ML Fri Apr 02 12:25:48 2004 +0200
7.2 +++ b/src/Pure/Isar/isar_thy.ML Fri Apr 02 14:08:30 2004 +0200
7.3 @@ -48,6 +48,7 @@
7.4 val using_facts_i: (thm * Proof.context attribute list) list list
7.5 -> ProofHistory.T -> ProofHistory.T
7.6 val chain: ProofHistory.T -> ProofHistory.T
7.7 + val instantiate_locale: string * string -> ProofHistory.T -> ProofHistory.T
7.8 val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T
7.9 val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T
7.10 val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
7.11 @@ -290,6 +291,10 @@
7.12
7.13 val chain = ProofHistory.apply Proof.chain;
7.14
7.15 +(* locale instantiation *)
7.16 +
7.17 +fun instantiate_locale (prfx, loc) =
7.18 + ProofHistory.apply (Proof.instantiate_locale (loc, prfx));
7.19
7.20 (* context *)
7.21
8.1 --- a/src/Pure/Isar/locale.ML Fri Apr 02 12:25:48 2004 +0200
8.2 +++ b/src/Pure/Isar/locale.ML Fri Apr 02 14:08:30 2004 +0200
8.3 @@ -65,6 +65,7 @@
8.4 val add_thmss: string -> ((string * thm list) * context attribute list) list ->
8.5 theory * context -> (theory * context) * (string * thm list) list
8.6 val prune_prems: theory -> thm -> thm
8.7 + val instantiate: string -> string -> thm list option -> context -> context
8.8 val setup: (theory -> theory) list
8.9 end;
8.10
8.11 @@ -96,7 +97,7 @@
8.12
8.13 type locale =
8.14 {view: cterm list * thm list,
8.15 - (* If locale "loc" contains assumptions, either via import or in the
8.16 + (* CB: If locale "loc" contains assumptions, either via import or in the
8.17 locale body, a locale predicate "loc" is defined capturing all the
8.18 assumptions. If both import and body contain assumptions, additionally
8.19 a delta predicate "loc_axioms" is defined that abbreviates the
8.20 @@ -107,10 +108,11 @@
8.21 locales with import from the import hierarchy (duplicates removed,
8.22 cf. [1], normalisation of locale expressions).
8.23
8.24 - The first part of view in the above definition (also called statement)
8.25 - represents this list of assumptions. The second part (also called
8.26 - axioms) contains projections from the predicate "loc" to these
8.27 - assumptions.
8.28 + The record entry view is either ([], []) or ([statement], axioms)
8.29 + where statement is the predicate "loc" applied to the parameters,
8.30 + and axioms contains projections from "loc" to the list of assumptions
8.31 + generated when entering the locale.
8.32 + It appears that an axiom of the form A [A] is never generated.
8.33 *)
8.34 import: expr, (*dynamic import*)
8.35 elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*)
8.36 @@ -229,7 +231,7 @@
8.37 Remove internal delta predicates (generated by "includes") from the
8.38 premises of a theorem.
8.39
8.40 - Assumes no outer quanfifiers and no flex-flex pairs.
8.41 + Assumes no outer quantifiers and no flex-flex pairs.
8.42 May change names of TVars.
8.43 Performs compress and close_derivation on result, if modified. **)
8.44
8.45 @@ -466,6 +468,9 @@
8.46
8.47 (* parameter types *)
8.48
8.49 +(* CB: frozen_tvars has the following type:
8.50 + ProofContext.context -> Term.typ list -> (Term.indexname * Term.typ) list *)
8.51 +
8.52 fun frozen_tvars ctxt Ts =
8.53 let
8.54 val tvars = rev (foldl Term.add_tvarsT ([], Ts));
8.55 @@ -492,6 +497,9 @@
8.56 in map (apsome (Envir.norm_type unifier')) Vs end;
8.57
8.58 fun params_of elemss = gen_distinct eq_fst (flat (map (snd o fst) elemss));
8.59 +
8.60 +(* CB: param_types has the following type:
8.61 + ('a * 'b Library.option) list -> ('a * 'b) list *)
8.62 fun param_types ps = mapfilter (fn (_, None) => None | (x, Some T) => Some (x, T)) ps;
8.63
8.64
8.65 @@ -499,6 +507,11 @@
8.66
8.67 local
8.68
8.69 +(* CB: unique_parms has the following type:
8.70 + 'a ->
8.71 + (('b * (('c * 'd) list * Symtab.key list)) * 'e) list ->
8.72 + (('b * ('c * 'd) list) * 'e) list *)
8.73 +
8.74 fun unique_parms ctxt elemss =
8.75 let
8.76 val param_decls =
8.77 @@ -511,6 +524,12 @@
8.78 | None => map (apfst (apsnd #1)) elemss)
8.79 end;
8.80
8.81 +(* CB: unify_parms has the following type:
8.82 + ProofContext.context ->
8.83 + (string * Term.typ) list ->
8.84 + (string * Term.typ Library.option) list list ->
8.85 + ((string * Term.sort) * Term.typ) list list *)
8.86 +
8.87 fun unify_parms ctxt fixed_parms raw_parmss =
8.88 let
8.89 val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
8.90 @@ -649,13 +668,22 @@
8.91
8.92 in
8.93
8.94 +(* CB: activate_facts prep_facts ((ctxt, axioms), elemss),
8.95 + where elemss is a list of pairs consisting of identifiers and context
8.96 + elements, extends ctxt by the context elements yielding ctxt' and returns
8.97 + ((ctxt', axioms'), (elemss', facts)).
8.98 + Assumptions use entries from axioms to set up exporters in ctxt'. Unused
8.99 + axioms are returned as axioms'; elemss' is obtained from elemss (without
8.100 + identifier) and the intermediate context with prep_facts.
8.101 + If get_facts or get_facts_i is used for prep_facts, these also remove
8.102 + the internal/external markers from elemss. *)
8.103 +
8.104 fun activate_facts prep_facts arg =
8.105 apsnd (apsnd flat o Library.split_list) (activate_elemss prep_facts arg);
8.106
8.107 end;
8.108
8.109
8.110 -
8.111 (** prepare context elements **)
8.112
8.113 (* expressions *)
8.114 @@ -669,7 +697,7 @@
8.115
8.116 local fun read_att attrib (x, srcs) = (x, map attrib srcs) in
8.117
8.118 -(* Map attrib over
8.119 +(* CB: Map attrib over
8.120 * A context element: add attrib to attribute lists of assumptions,
8.121 definitions and facts (on both sides for facts).
8.122 * Locale expression: no effect. *)
8.123 @@ -705,6 +733,22 @@
8.124
8.125 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
8.126
8.127 +(* CB: flatten (ids, expr) normalises expr (which is either a locale
8.128 + expression or a single context element) wrt.
8.129 + to the list ids of already accumulated identifiers.
8.130 + It returns (ids', elemss) where ids' is an extension of ids
8.131 + with identifiers generated for expr, and elemss is the list of
8.132 + context elements generated from expr, decorated with additional
8.133 + information (the identifiers?), including parameter names.
8.134 + It appears that the identifier name is empty for external elements
8.135 + (this is suggested by the implementation of activate_facts). *)
8.136 +
8.137 +fun flatten _ (ids, Elem (Fixes fixes)) =
8.138 + (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
8.139 + | flatten _ (ids, Elem elem) = (ids, [(("", []), Ext elem)])
8.140 + | flatten (ctxt, prep_expr) (ids, Expr expr) =
8.141 + apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr));
8.142 +
8.143 local
8.144
8.145 local
8.146 @@ -752,6 +796,9 @@
8.147
8.148 local
8.149
8.150 +(* CB: following code (norm_term, abstract_term, abstract_thm, bind_def)
8.151 + used in eval_text for defines elements. *)
8.152 +
8.153 val norm_term = Envir.beta_norm oo Term.subst_atomic;
8.154
8.155 fun abstract_term eq = (*assumes well-formedness according to ProofContext.cert_def*)
8.156 @@ -845,12 +892,22 @@
8.157
8.158 fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
8.159 let
8.160 + (* CB: raw_elemss are list of pairs consisting of identifiers and
8.161 + context elements, the latter marked as internal or external. *)
8.162 val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
8.163 + (* CB: raw_ctxt is context with additional fixed variables derived from
8.164 + the fixes elements in raw_elemss,
8.165 + raw_proppss contains assumptions and definitions from the
8.166 + (external?) elements in raw_elemss. *)
8.167 val raw_propps = map flat raw_proppss;
8.168 val raw_propp = flat raw_propps;
8.169 val (ctxt, all_propp) =
8.170 prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
8.171 + (* CB: read/cert entire proposition (conclusion and premises from
8.172 + the context elements). *)
8.173 val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt;
8.174 + (* CB: it appears that terms declared in the propositions are added
8.175 + to the context here. *)
8.176
8.177 val all_propp' = map2 (op ~~)
8.178 (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);
8.179 @@ -863,9 +920,33 @@
8.180 (map (ProofContext.default_type raw_ctxt) xs)
8.181 (map (ProofContext.default_type ctxt) xs);
8.182 val parms = param_types (xs ~~ typing);
8.183 + (* CB: parms are the parameters from raw_elemss, with correct typing. *)
8.184
8.185 + (* CB: extract information from assumes and defines elements
8.186 + (fixes and notes in raw_elemss don't have an effect on text and elemss),
8.187 + compute final form of context elements. *)
8.188 val (text, elemss) = finish_elemss ctxt parms do_close
8.189 (((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss);
8.190 + (* CB: text has the following structure:
8.191 + (((exts, exts'), (ints, ints')), (xs, env, defs))
8.192 + where
8.193 + exts: external assumptions (terms in external assumes elements)
8.194 + exts': dito, normalised wrt. env
8.195 + ints: internal assumptions (terms in internal assumes elements)
8.196 + ints': dito, normalised wrt. env
8.197 + xs: the free variables in exts' and ints' and rhss of definitions,
8.198 + this includes parameters except defined parameters
8.199 + env: list of term pairs encoding substitutions, where the first term
8.200 + is a free variable; substitutions represent defines elements and
8.201 + the rhs is normalised wrt. the previous env
8.202 + defs: theorems representing the substitutions from defines elements
8.203 + (thms are normalised wrt. env).
8.204 + elemss is an updated version of raw_elemss:
8.205 + - type info added to Fixes
8.206 + - axiom and definition statement replaced by corresponding one
8.207 + from proppss in Assumes and Defines
8.208 + - Facts unchanged
8.209 + *)
8.210 in ((parms, elemss, concl), text) end;
8.211
8.212 in
8.213 @@ -881,6 +962,7 @@
8.214 local
8.215
8.216 fun prep_name ctxt (name, atts) =
8.217 + (* CB: reject qualified names in locale declarations *)
8.218 if NameSpace.is_qualified name then
8.219 raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
8.220 else (name, atts);
8.221 @@ -909,15 +991,12 @@
8.222 let
8.223 val sign = ProofContext.sign_of context;
8.224
8.225 - fun flatten (ids, Elem (Fixes fixes)) =
8.226 - (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
8.227 - | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)])
8.228 - | flatten (ids, Expr expr) =
8.229 - apsnd (map (apsnd Int)) (flatten_expr context (ids, prep_expr sign expr));
8.230 -
8.231 - val (import_ids, raw_import_elemss) = flatten ([], Expr import);
8.232 + val (import_ids, raw_import_elemss) = flatten (context, prep_expr sign) ([], Expr import);
8.233 (* CB: normalise "includes" among elements *)
8.234 - val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
8.235 + val raw_elemss = flat (#2 ((foldl_map (flatten (context, prep_expr sign))
8.236 + (import_ids, elements))));
8.237 + (* CB: raw_import_elemss @ raw_elemss is the normalised list of
8.238 + context elements obtained from import and elements. *)
8.239 val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
8.240 context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
8.241 val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
8.242 @@ -938,7 +1017,7 @@
8.243 val thy = ProofContext.theory_of ctxt;
8.244 val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale;
8.245 val ((view_statement, view_axioms), fixed_params, import) =
8.246 -(* view_axioms are xxx.axioms of locale xxx *)
8.247 +(* CB: view_axioms are xxx.axioms of locale xxx *)
8.248 (case locale of None => (([], []), [], empty)
8.249 | Some name =>
8.250 let val {view, params = (ps, _), ...} = the_locale thy name
8.251 @@ -949,7 +1028,7 @@
8.252
8.253 in
8.254
8.255 -(* CB: arguments are: x->import, y->body (elements?), z->context *)
8.256 +(* CB: arguments are: x->import, y->body (elements), z->context *)
8.257 fun read_context x y z = #1 (gen_context true [] [] x y [] z);
8.258 fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z);
8.259
8.260 @@ -959,6 +1038,157 @@
8.261 end;
8.262
8.263
8.264 +(** CB: experimental instantiation mechanism **)
8.265 +
8.266 +fun instantiate loc_name prfx raw_inst ctxt =
8.267 + let
8.268 + val thy = ProofContext.theory_of ctxt;
8.269 + val sign = Theory.sign_of thy;
8.270 + val tsig = Sign.tsig_of sign;
8.271 + val cert = cterm_of sign;
8.272 +
8.273 + (** process the locale **)
8.274 +
8.275 + val {view = (_, axioms), params = (ps, _), ...} =
8.276 + the_locale thy (intern sign loc_name);
8.277 + val fixed_params = param_types ps;
8.278 + val (ids, raw_elemss) =
8.279 + flatten (ctxt, intern_expr sign) ([], Expr (Locale loc_name));
8.280 + val ((parms, all_elemss, concl),
8.281 + (spec as (_, (ints, _)), (xs, env, defs))) =
8.282 + read_elemss false (* do_close *) ctxt
8.283 + fixed_params (* could also put [] here??? *) raw_elemss
8.284 + [] (* concl *);
8.285 +
8.286 + (** analyse the instantiation theorem inst **)
8.287 +
8.288 + val inst = case raw_inst of
8.289 + None => if null ints
8.290 + then None
8.291 + else error "Locale has assumptions but no chained fact was found"
8.292 + | Some [] => if null ints
8.293 + then None
8.294 + else error "Locale has assumptions but no chained fact was found"
8.295 + | Some [thm] => if null ints
8.296 + then (warning "Locale has no assumptions: fact ignored"; None)
8.297 + else Some thm
8.298 + | Some _ => error "Multiple facts are not allowed";
8.299 +
8.300 + val args = case inst of
8.301 + None => []
8.302 + | Some thm => thm |> prop_of |> ObjectLogic.drop_judgment sign
8.303 + |> Term.strip_comb |> snd;
8.304 + val cargs = map cert args;
8.305 +
8.306 + (* process parameters: match their types with those of arguments *)
8.307 +
8.308 + val def_names = map (fn (Free (s, _), _) => s) env;
8.309 + val (defined, assumed) = partition
8.310 + (fn (s, _) => s mem def_names) fixed_params;
8.311 + val cassumed = map (cert o Free) assumed;
8.312 + val cdefined = map (cert o Free) defined;
8.313 +
8.314 + val param_types = map snd assumed;
8.315 + val v_param_types = map Type.varifyT param_types;
8.316 + val arg_types = map Term.fastype_of args;
8.317 + val Tenv = foldl (Type.typ_match tsig)
8.318 + (Vartab.empty, v_param_types ~~ arg_types)
8.319 + handle Library.LIST "~~" => error "Number of parameters does not match number of arguments of chained fact";
8.320 + (* get their sorts *)
8.321 + val tfrees = foldr Term.add_typ_tfrees (param_types, []);
8.322 + val Tenv' = map
8.323 + (fn ((a, i), T) => ((a, the (assoc_string (tfrees, a))), T))
8.324 + (Vartab.dest Tenv);
8.325 +
8.326 + (* process (internal) elements *)
8.327 +
8.328 + fun inst_type [] T = T
8.329 + | inst_type env T =
8.330 + Term.map_type_tfree (fn v => if_none (assoc (env, v)) (TFree v)) T;
8.331 +
8.332 + fun inst_term [] t = t
8.333 + | inst_term env t = Term.map_term_types (inst_type env) t;
8.334 +
8.335 + (* parameters with argument types *)
8.336 +
8.337 + val cparams' = map (cterm_of sign o inst_term Tenv' o term_of) cassumed;
8.338 + val cdefined' = map (cert o inst_term Tenv' o term_of) cdefined;
8.339 + val cdefining = map (cert o inst_term Tenv' o snd) env;
8.340 +
8.341 + fun inst_thm _ [] th = th
8.342 + | inst_thm ctxt Tenv th =
8.343 + let
8.344 + val sign = ProofContext.sign_of ctxt;
8.345 + val cert = Thm.cterm_of sign;
8.346 + val certT = Thm.ctyp_of sign;
8.347 + val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
8.348 + val tfrees = foldr Term.add_term_tfree_names (prop :: hyps, []);
8.349 + val Tenv' = filter (fn ((a, _), _) => a mem_string tfrees) Tenv;
8.350 + in
8.351 + if null Tenv' then th
8.352 + else
8.353 + th
8.354 + |> Drule.implies_intr_list (map cert hyps)
8.355 + |> Drule.tvars_intr_list (map (#1 o #1) Tenv')
8.356 + |> (fn (th', al) => th' |>
8.357 + Thm.instantiate ((map (fn ((a, _), T) =>
8.358 + (the (assoc (al, a)), certT T)) Tenv'), []))
8.359 + |> (fn th'' => Drule.implies_elim_list th''
8.360 + (map (Thm.assume o cert o inst_term Tenv') hyps))
8.361 + end;
8.362 +
8.363 + fun inst_thm' thm =
8.364 + let
8.365 + (* not all axs are normally applicable *)
8.366 + val hyps = #hyps (rep_thm thm);
8.367 + val ass = map (fn ax => (prop_of ax, ax)) axioms;
8.368 + val axs' = foldl (fn (axs, hyp) =>
8.369 + (case assoc (ass, hyp) of None => axs
8.370 + | Some ax => axs @ [ax])) ([], hyps);
8.371 + val thm' = Drule.satisfy_hyps axs' thm;
8.372 + (* instantiate types *)
8.373 + val thm'' = inst_thm ctxt Tenv' thm';
8.374 + (* substitute arguments and discharge hypotheses *)
8.375 + val thm''' = case inst of
8.376 + None => thm''
8.377 + | Some inst_thm => let
8.378 + val hyps = #hyps (rep_thm thm'');
8.379 + val th = thm'' |> implies_intr_hyps
8.380 + |> forall_intr_list (cparams' @ cdefined')
8.381 + |> forall_elim_list (cargs @ cdefining)
8.382 + (* th has premises of the form either inst_thm or x==x *)
8.383 + fun mk hyp = if Logic.is_equals hyp
8.384 + then hyp |> Logic.dest_equals |> snd |> cert
8.385 + |> reflexive
8.386 + else inst_thm
8.387 + in implies_elim_list th (map mk hyps)
8.388 + end;
8.389 + in thm''' end;
8.390 +
8.391 + fun inst_elem (ctxt, (Ext _)) = ctxt
8.392 + | inst_elem (ctxt, (Int (Notes facts))) =
8.393 + (* instantiate fact *)
8.394 + let val facts' =
8.395 + map (apsnd (map (apfst (map inst_thm')))) facts
8.396 + (* rename fact *)
8.397 + val facts'' =
8.398 + map (apfst (apfst (fn "" => ""
8.399 + | s => NameSpace.append prfx s)))
8.400 + facts'
8.401 + in fst (ProofContext.have_thmss_i facts'' ctxt)
8.402 + end
8.403 + | inst_elem (ctxt, (Int _)) = ctxt;
8.404 +
8.405 + fun inst_elems (ctxt, (id, elems)) = foldl inst_elem (ctxt, elems);
8.406 +
8.407 + fun inst_elemss ctxt elemss = foldl inst_elems (ctxt, elemss);
8.408 +
8.409 + (* main part *)
8.410 +
8.411 + val ctxt' = ProofContext.qualified true ctxt;
8.412 + in ProofContext.restore_qualified ctxt (inst_elemss ctxt' all_elemss)
8.413 + end;
8.414 +
8.415
8.416 (** define locales **)
8.417
8.418 @@ -1019,6 +1249,7 @@
8.419
8.420 fun smart_have_thmss kind None = PureThy.have_thmss_i (Drule.kind kind)
8.421 | smart_have_thmss kind (Some (loc, _)) = have_thmss_qualified kind loc;
8.422 + (* CB: only used in Proof.finish_global. *)
8.423
8.424 end;
8.425
8.426 @@ -1050,6 +1281,8 @@
8.427
8.428 val have_thmss = gen_have_thmss intern ProofContext.get_thms;
8.429 val have_thmss_i = gen_have_thmss (K I) (K I);
8.430 + (* CB: have_thmss(_i) is the base for the Isar commands
8.431 + "theorems (in loc)" and "declare (in loc)". *)
8.432
8.433 fun add_thmss loc args (thy, ctxt) =
8.434 let
8.435 @@ -1059,6 +1292,7 @@
8.436 val ((ctxt', _), (_, facts')) =
8.437 activate_facts (K I) ((ctxt, view_axioms), [(("", []), [Notes args'])]);
8.438 in ((thy', ctxt'), facts') end;
8.439 + (* CB: only used in Proof.finish_global. *)
8.440
8.441 end;
8.442
9.1 --- a/src/Pure/Isar/method.ML Fri Apr 02 12:25:48 2004 +0200
9.2 +++ b/src/Pure/Isar/method.ML Fri Apr 02 14:08:30 2004 +0200
9.3 @@ -368,7 +368,8 @@
9.4 val params = Logic.strip_params Bi
9.5 (* params of subgoal i as string typ pairs *)
9.6 val params = rev(Term.rename_wrt_term Bi params)
9.7 - (* as they are printed *)
9.8 + (* as they are printed: bound variables with *)
9.9 + (* the same name are renamed during printing *)
9.10 fun types' (a, ~1) = (case assoc (params, a) of
9.11 None => types (a, ~1)
9.12 | some => some)
10.1 --- a/src/Pure/Isar/outer_parse.ML Fri Apr 02 12:25:48 2004 +0200
10.2 +++ b/src/Pure/Isar/outer_parse.ML Fri Apr 02 14:08:30 2004 +0200
10.3 @@ -174,7 +174,8 @@
10.4 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
10.5
10.6 val uname = underscore >> K None || name >> Some;
10.7 -
10.8 + (* CB: underscore yields None, any other name Some with that string.
10.9 + Used, for example, in the renaming of locale parameters. *)
10.10
10.11 (* sorts and arities *)
10.12
11.1 --- a/src/Pure/Isar/proof.ML Fri Apr 02 12:25:48 2004 +0200
11.2 +++ b/src/Pure/Isar/proof.ML Fri Apr 02 14:08:30 2004 +0200
11.3 @@ -65,6 +65,7 @@
11.4 (thm list * context attribute list) list) list -> state -> state
11.5 val using_thmss: ((xstring * context attribute list) list) list -> state -> state
11.6 val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state
11.7 + val instantiate_locale: string * string -> state -> state
11.8 val fix: (string list * string option) list -> state -> state
11.9 val fix_i: (string list * typ option) list -> state -> state
11.10 val assm: ProofContext.exporter
11.11 @@ -510,6 +511,7 @@
11.12
11.13
11.14 (* have_thmss *)
11.15 +(* CB: this implements "note" of the Isar/VM *)
11.16
11.17 local
11.18
11.19 @@ -565,6 +567,19 @@
11.20 end;
11.21
11.22
11.23 +(* locale instantiation *)
11.24 +
11.25 +fun instantiate_locale (loc_name, prfx) state = let
11.26 + val ctxt = context_of state;
11.27 + val facts = if is_chain state then get_facts state else None;
11.28 + in
11.29 + state
11.30 + |> assert_forward_or_chain
11.31 + |> enter_forward
11.32 + |> reset_facts
11.33 + |> map_context (Locale.instantiate loc_name prfx facts)
11.34 + end;
11.35 +
11.36 (* fix *)
11.37
11.38 fun gen_fix f xs state =
12.1 --- a/src/Pure/Isar/proof_context.ML Fri Apr 02 12:25:48 2004 +0200
12.2 +++ b/src/Pure/Isar/proof_context.ML Fri Apr 02 14:08:30 2004 +0200
12.3 @@ -160,9 +160,17 @@
12.4 ((cterm list * exporter) list * (*assumes: A ==> _*)
12.5 (string * thm list) list) *
12.6 (string * string) list, (*fixes: !!x. _*)
12.7 + (* CB: asms is of the form ((asms, prems), fixed) *)
12.8 binds: (term * typ) option Vartab.table, (*term bindings*)
12.9 thms: bool * NameSpace.T * thm list option Symtab.table
12.10 * FactIndex.T, (*local thms*)
12.11 + (* CB: thms is of the form (q, n, t, i) where
12.12 + q: indicates whether theorems with qualified names may be stored;
12.13 + this is initially forbidden (false); flag may be changed with
12.14 + qualified and restore_qualified;
12.15 + n: theorem namespace;
12.16 + t: table of theorems;
12.17 + i: index for theorem lookup (find theorem command) *)
12.18 cases: (string * RuleCases.T) list, (*local contexts*)
12.19 defs:
12.20 typ Vartab.table * (*type constraints*)
12.21 @@ -1215,6 +1223,8 @@
12.22
12.23 end;
12.24
12.25 +(* CB: fix free variables occuring in ts, unless already fixed. *)
12.26 +
12.27 fun fix_frees ts ctxt =
12.28 let
12.29 val frees = foldl Term.add_frees ([], ts);