# HG changeset patch # User wenzelm # Date 1303938268 -7200 # Node ID 9e1a77ad7ca37af5a071acc0950241376194a31d # Parent 89acb654d8eb2298d8193af9d3ce766f76dff8eb# Parent 65ec88b369fdf7b7f45e56b84c2a1f8cda5879f9 merged diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Nominal/nominal_induct.ML --- a/src/HOL/Nominal/nominal_induct.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/HOL/Nominal/nominal_induct.ML Wed Apr 27 23:04:28 2011 +0200 @@ -92,7 +92,7 @@ val finish_rule = split_all_tuples #> rename_params_rule true - (map (Name.clean o Proof_Context.revert_skolem defs_ctxt o fst) avoiding); + (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); fun rule_cases ctxt r = let val r' = if simp then Induct.simplified_rule ctxt r else r diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/HOL/Statespace/state_space.ML Wed Apr 27 23:04:28 2011 +0200 @@ -187,16 +187,11 @@ Symtab.lookup (StateSpaceData.get ctxt) name; -fun lookupI eq xs n = - (case AList.lookup eq xs n of - SOME v => v - | NONE => n); - fun mk_free ctxt name = if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name then - let val n' = lookupI (op =) (Variable.fixes_of ctxt) name - in SOME (Free (n',Proof_Context.infer_type ctxt (n', dummyT))) end + let val n' = Variable.intern_fixed ctxt name + in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end else NONE diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Function/context_tree.ML --- a/src/HOL/Tools/Function/context_tree.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/HOL/Tools/Function/context_tree.ML Wed Apr 27 23:04:28 2011 +0200 @@ -103,10 +103,10 @@ (* Called on the INSTANTIATED branches of the congruence rule *) fun mk_branch ctxt t = let - val ((fixes, impl), ctxt') = Function_Lib.focus_term t ctxt + val ((params, impl), ctxt') = Variable.focus t ctxt val (assms, concl) = Logic.strip_horn impl in - (ctxt', fixes, assms, rhs_of concl) + (ctxt', map #2 params, assms, rhs_of concl) end fun find_cong_rule ctxt fvar h ((r,dep)::rs) t = diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/HOL/Tools/Function/function_lib.ML Wed Apr 27 23:04:28 2011 +0200 @@ -9,7 +9,6 @@ sig val plural: string -> string -> 'a list -> string - val focus_term: term -> Proof.context -> ((string * typ) list * term) * Proof.context val dest_all_all: term -> term list * term val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list @@ -38,19 +37,6 @@ | plural sg pl _ = pl -(*term variant of Variable.focus*) -fun focus_term 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') = Variable.variant_fixes xs ctxt; - val ps' = xs' ~~ Ts; - val inst = map Free ps' - val t' = Term.subst_bounds (rev inst, Term.strip_all_body t); - val ctxt'' = ctxt' |> fold Variable.declare_constraints inst; - in ((ps', t'), ctxt'') end; - - (* Removes all quantifiers from a term, replacing bound variables by frees. *) fun dest_all_all (t as (Const ("all",_) $ _)) = let diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/HOL/Tools/Function/induction_schema.ML Wed Apr 27 23:04:28 2011 +0200 @@ -55,9 +55,9 @@ fun dest_hhf ctxt t = let - val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt + val ((params, imp), ctxt') = Variable.focus t ctxt in - (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp) + (ctxt', map #2 params, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp) end fun mk_scheme' ctxt cases concl = diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Wed Apr 27 23:04:28 2011 +0200 @@ -165,7 +165,7 @@ "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]); val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy; - val ((_, plain_eqn), _) = Function_Lib.focus_term eqn lthy; + val ((_, plain_eqn), _) = Variable.focus eqn lthy; val ((f_binding, fT), mixfix) = the_single fixes; val fname = Binding.name_of f_binding; diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 27 23:04:28 2011 +0200 @@ -1047,15 +1047,14 @@ end end -fun is_fixed_equation fixes +fun is_fixed_equation ctxt (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) = - member (op =) fixes s + Variable.is_fixed ctxt s | is_fixed_equation _ _ = false fun extract_fixed_frees ctxt (assms, t) = let - val fixes = Variable.fixes_of ctxt |> map snd val (subst, other_assms) = - List.partition (is_fixed_equation fixes) assms + List.partition (is_fixed_equation ctxt) assms |>> map Logic.dest_equals in (subst, other_assms, subst_atomic subst t) end diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Apr 27 23:04:28 2011 +0200 @@ -956,7 +956,7 @@ fun mk_insert x S = Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S fun mk_set_compr in_insert [] xs = - rev ((Free ("...", fastype_of t_compr)) :: + rev ((Free ("dots", fastype_of t_compr)) :: (* FIXME proper name!? *) (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs)) | mk_set_compr in_insert (t :: ts) xs = let diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Apr 27 23:04:28 2011 +0200 @@ -1902,7 +1902,7 @@ val ((T, ts), statistics) = eval ctxt stats param_user_modes comp_options k t_compr val setT = HOLogic.mk_setT T val elems = HOLogic.mk_set T ts - val cont = Free ("...", setT) + val cont = Free ("dots", setT) (* FIXME proper name!? *) (* check expected values *) val () = case raw_expected of diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Wed Apr 27 23:04:28 2011 +0200 @@ -51,7 +51,7 @@ fun sanity_test NONE _ = true | sanity_test (SOME bind) str = - if Variable.name bind = str then true + if Variable.check_name bind = str then true else error_msg bind str val _ = sanity_test optbind lhs_str diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/HOL/Tools/inductive.ML Wed Apr 27 23:04:28 2011 +0200 @@ -552,10 +552,10 @@ val ind_cases_setup = Method.setup @{binding ind_cases} (Scan.lift (Scan.repeat1 Args.name_source -- - Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >> + Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >> (fn (raw_props, fixes) => fn ctxt => let - val (_, ctxt') = Variable.add_fixes fixes ctxt; + val (_, ctxt') = Variable.add_fixes_binding fixes ctxt; val props = Syntax.read_props ctxt' raw_props; val ctxt'' = fold Variable.declare_term props ctxt'; val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props) diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/General/markup.ML Wed Apr 27 23:04:28 2011 +0200 @@ -36,7 +36,6 @@ val hiddenN: string val hidden: T val tclassN: string val tclass: string -> T val tyconN: string val tycon: string -> T - val fixed_declN: string val fixed_decl: string -> T val fixedN: string val fixed: string -> T val constN: string val const: string -> T val dynamic_factN: string val dynamic_fact: string -> T @@ -209,7 +208,6 @@ val (tclassN, tclass) = markup_string "tclass" nameN; val (tyconN, tycon) = markup_string "tycon" nameN; -val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN; val (fixedN, fixed) = markup_string "fixed" nameN; val (constN, const) = markup_string "constant" nameN; val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/General/markup.scala Wed Apr 27 23:04:28 2011 +0200 @@ -149,7 +149,6 @@ val TCLASS = "tclass" val TYCON = "tycon" - val FIXED_DECL = "fixed_decl" val FIXED = "fixed" val CONST = "constant" val DYNAMIC_FACT = "dynamic_fact" diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/General/name_space.ML Wed Apr 27 23:04:28 2011 +0200 @@ -16,6 +16,7 @@ val kind_of: T -> string val the_entry: T -> string -> {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial} + val entry_ord: T -> string * string -> order val markup: T -> string -> Markup.T val is_concealed: T -> string -> bool val intern: T -> xstring -> string @@ -125,9 +126,11 @@ NONE => error ("Unknown " ^ kind ^ " " ^ quote name) | SOME (_, entry) => entry); +fun entry_ord space = int_ord o pairself (#id o the_entry space); + fun markup (Name_Space {kind, entries, ...}) name = (case Symtab.lookup entries name of - NONE => Markup.malformed + NONE => Markup.hilite | SOME (_, entry) => entry_markup false kind (name, entry)); fun is_concealed space name = #concealed (the_entry space name); diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Isar/class_declaration.ML Wed Apr 27 23:04:28 2011 +0200 @@ -254,7 +254,7 @@ thy |> Sign.declare_const_global ((b, ty0), syn) |> snd - |> pair ((Variable.name b, ty), (c, ty')) + |> pair ((Variable.check_name b, ty), (c, ty')) end; in thy diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Isar/element.ML Wed Apr 27 23:04:28 2011 +0200 @@ -99,7 +99,7 @@ fun map_ctxt {binding, typ, term, pattern, fact, attrib} = fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx))) | Constrains xs => Constrains (xs |> map (fn (x, T) => - (Variable.name (binding (Binding.name x)), typ T))) + (Variable.check_name (binding (Binding.name x)), typ T))) | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps))))) | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => @@ -222,9 +222,9 @@ fun obtain prop ctxt = let val ((ps, prop'), ctxt') = Variable.focus prop ctxt; - fun fix (x, T) = (Binding.name (Proof_Context.revert_skolem ctxt' x), SOME T); - val xs = map (fix o Term.dest_Free o Thm.term_of o #2) ps; - val As = Logic.strip_imp_prems (Thm.term_of prop'); + fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T); + val xs = map (fix o #2) ps; + val As = Logic.strip_imp_prems prop'; in ((Binding.empty, (xs, As)), ctxt') end; in @@ -232,7 +232,6 @@ fun pretty_statement ctxt kind raw_th = let val thy = Proof_Context.theory_of ctxt; - val cert = Thm.cterm_of thy; val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th); val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt); @@ -242,7 +241,7 @@ val fixes = fold_aterms (fn v as Free (x, T) => if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term) - then insert (op =) (Proof_Context.revert_skolem ctxt' x, T) else I | _ => I) prop [] |> rev; + then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop [] |> rev; val (assumes, cases) = take_suffix (fn prem => is_elim andalso concl aconv Logic.strip_assums_concl prem) prems; in @@ -250,7 +249,7 @@ pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @ (if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])]) else - let val (clauses, ctxt'') = fold_map (obtain o cert) cases ctxt' + let val (clauses, ctxt'') = fold_map obtain cases ctxt' in pretty_stmt ctxt'' (Obtains clauses) end) end |> thm_name kind raw_th; @@ -526,7 +525,7 @@ fun activate raw_elem ctxt = let val elem = raw_elem |> map_ctxt - {binding = tap Variable.name, + {binding = tap Variable.check_name, typ = I, term = I, pattern = I, diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Isar/expression.ML Wed Apr 27 23:04:28 2011 +0200 @@ -128,7 +128,7 @@ val (implicit, expr') = params_expr expr; val implicit' = map #1 implicit; - val fixed' = map (Variable.name o #1) fixed; + val fixed' = map (Variable.check_name o #1) fixed; val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; val implicit'' = if strict then [] @@ -393,7 +393,7 @@ val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5); (* Retrieve parameter types *) - val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.name o #1) fixes) + val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.check_name o #1) fixes) | _ => fn ps => ps) (Fixes fors :: elems') []; val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6; val parms = xs ~~ Ts; (* params from expression and elements *) diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Isar/generic_target.ML Wed Apr 27 23:04:28 2011 +0200 @@ -67,12 +67,11 @@ val mx' = check_mixfix lthy (b, extra_tfrees) mx; val type_params = map (Logic.mk_type o TFree) extra_tfrees; + val target_ctxt = Local_Theory.target_of lthy; val term_params = - rev (Variable.fixes_of (Local_Theory.target_of lthy)) - |> map_filter (fn (_, x) => - (case AList.lookup (op =) xs x of - SOME T => SOME (Free (x, T)) - | NONE => NONE)); + filter (Variable.is_fixed target_ctxt o #1) xs + |> sort (Variable.fixed_ord target_ctxt o pairself #1) + |> map Free; val params = type_params @ term_params; val U = map Term.fastype_of params ---> T; diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed Apr 27 23:04:28 2011 +0200 @@ -632,7 +632,7 @@ val case_spec = (Parse.$$$ "(" |-- - Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") || + Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.binding) --| Parse.$$$ ")") || Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1; val _ = diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Isar/local_defs.ML Wed Apr 27 23:04:28 2011 +0200 @@ -8,7 +8,7 @@ sig val cert_def: Proof.context -> term -> (string * typ) * term val abs_def: term -> (string * typ) * term - val mk_def: Proof.context -> (string * term) list -> term list + val mk_def: Proof.context -> (binding * term) list -> term list val expand: cterm list -> thm -> thm val def_export: Assumption.export val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context -> @@ -59,7 +59,7 @@ let val (xs, rhss) = split_list args; val (bind, _) = Proof_Context.bind_fixes xs ctxt; - val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args; + val lhss = map (fn (x, rhs) => bind (Free (Binding.name_of x, Term.fastype_of rhs))) args; in map Logic.mk_equals (lhss ~~ rhss) end; @@ -90,15 +90,14 @@ fun add_defs defs ctxt = let - val ((bvars, mxs), specs) = defs |> split_list |>> split_list; + val ((xs, mxs), specs) = defs |> split_list |>> split_list; val ((bfacts, atts), rhss) = specs |> split_list |>> split_list; - val xs = map Variable.name bvars; - val names = map2 Thm.def_binding_optional bvars bfacts; + val names = map2 Thm.def_binding_optional xs bfacts; val eqs = mk_def ctxt (xs ~~ rhss); val lhss = map (fst o Logic.dest_equals) eqs; in ctxt - |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2 + |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2 |> fold Variable.declare_term eqs |> Proof_Context.add_assms_i def_export (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs) diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Isar/obtain.ML Wed Apr 27 23:04:28 2011 +0200 @@ -99,7 +99,7 @@ fun bind_judgment ctxt name = let - val (bind, ctxt') = Proof_Context.bind_fixes [name] ctxt; + val (bind, ctxt') = Proof_Context.bind_fixes [Binding.name name] ctxt; val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) name); in ((v, t), ctxt') end; @@ -118,25 +118,23 @@ (*obtain vars*) val (vars, vars_ctxt) = prep_vars raw_vars ctxt; - val (_, fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars; - val xs = map (Variable.name o #1) vars; + val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars; + val xs = map (Variable.check_name o #1) vars; (*obtain asms*) val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); val asm_props = maps (map fst) proppss; val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss; - val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt; + (*obtain parms*) + val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt; + val parms = xs' ~~ Ts; + val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt; (*obtain statements*) val thesisN = Name.variant xs Auto_Bind.thesisN; val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN); - val asm_frees = fold Term.add_frees asm_props []; - val parms = xs |> map (fn x => - let val x' = Proof_Context.get_skolem fix_ctxt x - in (x', the_default propT (AList.lookup (op =) asm_frees x')) end); - val that_name = if name = "" then thatN else name; val that_prop = Term.list_all_free (parms, Logic.list_implies (asm_props, thesis)) @@ -198,7 +196,7 @@ val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule; val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt; val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule'; - val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt'; + val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt'; val (prems, ctxt'') = Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params)) (Drule.strip_imp_prems stmt) fix_ctxt; @@ -257,7 +255,7 @@ fun inferred_type (binding, _, mx) ctxt = let - val x = Variable.name binding; + val x = Variable.check_name binding; val (T, ctxt') = Proof_Context.inferred_param x ctxt in ((x, T, mx), ctxt') end; @@ -280,7 +278,7 @@ let val ((parms, rule), ctxt') = unify_params vars thesis_var raw_rule (Proof.context_of state'); - val (bind, _) = Proof_Context.bind_fixes (map (#1 o #1) parms) ctxt'; + val (bind, _) = Proof_Context.bind_fixes (map (Binding.name o #1 o #1) parms) ctxt'; val ts = map (bind o Free o #1) parms; val ps = map dest_Free ts; val asms = diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Isar/proof.ML Wed Apr 27 23:04:28 2011 +0200 @@ -71,8 +71,8 @@ val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state val unfolding: ((thm list * attribute list) list) list -> state -> state val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state - val invoke_case: string * string option list * attribute list -> state -> state - val invoke_case_cmd: string * string option list * Attrib.src list -> state -> state + val invoke_case: string * binding option list * attribute list -> state -> state + val invoke_case_cmd: string * binding option list * Attrib.src list -> state -> state val begin_block: state -> state val next_block: state -> state val end_block: state -> state diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Apr 27 23:04:28 2011 +0200 @@ -63,8 +63,6 @@ val cert_typ: Proof.context -> typ -> typ val cert_typ_syntax: Proof.context -> typ -> typ val cert_typ_abbrev: Proof.context -> typ -> typ - val get_skolem: Proof.context -> string -> string - val revert_skolem: Proof.context -> string -> string val infer_type: Proof.context -> string * typ -> typ val inferred_param: string -> Proof.context -> typ * Proof.context val inferred_fixes: Proof.context -> (string * typ) list * Proof.context @@ -127,7 +125,7 @@ val add_fixes: (binding * typ option * mixfix) list -> Proof.context -> string list * Proof.context val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a) - val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context + val bind_fixes: binding list -> Proof.context -> (term -> term) * Proof.context val add_assms: Assumption.export -> (Thm.binding * (string * string list) list) list -> Proof.context -> (string * thm list) list * Proof.context @@ -136,7 +134,7 @@ Proof.context -> (string * thm list) list * Proof.context val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context - val get_case: Proof.context -> string -> string option list -> Rule_Cases.T + val get_case: Proof.context -> string -> binding option list -> Rule_Cases.T val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context val target_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism -> @@ -408,10 +406,7 @@ (** prepare variables **) -(* internalize Skolem constants *) - -val lookup_skolem = AList.lookup (op =) o Variable.fixes_of; -fun get_skolem ctxt x = the_default x (lookup_skolem ctxt x); +(* check Skolem constants *) fun no_skolem internal x = if can Name.dest_skolem x then @@ -421,14 +416,6 @@ else x; -(* revert Skolem constants -- if possible *) - -fun revert_skolem ctxt x = - (case find_first (fn (_, y) => y = x) (Variable.fixes_of ctxt) of - SOME (x', _) => if lookup_skolem ctxt x' = SOME x then x' else x - | NONE => x); - - (** prepare terms and propositions **) @@ -443,7 +430,7 @@ fun inferred_fixes ctxt = let - val xs = rev (map #2 (Variable.fixes_of ctxt)); + val xs = map #2 (Variable.dest_fixes ctxt); val (Ts, ctxt') = fold_map inferred_param xs ctxt; in (xs ~~ Ts, ctxt') end; @@ -508,7 +495,7 @@ val (c, pos) = token_content text; val _ = no_skolem false c; in - (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of + (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of (SOME x, false) => (Context_Position.report ctxt pos (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free)); @@ -524,7 +511,7 @@ fun intern_skolem ctxt x = let val _ = no_skolem false x; - val sko = lookup_skolem ctxt x; + val sko = Variable.lookup_fixed ctxt x; val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x; val is_declared = is_some (Variable.def_type ctxt false (x, ~1)); in @@ -941,7 +928,7 @@ fun prep_vars prep_typ internal = fold_map (fn (b, raw_T, mx) => fn ctxt => let - val x = Variable.name b; + val x = Variable.check_name b; val _ = Lexicon.is_identifier (no_skolem internal x) orelse error ("Illegal variable name: " ^ Binding.print b); @@ -1040,15 +1027,16 @@ fun add_fixes raw_vars ctxt = let - val (vars, _) = cert_vars raw_vars ctxt; - val (xs', ctxt') = Variable.add_fixes (map (Variable.name o #1) vars) ctxt; - val ctxt'' = - ctxt' - |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars) - |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed)); - val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') => - Context_Position.report ctxt (Binding.pos_of b) (Markup.fixed_decl x')); - in (xs', ctxt'') end; + val thy = theory_of ctxt; + val vars = #1 (cert_vars raw_vars ctxt); + in + ctxt + |> Variable.add_fixes_binding (map #1 vars) + |-> (fn xs => + fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars) + #-> (map_syntax o Local_Syntax.add_syntax thy o map (pair Local_Syntax.Fixed)) + #> pair xs) + end; (* fixes vs. frees *) @@ -1056,12 +1044,13 @@ fun auto_fixes (ctxt, (propss, x)) = ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x)); -fun bind_fixes xs ctxt = +fun bind_fixes bs ctxt = let - val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs); + val (_, ctxt') = ctxt |> add_fixes (map (fn b => (b, NONE, NoSyn)) bs); + val xs = map Binding.name_of bs; fun bind (t as Free (x, T)) = if member (op =) xs x then - (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t) + (case Variable.lookup_fixed ctxt' x of SOME x' => Free (x', T) | NONE => t) else t | bind (t $ u) = bind t $ bind u | bind (Abs (x, T, t)) = Abs (x, T, bind t) @@ -1123,7 +1112,7 @@ fun fix (x, T) ctxt = let val (bind, ctxt') = bind_fixes [x] ctxt; - val t = bind (Free (x, T)); + val t = bind (Free (Binding.name_of x, T)); in (t, ctxt' |> Variable.declare_constraints t) end; in @@ -1233,7 +1222,7 @@ in Pretty.block (Pretty.fbreaks (Pretty.str (name ^ ":") :: - prt_sect "fix" [] (Pretty.str o fst) fixes @ + prt_sect "fix" [] (Pretty.str o Binding.name_of o fst) fixes @ prt_sect "let" [Pretty.str "and"] prt_let (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @ (if forall (null o #2) asms then [] @@ -1282,8 +1271,8 @@ if x = x' then Pretty.str x else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')]; val fixes = - rev (filter_out ((can Name.dest_internal orf member (op =) structs) o #1) - (Variable.fixes_of ctxt)); + filter_out ((can Name.dest_internal orf member (op =) structs) o #1) + (Variable.dest_fixes ctxt); val prt_fixes = if null fixes then [] else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 :: diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Isar/rule_cases.ML Wed Apr 27 23:04:28 2011 +0200 @@ -20,7 +20,7 @@ sig include BASIC_RULE_CASES datatype T = Case of - {fixes: (string * typ) list, + {fixes: (binding * typ) list, assumes: (string * term list) list, binds: (indexname * term option) list, cases: (string * T) list} @@ -56,7 +56,7 @@ (** cases **) datatype T = Case of - {fixes: (string * typ) list, + {fixes: (binding * typ) list, assumes: (string * term list) list, binds: (indexname * term option) list, cases: (string * T) list}; @@ -93,6 +93,8 @@ chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop) in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end; +fun bindings args = map (apfst Binding.name) args; + fun extract_case thy (case_outline, raw_prop) name concls = let val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop); @@ -122,11 +124,12 @@ val cases = map extract props; fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) = - Case {fixes = fixes1 @ fixes2, assumes = assumes1 @ assumes2, binds = binds, cases = []}; + Case {fixes = bindings (fixes1 @ fixes2), + assumes = assumes1 @ assumes2, binds = binds, cases = []}; fun inner_case (_, ((fixes2, assumes2), binds)) = - Case {fixes = fixes2, assumes = assumes2, binds = binds, cases = []}; + Case {fixes = bindings fixes2, assumes = assumes2, binds = binds, cases = []}; fun nested_case ((fixes1, assumes1), _) = - Case {fixes = fixes1, assumes = assumes1, binds = [], + Case {fixes = bindings fixes1, assumes = assumes1, binds = [], cases = map string_of_int (1 upto len) ~~ map inner_case cases}; in if len = 0 then NONE diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Isar/specification.ML Wed Apr 27 23:04:28 2011 +0200 @@ -169,7 +169,7 @@ fun gen_axioms do_print prep raw_vars raw_specs thy = let val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy); - val xs = map (fn ((b, T), _) => (Variable.name b, T)) vars; + val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) vars; (*consts*) val (consts, consts_thy) = thy |> fold_map Theory.specify_const vars; @@ -179,7 +179,7 @@ val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) => fold_map Thm.add_axiom_global (map (apfst (fn a => Binding.map_name (K a) b)) - (Global_Theory.name_multi (Variable.name b) (map subst props))) + (Global_Theory.name_multi (Variable.check_name b) (map subst props))) #>> (fn ths => ((b, atts), [(map #2 ths, [])]))); (*facts*) @@ -211,7 +211,7 @@ [] => (Binding.name x, NoSyn) | [((b, _), mx)] => let - val y = Variable.name b; + val y = Variable.check_name b; val _ = x = y orelse error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ Position.str_of (Binding.pos_of b)); @@ -250,7 +250,7 @@ [] => (Binding.name x, NoSyn) | [((b, _), mx)] => let - val y = Variable.name b; + val y = Variable.check_name b; val _ = x = y orelse error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^ Position.str_of (Binding.pos_of b)); @@ -320,10 +320,10 @@ | Element.Obtains obtains => let val case_names = obtains |> map_index (fn (i, (b, _)) => - if Binding.is_empty b then string_of_int (i + 1) else Variable.name b); + if Binding.is_empty b then string_of_int (i + 1) else Variable.check_name b); val constraints = obtains |> map (fn (_, (vars, _)) => Element.Constrains - (vars |> map_filter (fn (x, SOME T) => SOME (Variable.name x, T) | _ => NONE))); + (vars |> map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T) | _ => NONE))); val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props); val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt; @@ -333,7 +333,7 @@ fun assume_case ((name, (vars, _)), asms) ctxt' = let val bs = map fst vars; - val xs = map Variable.name bs; + val xs = map Variable.check_name bs; val props = map fst asms; val (Ts, _) = ctxt' |> fold Variable.declare_term props diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Apr 27 23:04:28 2011 +0200 @@ -31,8 +31,9 @@ fun markup_free ctxt x = [if can Name.dest_skolem x then Markup.skolem else Markup.free] @ - (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] - else [Markup.hilite]); + (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x + then [Variable.markup_fixed ctxt x] + else []); fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var]; @@ -592,7 +593,7 @@ else Markup.hilite; in if can Name.dest_skolem x - then ([m, Markup.skolem], Proof_Context.revert_skolem ctxt x) + then ([m, Markup.skolem], Variable.revert_fixed ctxt x) else ([m, Markup.free], x) end; diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/conv.ML --- a/src/Pure/conv.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/conv.ML Wed Apr 27 23:04:28 2011 +0200 @@ -93,7 +93,7 @@ (case Thm.term_of ct of Abs (x, _, _) => let - val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt; + val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt; val (v, ct') = Thm.dest_abs (SOME u) ct; val eq = cv (v, ctxt') ct'; in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/goal.ML --- a/src/Pure/goal.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/goal.ML Wed Apr 27 23:04:28 2011 +0200 @@ -326,7 +326,7 @@ fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) => let - val ((_, goal'), ctxt') = Variable.focus goal ctxt; + val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt; val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); val tacs = Rs |> map (fn R => diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/subgoal.ML --- a/src/Pure/subgoal.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/subgoal.ML Wed Apr 27 23:04:28 2011 +0200 @@ -33,7 +33,7 @@ let val st = Simplifier.norm_hhf_protect raw_st; val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt; - val ((params, goal), ctxt2) = Variable.focus (Thm.cprem_of st' i) ctxt1; + val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1; val (asms, concl) = if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal) diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Pure/variable.ML --- a/src/Pure/variable.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Pure/variable.ML Wed Apr 27 23:04:28 2011 +0200 @@ -10,15 +10,12 @@ val set_body: bool -> Proof.context -> Proof.context val restore_body: Proof.context -> Proof.context -> Proof.context val names_of: Proof.context -> Name.context - val fixes_of: Proof.context -> (string * string) list val binds_of: Proof.context -> (typ * term) Vartab.table val maxidx_of: Proof.context -> int val sorts_of: Proof.context -> sort list val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table val is_declared: Proof.context -> string -> bool - val is_fixed: Proof.context -> string -> bool - val newly_fixed: Proof.context -> Proof.context -> string -> bool - val name: binding -> string + 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 @@ -35,14 +32,23 @@ 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 is_fixed: Proof.context -> string -> bool + val newly_fixed: Proof.context -> Proof.context -> string -> bool + val fixed_ord: Proof.context -> string * string -> order + val intern_fixed: Proof.context -> string -> string + val markup_fixed: Proof.context -> string -> Markup.T + val lookup_fixed: Proof.context -> string -> string option + val revert_fixed: Proof.context -> string -> string 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_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 auto_fixes: term -> Proof.context -> Proof.context val variant_fixes: string list -> Proof.context -> string list * Proof.context + val dest_fixes: Proof.context -> (string * string) list val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context val export_terms: Proof.context -> Proof.context -> term list -> term list val exportT_terms: Proof.context -> Proof.context -> term list -> term list @@ -61,7 +67,8 @@ (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context 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 focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context + val focus: term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context + val focus_cterm: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context val focus_subgoal: 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 @@ -73,11 +80,14 @@ (** local context data **) +type fixes = string Name_Space.table; +val empty_fixes: fixes = Name_Space.empty_table "fixed variable"; + datatype data = Data of {is_body: bool, (*inner body mode*) names: Name.context, (*type/term variable names*) consts: string Symtab.table, (*consts within the local scope*) - fixes: (string * string) list, (*term fixes -- extern/intern*) + 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*) @@ -94,8 +104,8 @@ ( type T = data; fun init _ = - make_data (false, Name.context, Symtab.empty, [], Vartab.empty, Symtab.empty, - ~1, [], (Vartab.empty, Vartab.empty)); + make_data (false, Name.context, Symtab.empty, empty_fixes, Vartab.empty, + Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); ); fun map_data f = @@ -146,6 +156,7 @@ val names_of = #names o rep_data; val fixes_of = #fixes o rep_data; +val fixes_space = #1 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; @@ -153,11 +164,8 @@ val constraints_of = #constraints o rep_data; val is_declared = Name.is_declared o names_of; -fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt); -fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x); -(*checked name binding*) -val name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming; +val check_name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming; @@ -281,6 +289,29 @@ (** fixes **) +(* specialized name space *) + +fun is_fixed ctxt x = can (Name_Space.the_entry (fixes_space ctxt)) x; +fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x); + +val fixed_ord = Name_Space.entry_ord o fixes_space; +val intern_fixed = Name_Space.intern o fixes_space; +val markup_fixed = Name_Space.markup 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 Symtab.lookup (#2 (fixes_of ctxt)) x of + SOME x' => if intern_fixed ctxt x' = x then x' else x + | NONE => x); + +fun dest_fixes ctxt = + let val (space, tab) = fixes_of ctxt + in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end; + + (* collect variables *) fun add_free_names ctxt = @@ -300,41 +331,54 @@ local -fun no_dups [] = () - | no_dups dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups); +fun err_dups dups = + error ("Duplicate fixed variable(s): " ^ commas (map Binding.print dups)); -fun new_fixes names' xs xs' = +fun new_fixed ((x, x'), pos) ctxt = + if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)] + else + ctxt + |> map_fixes + (Name_Space.define ctxt true Name_Space.default_naming (Binding.make (x', pos), x) #> snd #>> + Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x') + |> declare_fixed x + |> declare_constraints (Syntax.free x'); + +fun new_fixes names' xs xs' ps = map_names (K names') #> - fold declare_fixed xs #> - map_fixes (fn fixes => (rev (xs ~~ xs') @ fixes)) #> - fold (declare_constraints o Syntax.free) xs' #> + fold new_fixed ((xs ~~ xs') ~~ ps) #> pair xs'; in -fun add_fixes xs ctxt = +fun add_fixes_binding bs ctxt = let val _ = - (case filter (can Name.dest_skolem) xs of [] => () - | bads => error ("Illegal internal Skolem constant(s): " ^ commas_quote bads)); - val _ = no_dups (duplicates (op =) xs); - val (ys, zs) = split_list (fixes_of ctxt); + (case filter (can Name.dest_skolem o Binding.name_of) bs of + [] => () + | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads))); + val _ = + (case duplicates (op = o pairself 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 Name.variants xs names |>> map Name.skolem - else (no_dups (inter (op =) xs ys); no_dups (inter (op =) xs zs); - (xs, fold Name.declare xs names)); - in ctxt |> new_fixes names' xs xs' end; + else (xs, fold Name.declare xs names); + in ctxt |> new_fixes names' xs xs' (map Binding.pos_of bs) end; fun variant_fixes raw_xs ctxt = let val names = names_of ctxt; val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs; val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem); - in ctxt |> new_fixes names' xs xs' end; + in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end; end; +val add_fixes = add_fixes_binding o map Binding.name; fun add_fixes_direct xs ctxt = ctxt |> set_body false @@ -358,10 +402,10 @@ fun export_inst inner outer = let val declared_outer = is_declared outer; - val fixes_inner = fixes_of inner; - val fixes_outer = fixes_of outer; - val gen_fixes = map #2 (take (length fixes_inner - length fixes_outer) fixes_inner); + val gen_fixes = + Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y) + (#2 (fixes_of inner)) []; val still_fixed = not o member (op =) gen_fixes; val type_occs_inner = type_occs_of inner; @@ -473,23 +517,34 @@ val trade = gen_trade (import true) export; -(* focus on outermost parameters *) +(* focus on outermost parameters: !!x y z. B *) + +fun focus_params t ctxt = + let + val (xs, Ts) = + split_list (Term.variant_frees t (Term.strip_all_vars t)); (*as they are printed :-*) + val (xs', ctxt') = variant_fixes xs ctxt; + val ps = xs' ~~ Ts; + val ctxt'' = ctxt' |> fold (declare_constraints o Free) ps; + in ((xs, ps), ctxt'') end; + +fun focus t ctxt = + let + val ((xs, ps), ctxt') = focus_params 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.capply (Thm.dest_arg prop) t) |> Thm.cprop_of |> Thm.dest_arg; -fun focus goal ctxt = +fun focus_cterm goal ctxt = let val cert = Thm.cterm_of (Thm.theory_of_cterm goal); - val t = Thm.term_of goal; - val ps = Term.variant_frees t (Term.strip_all_vars t); (*as they are printed :-*) - val (xs, Ts) = split_list ps; - val (xs', ctxt') = variant_fixes xs ctxt; - val ps' = ListPair.map (cert o Free) (xs', Ts); + val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt; + val ps' = map (cert o Free) ps; val goal' = fold forall_elim_prop ps' goal; - val ctxt'' = ctxt' |> fold (declare_constraints o Thm.term_of) ps'; - in ((xs ~~ ps', goal'), ctxt'') end; + in ((xs ~~ ps', goal'), ctxt') end; fun focus_subgoal i st = let @@ -498,7 +553,7 @@ in fold bind_term no_binds #> fold (declare_constraints o Var) all_vars #> - focus (Thm.cprem_of st i) + focus_cterm (Thm.cprem_of st i) end; diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Tools/coherent.ML --- a/src/Tools/coherent.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Tools/coherent.ML Wed Apr 27 23:04:28 2011 +0200 @@ -213,7 +213,7 @@ SUBPROOF (fn {prems = prems', concl, context, ...} => let val xs = map (term_of o #2) params @ map (fn (_, s) => Free (s, the (Variable.default_type context s))) - (Variable.fixes_of context) + (rev (Variable.dest_fixes context)) (* FIXME !? *) in case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl) (mk_dom xs) Net.empty 0 0 of diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Tools/induct.ML --- a/src/Tools/induct.ML Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Tools/induct.ML Wed Apr 27 23:04:28 2011 +0200 @@ -599,7 +599,7 @@ fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] = let - val x = Name.clean (Proof_Context.revert_skolem ctxt z); + val x = Name.clean (Variable.revert_fixed ctxt z); fun index i [] = [] | index i (y :: ys) = if x = y then x ^ string_of_int i :: index (i + 1) ys @@ -646,7 +646,7 @@ val v = Free (x, T); fun spec_rule prfx (xs, body) = @{thm Pure.meta_spec} - |> Thm.rename_params_rule ([Name.clean (Proof_Context.revert_skolem ctxt x)], 1) + |> Thm.rename_params_rule ([Name.clean (Variable.revert_fixed ctxt x)], 1) |> Thm.lift_rule (cert prfx) |> `(Thm.prop_of #> Logic.strip_assums_concl) |-> (fn pred $ arg => diff -r 89acb654d8eb -r 9e1a77ad7ca3 src/Tools/jEdit/src/jedit/isabelle_markup.scala --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Apr 27 21:17:47 2011 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Apr 27 23:04:28 2011 +0200 @@ -152,7 +152,6 @@ // logical entities Markup.TCLASS -> NULL, Markup.TYCON -> NULL, - Markup.FIXED_DECL -> FUNCTION, Markup.FIXED -> NULL, Markup.CONST -> LITERAL2, Markup.DYNAMIC_FACT -> LABEL,