--- a/src/HOL/Nominal/nominal_induct.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Thu Apr 28 09:32: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
--- a/src/HOL/Statespace/state_space.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu Apr 28 09:32: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
--- a/src/HOL/Tools/Function/context_tree.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML Thu Apr 28 09:32: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 =
--- a/src/HOL/Tools/Function/function_lib.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Thu Apr 28 09:32: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
@@ -18,7 +17,6 @@
val unordered_pairs: 'a list -> ('a * 'a) list
- val replace_frees: (string * term) list -> term -> term
val rename_bound: string -> term -> term
val mk_forall_rename: (string * term) -> term -> term
val forall_intr_rename: (string * cterm) -> thm -> thm
@@ -39,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
@@ -78,11 +63,7 @@
| unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
-(* Replaces Frees by name. Works with loose Bounds. *)
-fun replace_frees assoc =
- map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
- | t => t)
-
+(* renaming bound variables *)
fun rename_bound n (Q $ Abs (_, T, b)) = (Q $ Abs (n, T, b))
| rename_bound n _ = raise Match
--- a/src/HOL/Tools/Function/induction_schema.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Thu Apr 28 09:32: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 =
--- a/src/HOL/Tools/Function/mutual.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Thu Apr 28 09:32:28 2011 +0200
@@ -114,10 +114,11 @@
fun convert_eqs (f, qs, gs, args, rhs) =
let
val MutualPart {i, i', ...} = get_part f parts
+ val rhs' = rhs
+ |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t)
in
(qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
- SumTree.mk_inj RST n' i' (replace_frees rews rhs)
- |> Envir.beta_norm)
+ Envir.beta_norm (SumTree.mk_inj RST n' i' rhs'))
end
val qglrs = map convert_eqs fqgars
--- a/src/HOL/Tools/Function/partial_function.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Thu Apr 28 09:32: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;
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Apr 28 09:32: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
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Apr 28 09:32: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
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Apr 28 09:32: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
--- a/src/HOL/Tools/Quotient/quotient_def.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Apr 28 09:32: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
--- a/src/HOL/Tools/inductive.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/HOL/Tools/inductive.ML Thu Apr 28 09:32: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)
--- a/src/Pure/General/markup.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/General/markup.ML Thu Apr 28 09:32: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;
--- a/src/Pure/General/markup.scala Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/General/markup.scala Thu Apr 28 09:32: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"
--- a/src/Pure/General/name_space.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/General/name_space.ML Thu Apr 28 09:32: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);
--- a/src/Pure/Isar/class_declaration.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Isar/class_declaration.ML Thu Apr 28 09:32: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
--- a/src/Pure/Isar/element.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Isar/element.ML Thu Apr 28 09:32: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,
--- a/src/Pure/Isar/expression.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Isar/expression.ML Thu Apr 28 09:32: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 *)
--- a/src/Pure/Isar/generic_target.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML Thu Apr 28 09:32: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;
--- a/src/Pure/Isar/isar_syn.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Apr 28 09:32: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 _ =
--- a/src/Pure/Isar/local_defs.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Isar/local_defs.ML Thu Apr 28 09:32: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)
--- a/src/Pure/Isar/obtain.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Isar/obtain.ML Thu Apr 28 09:32: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 =
--- a/src/Pure/Isar/proof.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Isar/proof.ML Thu Apr 28 09:32: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
--- a/src/Pure/Isar/proof_context.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Apr 28 09:32: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 ::
--- a/src/Pure/Isar/rule_cases.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Isar/rule_cases.ML Thu Apr 28 09:32: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
--- a/src/Pure/Isar/specification.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Isar/specification.ML Thu Apr 28 09:32: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
--- a/src/Pure/Syntax/syntax_phases.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Thu Apr 28 09:32: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;
--- a/src/Pure/conv.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/conv.ML Thu Apr 28 09:32: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
--- a/src/Pure/goal.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/goal.ML Thu Apr 28 09:32: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 =>
--- a/src/Pure/subgoal.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/subgoal.ML Thu Apr 28 09:32: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)
--- a/src/Pure/variable.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Pure/variable.ML Thu Apr 28 09:32: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;
--- a/src/Tools/coherent.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Tools/coherent.ML Thu Apr 28 09:32: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
--- a/src/Tools/induct.ML Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Tools/induct.ML Thu Apr 28 09:32: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 =>
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Apr 27 19:27:06 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Thu Apr 28 09:32: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,