# HG changeset patch # User ballarin # Date 1114444721 -7200 # Node ID 7a567dcd4cda394e6a98e4645058186ab7ce2c0e # Parent b805d85909c7d8f45348058ec156415aa19db36b Subsumption of locale interpretations. diff -r b805d85909c7 -r 7a567dcd4cda doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Sat Apr 23 19:51:54 2005 +0200 +++ b/doc-src/IsarRef/generic.tex Mon Apr 25 17:58:41 2005 +0200 @@ -296,6 +296,12 @@ \end{descr} +\begin{warn} + Since attributes are applied to interpreted theorems, interpretation + may modify the current simpset and claset. Take this into + account when choosing attributes for local theorems. +\end{warn} + \section{Derived proof schemes} diff -r b805d85909c7 -r 7a567dcd4cda src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Sat Apr 23 19:51:54 2005 +0200 +++ b/src/FOL/ex/LocaleTest.thy Mon Apr 25 17:58:41 2005 +0200 @@ -24,8 +24,8 @@ interpretation test [simp]: L + M a b c [x y z] . -print_interps L -print_interps M +print_interps L (* output: test *) +print_interps M (* output: test *) interpretation test [simp]: L print_interps M . @@ -52,9 +52,9 @@ arities i :: "term" -interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro) +interpretation p1: C ["X::i" "Y::i"] by (auto intro: A.intro C_axioms.intro) -print_interps A +print_interps A (* output: p1 *) (* possible accesses *) thm p1.a.asm_A thm LocaleTest.p1.a.asm_A @@ -63,70 +63,69 @@ (* without prefix *) -interpretation C ["W::'b" "Z::'b"] by (auto intro: A.intro C_axioms.intro) - -print_interps A - -(* possible accesses *) -thm a.asm_A thm asm_A thm LocaleTest.a.asm_A thm LocaleTest.asm_A +interpretation C ["W::i" "Z::i"] . (* subsumed by p1: C *) +interpretation C ["W::'a" "Z::i"] by (auto intro: A.intro C_axioms.intro) + (* subsumes p1: A and p1: C *) -interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute) +print_interps A (* output: , p1 *) -print_interps D - -thm p2.a.asm_A +(* possible accesses *) +thm asm_C thm a_b.asm_C thm LocaleTest.a_b.asm_C thm LocaleTest.a_b.asm_C -interpretation p3: D [X Y] . +interpretation p2: D [X "Y::i" "Y = X"] by (simp add: eq_commute) + +print_interps A (* output: , p1 *) +print_interps D (* output: p2 *) + + +interpretation p3: D [X "Y::i"] . (* duplicate: not registered *) (* thm p3.a.asm_A *) -print_interps A -print_interps B -print_interps C -print_interps D +print_interps A (* output: , p1 *) +print_interps B (* output: p1 *) +print_interps C (* output: , p1 *) +print_interps D (* output: p2, p3 *) -(* not permitted - +(* schematic vars in instantiation not permitted *) +(* interpretation p4: A ["?x::?'a1"] apply (rule A.intro) apply rule done - print_interps A *) -interpretation p10: D + D a' b' d' [X Y _ U V _] by (auto intro: A.intro) +interpretation p10: D + D a' b' d' [X "Y::i" _ U "V::i" _] . corollary (in D) th_x: True .. (* possible accesses: for each registration *) -thm p2.th_x thm p3.th_x thm p10.th_x +thm p2.th_x thm p3.th_x lemma (in D) th_y: "d == (a = b)" . -thm p2.th_y thm p3.th_y thm p10.th_y +thm p2.th_y thm p3.th_y lemmas (in D) th_z = th_y thm p2.th_z -thm asm_A - section {* Interpretation in proof contexts *} theorem True proof - - fix alpha::i and beta::i and gamma::i + fix alpha::i and beta::'a and gamma::i + (* FIXME: omitting type of beta leads to error later at interpret p6 *) have alpha_A: "A(alpha)" by (auto intro: A.intro) - then interpret p5: A [alpha] . - print_interps A - thm p5.asm_A + interpret p5: A [alpha] . (* subsumed *) + print_interps A (* output: , p1 *) interpret p6: C [alpha beta] by (auto intro: C_axioms.intro) - print_interps A (* p6 not added! *) - print_interps C + print_interps A (* output: , p1 *) + print_interps C (* output: , p1, p6 *) qed rule theorem (in A) True diff -r b805d85909c7 -r 7a567dcd4cda src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sat Apr 23 19:51:54 2005 +0200 +++ b/src/HOL/Finite_Set.thy Mon Apr 25 17:58:41 2005 +0200 @@ -1132,6 +1132,8 @@ finally show ?thesis . qed +(* FIXME: this is distributitivty, name as such! *) + lemma setsum_mult: fixes f :: "'a => ('b::semiring_0_cancel)" shows "r * setsum f A = setsum (%n. r * f n) A" @@ -2227,51 +2229,51 @@ text{* Before we can do anything, we need to show that @{text min} and @{text max} are ACI and the ordering is linear: *} -interpretation min [rule del]: ACf ["min:: 'a::linorder \ 'a \ 'a"] +interpretation min: ACf ["min:: 'a::linorder \ 'a \ 'a"] apply(rule ACf.intro) apply(auto simp:min_def) done -interpretation min [rule del]: ACIf ["min:: 'a::linorder \ 'a \ 'a"] +interpretation min: ACIf ["min:: 'a::linorder \ 'a \ 'a"] apply(rule ACIf_axioms.intro) apply(auto simp:min_def) done -interpretation max [rule del]: ACf ["max :: 'a::linorder \ 'a \ 'a"] +interpretation max: ACf ["max :: 'a::linorder \ 'a \ 'a"] apply(rule ACf.intro) apply(auto simp:max_def) done -interpretation max [rule del]: ACIf ["max:: 'a::linorder \ 'a \ 'a"] +interpretation max: ACIf ["max:: 'a::linorder \ 'a \ 'a"] apply(rule ACIf_axioms.intro) apply(auto simp:max_def) done -interpretation min [rule del]: +interpretation min: ACIfSL ["min:: 'a::linorder \ 'a \ 'a" "op \"] apply(rule ACIfSL_axioms.intro) apply(auto simp:min_def) done -interpretation min [rule del]: +interpretation min: ACIfSLlin ["min :: 'a::linorder \ 'a \ 'a" "op \"] apply(rule ACIfSLlin_axioms.intro) apply(auto simp:min_def) done -interpretation max [rule del]: +interpretation max: ACIfSL ["max :: 'a::linorder \ 'a \ 'a" "%x y. y\x"] apply(rule ACIfSL_axioms.intro) apply(auto simp:max_def) done -interpretation max [rule del]: +interpretation max: ACIfSLlin ["max :: 'a::linorder \ 'a \ 'a" "%x y. y\x"] apply(rule ACIfSLlin_axioms.intro) apply(auto simp:max_def) done -interpretation min_max [rule del]: +interpretation min_max: Lattice ["op \" "min :: 'a::linorder \ 'a \ 'a" "max" "Min" "Max"] apply - apply(rule Min_def) @@ -2279,14 +2281,10 @@ done -interpretation min_max [rule del]: +interpretation min_max: Distrib_Lattice ["op \" "min :: 'a::linorder \ 'a \ 'a" "max" "Min" "Max"] . -text {* Classical rules from the locales are deleted in the above - interpretations, since they interfere with the claset setup for - @{text "op \"}. *} - text{* Now we instantiate the recursion equations and declare them simplification rules: *} diff -r b805d85909c7 -r 7a567dcd4cda src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Sat Apr 23 19:51:54 2005 +0200 +++ b/src/HOL/Orderings.thy Mon Apr 25 17:58:41 2005 +0200 @@ -93,7 +93,7 @@ text{* Connection to locale: *} -interpretation order[rule del]: +interpretation order: partial_order["op \ :: 'a::order \ 'a \ bool"] apply(rule partial_order.intro) apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym) @@ -226,16 +226,6 @@ axclass linorder < order linorder_linear: "x <= y | y <= x" -(* Could (should?) follow automatically from the interpretation of - partial_order by class order. rule del is needed because two copies - of refl with classes order and linorder confuse blast (and are pointless)*) -interpretation order[rule del]: - partial_order["op \ :: 'a::linorder \ 'a \ bool"] -apply(rule partial_order.intro) -apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym) -done - - lemma linorder_less_linear: "!!x::'a::linorder. x" "min :: 'a::linorder \ 'a \ 'a"] apply - apply(rule lower_semilattice_axioms.intro) @@ -401,7 +391,7 @@ apply(simp add:min_def linorder_not_le order_less_imp_le) done -interpretation min_max [rule del]: +interpretation min_max: upper_semilattice["op \" "max :: 'a::linorder \ 'a \ 'a"] apply - apply(rule upper_semilattice_axioms.intro) @@ -410,11 +400,11 @@ apply(simp add: max_def linorder_not_le order_less_imp_le) done -interpretation min_max [rule del]: +interpretation min_max: lattice["op \" "min :: 'a::linorder \ 'a \ 'a" "max"] . -interpretation min_max [rule del]: +interpretation min_max: distrib_lattice["op \" "min :: 'a::linorder \ 'a \ 'a" "max"] apply(rule distrib_lattice_axioms.intro) apply(rule_tac x=x and y=y in linorder_le_cases) diff -r b805d85909c7 -r 7a567dcd4cda src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sat Apr 23 19:51:54 2005 +0200 +++ b/src/Pure/Isar/locale.ML Mon Apr 25 17:58:41 2005 +0200 @@ -141,22 +141,186 @@ -(** theory data **) +(** term and type instantiation, using symbol tables **) + +(* instantiate TFrees *) + +fun tinst_tab_type tinst T = if Symtab.is_empty tinst + then T + else Term.map_type_tfree + (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T; + +fun tinst_tab_term tinst t = if Symtab.is_empty tinst + then t + else Term.map_term_types (tinst_tab_type tinst) t; + +fun tinst_tab_thm sg tinst thm = if Symtab.is_empty tinst + then thm + else let + val cert = Thm.cterm_of sg; + val certT = Thm.ctyp_of sg; + val {hyps, prop, ...} = Thm.rep_thm thm; + val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); + val tinst' = Symtab.dest tinst |> + List.filter (fn (a, _) => a mem_string tfrees); + in + if null tinst' then thm + else thm |> Drule.implies_intr_list (map cert hyps) + |> Drule.tvars_intr_list (map #1 tinst') + |> (fn (th, al) => th |> Thm.instantiate + ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'), + [])) + |> (fn th => Drule.implies_elim_list th + (map (Thm.assume o cert o tinst_tab_term tinst) hyps)) + end; + + +(* instantiate TFrees and Frees *) + +fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst + then tinst_tab_term tinst + else (* instantiate terms and types simultaneously *) + let + fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T) + | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of + NONE => Free (x, tinst_tab_type tinst T) + | SOME t => t) + | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T) + | instf (b as Bound _) = b + | instf (Abs (x, T, t)) = Abs (x, tinst_tab_type tinst T, instf t) + | instf (s $ t) = instf s $ instf t + in instf end; + +fun inst_tab_thm sg (inst, tinst) thm = if Symtab.is_empty inst + then tinst_tab_thm sg tinst thm + else let + val cert = Thm.cterm_of sg; + val certT = Thm.ctyp_of sg; + val {hyps, prop, ...} = Thm.rep_thm thm; + (* type instantiations *) + val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); + val tinst' = Symtab.dest tinst |> + List.filter (fn (a, _) => a mem_string tfrees); + (* term instantiations; + note: lhss are type instantiated, because + type insts will be done first*) + val frees = foldr Term.add_term_frees [] (prop :: hyps); + val inst' = Symtab.dest inst |> + List.mapPartial (fn (a, t) => + get_first (fn (Free (x, T)) => + if a = x then SOME (Free (x, tinst_tab_type tinst T), t) + else NONE) frees); + in + if null tinst' andalso null inst' then tinst_tab_thm sg tinst thm + else thm |> Drule.implies_intr_list (map cert hyps) + |> Drule.tvars_intr_list (map #1 tinst') + |> (fn (th, al) => th |> Thm.instantiate + ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'), + [])) + |> Drule.forall_intr_list (map (cert o #1) inst') + |> Drule.forall_elim_list (map (cert o #2) inst') + |> (fn th => Drule.implies_elim_list th + (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps)) + end; + + +(** registration management **) -structure Termlisttab = TableFun(type key = term list - val ord = Library.list_ord Term.term_ord); +structure Registrations : + sig + type T + val empty: T + val join: T * T -> T + val dest: T -> (term list * ((string * Attrib.src list) * thm list)) list + val lookup: Sign.sg -> T * term list -> + ((string * Attrib.src list) * thm list) option + val insert: Sign.sg -> term list * (string * Attrib.src list) -> T -> + T * (term list * ((string * Attrib.src list) * thm list)) list + val add_witness: term list -> thm -> T -> T + end = +struct + (* a registration consists of theorems instantiating locale assumptions + and prefix and attributes, indexed by parameter instantiation *) + type T = ((string * Attrib.src list) * thm list) Termtab.table; + + val empty = Termtab.empty; + + (* term list represented as single term, for simultaneous matching *) + fun termify ts = + Library.foldl (op $) (Const ("", map fastype_of ts ---> propT), ts); + fun untermify t = + let fun ut (Const _) ts = ts + | ut (s $ t) ts = ut s (t::ts) + in ut t [] end; + + (* joining of registrations: prefix and attributs of left theory, + thms are equal, no attempt to subsumption testing *) + val join = Termtab.join (fn (reg, _) => SOME reg); + + fun dest regs = map (apfst untermify) (Termtab.dest regs); + + (* registrations that subsume t *) + fun subsumers tsig t regs = + List.filter (fn (t', _) => Pattern.matches tsig (t', t)) (Termtab.dest regs); + + (* look up registration, pick one that subsumes the query *) + fun lookup sign (regs, ts) = + let + val tsig = Sign.tsig_of sign; + val t = termify ts; + val subs = subsumers tsig t regs; + in (case subs of + [] => NONE + | ((t', (attn, thms)) :: _) => let + val (tinst, inst) = Pattern.match tsig (t', t); + (* thms contain Frees, not Vars *) + val tinst' = tinst |> Vartab.dest + |> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T)) + |> Symtab.make; + val inst' = inst |> Vartab.dest + |> map (fn ((x, 0), (_, t)) => (x, Logic.unvarify t)) + |> Symtab.make; + in + SOME (attn, map (inst_tab_thm sign (inst', tinst')) thms) + end) + end; + + (* add registration if not subsumed by ones already present, + additionally returns registrations that are strictly subsumed *) + fun insert sign (ts, attn) regs = + let + val tsig = Sign.tsig_of sign; + val t = termify ts; + val subs = subsumers tsig t regs ; + in (case subs of + [] => let + val sups = + List.filter (fn (t', _) => Pattern.matches tsig (t, t')) (Termtab.dest regs); + val sups' = map (apfst untermify) sups + in (Termtab.update ((t, (attn, [])), regs), sups') end + | _ => (regs, [])) + end; + + (* add witness theorem to registration, + only if instantiation is exact, otherwise excpetion Option raised *) + fun add_witness ts thm regs = + let + val t = termify ts; + val (x, thms) = valOf (Termtab.lookup (regs, t)); + in + Termtab.update ((t, (x, thm::thms)), regs) + end; +end; + +(** theory data **) structure GlobalLocalesArgs = struct val name = "Isar/locales"; - type T = NameSpace.T * locale Symtab.table * - ((string * Attrib.src list) * thm list) Termlisttab.table - Symtab.table; + type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table; (* 1st entry: locale namespace, 2nd entry: locales of the theory, - 3rd entry: registrations: theorems instantiating locale assumptions, - with prefix and attributes, indexed by locale name and parameter - instantiation *) + 3rd entry: registrations, indexed by locale name *) val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); val copy = I; @@ -167,12 +331,9 @@ SOME {predicate = predicate, import = import, elems = gen_merge_lists eq_snd elems elems', params = params}; - (* joining of registrations: prefix and attributes of left theory, - thmsss are equal *) - fun join_regs (reg, _) = SOME reg; fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) = (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), - Symtab.join (SOME o Termlisttab.join join_regs) (regs1, regs2)); + Symtab.join (SOME o Registrations.join) (regs1, regs2)); fun print _ (space, locs, _) = Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs)) @@ -189,11 +350,8 @@ structure LocalLocalesArgs = struct val name = "Isar/locales"; - type T = ((string * Args.src list) * thm list) Termlisttab.table - Symtab.table; - (* registrations: theorems instantiating locale assumptions, - with prefix and attributes, indexed by locale name and parameter - instantiation *) + type T = Registrations.T Symtab.table; + (* registrations, indexed by locale name *) fun init _ = Symtab.empty; fun print _ _ = (); end; @@ -236,22 +394,22 @@ fun gen_get_registrations get thy_ctxt name = case Symtab.lookup (get thy_ctxt, name) of NONE => [] - | SOME tab => Termlisttab.dest tab; + | SOME reg => Registrations.dest reg; val get_global_registrations = gen_get_registrations (#3 o GlobalLocalesData.get); val get_local_registrations = gen_get_registrations LocalLocalesData.get; -fun gen_get_registration get thy_ctxt (name, ps) = +fun gen_get_registration get get_sg thy_ctxt (name, ps) = case Symtab.lookup (get thy_ctxt, name) of NONE => NONE - | SOME tab => Termlisttab.lookup (tab, ps); + | SOME reg => Registrations.lookup (get_sg thy_ctxt) (reg, ps); val get_global_registration = - gen_get_registration (#3 o GlobalLocalesData.get); + gen_get_registration (#3 o GlobalLocalesData.get) Theory.sign_of; val get_local_registration = - gen_get_registration LocalLocalesData.get; + gen_get_registration LocalLocalesData.get ProofContext.sign_of; val test_global_registration = isSome oo get_global_registration; val test_local_registration = isSome oo get_local_registration; @@ -263,24 +421,31 @@ end; -(* add registration to theory or context, ignored if already present *) +(* add registration to theory or context, ignored if subsumed *) -fun gen_put_registration map (name, ps) attn = - map (fn regs => - let - val tab = getOpt (Symtab.lookup (regs, name), Termlisttab.empty); - in - Symtab.update ((name, Termlisttab.update_new ((ps, (attn, [])), tab)), - regs) - end handle Termlisttab.DUP _ => regs); +fun gen_put_registration map_data get_sg (name, ps) attn thy_ctxt = + map_data (fn regs => + let + val sg = get_sg thy_ctxt; + val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty); + val (reg', sups) = Registrations.insert sg (ps, attn) reg; + val _ = if not (null sups) then warning + ("Subsumed interpretation(s) of locale " ^ + quote (cond_extern sg name) ^ + "\nby interpretation(s) with the following prefix(es):\n" ^ + commas_quote (map (fn (_, ((s, _), _)) => s) sups)) + else (); + in Symtab.update ((name, reg'), regs) end) thy_ctxt; val put_global_registration = gen_put_registration (fn f => GlobalLocalesData.map (fn (space, locs, regs) => - (space, locs, f regs))); -val put_local_registration = gen_put_registration LocalLocalesData.map; + (space, locs, f regs))) Theory.sign_of; +val put_local_registration = + gen_put_registration LocalLocalesData.map ProofContext.sign_of; (* TODO: needed? *) +(* fun smart_put_registration id attn ctxt = (* ignore registration if already present in theory *) let @@ -289,7 +454,7 @@ NONE => put_local_registration id attn ctxt | SOME _ => ctxt end; - +*) (* add witness theorem to registration in theory or context, ignored if registration not present *) @@ -297,11 +462,9 @@ fun gen_add_witness map (name, ps) thm = map (fn regs => let - val tab = valOf (Symtab.lookup (regs, name)); - val (x, thms) = valOf (Termlisttab.lookup (tab, ps)); + val reg = valOf (Symtab.lookup (regs, name)); in - Symtab.update ((name, Termlisttab.update ((ps, (x, thm::thms)), tab)), - regs) + Symtab.update ((name, Registrations.add_witness ps thm reg), regs) end handle Option => regs); val add_global_witness = @@ -342,9 +505,10 @@ fun prt_inst (ts, (("", []), thms)) = Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts)) | prt_inst (ts, ((prfx, atts), thms)) = - Pretty.block (Pretty.breaks - (Pretty.str prfx :: prt_atts atts @ [Pretty.str ":", Pretty.brk 1, - Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))])); + Pretty.block ( + (Pretty.breaks (Pretty.str prfx :: prt_atts atts) @ + [Pretty.str ":", Pretty.brk 1, + Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))])); val loc_int = intern sg loc; val regs = get_regs thy_ctxt; @@ -353,7 +517,7 @@ (case loc_regs of NONE => Pretty.str ("No interpretations in " ^ msg ^ ".") | SOME r => let - val r' = Termlisttab.dest r; + val r' = Registrations.dest r; val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r'; in Pretty.big_list ("Interpretations in " ^ msg ^ ":") (map prt_inst r'') @@ -514,86 +678,11 @@ (* instantiate TFrees *) -fun tinst_tab_type tinst T = if Symtab.is_empty tinst - then T - else Term.map_type_tfree - (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T; - -fun tinst_tab_term tinst t = if Symtab.is_empty tinst - then t - else Term.map_term_types (tinst_tab_type tinst) t; - -fun tinst_tab_thm sg tinst thm = if Symtab.is_empty tinst - then thm - else let - val cert = Thm.cterm_of sg; - val certT = Thm.ctyp_of sg; - val {hyps, prop, ...} = Thm.rep_thm thm; - val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); - val tinst' = Symtab.dest tinst |> - List.filter (fn (a, _) => a mem_string tfrees); - in - if null tinst' then thm - else thm |> Drule.implies_intr_list (map cert hyps) - |> Drule.tvars_intr_list (map #1 tinst') - |> (fn (th, al) => th |> Thm.instantiate - ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'), - [])) - |> (fn th => Drule.implies_elim_list th - (map (Thm.assume o cert o tinst_tab_term tinst) hyps)) - end; - fun tinst_tab_elem sg tinst = map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm sg tinst); (* instantiate TFrees and Frees *) -fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst - then tinst_tab_term tinst - else (* instantiate terms and types simultaneously *) - let - fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T) - | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of - NONE => Free (x, tinst_tab_type tinst T) - | SOME t => t) - | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T) - | instf (b as Bound _) = b - | instf (Abs (x, T, t)) = Abs (x, tinst_tab_type tinst T, instf t) - | instf (s $ t) = instf s $ instf t - in instf end; - -fun inst_tab_thm sg (inst, tinst) thm = if Symtab.is_empty inst - then tinst_tab_thm sg tinst thm - else let - val cert = Thm.cterm_of sg; - val certT = Thm.ctyp_of sg; - val {hyps, prop, ...} = Thm.rep_thm thm; - (* type instantiations *) - val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); - val tinst' = Symtab.dest tinst |> - List.filter (fn (a, _) => a mem_string tfrees); - (* term instantiations; - note: lhss are type instantiated, because - type insts will be done first*) - val frees = foldr Term.add_term_frees [] (prop :: hyps); - val inst' = Symtab.dest inst |> - List.mapPartial (fn (a, t) => - get_first (fn (Free (x, T)) => - if a = x then SOME (Free (x, tinst_tab_type tinst T), t) - else NONE) frees); - in - if null tinst' andalso null inst' then tinst_tab_thm sg tinst thm - else thm |> Drule.implies_intr_list (map cert hyps) - |> Drule.tvars_intr_list (map #1 tinst') - |> (fn (th, al) => th |> Thm.instantiate - ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'), - [])) - |> Drule.forall_intr_list (map (cert o #1) inst') - |> Drule.forall_elim_list (map (cert o #2) inst') - |> (fn th => Drule.implies_elim_list th - (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps)) - end; - fun inst_tab_elem sg (inst as (_, tinst)) = map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm sg inst); @@ -1963,7 +2052,8 @@ handle Option => error ("(internal) unknown registration of " ^ quote (fst id) ^ " while activating facts.")) all_elemss); in Library.foldl (activate_facts_elems get_reg note_thmss attrib - (standard o Drule.satisfy_hyps prems)) (thy_ctxt, new_elemss) end; + (Drule.standard o Drule.fconv_rule (Thm.beta_conversion true) o + Drule.satisfy_hyps prems)) (thy_ctxt, new_elemss) end; val global_activate_facts_elemss = gen_activate_facts_elemss (fn thy => fn (name, ps) =>