# HG changeset patch # User ballarin # Date 1110473316 -3600 # Node ID 4ab52355bb534715c2c45658ebbf4ea96ad7393e # Parent b5f5722ed703369634f70f50471bbedcb30716c4 Registrations of global locale interpretations: improved, better naming. diff -r b5f5722ed703 -r 4ab52355bb53 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Thu Mar 10 09:11:57 2005 +0100 +++ b/etc/isar-keywords-ZF.el Thu Mar 10 17:48:36 2005 +0100 @@ -74,6 +74,7 @@ "init_toplevel" "instance" "instantiate" + "interpretation" "judgment" "kill" "kill_thy" @@ -109,11 +110,11 @@ "print_drafts" "print_facts" "print_induct_rules" + "print_interps" "print_intros" "print_locale" "print_locales" "print_methods" - "print_registrations" "print_rules" "print_simpset" "print_syntax" @@ -132,7 +133,6 @@ "realizability" "realizers" "redo" - "registration" "remove_thy" "rep_datatype" "sect" @@ -261,11 +261,11 @@ "print_drafts" "print_facts" "print_induct_rules" + "print_interps" "print_intros" "print_locale" "print_locales" "print_methods" - "print_registrations" "print_rules" "print_simpset" "print_syntax" @@ -364,8 +364,8 @@ (defconst isar-keywords-theory-goal '("corollary" "instance" + "interpretation" "lemma" - "registration" "theorem")) (defconst isar-keywords-qed diff -r b5f5722ed703 -r 4ab52355bb53 etc/isar-keywords.el --- a/etc/isar-keywords.el Thu Mar 10 09:11:57 2005 +0100 +++ b/etc/isar-keywords.el Thu Mar 10 17:48:36 2005 +0100 @@ -77,6 +77,7 @@ "init_toplevel" "instance" "instantiate" + "interpretation" "judgment" "kill" "kill_thy" @@ -112,11 +113,11 @@ "print_drafts" "print_facts" "print_induct_rules" + "print_interps" "print_intros" "print_locale" "print_locales" "print_methods" - "print_registrations" "print_rules" "print_simpset" "print_syntax" @@ -137,7 +138,6 @@ "recdef_tc" "record" "redo" - "registration" "refute" "refute_params" "remove_thy" @@ -286,11 +286,11 @@ "print_drafts" "print_facts" "print_induct_rules" + "print_interps" "print_intros" "print_locale" "print_locales" "print_methods" - "print_registrations" "print_rules" "print_simpset" "print_syntax" @@ -395,9 +395,9 @@ '("ax_specification" "corollary" "instance" + "interpretation" "lemma" "recdef_tc" - "registration" "specification" "theorem" "typedef")) diff -r b5f5722ed703 -r 4ab52355bb53 src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Thu Mar 10 09:11:57 2005 +0100 +++ b/src/FOL/ex/LocaleTest.thy Thu Mar 10 17:48:36 2005 +0100 @@ -10,19 +10,19 @@ theory LocaleTest = FOL: -(* registration input syntax *) +(* interpretation input syntax *) locale L locale M = fixes a and b and c -registration test [simp]: L + M a b c [x y z] . +interpretation test [simp]: L + M a b c [x y z] . -print_registrations L -print_registrations M +print_interps L +print_interps M -registration test [simp]: L . +interpretation test [simp]: L . -registration L . +interpretation L . (* processing of locale expression *) @@ -44,33 +44,47 @@ ML {* set Toplevel.debug *} -registration p1: C ["X::'b" "Y"] by (auto intro: A.intro C_axioms.intro) +ML {* set show_hyps *} + +interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro) (* both X and Y get type 'b since 'b is the internal type of parameter b, not wanted, but put up with for now. *) -ML {* set show_hyps *} - -print_registrations A - -(* thm asm_A a.asm_A p1.a.asm_A *) +print_interps A (* -registration p2: D [X Y Z] sorry +thm asm_A a.asm_A p1.a.asm_A +*) + +interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute) -print_registrations D +print_interps D + +(* +thm p2.a.asm_A *) -registration p3: D [X Y] by (auto intro: A.intro) +interpretation p3: D [X Y] by (auto intro: A.intro) + +(* duplicate: not registered *) +(* +thm p3.a.asm_A +*) -print_registrations A -print_registrations B -print_registrations C -print_registrations D +print_interps A +print_interps B +print_interps C +print_interps D -(* not permitted -registration p4: A ["?x10"] apply (rule A.intro) apply rule done +(* not permitted *) +(* +interpretation p4: A ["x::?'a1"] apply (rule A.intro) apply rule done +*) +print_interps A -print_registrations A +(* without a prefix *) +(* TODO!!! +interpretation A [Z] apply - apply (auto intro: A.intro) done *) end diff -r b5f5722ed703 -r 4ab52355bb53 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Mar 10 09:11:57 2005 +0100 +++ b/src/Pure/Isar/isar_syn.ML Thu Mar 10 17:48:36 2005 +0100 @@ -315,9 +315,9 @@ val view_val = Scan.optional (P.$$$ "[" |-- Scan.repeat1 uterm --| P.$$$ "]") []; -val registrationP = - OuterSyntax.command "registration" - "prove and register instance of locale expression" K.thy_goal +val interpretationP = + OuterSyntax.command "interpretation" + "prove and register interpretation of locale expression" K.thy_goal ((P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val >> IsarThy.register_globally) >> (Toplevel.print oo Toplevel.theory_to_proof)); @@ -594,8 +594,8 @@ (locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); val print_registrationsP = - OuterSyntax.improper_command "print_registrations" - "print registrations of named locale in this theory" K.diag + OuterSyntax.improper_command "print_interps" + "print interpretations of named locale in this theory" K.diag (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations)); val print_attributesP = @@ -800,7 +800,7 @@ default_proofP, immediate_proofP, done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP, - redoP, undos_proofP, undoP, killP, registrationP, instantiateP, + redoP, undos_proofP, undoP, killP, interpretationP, instantiateP, (*diagnostic commands*) pretty_setmarginP, print_commandsP, print_contextP, print_theoryP, print_syntaxP, print_theoremsP, print_localesP, print_localeP, diff -r b5f5722ed703 -r 4ab52355bb53 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Thu Mar 10 09:11:57 2005 +0100 +++ b/src/Pure/Isar/isar_thy.ML Thu Mar 10 17:48:36 2005 +0100 @@ -625,21 +625,20 @@ val context = init_context (ThyInfo.quiet_update_thy true); -(* global locale registration *) +(* global registration of locale interpretation *) fun register_globally (((prfx, atts), expr), insts) b (* bool *) thy = let - val (thy', propss, activate) = - Locale.prep_registration (prfx, []) expr insts thy; -(* TODO: convert atts *) - fun register id (thy, thm) = let + val (thy', propss, activate) = Locale.prep_registration + (prfx, map (Attrib.global_attribute thy) atts) expr insts thy; + fun witness id (thy, thm) = let val thm' = Drule.freeze_all thm; in - (Locale.global_activate_thm id thm' thy, thm') + (Locale.global_add_witness id thm' thy, thm') end; in multi_theorem_i Drule.internalK activate ("", []) [] - (map (fn (id as (n, _), props) => ((NameSpace.base n, [register id]), + (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]), map (fn prop => (prop, ([], []))) props)) propss) b thy' end; diff -r b5f5722ed703 -r 4ab52355bb53 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Mar 10 09:11:57 2005 +0100 +++ b/src/Pure/Isar/locale.ML Thu Mar 10 17:48:36 2005 +0100 @@ -90,7 +90,7 @@ val prep_registration: string * theory attribute list -> expr -> string option list -> theory -> theory * ((string * term list) * term list) list * (theory -> theory) - val global_activate_thm: + val global_add_witness: string * term list -> thm -> theory -> theory val setup: (theory -> theory) list @@ -218,10 +218,10 @@ regs) end handle Termlisttab.DUP _ => regs)); -(* add theorem to registration in theory, +(* add witness theorem to registration in theory, ignored if registration not present *) -fun global_put_registration_thm (name, ps) thm = +fun global_add_witness (name, ps) thm = LocalesData.map (fn (space, locs, regs) => (space, locs, let val tab = valOf (Symtab.lookup (regs, name)); @@ -271,8 +271,8 @@ val loc_regs = Symtab.lookup (regs, loc_int); in (case loc_regs of - NONE => Pretty.str "No registrations." - | SOME r => Pretty.big_list "registrations:" + NONE => Pretty.str "No interpretations." + | SOME r => Pretty.big_list "interpretations:" (map prt_inst (Termlisttab.dest r))) |> Pretty.writeln end; @@ -1610,7 +1610,7 @@ -(** Registration commands **) +(** Interpretation commands **) local @@ -1761,10 +1761,12 @@ let (* extract theory attributes *) val (Notes facts) = map_attrib_element_i fst (Notes facts); + (* add attributs from registration *) val facts' = map (apfst (apsnd (fn a => a @ atts))) facts; - val facts'' = map (apsnd (map (apfst (map disch)))) facts'; + (* discharge hyps and varify *) + val facts'' = map (apsnd (map (apfst (map (Drule.standard o disch))))) facts'; in - fst (note_thmss_qualified' "" prfx facts thy) + fst (note_thmss_qualified' "" prfx facts'' thy) end; fun activate_facts_elems disch (thy, (id, elems)) = @@ -1782,9 +1784,8 @@ Option.map snd (global_get_registration thy id) handle Option => error ("(internal) unknown registration of " ^ quote (fst id) ^ " while activating facts.")) all_elemss); - fun disch thm = let - in Drule.satisfy_hyps prems thm end; - in Library.foldl (activate_facts_elems disch) (thy, new_elemss) end; + in Library.foldl (activate_facts_elems (Drule.satisfy_hyps prems)) + (thy, new_elemss) end; in @@ -1803,23 +1804,34 @@ (** compute instantiation **) - (* user input *) + (* check user input *) val insts = if length parms < length insts then error "More arguments than parameters in instantiation." else insts @ replicate (length parms - length insts) NONE; + val (ps, pTs) = split_list parms; val pvTs = map Type.varifyT pTs; + + (* instantiations given by user *) val given = List.mapPartial (fn (_, (NONE, _)) => NONE | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs)); val (given_ps, given_insts) = split_list given; val tvars = foldr Term.add_typ_tvars [] pvTs; val used = foldr Term.add_typ_varnames [] pvTs; fun sorts (a, i) = assoc (tvars, (a, i)); - val (tvs, tvinst) = Sign.read_def_terms (sign, K NONE, sorts) used true + val (vs, vinst) = Sign.read_def_terms (sign, K NONE, sorts) used true given_insts; - val tinst = Symtab.make (map (fn ((x, 0), T) => (x, Type.unvarifyT T) - | ((_, n), _) => error "Var in prep_registration") tvinst); - val inst = Symtab.make (given_ps ~~ map Logic.unvarify tvs); + (* replace new types (which are TFrees) by ones with new names *) + val new_Tnames = foldr Term.add_term_tfree_names [] vs; + val new_Tnames' = Term.invent_names used "'a" (length new_Tnames); + val renameT = Term.map_type_tfree (fn (a, s) => + TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s)); + val rename = Term.map_term_types renameT; + + val tinst = Symtab.make (map + (fn ((x, 0), T) => (x, T |> renameT |> Type.unvarifyT) + | ((_, n), _) => error "Var in prep_registration") vinst); + val inst = Symtab.make (given_ps ~~ map (Logic.unvarify o rename) vs); (* defined params without user input *) val not_given = List.mapPartial (fn (x, (NONE, T)) => SOME (x, T) @@ -1836,7 +1848,7 @@ (** compute proof obligations **) - (* restore small ids *) + (* restore "small" ids *) val ids' = map (fn ((n, ps), _) => (n, map (fn p => Free (p, valOf (assoc (parms, p)))) ps)) ids; @@ -1846,17 +1858,10 @@ map (fn Int e => e) elems)) (ids' ~~ all_elemss); -(* - (* varify ids, props are varified after they are proved *) - val inst_elemss' = map (fn ((n, ps), elems) => - ((n, map Logic.varify ps), elems)) inst_elemss; -*) - (* remove fragments already registered with theory *) val new_inst_elemss = List.filter (fn (id, _) => is_none (global_get_registration thy id)) inst_elemss; - val propss = extract_asms_elemss new_inst_elemss; @@ -1867,11 +1872,6 @@ in (thy', propss, activate_facts_elemss inst_elemss new_inst_elemss) end; - -(* Add registrations and theorems to theory context *) - -val global_activate_thm = global_put_registration_thm - end; (* local *) diff -r b5f5722ed703 -r 4ab52355bb53 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Mar 10 09:11:57 2005 +0100 +++ b/src/Pure/Isar/toplevel.ML Thu Mar 10 17:48:36 2005 +0100 @@ -471,6 +471,8 @@ | exn_message (THM (msg, i, thms)) = msg_on_debug (THM (msg, i, thms)) | exn_message Option = raised "Option" | exn_message UnequalLengths = raised "UnequalLengths" + | exn_message Empty = raised "Empty" + | exn_message Subscript = raised "Subscript" | exn_message exn = General.exnMessage exn and fail_message kind ((name, pos), exn) = "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_message exn; diff -r b5f5722ed703 -r 4ab52355bb53 src/Pure/term.ML --- a/src/Pure/term.ML Thu Mar 10 09:11:57 2005 +0100 +++ b/src/Pure/term.ML Thu Mar 10 17:48:36 2005 +0100 @@ -133,6 +133,7 @@ val maxidx_of_terms: term list -> int val variant: string list -> string -> string val variantlist: string list * string list -> string list + (* note reversed order of args wrt. variant! *) val variant_abs: string * typ * term -> string * term val rename_wrt_term: term -> (string * typ) list -> (string * typ) list val add_new_id: string list * string -> string list