diff --git a/src/Pure/Isar/generic_target.ML b/src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML +++ b/src/Pure/Isar/generic_target.ML @@ -1,472 +1,476 @@ (* Title: Pure/Isar/generic_target.ML Author: Makarius Author: Florian Haftmann, TU Muenchen Common target infrastructure. *) signature GENERIC_TARGET = sig (*auxiliary*) val export_abbrev: Proof.context -> (term -> term) -> term -> term * ((string * sort) list * (term list * term list)) val check_mixfix: Proof.context -> binding * (string * sort) list -> mixfix -> mixfix val check_mixfix_global: binding * bool -> mixfix -> mixfix (*background primitives*) val background_foundation: ((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory val background_declaration: declaration -> local_theory -> local_theory val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory val add_foundation_interpretation: (binding * (term * term list) -> Context.generic -> Context.generic) -> theory -> theory (*nested local theories primitives*) val standard_facts: local_theory -> Proof.context -> Attrib.fact list -> Attrib.fact list val standard_notes: (int * int -> bool) -> string -> Attrib.fact list -> local_theory -> local_theory val standard_declaration: (int * int -> bool) -> (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory val local_interpretation: Locale.registration -> local_theory -> local_theory (*lifting target primitives to local theory operations*) val define: (((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory) -> bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory val notes: (string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory) -> string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory val abbrev: (Syntax.mode -> binding * mixfix -> term -> term list * term list -> local_theory -> local_theory) -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory (*theory target primitives*) val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory val theory_target_notes: string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory (*theory target operations*) val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val theory_declaration: declaration -> local_theory -> local_theory val theory_registration: Locale.registration -> local_theory -> local_theory (*locale target primitives*) val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory val locale_target_const: string -> (morphism -> bool) -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory (*locale operations*) val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory val locale_const: string -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory val locale_dependency: string -> Locale.registration -> local_theory -> local_theory end structure Generic_Target: GENERIC_TARGET = struct (** consts **) fun export_abbrev lthy preprocess rhs = let val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); val rhs' = rhs |> Assumption.export_term lthy (Local_Theory.target_of lthy) |> preprocess; val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' [])); val u = fold_rev lambda term_params rhs'; val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; val type_tfrees = TFrees.build (TFrees.add_tfreesT (Term.fastype_of u)); val extra_tfrees = TFrees.build (TFrees.add_tfrees_unless (TFrees.defined type_tfrees) u) |> TFrees.list_set; val type_params = map (Logic.mk_type o TFree) extra_tfrees; in (global_rhs, (extra_tfrees, (type_params, term_params))) end; fun check_mixfix ctxt (b, extra_tfrees) mx = if null extra_tfrees then mx else (if Context_Position.is_visible ctxt then warning ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^ commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^ (if Mixfix.is_empty mx then "" else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))) else (); NoSyn); fun check_mixfix_global (b, no_params) mx = if no_params orelse Mixfix.is_empty mx then mx else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn); fun same_const (Const (c, _), Const (c', _)) = c = c' | same_const (t $ _, t' $ _) = same_const (t, t') | same_const (_, _) = false; fun const_decl phi_pred prmode ((b, mx), rhs) phi context = if phi_pred phi then let val b' = Morphism.binding phi b; val rhs' = Morphism.term phi rhs; val same_shape = Term.aconv_untyped (rhs, rhs'); val same_stem = same_shape orelse same_const (rhs, rhs'); val const_alias = if same_shape then (case rhs' of Const (c, T) => let val thy = Context.theory_of context; val ctxt = Context.proof_of context; in (case Type_Infer_Context.const_type ctxt c of SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE | NONE => NONE) end | _ => NONE) else NONE; in (case const_alias of SOME c => context |> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c) |> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)]) | NONE => context |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs') |-> (fn (const as Const (c, _), _) => same_stem ? (Proof_Context.generic_revert_abbrev (#1 prmode) c #> same_shape ? Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) end else context; (** background primitives **) structure Foundation_Interpretations = Theory_Data ( type T = (binding * (term * term list) -> Context.generic -> Context.generic) Inttab.table; val empty = Inttab.empty; val extend = I; val merge = Inttab.merge (K true); ); fun add_foundation_interpretation f = Foundation_Interpretations.map (Inttab.update_new (serial (), f)); fun foundation_interpretation binding_const_params lthy = let val interps = Foundation_Interpretations.get (Proof_Context.theory_of lthy); val interp = Inttab.fold (fn (_, f) => f binding_const_params) interps; in lthy |> Local_Theory.background_theory (Context.theory_map interp) |> Local_Theory.map_contexts (K (Context.proof_map interp)) end; fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = let val params = type_params @ term_params; val target_params = type_params @ take_prefix is_Free (Variable.export_terms lthy (Local_Theory.target_of lthy) term_params); val mx' = check_mixfix_global (b, null params) mx; val (const, lthy2) = lthy |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx')); val lhs = Term.list_comb (const, params); val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result (Thm.add_def (Proof_Context.defs_context lthy2) false false (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))) ||> foundation_interpretation (b, (const, target_params)); in ((lhs, def), lthy3) end; fun background_declaration decl lthy = let fun theory_decl context = Local_Theory.standard_form lthy (Proof_Context.init_global (Context.theory_of context)) decl context; in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end; fun background_abbrev (b, global_rhs) params = Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs)) #>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params)) (** nested local theories primitives **) fun standard_facts lthy ctxt = Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt); fun standard_notes pred kind facts lthy = Local_Theory.map_contexts (fn level => fn ctxt => if pred (Local_Theory.level lthy, level) then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd else ctxt) lthy; fun standard_declaration pred decl lthy = Local_Theory.map_contexts (fn level => fn ctxt => if pred (Local_Theory.level lthy, level) then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt else ctxt) lthy; fun standard_const pred prmode ((b, mx), rhs) = standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs)); fun standard_registration pred registration lthy = Local_Theory.map_contexts (fn level => if pred (Local_Theory.level lthy, level) then Context.proof_map (Locale.add_registration registration) else I) lthy; val local_interpretation = standard_registration (fn (n, level) => level = n - 1); (** lifting target primitives to local theory operations **) (* define *) fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy = let val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); (*term and type parameters*) val ((defs, _), rhs') = Thm.cterm_of lthy rhs |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of; val xs = Variable.add_fixed lthy rhs' []; val T = Term.fastype_of rhs; val type_tfrees = TFrees.build (TFrees.add_tfreesT T #> fold (TFrees.add_tfreesT o #2) xs); val extra_tfrees = TFrees.build (rhs |> TFrees.add_tfrees_unless (TFrees.defined type_tfrees)) |> TFrees.list_set; val mx' = check_mixfix lthy (b, extra_tfrees) mx; val type_params = map (Logic.mk_type o TFree) extra_tfrees; val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) xs); val params = type_params @ term_params; val U = map Term.fastype_of params ---> T; (*foundation*) val ((lhs', global_def), lthy2) = lthy |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params); (*local definition*) val ([(lhs, (_, local_def))], lthy3) = lthy2 |> Context_Position.set_visible false |> Local_Defs.define [((b, NoSyn), (Binding.empty_atts, lhs'))] ||> Context_Position.restore_visible lthy2; (*result*) val def = Thm.transitive local_def global_def |> Local_Defs.contract lthy3 defs (Thm.cterm_of lthy3 (Logic.mk_equals (lhs, rhs))); val ([(res_name, [res])], lthy4) = lthy3 |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])]; in ((lhs, (res_name, res)), lthy4) end; (* notes *) local fun import_export_proof ctxt (name, raw_th) = let val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt); (*export assumes/defines*) val th = Goal.norm_result ctxt raw_th; val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th; val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms; (*export fixes*) - val tfrees = map TFree (Thm.fold_terms {hyps = true} Term.add_tfrees th' []); - val frees = map Free (Thm.fold_terms {hyps = true} Term.add_frees th' []); + val tfrees = + TFrees.build (Thm.fold_terms {hyps = true} TFrees.add_tfrees th') + |> TFrees.list_set_rev |> map TFree; + val frees = + Frees.build (Thm.fold_terms {hyps = true} Frees.add_frees th') + |> Frees.list_set_rev |> map Free; val (th'' :: vs) = (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees)) |> Variable.export ctxt thy_ctxt |> Drule.zero_var_indexes_list; (*thm definition*) val result = Global_Theory.name_thm Global_Theory.official1 name th''; (*import fixes*) val (tvars, vars) = chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) |>> map Logic.dest_type; val instT = TVars.build (fold2 (fn a => fn b => (case a of TVar v => TVars.add (v, b) | _ => I)) tvars tfrees); val cinstT = TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt T)) instT []; val cinst = map_filter (fn (Var (xi, T), t) => SOME ((xi, Term_Subst.instantiateT instT T), Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t)) | _ => NONE) (vars ~~ frees); val result' = Thm.instantiate (cinstT, cinst) result; (*import assumes/defines*) val result'' = (fold (curry op COMP) asms' result' handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms')) |> Local_Defs.contract ctxt defs (Thm.cprop_of th) |> Goal.norm_result ctxt |> Global_Theory.name_thm Global_Theory.unofficial2 name; in (result'', result) end; fun bind_name lthy b = (Local_Theory.full_name lthy b, Binding.default_pos_of b); fun map_facts f = map (apsnd (map (apfst (map f)))); in fun notes target_notes kind facts lthy = let val facts' = facts |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs)) |> map_facts (import_export_proof lthy); val local_facts = map_facts #1 facts'; val global_facts = map_facts #2 facts'; in lthy |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts) |> Attrib.local_notes kind local_facts end; end; (* abbrev *) fun abbrev target_abbrev prmode ((b, mx), rhs) lthy = let val (global_rhs, (extra_tfrees, (type_params, term_params))) = export_abbrev lthy I rhs; val mx' = check_mixfix lthy (b, extra_tfrees) mx; in lthy |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params) |> Context_Position.set_visible false |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs) ||> Context_Position.restore_visible lthy end; (** theory target primitives **) fun theory_target_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) = background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) #-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs) #> pair (lhs, def)); fun theory_target_notes kind global_facts local_facts = Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #> standard_notes (op <>) kind local_facts; fun theory_target_abbrev prmode (b, mx) global_rhs params = Local_Theory.background_theory_result (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) => (* FIXME type_params!? *) Sign.notation true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs)) #-> (fn lhs => standard_const (op <>) prmode ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params))); (** theory operations **) val theory_abbrev = abbrev theory_target_abbrev; fun theory_declaration decl = background_declaration decl #> standard_declaration (K true) decl; fun target_registration lthy {inst, mixin, export} = {inst = inst, mixin = mixin, export = export $> Proof_Context.export_morphism lthy (Local_Theory.target_of lthy)}; fun theory_registration registration lthy = lthy |> (Local_Theory.raw_theory o Context.theory_map) (Locale.add_registration (target_registration lthy registration)) |> standard_registration (K true) registration; (** locale target primitives **) fun locale_target_notes locale kind global_facts local_facts = Local_Theory.background_theory (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #> (fn lthy => lthy |> Local_Theory.target (fn ctxt => ctxt |> Locale.add_facts locale kind (standard_facts lthy ctxt local_facts))) #> standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts; fun locale_target_declaration locale syntax decl lthy = lthy |> Local_Theory.target (fn ctxt => ctxt |> Locale.add_declaration locale syntax (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl)); fun locale_target_const locale phi_pred prmode ((b, mx), rhs) = locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs)) (** locale operations **) fun locale_declaration locale {syntax, pervasive} decl = pervasive ? background_declaration decl #> locale_target_declaration locale syntax decl #> standard_declaration (fn (_, other) => other <> 0) decl; fun locale_const locale prmode ((b, mx), rhs) = locale_target_const locale (K true) prmode ((b, mx), rhs) #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); fun locale_dependency loc registration lthy = lthy |> Local_Theory.raw_theory (Locale.add_dependency loc registration) |> standard_registration (K true) registration; (** locale abbreviations **) fun locale_target_abbrev locale prmode (b, mx) global_rhs params = background_abbrev (b, global_rhs) (snd params) #-> (fn (lhs, _) => locale_const locale prmode ((b, mx), lhs)); fun locale_abbrev locale = abbrev (locale_target_abbrev locale); end; diff --git a/src/Pure/Isar/subgoal.ML b/src/Pure/Isar/subgoal.ML --- a/src/Pure/Isar/subgoal.ML +++ b/src/Pure/Isar/subgoal.ML @@ -1,255 +1,255 @@ (* Title: Pure/Isar/subgoal.ML Author: Makarius Author: Daniel Matichuk, NICTA/UNSW Tactical operations with explicit subgoal focus, based on canonical proof decomposition. The "visible" part of the text within the context is fixed, the remaining goal may be schematic. Isar subgoal command for proof structure within unstructured proof scripts. *) signature SUBGOAL = sig type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list, concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list} val focus_params: Proof.context -> int -> binding list option -> thm -> focus * thm val focus_params_fixed: Proof.context -> int -> binding list option -> thm -> focus * thm val focus_prems: Proof.context -> int -> binding list option -> thm -> focus * thm val focus: Proof.context -> int -> binding list option -> thm -> focus * thm val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list -> int -> thm -> thm -> thm Seq.seq val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic val FOCUS_PARAMS_FIXED: (focus -> tactic) -> Proof.context -> int -> tactic val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic val subgoal: Attrib.binding -> Attrib.binding option -> bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state val subgoal_cmd: Attrib.binding -> Attrib.binding option -> bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state end; structure Subgoal: SUBGOAL = struct (* focus *) type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list, concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}; fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st = let val st = raw_st |> Thm.solve_constraints |> Thm.transfer' ctxt |> Raw_Simplifier.norm_hhf_protect ctxt; val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt; val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1; val (asms, concl) = if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal) else ([], goal); val text = asms @ (if do_concl then [concl] else []); val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2; val schematic_terms = Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst []; val schematics = (TVars.dest schematic_types, schematic_terms); val asms' = map (Thm.instantiate_cterm schematics) asms; val concl' = Thm.instantiate_cterm schematics concl; val (prems, context) = Assumption.add_assumes asms' ctxt3; in ({context = context, params = params, prems = prems, asms = asms', concl = concl', schematics = schematics}, Goal.init concl') end; val focus_params = gen_focus (false, false); val focus_params_fixed = gen_focus (false, true); val focus_prems = gen_focus (true, false); val focus = gen_focus (true, true); (* lift and retrofit *) (* B [?'b, ?y] ---------------- B ['b, y params] *) fun lift_import idx params th ctxt = let val ((_, [th']), ctxt') = Variable.importT [th] ctxt; val Ts = map Thm.typ_of_cterm params; val ts = map Thm.term_of params; val prop = Thm.full_prop_of th'; val concl_vars = Vars.build (Vars.add_vars (Logic.strip_imp_concl prop)); - val vars = build_rev (Term.add_vars prop); + val vars = Vars.build (Vars.add_vars prop) |> Vars.list_set; val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt'; fun var_inst v y = let val ((x, i), T) = v; val (U, args) = if Vars.defined concl_vars v then (T, []) else (Ts ---> T, ts); val u = Free (y, U); in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end; val (inst1, inst2) = split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys)); val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th'; in ((inst2, th''), ctxt'') end; (* [x, A x] : B x \ C ------------------ [\x. A x \ B x] : C *) fun lift_subgoals ctxt params asms th = let fun lift ct = fold_rev (Thm.all_name ctxt) params (Drule.list_implies (asms, ct)); val unlift = fold (Thm.elim_implies o Thm.assume) asms o Drule.forall_elim_list (map #2 params) o Thm.assume; val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th)); val th' = fold (Thm.elim_implies o unlift) subgoals th; in (subgoals, th') end; fun retrofit ctxt1 ctxt0 params asms i st1 st0 = let val idx = Thm.maxidx_of st0 + 1; val ps = map #2 params; val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1; val (subgoals, st3) = lift_subgoals ctxt2 params asms st2; val result = st3 |> Goal.conclude |> Drule.implies_intr_list asms |> Drule.forall_intr_list ps |> Drule.implies_intr_list subgoals |> fold_rev (Thm.forall_intr o #1) subgoal_inst |> fold (Thm.forall_elim o #2) subgoal_inst |> Thm.adjust_maxidx_thm idx |> singleton (Variable.export ctxt2 ctxt0); in Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false} (false, result, Thm.nprems_of st1) i st0 end; (* tacticals *) fun GEN_FOCUS flags tac ctxt i st = if Thm.nprems_of st < i then Seq.empty else let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags (ctxt |> Variable.set_bound_focus true) i NONE st; in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end; val FOCUS_PARAMS = GEN_FOCUS (false, false); val FOCUS_PARAMS_FIXED = GEN_FOCUS (false, true); val FOCUS_PREMS = GEN_FOCUS (true, false); val FOCUS = GEN_FOCUS (true, true); fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt; (* Isar subgoal command *) local fun param_bindings ctxt (param_suffix, raw_param_specs) st = let val _ = if Thm.no_prems st then error "No subgoals!" else (); val subgoal = #1 (Logic.dest_implies (Thm.prop_of st)); val subgoal_params = map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal) |> Term.variant_frees subgoal |> map #1; val n = length subgoal_params; val m = length raw_param_specs; val _ = m <= n orelse error ("Excessive subgoal parameter specification" ^ Position.here_list (map snd (drop n raw_param_specs))); val param_specs = raw_param_specs |> map (fn (NONE, _) => NONE | (SOME x, pos) => let val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt)); val _ = Variable.check_name b; in SOME b end) |> param_suffix ? append (replicate (n - m) NONE); fun bindings (SOME x :: xs) (_ :: ys) = x :: bindings xs ys | bindings (NONE :: xs) (y :: ys) = Binding.name y :: bindings xs ys | bindings _ ys = map Binding.name ys; in bindings param_specs subgoal_params end; fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state = let val _ = Proof.assert_backward state; val state1 = state |> Proof.refine_insert []; val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1; val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding; val (prems_binding, do_prems) = (case raw_prems_binding of SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true) | NONE => (Binding.empty_atts, false)); val (subgoal_focus, _) = (if do_prems then focus else focus_params_fixed) ctxt 1 (SOME (param_bindings ctxt param_specs st)) st; fun after_qed (ctxt'', [[result]]) = Proof.end_block #> (fn state' => let val ctxt' = Proof.context_of state'; val results' = Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result); in state' |> Proof.refine_primitive (fn _ => fn _ => retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1 (Goal.protect 0 result) st |> Seq.hd) |> Proof.map_context (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])]) end) #> Proof.reset_facts #> Proof.enter_backward; in state1 |> Proof.enter_forward |> Proof.using_facts [] |> Proof.begin_block |> Proof.map_context (fn _ => #context subgoal_focus |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2) |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal" NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2 |> Proof.using_facts facts |> pair subgoal_focus end; in val subgoal = gen_subgoal Attrib.attribute; val subgoal_cmd = gen_subgoal Attrib.attribute_cmd; end; end; val SUBPROOF = Subgoal.SUBPROOF; diff --git a/src/Pure/Tools/rule_insts.ML b/src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML +++ b/src/Pure/Tools/rule_insts.ML @@ -1,353 +1,353 @@ (* Title: Pure/Tools/rule_insts.ML Author: Makarius Rule instantiations -- operations within implicit rule / subgoal context. *) signature RULE_INSTS = sig val where_rule: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> thm val of_rule: Proof.context -> string option list * string option list -> (binding * string option * mixfix) list -> thm -> thm val read_instantiate: Proof.context -> ((indexname * Position.T) * string) list -> string list -> thm -> thm val read_term: string -> Proof.context -> term * Proof.context val goal_context: term -> Proof.context -> (string * typ) list * Proof.context val res_inst_tac: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic val eres_inst_tac: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic val cut_inst_tac: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic val forw_inst_tac: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic val dres_inst_tac: Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic val thin_tac: Proof.context -> string -> (binding * string option * mixfix) list -> int -> tactic val subgoal_tac: Proof.context -> string -> (binding * string option * mixfix) list -> int -> tactic val make_elim_preserve: Proof.context -> thm -> thm val method: (Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic) -> (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser end; structure Rule_Insts: RULE_INSTS = struct (** read instantiations **) local fun error_var msg (xi, pos) = error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos); fun the_sort tvars (ai, pos) : sort = (case TVars.get_first (fn ((bi, S), _) => if ai = bi then SOME S else NONE) tvars of SOME S => S | NONE => error_var "No such type variable in theorem: " (ai, pos)); fun the_type vars (xi, pos) : typ = (case Vartab.lookup vars xi of SOME T => T | NONE => error_var "No such variable in theorem: " (xi, pos)); fun read_type ctxt tvars ((xi, pos), s) = let val S = the_sort tvars (xi, pos); val T = Syntax.read_typ ctxt s; in if Sign.of_sort (Proof_Context.theory_of ctxt) (T, S) then ((xi, S), T) else error_var "Bad sort for instantiation of type variable: " (xi, pos) end; fun make_instT f (tvars: TVars.set) = let fun add v = let val T = TVar v; val T' = f T; in if T = T' then I else cons (v, T') end; in TVars.fold (add o #1) tvars [] end; fun make_inst f vars = let fun add v = let val t = Var v; val t' = f t; in if t aconv t' then I else cons (v, t') end; in fold add vars [] end; fun read_terms ss Ts ctxt = let fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt; val (ts, ctxt') = fold_map Variable.fix_dummy_patterns (map2 parse Ts ss) ctxt; val ts' = map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts |> Syntax.check_terms ctxt' |> Variable.polymorphic ctxt'; val Ts' = map Term.fastype_of ts'; val tyenv = Vartab.build (fold (Sign.typ_match (Proof_Context.theory_of ctxt)) (Ts ~~ Ts')); val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv []; in ((ts', tyenv'), ctxt') end; in fun read_term s ctxt = let val (t, ctxt') = Variable.fix_dummy_patterns (Syntax.parse_term ctxt s) ctxt; val t' = Syntax.check_term ctxt' t; in (t', ctxt') end; fun read_insts thm raw_insts raw_fixes ctxt = let val (type_insts, term_insts) = List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts; val tvars = TVars.build (Thm.fold_terms {hyps = false} TVars.add_tvars thm); val vars = Vars.build (Thm.fold_terms {hyps = false} Vars.add_vars thm); (*eigen-context*) val (_, ctxt1) = ctxt |> TVars.fold (Variable.declare_internal o Logic.mk_type o TVar o #1) tvars |> Vars.fold (Variable.declare_internal o Var o #1) vars |> Proof_Context.add_fixes_cmd raw_fixes; (*explicit type instantiations*) val instT1 = Term_Subst.instantiateT (TVars.make (map (read_type ctxt1 tvars) type_insts)); val vars1 = Vartab.build (vars |> Vars.fold (fn ((v, T), _) => Vartab.insert (K true) (v, instT1 T))); (*term instantiations*) val (xs, ss) = split_list term_insts; val Ts = map (the_type vars1) xs; val ((ts, inferred), ctxt2) = read_terms ss Ts ctxt1; (*implicit type instantiations*) val instT2 = Term_Subst.instantiateT (TVars.make inferred); val vars2 = Vartab.fold (fn (v, T) => cons (v, instT2 T)) vars1 []; val inst2 = Term_Subst.instantiate (TVars.empty, Vars.build (fold2 (fn (xi, _) => fn t => Vars.add ((xi, Term.fastype_of t), t)) xs ts)) #> Envir.beta_norm; val inst_tvars = make_instT (instT2 o instT1) tvars; val inst_vars = make_inst inst2 vars2; in ((inst_tvars, inst_vars), ctxt2) end; end; (** forward rules **) fun where_rule ctxt raw_insts raw_fixes thm = let val ((inst_tvars, inst_vars), ctxt') = read_insts thm raw_insts raw_fixes ctxt; in thm |> Drule.instantiate_normalize (map (apsnd (Thm.ctyp_of ctxt')) inst_tvars, map (apsnd (Thm.cterm_of ctxt')) inst_vars) |> singleton (Variable.export ctxt' ctxt) |> Rule_Cases.save thm end; fun of_rule ctxt (args, concl_args) fixes thm = let fun zip_vars _ [] = [] | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest | zip_vars ((x, _) :: xs) (SOME t :: rest) = ((x, Position.none), t) :: zip_vars xs rest | zip_vars [] _ = error "More instantiations than variables in theorem"; val insts = - zip_vars (build_rev (Term.add_vars (Thm.full_prop_of thm))) args @ - zip_vars (build_rev (Term.add_vars (Thm.concl_of thm))) concl_args; + zip_vars (Vars.build (Vars.add_vars (Thm.full_prop_of thm)) |> Vars.list_set) args @ + zip_vars (Vars.build (Vars.add_vars (Thm.concl_of thm)) |> Vars.list_set) concl_args; in where_rule ctxt insts fixes thm end; fun read_instantiate ctxt insts xs = where_rule ctxt insts (map (fn x => (Binding.name x, NONE, NoSyn)) xs); (** attributes **) (* where: named instantiation *) val named_insts = Parse.and_list1 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.embedded_inner_syntax)) -- Parse.for_fixes; val _ = Theory.setup (Attrib.setup \<^binding>\where\ (Scan.lift named_insts >> (fn args => Thm.rule_attribute [] (fn context => uncurry (where_rule (Context.proof_of context)) args))) "named instantiation of theorem"); (* of: positional instantiation (terms only) *) local val inst = Args.maybe Args.embedded_inner_syntax; val concl = Args.$$$ "concl" -- Args.colon; val insts = Scan.repeat (Scan.unless concl inst) -- Scan.optional (concl |-- Scan.repeat inst) []; in val _ = Theory.setup (Attrib.setup \<^binding>\of\ (Scan.lift (insts -- Parse.for_fixes) >> (fn args => Thm.rule_attribute [] (fn context => uncurry (of_rule (Context.proof_of context)) args))) "positional instantiation of theorem"); end; (** tactics **) (* goal context *) fun goal_context goal ctxt = let val ((_, params), ctxt') = ctxt |> Variable.declare_constraints goal |> Variable.improper_fixes |> Variable.focus_params NONE goal ||> Variable.restore_proper_fixes ctxt; in (params, ctxt') end; (* resolution after lifting and instantiation; may refer to parameters of the subgoal *) fun bires_inst_tac bires_flag ctxt raw_insts raw_fixes thm i st = CSUBGOAL (fn (cgoal, _) => let (*goal context*) val (params, goal_ctxt) = goal_context (Thm.term_of cgoal) ctxt; val paramTs = map #2 params; (*instantiation context*) val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm raw_insts raw_fixes goal_ctxt; val fixed = map #1 (fold (Variable.add_newly_fixed inst_ctxt goal_ctxt o #2) inst_vars []); (* lift and instantiate rule *) val inc = Thm.maxidx_of st + 1; val lift_type = Logic.incr_tvar inc; fun lift_var ((a, j), T) = ((a, j + inc), paramTs ---> lift_type T); fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t); val inst_tvars' = inst_tvars |> map (fn (((a, i), S), T) => (((a, i + inc), S), Thm.ctyp_of inst_ctxt (lift_type T))); val inst_vars' = inst_vars |> map (fn (v, t) => (lift_var v, Thm.cterm_of inst_ctxt (lift_term t))); val thm' = Thm.lift_rule cgoal thm |> Drule.instantiate_normalize (inst_tvars', inst_vars') |> singleton (Variable.export inst_ctxt ctxt); in compose_tac ctxt (bires_flag, thm', Thm.nprems_of thm) i end) i st; val res_inst_tac = bires_inst_tac false; val eres_inst_tac = bires_inst_tac true; (* forward resolution *) fun make_elim_preserve ctxt rl = let val maxidx = Thm.maxidx_of rl; fun var x = ((x, 0), propT); fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT)); val revcut_rl' = Drule.instantiate_normalize ([], [(var "V", cvar ("V", maxidx + 1)), (var "W", cvar ("W", maxidx + 1))]) Drule.revcut_rl; in (case Seq.list_of (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} (false, rl, Thm.nprems_of rl) 1 revcut_rl') of [th] => th | _ => raise THM ("make_elim_preserve", 1, [rl])) end; (*instantiate and cut -- for atomic fact*) fun cut_inst_tac ctxt insts fixes rule = res_inst_tac ctxt insts fixes (make_elim_preserve ctxt rule); (*forward tactic applies a rule to an assumption without deleting it*) fun forw_inst_tac ctxt insts fixes rule = cut_inst_tac ctxt insts fixes rule THEN' assume_tac ctxt; (*dresolve tactic applies a rule to replace an assumption*) fun dres_inst_tac ctxt insts fixes rule = eres_inst_tac ctxt insts fixes (make_elim_preserve ctxt rule); (* derived tactics *) (*deletion of an assumption*) fun thin_tac ctxt s fixes = eres_inst_tac ctxt [((("V", 0), Position.none), s)] fixes Drule.thin_rl; (*Introduce the given proposition as lemma and subgoal*) fun subgoal_tac ctxt A fixes = DETERM o res_inst_tac ctxt [((("psi", 0), Position.none), A)] fixes cut_rl; (* method wrapper *) fun method inst_tac tac = Args.goal_spec -- Scan.optional (Scan.lift (named_insts --| Args.$$$ "in")) ([], []) -- Attrib.thms >> (fn ((quant, (insts, fixes)), thms) => fn ctxt => METHOD (fn facts => if null insts andalso null fixes then quant (Method.insert_tac ctxt facts THEN' tac ctxt thms) else (case thms of [thm] => quant (Method.insert_tac ctxt facts THEN' inst_tac ctxt insts fixes thm) | _ => error "Cannot have instantiations with multiple rules"))); (* setup *) (*warning: rule_tac etc. refer to dynamic subgoal context!*) val _ = Theory.setup (Method.setup \<^binding>\rule_tac\ (method res_inst_tac resolve_tac) "apply rule (dynamic instantiation)" #> Method.setup \<^binding>\erule_tac\ (method eres_inst_tac eresolve_tac) "apply rule in elimination manner (dynamic instantiation)" #> Method.setup \<^binding>\drule_tac\ (method dres_inst_tac dresolve_tac) "apply rule in destruct manner (dynamic instantiation)" #> Method.setup \<^binding>\frule_tac\ (method forw_inst_tac forward_tac) "apply rule in forward manner (dynamic instantiation)" #> Method.setup \<^binding>\cut_tac\ (method cut_inst_tac (K cut_rules_tac)) "cut rule (dynamic instantiation)" #> Method.setup \<^binding>\subgoal_tac\ (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.embedded_inner_syntax -- Parse.for_fixes) >> (fn (quant, (props, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (EVERY' (map (fn prop => subgoal_tac ctxt prop fixes) props)))) "insert subgoal (dynamic instantiation)" #> Method.setup \<^binding>\thin_tac\ (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >> (fn (quant, (prop, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop fixes))) "remove premise (dynamic instantiation)"); end; diff --git a/src/Pure/logic.ML b/src/Pure/logic.ML --- a/src/Pure/logic.ML +++ b/src/Pure/logic.ML @@ -1,665 +1,666 @@ (* Title: Pure/logic.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Makarius Abstract syntax operations of the Pure meta-logic. *) signature LOGIC = sig val all_const: typ -> term val all: term -> term -> term val dependent_all_name: string * term -> term -> term val is_all: term -> bool val dest_all: term -> (string * typ) * term val list_all: (string * typ) list * term -> term val all_constraint: (string -> typ option) -> string * string -> term -> term val dependent_all_constraint: (string -> typ option) -> string * string -> term -> term val mk_equals: term * term -> term val dest_equals: term -> term * term val implies: term val mk_implies: term * term -> term val dest_implies: term -> term * term val list_implies: term list * term -> term val strip_imp_prems: term -> term list val strip_imp_concl: term -> term val strip_prems: int * term list * term -> term list * term val count_prems: term -> int val nth_prem: int * term -> term val close_term: (string * term) list -> term -> term val close_prop: (string * term) list -> term list -> term -> term val close_prop_constraint: (string -> typ option) -> (string * string) list -> term list -> term -> term val true_prop: term val conjunction: term val mk_conjunction: term * term -> term val mk_conjunction_list: term list -> term val mk_conjunction_balanced: term list -> term val dest_conjunction: term -> term * term val dest_conjunction_list: term -> term list val dest_conjunction_balanced: int -> term -> term list val dest_conjunctions: term -> term list val strip_horn: term -> term list * term val mk_type: typ -> term val dest_type: term -> typ val type_map: (term -> term) -> typ -> typ val const_of_class: class -> string val class_of_const: string -> class val mk_of_class: typ * class -> term val dest_of_class: term -> typ * class val mk_of_sort: typ * sort -> term list val name_classrel: string * string -> string val mk_classrel: class * class -> term val dest_classrel: term -> class * class val name_arities: arity -> string list val name_arity: string * sort list * class -> string val mk_arities: arity -> term list val mk_arity: string * sort list * class -> term val dest_arity: term -> string * sort list * class val dummy_tfree: sort -> typ type unconstrain_context = {present_map: (typ * typ) list, constraints_map: (sort * typ) list, atyp_map: typ -> typ, map_atyps: typ -> typ, constraints: ((typ * class) * term) list, outer_constraints: (typ * class) list}; val unconstrainT: sort list -> term -> unconstrain_context * term val protectC: term val protect: term -> term val unprotect: term -> term val mk_term: term -> term val dest_term: term -> term val occs: term * term -> bool val close_form: term -> term val combound: term * int * int -> term val rlist_abs: (string * typ) list * term -> term val incr_tvar_same: int -> typ Same.operation val incr_tvar: int -> typ -> typ val incr_indexes_same: string list * typ list * int -> term Same.operation val incr_indexes: string list * typ list * int -> term -> term val lift_abs: int -> term -> term -> term val lift_all: int -> term -> term -> term val strip_assums_hyp: term -> term list val strip_assums_concl: term -> term val strip_params: term -> (string * typ) list val has_meta_prems: term -> bool val flatten_params: int -> term -> term val list_rename_params: string list -> term -> term val assum_pairs: int * term -> (term * term) list val assum_problems: int * term -> (term -> term) * term list * term val bad_schematic: indexname -> string val bad_fixed: string -> string val varifyT_global: typ -> typ val unvarifyT_global: typ -> typ val varify_types_global: term -> term val unvarify_types_global: term -> term val varify_global: term -> term val unvarify_global: term -> term val get_goal: term -> int -> term val goal_params: term -> int -> term * term list val prems_of_goal: term -> int -> term list val concl_of_goal: term -> int -> term end; structure Logic : LOGIC = struct (*** Abstract syntax operations on the meta-connectives ***) (** all **) fun all_const T = Const ("Pure.all", (T --> propT) --> propT); fun all v t = all_const (Term.fastype_of v) $ lambda v t; fun dependent_all_name (x, v) t = let val x' = if x = "" then Term.term_name v else x; val T = Term.fastype_of v; val t' = Term.abstract_over (v, t); in if Term.is_dependent t' then all_const T $ Abs (x', T, t') else t end; fun is_all (Const ("Pure.all", _) $ Abs _) = true | is_all _ = false; fun dest_all (Const ("Pure.all", _) $ Abs (abs as (_, T, _))) = let val (x, b) = Term.dest_abs abs (*potentially slow*) in ((x, T), b) end | dest_all t = raise TERM ("dest_all", [t]); fun list_all ([], t) = t | list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t)); (* operations before type-inference *) local fun abs_body default_type z tm = let fun abs lev (Abs (x, T, b)) = Abs (x, T, abs (lev + 1) b) | abs lev (t $ u) = abs lev t $ abs lev u | abs lev (a as Free (x, T)) = if x = z then Type.constraint (the_default dummyT (default_type x)) (Type.constraint T (Bound lev)) else a | abs _ a = a; in abs 0 (Term.incr_boundvars 1 tm) end; in fun all_constraint default_type (y, z) t = all_const dummyT $ Abs (y, dummyT, abs_body default_type z t); fun dependent_all_constraint default_type (y, z) t = let val t' = abs_body default_type z t in if Term.is_dependent t' then all_const dummyT $ Abs (y, dummyT, t') else t end; end; (** equality **) fun mk_equals (t, u) = let val T = Term.fastype_of t in Const ("Pure.eq", T --> T --> propT) $ t $ u end; fun dest_equals (Const ("Pure.eq", _) $ t $ u) = (t, u) | dest_equals t = raise TERM ("dest_equals", [t]); (** implies **) val implies = Const ("Pure.imp", propT --> propT --> propT); fun mk_implies (A, B) = implies $ A $ B; fun dest_implies (Const ("Pure.imp", _) $ A $ B) = (A, B) | dest_implies A = raise TERM ("dest_implies", [A]); (** nested implications **) (* [A1,...,An], B goes to A1\...An\B *) fun list_implies ([], B) = B | list_implies (A::As, B) = implies $ A $ list_implies(As,B); (* A1\...An\B goes to [A1,...,An], where B is not an implication *) fun strip_imp_prems (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems B | strip_imp_prems _ = []; (* A1\...An\B goes to B, where B is not an implication *) fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B | strip_imp_concl A = A : term; (*Strip and return premises: (i, [], A1\...Ai\B) goes to ([Ai, A(i-1),...,A1] , B) (REVERSED) if i<0 or else i too big then raises TERM*) fun strip_prems (0, As, B) = (As, B) | strip_prems (i, As, Const("Pure.imp", _) $ A $ B) = strip_prems (i-1, A::As, B) | strip_prems (_, As, A) = raise TERM("strip_prems", A::As); (*Count premises -- quicker than (length o strip_prems) *) fun count_prems (Const ("Pure.imp", _) $ _ $ B) = 1 + count_prems B | count_prems _ = 0; (*Select Ai from A1\...Ai\B*) fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B) | nth_prem (_, A) = raise TERM ("nth_prem", [A]); (*strip a proof state (Horn clause): B1 \ ... Bn \ C goes to ([B1, ..., Bn], C) *) fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); (* close -- omit vacuous quantifiers *) val close_term = fold_rev Term.dependent_lambda_name; fun close_prop xs As B = fold_rev dependent_all_name xs (list_implies (As, B)); fun close_prop_constraint default_type xs As B = fold_rev (dependent_all_constraint default_type) xs (list_implies (As, B)); (** conjunction **) val true_prop = all_const propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)); val conjunction = Const ("Pure.conjunction", propT --> propT --> propT); (*A &&& B*) fun mk_conjunction (A, B) = conjunction $ A $ B; (*A &&& B &&& C -- improper*) fun mk_conjunction_list [] = true_prop | mk_conjunction_list ts = foldr1 mk_conjunction ts; (*(A &&& B) &&& (C &&& D) -- balanced*) fun mk_conjunction_balanced [] = true_prop | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts; (*A &&& B*) fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B) | dest_conjunction t = raise TERM ("dest_conjunction", [t]); (*A &&& B &&& C -- improper*) fun dest_conjunction_list t = (case try dest_conjunction t of NONE => [t] | SOME (A, B) => A :: dest_conjunction_list B); (*(A &&& B) &&& (C &&& D) -- balanced*) fun dest_conjunction_balanced 0 _ = [] | dest_conjunction_balanced n t = Balanced_Tree.dest dest_conjunction n t; (*((A &&& B) &&& C) &&& D &&& E -- flat*) fun dest_conjunctions t = (case try dest_conjunction t of NONE => [t] | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B); (** types as terms **) fun mk_type ty = Const ("Pure.type", Term.itselfT ty); fun dest_type (Const ("Pure.type", Type ("itself", [ty]))) = ty | dest_type t = raise TERM ("dest_type", [t]); fun type_map f = dest_type o f o mk_type; (** type classes **) (* const names *) val classN = "_class"; val const_of_class = suffix classN; fun class_of_const c = unsuffix classN c handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []); (* class/sort membership *) fun mk_of_class (ty, c) = Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty; fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class) | dest_of_class t = raise TERM ("dest_of_class", [t]); fun mk_of_sort (ty, S) = map (fn c => mk_of_class (ty, c)) S; (* class relations *) fun name_classrel (c1, c2) = Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2; fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2); fun dest_classrel tm = (case dest_of_class tm of (TVar (_, [c1]), c2) => (c1, c2) | _ => raise TERM ("dest_classrel", [tm])); (* type arities *) fun name_arities (t, _, S) = let val b = Long_Name.base_name t in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end; fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c])); fun mk_arities (t, Ss, S) = let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss)) in map (fn c => mk_of_class (T, c)) S end; fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c])); fun dest_arity tm = let fun err () = raise TERM ("dest_arity", [tm]); val (ty, c) = dest_of_class tm; val (t, tvars) = (case ty of Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ()) | _ => err ()); val Ss = if has_duplicates (eq_fst (op =)) tvars then err () else map snd tvars; in (t, Ss, c) end; (* internalized sort constraints *) fun dummy_tfree S = TFree ("'dummy", S); type unconstrain_context = {present_map: (typ * typ) list, constraints_map: (sort * typ) list, atyp_map: typ -> typ, map_atyps: typ -> typ, constraints: ((typ * class) * term) list, outer_constraints: (typ * class) list}; fun unconstrainT shyps prop = let val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []); val extra = fold (Sorts.remove_sort o #2) present shyps; val n = length present; val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n; val present_map = map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1; val constraints_map = map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @ map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2; fun atyp_map T = (case AList.lookup (op =) present_map T of SOME U => U | NONE => (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of SOME U => U | NONE => raise TYPE ("Dangling type variable ", [T], [prop]))); val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map); val constraints = constraints_map |> maps (fn (_, T as TVar (ai, S)) => map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S); val outer_constraints = maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra); val ucontext = {present_map = present_map, constraints_map = constraints_map, atyp_map = atyp_map, map_atyps = map_atyps, constraints = constraints, outer_constraints = outer_constraints}; val prop' = prop |> Term.map_types map_atyps |> curry list_implies (map #2 constraints); in (ucontext, prop') end; (** protected propositions and embedded terms **) val protectC = Const ("Pure.prop", propT --> propT); fun protect t = protectC $ t; fun unprotect (Const ("Pure.prop", _) $ t) = t | unprotect t = raise TERM ("unprotect", [t]); fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t; fun dest_term (Const ("Pure.term", _) $ t) = t | dest_term t = raise TERM ("dest_term", [t]); (*** Low-level term operations ***) (*Does t occur in u? Or is alpha-convertible to u? The term t must contain no loose bound variables*) fun occs (t, u) = exists_subterm (fn s => t aconv s) u; (*Close up a formula over all free variables by quantification*) -fun close_form A = fold (all o Free) (Term.add_frees A []) A; +fun close_form A = + fold_rev (all o Free) (Frees.build (Frees.add_frees A) |> Frees.list_set) A; (*** Specialized operations for resolution... ***) (*computes t(Bound(n+k-1),...,Bound(n)) *) fun combound (t, n, k) = if k>0 then combound (t,n+1,k-1) $ (Bound n) else t; (* ([xn,...,x1], t) goes to \x1 ... xn. t *) fun rlist_abs ([], body) = body | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body)); fun incr_tvar_same 0 = Same.same | incr_tvar_same k = Term_Subst.map_atypsT_same (fn TVar ((a, i), S) => TVar ((a, i + k), S) | _ => raise Same.SAME); fun incr_tvar k T = incr_tvar_same k T handle Same.SAME => T; (*For all variables in the term, increment indexnames and lift over the Us result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *) fun incr_indexes_same ([], [], 0) = Same.same | incr_indexes_same (fixed, Ts, k) = let val n = length Ts; val incrT = incr_tvar_same k; fun incr lev (Var ((x, i), T)) = combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n) | incr lev (Free (x, T)) = if member (op =) fixed x then combound (Free (x, Ts ---> Same.commit incrT T), lev, n) else Free (x, incrT T) | incr lev (Abs (x, T, body)) = (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body) handle Same.SAME => Abs (x, T, incr (lev + 1) body)) | incr lev (t $ u) = (incr lev t $ (incr lev u handle Same.SAME => u) handle Same.SAME => t $ incr lev u) | incr _ (Const (c, T)) = Const (c, incrT T) | incr _ (Bound _) = raise Same.SAME; in incr 0 end; fun incr_indexes arg t = incr_indexes_same arg t handle Same.SAME => t; (* Lifting functions from subgoal and increment: lift_abs operates on terms lift_all operates on propositions *) fun lift_abs inc = let fun lift Ts (Const ("Pure.imp", _) $ _ $ B) t = lift Ts B t | lift Ts (Const ("Pure.all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t) | lift Ts _ t = incr_indexes ([], rev Ts, inc) t; in lift [] end; fun lift_all inc = let fun lift Ts ((c as Const ("Pure.imp", _)) $ A $ B) t = c $ A $ lift Ts B t | lift Ts ((c as Const ("Pure.all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t) | lift Ts _ t = incr_indexes ([], rev Ts, inc) t; in lift [] end; (*Strips assumptions in goal, yielding list of hypotheses. *) fun strip_assums_hyp B = let fun strip Hs (Const ("Pure.imp", _) $ H $ B) = strip (H :: Hs) B | strip Hs (Const ("Pure.all", _) $ Abs (a, T, t)) = strip (map (incr_boundvars 1) Hs) t | strip Hs B = rev Hs in strip [] B end; (*Strips assumptions in goal, yielding conclusion. *) fun strip_assums_concl (Const("Pure.imp", _) $ H $ B) = strip_assums_concl B | strip_assums_concl (Const("Pure.all", _) $ Abs (a, T, t)) = strip_assums_concl t | strip_assums_concl B = B; (*Make a list of all the parameters in a subgoal, even if nested*) fun strip_params (Const("Pure.imp", _) $ H $ B) = strip_params B | strip_params (Const("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_params t | strip_params B = []; (*test for nested meta connectives in prems*) val has_meta_prems = let fun is_meta (Const ("Pure.eq", _) $ _ $ _) = true | is_meta (Const ("Pure.imp", _) $ _ $ _) = true | is_meta (Const ("Pure.all", _) $ _) = true | is_meta _ = false; fun ex_meta (Const ("Pure.imp", _) $ A $ B) = is_meta A orelse ex_meta B | ex_meta (Const ("Pure.all", _) $ Abs (_, _, B)) = ex_meta B | ex_meta _ = false; in ex_meta end; (*Removes the parameters from a subgoal and renumber bvars in hypotheses, where j is the total number of parameters (precomputed) If n>0 then deletes assumption n. *) fun remove_params j n A = if j=0 andalso n<=0 then A (*nothing left to do...*) else case A of Const("Pure.imp", _) $ H $ B => if n=1 then (remove_params j (n-1) B) else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B) | Const("Pure.all",_)$Abs(a,T,t) => remove_params (j-1) n t | _ => if n>0 then raise TERM("remove_params", [A]) else A; (*Move all parameters to the front of the subgoal, renaming them apart; if n>0 then deletes assumption n. *) fun flatten_params n A = let val params = strip_params A; val vars = ListPair.zip (Name.variant_list [] (map #1 params), map #2 params) in list_all (vars, remove_params (length vars) n A) end; (*Makes parameters in a goal have the names supplied by the list cs.*) fun list_rename_params cs (Const ("Pure.imp", _) $ A $ B) = implies $ A $ list_rename_params cs B | list_rename_params (c :: cs) ((a as Const ("Pure.all", _)) $ Abs (_, T, t)) = a $ Abs (c, T, list_rename_params cs t) | list_rename_params cs B = B; (*** Treatment of "assume", "erule", etc. ***) (*Strips assumptions in goal yielding HS = [Hn,...,H1], params = [xm,...,x1], and B, where x1...xm are the parameters. This version (21.1.2005) REQUIRES the the parameters to be flattened, but it allows erule to work on assumptions of the form \x. phi. Any \ after the outermost string will be regarded as belonging to the conclusion, and left untouched. Used ONLY by assum_pairs. Unless nasms<0, it can terminate the recursion early; that allows erule to work on assumptions of the form P\Q.*) fun strip_assums_imp (0, Hs, B) = (Hs, B) (*recursion terminated by nasms*) | strip_assums_imp (nasms, Hs, Const("Pure.imp", _) $ H $ B) = strip_assums_imp (nasms-1, H::Hs, B) | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*) (*Strips OUTER parameters only.*) fun strip_assums_all (params, Const("Pure.all",_)$Abs(a,T,t)) = strip_assums_all ((a,T)::params, t) | strip_assums_all (params, B) = (params, B); (*Produces disagreement pairs, one for each assumption proof, in order. A is the first premise of the lifted rule, and thus has the form H1 \ ... Hk \ B and the pairs are (H1,B),...,(Hk,B). nasms is the number of assumptions in the original subgoal, needed when B has the form B1 \ B2: it stops B1 from being taken as an assumption. *) fun assum_pairs(nasms,A) = let val (params, A') = strip_assums_all ([],A) val (Hs,B) = strip_assums_imp (nasms,[],A') fun abspar t = rlist_abs(params, t) val D = abspar B fun pairrev ([], pairs) = pairs | pairrev (H::Hs, pairs) = pairrev(Hs, (abspar H, D) :: pairs) in pairrev (Hs,[]) end; fun assum_problems (nasms, A) = let val (params, A') = strip_assums_all ([], A) val (Hs, B) = strip_assums_imp (nasms, [], A') fun abspar t = rlist_abs (params, t) in (abspar, rev Hs, B) end; (* global schematic variables *) fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi); fun bad_fixed x = "Illegal fixed variable: " ^ quote x; fun varifyT_global_same ty = ty |> Term_Subst.map_atypsT_same (fn TFree (a, S) => TVar ((a, 0), S) | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])); fun unvarifyT_global_same ty = ty |> Term_Subst.map_atypsT_same (fn TVar ((a, 0), S) => TFree (a, S) | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []) | TFree (a, _) => raise TYPE (bad_fixed a, [ty], [])); val varifyT_global = Same.commit varifyT_global_same; val unvarifyT_global = Same.commit unvarifyT_global_same; fun varify_types_global tm = tm |> Same.commit (Term_Subst.map_types_same varifyT_global_same) handle TYPE (msg, _, _) => raise TERM (msg, [tm]); fun unvarify_types_global tm = tm |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same) handle TYPE (msg, _, _) => raise TERM (msg, [tm]); fun varify_global tm = tm |> Same.commit (Term_Subst.map_aterms_same (fn Free (x, T) => Var ((x, 0), T) | Var (xi, _) => raise TERM (bad_schematic xi, [tm]) | _ => raise Same.SAME)) |> varify_types_global; fun unvarify_global tm = tm |> Same.commit (Term_Subst.map_aterms_same (fn Var ((x, 0), T) => Free (x, T) | Var (xi, _) => raise TERM (bad_schematic xi, [tm]) | Free (x, _) => raise TERM (bad_fixed x, [tm]) | _ => raise Same.SAME)) |> unvarify_types_global; (* goal states *) fun get_goal st i = nth_prem (i, st) handle TERM _ => error ("Subgoal number " ^ string_of_int i ^ " out of range (a total of " ^ string_of_int (count_prems st) ^ " subgoals)"); (*reverses parameters for substitution*) fun goal_params st i = let val gi = get_goal st i val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi)) in (gi, rfrees) end; fun concl_of_goal st i = let val (gi, rfrees) = goal_params st i val B = strip_assums_concl gi in subst_bounds (rfrees, B) end; fun prems_of_goal st i = let val (gi, rfrees) = goal_params st i val As = strip_assums_hyp gi in map (fn A => subst_bounds (rfrees, A)) As end; end; diff --git a/src/Pure/type_infer.ML b/src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML +++ b/src/Pure/type_infer.ML @@ -1,123 +1,124 @@ (* Title: Pure/type_infer.ML Author: Stefan Berghofer and Markus Wenzel, TU Muenchen Basic representation of type-inference problems. *) signature TYPE_INFER = sig val is_param: indexname -> bool val is_paramT: typ -> bool val param_maxidx: term -> int -> int val param_maxidx_of: term list -> int val param: int -> string * sort -> typ val mk_param: int -> sort -> typ val anyT: sort -> typ val paramify_vars: typ -> typ val deref: typ Vartab.table -> typ -> typ val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list val object_logic: bool Config.T val fixate: Proof.context -> bool -> term list -> term list end; structure Type_Infer: TYPE_INFER = struct (** type parameters and constraints **) (* type inference parameters -- may get instantiated *) fun is_param (x, _: int) = String.isPrefix "?" x; fun is_paramT (TVar (xi, _)) = is_param xi | is_paramT _ = false; val param_maxidx = (Term.fold_types o Term.fold_atyps) (fn (TVar (xi as (_, i), _)) => if is_param xi then Integer.max i else I | _ => I); fun param_maxidx_of ts = fold param_maxidx ts ~1; fun param i (x, S) = TVar (("?" ^ x, i), S); fun mk_param i S = TVar (("?'a", i), S); (* pre-stage parameters *) fun anyT S = TFree ("'_dummy_", S); val paramify_vars = Same.commit (Term_Subst.map_atypsT_same (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME)); (** results **) (* dereferenced views *) fun deref tye (T as TVar (xi, _)) = (case Vartab.lookup tye xi of NONE => T | SOME U => deref tye U) | deref _ T = T; fun add_parms tye T = (case deref tye T of Type (_, Ts) => fold (add_parms tye) Ts | TVar (xi, _) => if is_param xi then insert (op =) xi else I | _ => I); fun add_names tye T = (case deref tye T of Type (_, Ts) => fold (add_names tye) Ts | TFree (x, _) => Name.declare x | TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x); (* finish -- standardize remaining parameters *) fun finish ctxt tye (Ts, ts) = let val used = (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt)); val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts [])); val names = Name.invent used ("?" ^ Name.aT) (length parms); val tab = Vartab.make (parms ~~ names); fun finish_typ T = (case deref tye T of Type (a, Ts) => Type (a, map finish_typ Ts) | U as TFree _ => U | U as TVar (xi, S) => (case Vartab.lookup tab xi of NONE => U | SOME a => TVar ((a, 0), S))); in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end; (* fixate -- introduce fresh type variables *) val object_logic = Config.declare_bool ("Type_Infer.object_logic", \<^here>) (K true); fun fixate ctxt pattern ts = let val base_sort = Object_Logic.get_base_sort ctxt; val improve_sort = if is_some base_sort andalso not pattern andalso Config.get ctxt object_logic then fn [] => the base_sort | S => S else I; fun subst_param (xi, S) (inst, used) = if is_param xi then let val [a] = Name.invent used Name.aT 1; val used' = Name.declare a used; in (TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end else (inst, used); + val params = TVars.build (fold TVars.add_tvars ts) |> TVars.list_set; val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt); - val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) (TVars.empty, used); + val (inst, _) = fold subst_param params (TVars.empty, used); in (map o map_types) (Term_Subst.instantiateT inst) ts end; end; diff --git a/src/Pure/variable.ML b/src/Pure/variable.ML --- a/src/Pure/variable.ML +++ b/src/Pure/variable.ML @@ -1,743 +1,745 @@ (* Title: Pure/variable.ML Author: Makarius Fixed type/term variables and polymorphic term abbreviations. *) signature VARIABLE = sig val names_of: Proof.context -> Name.context val binds_of: Proof.context -> (typ * term) Vartab.table val maxidx_of: Proof.context -> int val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table val is_declared: Proof.context -> string -> bool val check_name: binding -> string val default_type: Proof.context -> string -> typ option val def_type: Proof.context -> bool -> indexname -> typ option val def_sort: Proof.context -> indexname -> sort option val declare_maxidx: int -> Proof.context -> Proof.context val declare_names: term -> Proof.context -> Proof.context val declare_constraints: term -> Proof.context -> Proof.context val declare_internal: term -> Proof.context -> Proof.context val declare_term: term -> Proof.context -> Proof.context val declare_typ: typ -> Proof.context -> Proof.context val declare_prf: Proofterm.proof -> Proof.context -> Proof.context val declare_thm: thm -> Proof.context -> Proof.context val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list val bind_term: indexname * term -> Proof.context -> Proof.context val unbind_term: indexname -> Proof.context -> Proof.context val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context val expand_binds: Proof.context -> term -> term val lookup_const: Proof.context -> string -> string option val is_const: Proof.context -> string -> bool val declare_const: string * string -> Proof.context -> Proof.context val next_bound: string * typ -> Proof.context -> term * Proof.context val revert_bounds: Proof.context -> term -> term val is_body: Proof.context -> bool val set_body: bool -> Proof.context -> Proof.context val restore_body: Proof.context -> Proof.context -> Proof.context val improper_fixes: Proof.context -> Proof.context val restore_proper_fixes: Proof.context -> Proof.context -> Proof.context val is_improper: Proof.context -> string -> bool val is_fixed: Proof.context -> string -> bool val is_newly_fixed: Proof.context -> Proof.context -> string -> bool val fixed_ord: Proof.context -> string ord val intern_fixed: Proof.context -> string -> string val lookup_fixed: Proof.context -> string -> string option val revert_fixed: Proof.context -> string -> string val markup_fixed: Proof.context -> string -> Markup.T val markup: Proof.context -> string -> Markup.T val markup_entity_def: Proof.context -> string -> Markup.T val dest_fixes: Proof.context -> (string * string) list val add_fixed_names: Proof.context -> term -> string list -> string list val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list val add_newly_fixed: Proof.context -> Proof.context -> term -> (string * typ) list -> (string * typ) list val add_free_names: Proof.context -> term -> string list -> string list val add_frees: Proof.context -> term -> (string * typ) list -> (string * typ) list val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context val add_fixes: string list -> Proof.context -> string list * Proof.context val add_fixes_direct: string list -> Proof.context -> Proof.context val add_fixes_implicit: term -> Proof.context -> Proof.context val fix_dummy_patterns: term -> Proof.context -> term * Proof.context val variant_fixes: string list -> Proof.context -> string list * Proof.context val gen_all: Proof.context -> thm -> thm val export_terms: Proof.context -> Proof.context -> term list -> term list val exportT_terms: Proof.context -> Proof.context -> term list -> term list val exportT: Proof.context -> Proof.context -> thm list -> thm list val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof val export: Proof.context -> Proof.context -> thm list -> thm list val export_morphism: Proof.context -> Proof.context -> morphism val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context val importT_inst: term list -> Proof.context -> typ TVars.table * Proof.context val import_inst: bool -> term list -> Proof.context -> (typ TVars.table * term Vars.table) * Proof.context val importT_terms: term list -> Proof.context -> term list * Proof.context val import_terms: bool -> term list -> Proof.context -> term list * Proof.context val importT: thm list -> Proof.context -> (ctyp TVars.table * thm list) * Proof.context val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context val import: bool -> thm list -> Proof.context -> ((ctyp TVars.table * cterm Vars.table) * thm list) * Proof.context val import_vars: Proof.context -> thm -> thm val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list val is_bound_focus: Proof.context -> bool val set_bound_focus: bool -> Proof.context -> Proof.context val restore_bound_focus: Proof.context -> Proof.context -> Proof.context val focus_params: binding list option -> term -> Proof.context -> (string list * (string * typ) list) * Proof.context val focus: binding list option -> term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context val focus_cterm: binding list option -> cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context val focus_subgoal: binding list option -> int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context val warn_extra_tfrees: Proof.context -> Proof.context -> unit val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list val polymorphic: Proof.context -> term list -> term list end; structure Variable: VARIABLE = struct (** local context data **) type fixes = (string * bool) Name_Space.table; val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN; datatype data = Data of {names: Name.context, (*type/term variable names*) consts: string Symtab.table, (*consts within the local scope*) bounds: int * ((string * typ) * string) list, (*next index, internal name, type, external name*) fixes: fixes, (*term fixes -- global name space, intern ~> extern*) binds: (typ * term) Vartab.table, (*term bindings*) type_occs: string list Symtab.table, (*type variables -- possibly within term variables*) maxidx: int, (*maximum var index*) constraints: typ Vartab.table * (*type constraints*) sort Vartab.table}; (*default sorts*) fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) = Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds, type_occs = type_occs, maxidx = maxidx, constraints = constraints}; val empty_data = make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, Symtab.empty, ~1, (Vartab.empty, Vartab.empty)); structure Data = Proof_Data ( type T = data; fun init _ = empty_data; ); fun map_data f = Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, constraints} => make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints))); fun map_names f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (f names, consts, bounds, fixes, binds, type_occs, maxidx, constraints)); fun map_consts f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, f consts, bounds, fixes, binds, type_occs, maxidx, constraints)); fun map_bounds f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, f bounds, fixes, binds, type_occs, maxidx, constraints)); fun map_fixes f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, bounds, f fixes, binds, type_occs, maxidx, constraints)); fun map_binds f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, bounds, fixes, f binds, type_occs, maxidx, constraints)); fun map_type_occs f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, bounds, fixes, binds, f type_occs, maxidx, constraints)); fun map_maxidx f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, bounds, fixes, binds, type_occs, f maxidx, constraints)); fun map_constraints f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, bounds, fixes, binds, type_occs, maxidx, f constraints)); fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); val names_of = #names o rep_data; val fixes_of = #fixes o rep_data; val fixes_space = Name_Space.space_of_table o fixes_of; val binds_of = #binds o rep_data; val type_occs_of = #type_occs o rep_data; val maxidx_of = #maxidx o rep_data; val constraints_of = #constraints o rep_data; val is_declared = Name.is_declared o names_of; val check_name = Name_Space.base_name o tap Binding.check; (** declarations **) (* default sorts and types *) fun default_type ctxt x = Vartab.lookup (#1 (constraints_of ctxt)) (x, ~1); fun def_type ctxt pattern xi = let val {binds, constraints = (types, _), ...} = rep_data ctxt in (case Vartab.lookup types xi of NONE => if pattern then NONE else Vartab.lookup binds xi |> Option.map (Type.mark_polymorphic o #1) | some => some) end; val def_sort = Vartab.lookup o #2 o constraints_of; (* maxidx *) val declare_maxidx = map_maxidx o Integer.max; (* names *) fun declare_type_names t = map_names (fold_types (fold_atyps Term.declare_typ_names) t) #> map_maxidx (fold_types Term.maxidx_typ t); fun declare_names t = declare_type_names t #> map_names (fold_aterms Term.declare_term_frees t) #> map_maxidx (Term.maxidx_term t); (* type occurrences *) fun decl_type_occsT T = fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I) T; val decl_type_occs = fold_term_types (fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I) | _ => decl_type_occsT); val declare_type_occsT = map_type_occs o fold_types decl_type_occsT; val declare_type_occs = map_type_occs o decl_type_occs; (* constraints *) fun constrain_tvar (xi, raw_S) = let val S = #2 (Term_Position.decode_positionS raw_S) in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end; fun declare_constraints t = map_constraints (fn (types, sorts) => let val types' = fold_aterms (fn Free (x, T) => Vartab.update ((x, ~1), T) | Var v => Vartab.update v | _ => I) t types; val sorts' = (fold_types o fold_atyps) (fn TFree (x, S) => constrain_tvar ((x, ~1), S) | TVar v => constrain_tvar v | _ => I) t sorts; in (types', sorts') end) #> declare_type_occsT t #> declare_type_names t; (* common declarations *) fun declare_internal t = declare_names t #> declare_type_occs t #> Thm.declare_term_sorts t; fun declare_term t = declare_internal t #> declare_constraints t; val declare_typ = declare_term o Logic.mk_type; val declare_prf = Proofterm.fold_proof_terms_types declare_internal (declare_internal o Logic.mk_type); val declare_thm = Thm.fold_terms {hyps = true} declare_internal; (* renaming term/type frees *) fun variant_frees ctxt ts frees = let val names = names_of (fold declare_names ts ctxt); val xs = fst (fold_map Name.variant (map #1 frees) names); in xs ~~ map snd frees end; (** term bindings **) fun bind_term ((x, i), t) = let val u = Term.close_schematic_term t; val U = Term.fastype_of u; in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end; val unbind_term = map_binds o Vartab.delete_safe; fun maybe_bind_term (xi, SOME t) = bind_term (xi, t) | maybe_bind_term (xi, NONE) = unbind_term xi; fun expand_binds ctxt = let val binds = binds_of ctxt; val get = fn Var (xi, _) => Vartab.lookup binds xi | _ => NONE; in Envir.beta_norm o Envir.expand_term get end; (** consts **) val lookup_const = Symtab.lookup o #consts o rep_data; val is_const = is_some oo lookup_const; val declare_fixed = map_consts o Symtab.delete_safe; val declare_const = map_consts o Symtab.update; (** bounds **) fun next_bound (a, T) ctxt = let val b = Name.bound (#1 (#bounds (rep_data ctxt))); val ctxt' = ctxt |> map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds)); in (Free (b, T), ctxt') end; fun revert_bounds ctxt t = (case #2 (#bounds (rep_data ctxt)) of [] => t | bounds => let val names = Term.declare_term_names t (names_of ctxt); val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names)); fun subst ((b, T), _) x' = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T)); in Term.subst_atomic (map2 subst bounds xs) t end); (** fixes **) (* inner body mode *) val inner_body = Config.declare_bool ("inner_body", \<^here>) (K false); val is_body = Config.apply inner_body; val set_body = Config.put inner_body; val restore_body = set_body o is_body; (* proper mode *) val proper_fixes = Config.declare_bool ("proper_fixes", \<^here>) (K true); val improper_fixes = Config.put proper_fixes false; val restore_proper_fixes = Config.put proper_fixes o Config.apply proper_fixes; fun is_improper ctxt x = (case Name_Space.lookup (fixes_of ctxt) x of SOME (_, proper) => not proper | NONE => false); (* specialized name space *) val is_fixed = Name_Space.defined o fixes_of; fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer); val fixed_ord = Name_Space.entry_ord o fixes_space; val intern_fixed = Name_Space.intern o fixes_space; fun lookup_fixed ctxt x = let val x' = intern_fixed ctxt x in if is_fixed ctxt x' then SOME x' else NONE end; fun revert_fixed ctxt x = (case Name_Space.lookup (fixes_of ctxt) x of SOME (x', _) => if intern_fixed ctxt x' = x then x' else x | NONE => x); fun markup_fixed ctxt x = Name_Space.markup (fixes_space ctxt) x |> Markup.name (revert_fixed ctxt x); fun markup ctxt x = if is_improper ctxt x then Markup.improper else if Name.is_skolem x then Markup.skolem else Markup.free; val markup_entity_def = Name_Space.markup_def o fixes_space; fun dest_fixes ctxt = Name_Space.fold_table (fn (x, (y, _)) => cons (y, x)) (fixes_of ctxt) [] |> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2); (* collect variables *) fun add_free_names ctxt = fold_aterms (fn Free (x, _) => not (is_fixed ctxt x) ? insert (op =) x | _ => I); fun add_frees ctxt = fold_aterms (fn Free (x, T) => not (is_fixed ctxt x) ? insert (op =) (x, T) | _ => I); fun add_fixed_names ctxt = fold_aterms (fn Free (x, _) => is_fixed ctxt x ? insert (op =) x | _ => I); fun add_fixed ctxt = fold_aterms (fn Free (x, T) => is_fixed ctxt x ? insert (op =) (x, T) | _ => I); fun add_newly_fixed ctxt' ctxt = fold_aterms (fn Free (x, T) => is_newly_fixed ctxt' ctxt x ? insert (op =) (x, T) | _ => I); (* declarations *) local fun err_dups dups = error ("Duplicate fixed variable(s): " ^ commas (map Binding.print dups)); fun new_fixed ((x, x'), pos) ctxt = if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)] else let val proper = Config.get ctxt proper_fixes; val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming) |> Context_Position.set_visible_generic false; in ctxt |> map_fixes (Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #> Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x') |> declare_fixed x |> declare_constraints (Syntax.free x') end; fun new_fixes names' args = map_names (K names') #> fold new_fixed args #> pair (map (#2 o #1) args); in fun add_fixes_binding bs ctxt = let val _ = (case filter (Name.is_skolem o Binding.name_of) bs of [] => () | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads))); val _ = (case duplicates (op = o apply2 Binding.name_of) bs of [] => () | dups => err_dups dups); val xs = map check_name bs; val names = names_of ctxt; val (xs', names') = if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem else (xs, fold Name.declare xs names); in ctxt |> new_fixes names' ((xs ~~ xs') ~~ map Binding.pos_of bs) end; fun variant_names ctxt raw_xs = let val names = names_of ctxt; val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs; val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem); in (names', xs ~~ xs') end; fun variant_fixes xs ctxt = let val (names', vs) = variant_names ctxt xs; in ctxt |> new_fixes names' (map (rpair Position.none) vs) end; fun bound_fixes xs ctxt = let val (names', vs) = variant_names ctxt (map #1 xs); val (ys, ctxt') = fold_map next_bound (map2 (fn (x', _) => fn (_, T) => (x', T)) vs xs) ctxt; val fixes = map2 (fn (x, _) => fn Free (y, _) => ((x, y), Position.none)) vs ys; in ctxt' |> new_fixes names' fixes end; end; val add_fixes = add_fixes_binding o map Binding.name; fun add_fixes_direct xs ctxt = ctxt |> set_body false |> (snd o add_fixes xs) |> restore_body ctxt; fun add_fixes_implicit t ctxt = ctxt |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t [])); (* dummy patterns *) fun fix_dummy_patterns (Const ("Pure.dummy_pattern", T)) ctxt = let val ([x], ctxt') = ctxt |> set_body true |> add_fixes [Name.uu_] ||> restore_body ctxt in (Free (x, T), ctxt') end | fix_dummy_patterns (Abs (x, T, b)) ctxt = let val (b', ctxt') = fix_dummy_patterns b ctxt in (Abs (x, T, b'), ctxt') end | fix_dummy_patterns (t $ u) ctxt = let val (t', ctxt') = fix_dummy_patterns t ctxt; val (u', ctxt'') = fix_dummy_patterns u ctxt'; in (t' $ u', ctxt'') end | fix_dummy_patterns a ctxt = (a, ctxt); (** export -- generalize type/term variables (beware of closure sizes) **) fun gen_all ctxt th = let val i = Thm.maxidx_thm th (maxidx_of ctxt) + 1; fun gen (x, T) = Thm.forall_elim (Thm.cterm_of ctxt (Var ((x, i), T))); in fold gen (Drule.outer_params (Thm.prop_of th)) th end; fun export_inst inner outer = let val declared_outer = is_declared outer; val still_fixed = not o is_newly_fixed inner outer; val gen_fixes = Names.build (fixes_of inner |> Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? Names.add_set y)); val type_occs_inner = type_occs_of inner; fun gen_fixesT ts = Names.build (fold decl_type_occs ts type_occs_inner |> Symtab.fold (fn (a, xs) => if declared_outer a orelse exists still_fixed xs then I else Names.add_set a)); in (gen_fixesT, gen_fixes) end; fun exportT_inst inner outer = #1 (export_inst inner outer); fun exportT_terms inner outer = let val mk_tfrees = exportT_inst inner outer; val maxidx = maxidx_of outer; in fn ts => ts |> map (Term_Subst.generalize (mk_tfrees ts, Names.empty) (fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1)) end; fun export_terms inner outer = let val (mk_tfrees, tfrees) = export_inst inner outer; val maxidx = maxidx_of outer; in fn ts => ts |> map (Term_Subst.generalize (mk_tfrees ts, tfrees) (fold Term.maxidx_term ts maxidx + 1)) end; fun export_prf inner outer prf = let val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer; val tfrees = mk_tfrees []; val maxidx = maxidx_of outer; val idx = Proofterm.maxidx_proof prf maxidx + 1; val gen_term = Term_Subst.generalize_same (tfrees, frees) idx; val gen_typ = Term_Subst.generalizeT_same tfrees idx; in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end; fun gen_export (mk_tfrees, frees) maxidx ths = let val tfrees = mk_tfrees (map Thm.full_prop_of ths); val idx = fold Thm.maxidx_thm ths maxidx + 1; in map (Thm.generalize (tfrees, frees) idx) ths end; fun exportT inner outer = gen_export (exportT_inst inner outer, Names.empty) (maxidx_of outer); fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer); fun export_morphism inner outer = let val fact = export inner outer; val term = singleton (export_terms inner outer); val typ = Logic.type_map term; in Morphism.transfer_morphism' inner $> Morphism.transfer_morphism' outer $> Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]} end; (** import -- fix schematic type/term variables **) fun invent_types Ss ctxt = let val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; in (tfrees, ctxt') end; fun importT_inst ts ctxt = let - val tvars = build_rev (fold Term.add_tvars ts); + val tvars = TVars.build (fold TVars.add_tvars ts) |> TVars.list_set; val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt; val instT = TVars.build (fold2 (fn a => fn b => TVars.add (a, TFree b)) tvars tfrees); in (instT, ctxt') end; fun import_inst is_open ts ctxt = let val ren = Name.clean #> (if is_open then I else Name.internal); val (instT, ctxt') = importT_inst ts ctxt; - val vars = map (apsnd (Term_Subst.instantiateT instT)) (build_rev (fold Term.add_vars ts)); + val vars = + Vars.build (fold Vars.add_vars ts) |> Vars.list_set + |> map (apsnd (Term_Subst.instantiateT instT)); val (ys, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt'; val inst = Vars.build (fold2 (fn (x, T) => fn y => Vars.add ((x, T), Free (y, T))) vars ys); in ((instT, inst), ctxt'') end; fun importT_terms ts ctxt = let val (instT, ctxt') = importT_inst ts ctxt in (map (Term_Subst.instantiate (instT, Vars.empty)) ts, ctxt') end; fun import_terms is_open ts ctxt = let val (inst, ctxt') = import_inst is_open ts ctxt in (map (Term_Subst.instantiate inst) ts, ctxt') end; fun importT ths ctxt = let val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT; val ths' = map (Thm.instantiate (TVars.dest instT', [])) ths; in ((instT', ths'), ctxt') end; fun import_prf is_open prf ctxt = let val ts = rev (Proofterm.fold_proof_terms_types cons (cons o Logic.mk_type) prf []); val (insts, ctxt') = import_inst is_open ts ctxt; in (Proofterm.instantiate insts prf, ctxt') end; fun import is_open ths ctxt = let val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT; val inst' = Vars.map (K (Thm.cterm_of ctxt')) inst; val ths' = map (Thm.instantiate (TVars.dest instT', Vars.dest inst')) ths; in (((instT', inst'), ths'), ctxt') end; fun import_vars ctxt th = let val ((_, [th']), _) = ctxt |> set_body false |> import true [th]; in th' end; (* import/export *) fun gen_trade imp exp f ctxt ths = let val ((_, ths'), ctxt') = imp ths ctxt in exp ctxt' ctxt (f ctxt' ths') end; val tradeT = gen_trade importT exportT; val trade = gen_trade (import true) export; (* focus on outermost parameters: \x y z. B *) val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false); val is_bound_focus = Config.apply bound_focus; val set_bound_focus = Config.put bound_focus; val restore_bound_focus = set_bound_focus o is_bound_focus; fun focus_params bindings t ctxt = let val ps = Term.variant_frees t (Term.strip_all_vars t); (*as they are printed :-*) val (xs, Ts) = split_list ps; val (xs', ctxt') = (case bindings of SOME bs => ctxt |> set_body true |> add_fixes_binding bs ||> restore_body ctxt | NONE => if is_bound_focus ctxt then bound_fixes ps ctxt else variant_fixes xs ctxt); val ps' = xs' ~~ Ts; val ctxt'' = ctxt' |> fold (declare_constraints o Free) ps'; in ((xs, ps'), ctxt'') end; fun focus bindings t ctxt = let val ((xs, ps), ctxt') = focus_params bindings t ctxt; val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t); in (((xs ~~ ps), t'), ctxt') end; fun forall_elim_prop t prop = Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t) |> Thm.cprop_of |> Thm.dest_arg; fun focus_cterm bindings goal ctxt = let val ((xs, ps), ctxt') = focus_params bindings (Thm.term_of goal) ctxt; val ps' = map (Thm.cterm_of ctxt' o Free) ps; val goal' = fold forall_elim_prop ps' goal; in ((xs ~~ ps', goal'), ctxt') end; fun focus_subgoal bindings i st = let val all_vars = Vars.build (Thm.fold_terms {hyps = false} Vars.add_vars st); in Vars.fold (unbind_term o #1 o #1) all_vars #> Vars.fold (declare_constraints o Var o #1) all_vars #> focus_cterm bindings (Thm.cprem_of st i) end; (** implicit polymorphism **) (* warn_extra_tfrees *) fun warn_extra_tfrees ctxt1 ctxt2 = let fun occs_typ a = Term.exists_subtype (fn TFree (b, _) => a = b | _ => false); fun occs_free a x = (case def_type ctxt1 false (x, ~1) of SOME T => if occs_typ a T then I else cons (a, x) | NONE => cons (a, x)); val occs1 = type_occs_of ctxt1; val occs2 = type_occs_of ctxt2; val extras = Symtab.fold (fn (a, xs) => if Symtab.defined occs1 a then I else fold (occs_free a) xs) occs2 []; val tfrees = map #1 extras |> sort_distinct string_ord; val frees = map #2 extras |> sort_distinct string_ord; in if null extras orelse not (Context_Position.is_visible ctxt2) then () else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^ space_implode " or " (map quote frees)) end; (* polymorphic terms *) fun polymorphic_types ctxt ts = let val ctxt' = fold declare_term ts ctxt; val occs = type_occs_of ctxt; val occs' = type_occs_of ctxt'; val types = Names.build (occs' |> Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else Names.add_set a)); val idx = maxidx_of ctxt' + 1; val Ts' = (fold o fold_types o fold_atyps) (fn T as TFree _ => (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I) | _ => I) ts []; val ts' = map (Term_Subst.generalize (types, Names.empty) idx) ts; in (rev Ts', ts') end; fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts); end;