--- a/src/HOL/FunDef.thy Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/FunDef.thy Thu Mar 12 22:16:25 2009 +0100
@@ -314,13 +314,11 @@
use "Tools/function_package/scnp_reconstruct.ML"
setup {* ScnpReconstruct.setup *}
-(*
-setup {*
+
+ML_val -- "setup inactive"
+{*
Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp
[ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
*}
-*)
-
-
end
--- a/src/HOL/Import/shuffler.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Import/shuffler.ML Thu Mar 12 22:16:25 2009 +0100
@@ -662,7 +662,7 @@
fun search_meth ctxt =
let
val thy = ProofContext.theory_of ctxt
- val prems = Assumption.prems_of ctxt
+ val prems = Assumption.all_prems_of ctxt
in
Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
end
--- a/src/HOL/Nominal/nominal_primrec.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Nominal/nominal_primrec.ML Thu Mar 12 22:16:25 2009 +0100
@@ -12,6 +12,10 @@
(binding * typ option * mixfix) list ->
(binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> local_theory -> Proof.state
+ val add_primrec_cmd: string list option -> string option ->
+ (binding * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
+ (Attrib.binding * string) list -> local_theory -> Proof.state
end;
structure NominalPrimrec : NOMINAL_PRIMREC =
@@ -36,10 +40,10 @@
(fn Free (v, _) => insert (op =) v | _ => I) body []))
in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
-fun process_eqn lthy is_fixed spec rec_fns =
+fun process_eqn lthy is_fixed spec rec_fns =
let
val eq = unquantify spec;
- val (lhs, rhs) =
+ val (lhs, rhs) =
HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))
handle TERM _ => raise RecError "not a proper equation";
@@ -67,7 +71,7 @@
fun check_vars _ [] = ()
| check_vars s vars = raise RecError (s ^ commas_quote (map fst vars))
in
- if length middle > 1 then
+ if length middle > 1 then
raise RecError "more than one non-variable in pattern"
else
(check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
@@ -159,7 +163,7 @@
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
(Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle RecError s => primrec_eq_err lthy s eq
- in (fnames'', fnss'',
+ in (fnames'', fnss'',
(list_abs_free (cargs' @ subs, rhs'))::fns)
end)
@@ -172,7 +176,7 @@
val SOME (_, _, eqns' as (_, (ls, _, rs, _, _)) :: _) =
AList.lookup (op =) eqns fname;
val (fnames', fnss', fns) = fold_rev (trans eqns') constrs
- ((i, fname)::fnames, fnss, [])
+ ((i, fname)::fnames, fnss, [])
in
(fnames', (i, (fname, ls, rs, fns))::fnss')
end
@@ -235,15 +239,9 @@
local
-fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
- let
- val ((fixes, spec), _) = prep_spec
- raw_fixes (map (single o apsnd single) raw_spec) ctxt
- in (fixes, map (apsnd the_single) spec) end;
-
fun gen_primrec set_group prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
let
- val (fixes', spec) = prepare_spec prep_spec lthy (raw_fixes @ raw_params) raw_spec;
+ val (fixes', spec) = fst (prep_spec (raw_fixes @ raw_params) raw_spec lthy);
val fixes = List.take (fixes', length raw_fixes);
val (names_atts, spec') = split_list spec;
val eqns' = map unquantify spec'
@@ -261,12 +259,12 @@
then () else primrec_err param_err);
val tnames = distinct (op =) (map (#1 o snd) eqns);
val dts = find_dts dt_info tnames tnames;
- val main_fns =
+ val main_fns =
map (fn (tname, {index, ...}) =>
- (index,
+ (index,
(fst o the o find_first (fn (_, x) => #1 x = tname)) eqns))
dts;
- val {descr, rec_names, rec_rewrites, ...} =
+ val {descr, rec_names, rec_rewrites, ...} =
if null dts then
primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
else snd (hd dts);
@@ -388,15 +386,15 @@
in
-val add_primrec = gen_primrec false Specification.check_specification (K I);
-val add_primrec_cmd = gen_primrec true Specification.read_specification Syntax.read_term;
+val add_primrec = gen_primrec false Specification.check_spec (K I);
+val add_primrec_cmd = gen_primrec true Specification.read_spec Syntax.read_term;
end;
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = OuterParse in
val freshness_context = P.reserved "freshness_context";
val invariant = P.reserved "invariant";
@@ -408,28 +406,16 @@
(Scan.repeat1 (unless_flag P.term) >> SOME) -- Scan.optional parser1 NONE ||
(parser1 >> pair NONE);
val options =
- Scan.optional (P.$$$ "(" |-- P.!!!
- (parser2 --| P.$$$ ")")) (NONE, NONE);
-
-fun pipe_error t = P.!!! (Scan.fail_with (K
- (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
-
-val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
- ((P.term :-- pipe_error) || Scan.succeed ("",""));
-
-val statements = P.enum1 "|" statement;
-
-val primrec_decl = P.opt_target -- options --
- P.fixes -- P.for_fixes --| P.$$$ "where" -- statements;
+ Scan.optional (P.$$$ "(" |-- P.!!! (parser2 --| P.$$$ ")")) (NONE, NONE);
val _ =
- OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
- (primrec_decl >> (fn ((((opt_target, (invs, fctxt)), raw_fixes), raw_params), raw_spec) =>
- Toplevel.print o Toplevel.local_theory_to_proof opt_target
- (add_primrec_cmd invs fctxt raw_fixes raw_params raw_spec)));
+ OuterSyntax.local_theory_to_proof "nominal_primrec"
+ "define primitive recursive functions on nominal datatypes" OuterKeyword.thy_goal
+ (options -- P.fixes -- P.for_fixes -- SpecParse.where_alt_specs
+ >> (fn ((((invs, fctxt), fixes), params), specs) =>
+ add_primrec_cmd invs fctxt fixes params specs));
end;
-
end;
--- a/src/HOL/Statespace/state_space.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Statespace/state_space.ML Thu Mar 12 22:16:25 2009 +0100
@@ -419,7 +419,7 @@
val expr = ([(suffix valuetypesN name,
(("",false),Expression.Positional (map SOME pars)))],[]);
in
- prove_interpretation_in (ALLGOALS o solve_tac o Assumption.prems_of)
+ prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of)
(suffix valuetypesN name, expr) thy
end;
--- a/src/HOL/Tools/function_package/fundef_common.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_common.ML Thu Mar 12 22:16:25 2009 +0100
@@ -359,7 +359,7 @@
>> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
in
fun fundef_parser default_cfg =
- config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements
+ config_parser default_cfg -- P.fixes --| P.where_ -- flags_statements
end
--- a/src/HOL/Tools/function_package/fundef_package.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Mar 12 22:16:25 2009 +0100
@@ -93,13 +93,12 @@
end
-fun gen_add_fundef is_external prep default_constraint fixspec eqnss config flags lthy =
+fun gen_add_fundef is_external prep default_constraint fixspec eqns config flags lthy =
let
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
- val ((fixes0, spec0), ctxt') =
- prep (constrn_fxs fixspec) (map (single o apsnd single) eqnss) lthy
+ val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
val fixes = map (apfst (apfst Binding.name_of)) fixes0;
- val spec = map (apfst (apfst Binding.name_of)) spec0;
+ val spec = map (fn ((b, atts), prop) => ((Binding.name_of b, atts), [prop])) spec0;
val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
val defname = mk_defname fixes
@@ -163,9 +162,8 @@
|> LocalTheory.set_group (serial_string ())
|> setup_termination_proof term_opt;
-val add_fundef = gen_add_fundef true Specification.read_specification "_::type"
-val add_fundef_i =
- gen_add_fundef false Specification.check_specification (TypeInfer.anyT HOLogic.typeS)
+val add_fundef = gen_add_fundef true Specification.read_spec "_::type"
+val add_fundef_i = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
(* Datatype hook to declare datatype congs as "fundef_congs" *)
--- a/src/HOL/Tools/inductive_package.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Tools/inductive_package.ML Thu Mar 12 22:16:25 2009 +0100
@@ -842,11 +842,10 @@
fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
let
- val ((vars, specs), _) = lthy |> ProofContext.set_mode ProofContext.mode_abbrev
- |> Specification.read_specification
- (cnames_syn @ pnames_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs);
+ val ((vars, intrs), _) = lthy
+ |> ProofContext.set_mode ProofContext.mode_abbrev
+ |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
val (cs, ps) = chop (length cnames_syn) vars;
- val intrs = map (apsnd the_single) specs;
val monos = Attrib.eval_thms lthy raw_monos;
val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
@@ -946,22 +945,12 @@
val _ = OuterKeyword.keyword "monos";
-(* FIXME eliminate *)
-fun flatten_specification specs = specs |> maps
- (fn (a, (concl, [])) => concl |> map
- (fn ((b, atts), [B]) =>
- if Binding.is_empty a then ((b, atts), B)
- else if Binding.is_empty b then ((a, atts), B)
- else error "Illegal nested case names"
- | ((b, _), _) => error "Illegal simultaneous specification")
- | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.str_of a)));
-
fun gen_ind_decl mk_def coind =
P.fixes -- P.for_fixes --
- Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] --
+ Scan.optional SpecParse.where_alt_specs [] --
Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
>> (fn (((preds, params), specs), monos) =>
- (snd oo gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
+ (snd oo gen_add_inductive mk_def true coind preds params specs monos));
val ind_decl = gen_ind_decl add_ind_def;
@@ -971,7 +960,7 @@
val _ =
OuterSyntax.local_theory "inductive_cases"
"create simplified instances of elimination rules (improper)" K.thy_script
- (P.and_list1 SpecParse.spec >> (fn specs => snd o inductive_cases specs));
+ (P.and_list1 SpecParse.specs >> (snd oo inductive_cases));
end;
--- a/src/HOL/Tools/primrec_package.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOL/Tools/primrec_package.ML Thu Mar 12 22:16:25 2009 +0100
@@ -9,6 +9,8 @@
sig
val add_primrec: (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> local_theory -> thm list * local_theory
+ val add_primrec_cmd: (binding * string option * mixfix) list ->
+ (Attrib.binding * string) list -> local_theory -> thm list * local_theory
val add_primrec_global: (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> theory -> thm list * theory
val add_primrec_overloaded: (string * (string * typ) * bool) list ->
@@ -213,12 +215,6 @@
local
-fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
- let
- val ((fixes, spec), _) = prep_spec
- raw_fixes (map (single o apsnd single) raw_spec) ctxt
- in (fixes, map (apsnd the_single) spec) end;
-
fun prove_spec ctxt names rec_rewrites defs eqs =
let
val rewrites = map mk_meta_eq rec_rewrites @ map (snd o snd) defs;
@@ -228,7 +224,7 @@
fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
let
- val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
+ val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes) o snd) spec [];
val tnames = distinct (op =) (map (#1 o snd) eqns);
@@ -268,8 +264,8 @@
in
-val add_primrec = gen_primrec false Specification.check_specification;
-val add_primrec_cmd = gen_primrec true Specification.read_specification;
+val add_primrec = gen_primrec false Specification.check_spec;
+val add_primrec_cmd = gen_primrec true Specification.read_spec;
end;
@@ -300,24 +296,16 @@
val old_primrec_decl =
opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
-fun pipe_error t = P.!!! (Scan.fail_with (K
- (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
-
-val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
- ((P.term :-- pipe_error) || Scan.succeed ("",""));
-
-val statements = P.enum1 "|" statement;
-
-val primrec_decl = P.opt_target -- P.fixes --| P.$$$ "where" -- statements;
+val primrec_decl = P.opt_target -- P.fixes -- SpecParse.where_alt_specs;
val _ =
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
- ((primrec_decl >> (fn ((opt_target, raw_fixes), raw_spec) =>
- Toplevel.local_theory opt_target (add_primrec_cmd raw_fixes raw_spec #> snd)))
+ ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
+ Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
|| (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
Toplevel.theory (snd o
- (if unchecked then OldPrimrecPackage.add_primrec_unchecked else OldPrimrecPackage.add_primrec) alt_name
- (map P.triple_swap eqns)))));
+ (if unchecked then OldPrimrecPackage.add_primrec_unchecked else OldPrimrecPackage.add_primrec)
+ alt_name (map P.triple_swap eqns)))));
end;
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Thu Mar 12 22:16:25 2009 +0100
@@ -108,7 +108,16 @@
[take_def, finite_def])
end; (* let (calc_axioms) *)
-fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
+
+(* legacy type inference *)
+
+fun legacy_infer_term thy t =
+ singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
+
+fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
+
+fun infer_props thy = map (apsnd (legacy_infer_prop thy));
+
fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
--- a/src/HOLCF/Tools/fixrec_package.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/HOLCF/Tools/fixrec_package.ML Thu Mar 12 22:16:25 2009 +0100
@@ -6,17 +6,12 @@
signature FIXREC_PACKAGE =
sig
- val legacy_infer_term: theory -> term -> term
- val legacy_infer_prop: theory -> term -> term
-
- val add_fixrec: bool -> (binding * string option * mixfix) list
+ val add_fixrec: bool -> (binding * typ option * mixfix) list
+ -> (Attrib.binding * term) list -> local_theory -> local_theory
+ val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
-> (Attrib.binding * string) list -> local_theory -> local_theory
-
- val add_fixrec_i: bool -> (binding * typ option * mixfix) list
- -> (Attrib.binding * term) list -> local_theory -> local_theory
-
- val add_fixpat: Attrib.binding * string list -> theory -> theory
- val add_fixpat_i: Thm.binding * term list -> theory -> theory
+ val add_fixpat: Thm.binding * term list -> theory -> theory
+ val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
val add_matchers: (string * string) list -> theory -> theory
val setup: theory -> theory
end;
@@ -24,14 +19,6 @@
structure FixrecPackage: FIXREC_PACKAGE =
struct
-(* legacy type inference *)
-(* used by the domain package *)
-fun legacy_infer_term thy t =
- singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
-
-fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
-
-
val fix_eq2 = @{thm fix_eq2};
val def_fix_ind = @{thm def_fix_ind};
@@ -341,20 +328,9 @@
local
(* code adapted from HOL/Tools/primrec_package.ML *)
-fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
- let
- val ((fixes, spec), _) = prep_spec
- raw_fixes (map (single o apsnd single) raw_spec) ctxt
- in (fixes, map (apsnd the_single) spec) end;
-
fun gen_fixrec
(set_group : bool)
- (prep_spec : (binding * 'a option * mixfix) list ->
- (Attrib.binding * 'b list) list list ->
- Proof.context ->
- (((binding * typ) * mixfix) list * (Attrib.binding * term list) list)
- * Proof.context
- )
+ prep_spec
(strict : bool)
raw_fixes
raw_spec
@@ -362,7 +338,7 @@
let
val (fixes : ((binding * typ) * mixfix) list,
spec : (Attrib.binding * term) list) =
- prepare_spec prep_spec lthy raw_fixes raw_spec;
+ fst (prep_spec raw_fixes raw_spec lthy);
val chead_of_spec =
chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd;
fun name_of (Free (n, _)) = n
@@ -405,8 +381,8 @@
in
-val add_fixrec_i = gen_fixrec false Specification.check_specification;
-val add_fixrec = gen_fixrec true Specification.read_specification;
+val add_fixrec = gen_fixrec false Specification.check_spec;
+val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
end; (* local *)
@@ -434,8 +410,8 @@
(snd o PureThy.add_thmss [((name, simps), atts)]) thy
end;
-val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
-val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);
+val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
+val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
(*************************************************************************)
@@ -444,43 +420,14 @@
local structure P = OuterParse and K = OuterKeyword in
-(* bool parser *)
-val fixrec_strict = P.opt_keyword "permissive" >> not;
-
-fun pipe_error t = P.!!! (Scan.fail_with (K
- (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
-
-(* (Attrib.binding * string) parser *)
-val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
- ((P.term :-- pipe_error) || Scan.succeed ("",""));
-
-(* ((Attrib.binding * string) list) parser *)
-val statements = P.enum1 "|" statement;
-
-(* (((xstring option * bool) * (Binding.binding * string option * Mixfix.mixfix) list)
- * (Attrib.binding * string) list) parser *)
-val fixrec_decl =
- P.opt_target -- fixrec_strict -- P.fixes --| P.$$$ "where" -- statements;
+val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
+ ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
+ >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
-(* this builds a parser for a new keyword, fixrec, whose functionality
-is defined by add_fixrec *)
-val _ =
- let
- val desc = "define recursive functions (HOLCF)";
- fun fixrec (((opt_target, strict), raw_fixes), raw_spec) =
- Toplevel.local_theory opt_target (add_fixrec strict raw_fixes raw_spec);
- in
- OuterSyntax.command "fixrec" desc K.thy_decl (fixrec_decl >> fixrec)
- end;
-
-(* fixpat parser *)
-val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
-
-val _ =
- OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
- (fixpat_decl >> (Toplevel.theory o add_fixpat));
+val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
+ (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
-end; (* local structure *)
+end;
val setup = FixrecMatchData.init;
--- a/src/Pure/Isar/args.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/args.ML Thu Mar 12 22:16:25 2009 +0100
@@ -227,7 +227,7 @@
val bang_facts = Scan.peek (fn context =>
P.position ($$$ "!") >> (fn (_, pos) =>
(warning ("use of prems in proof method" ^ Position.str_of pos);
- Assumption.prems_of (Context.proof_of context))) || Scan.succeed []);
+ Assumption.all_prems_of (Context.proof_of context))) || Scan.succeed []);
val from_to =
P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
--- a/src/Pure/Isar/isar_syn.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/isar_syn.ML Thu Mar 12 22:16:25 2009 +0100
@@ -185,9 +185,11 @@
(* axioms and definitions *)
+val named_spec = SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
+
val _ =
OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
- (Scan.repeat1 SpecParse.spec_name >> (Toplevel.theory o IsarCmd.add_axioms));
+ (Scan.repeat1 named_spec >> (Toplevel.theory o IsarCmd.add_axioms));
val opt_unchecked_overloaded =
Scan.optional (P.$$$ "(" |-- P.!!!
@@ -196,7 +198,7 @@
val _ =
OuterSyntax.command "defs" "define constants" K.thy_decl
- (opt_unchecked_overloaded -- Scan.repeat1 SpecParse.spec_name
+ (opt_unchecked_overloaded -- Scan.repeat1 named_spec
>> (Toplevel.theory o IsarCmd.add_defs));
@@ -254,7 +256,7 @@
val _ =
OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
(Scan.optional P.fixes [] --
- Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) []
+ Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.specs)) []
>> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
--- a/src/Pure/Isar/local_defs.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/local_defs.ML Thu Mar 12 22:16:25 2009 +0100
@@ -135,7 +135,7 @@
fun export inner outer = (*beware of closure sizes*)
let
val exp = Assumption.export false inner outer;
- val prems = Assumption.prems_of inner;
+ val prems = Assumption.all_prems_of inner;
in fn th =>
let
val th' = exp th;
--- a/src/Pure/Isar/proof_context.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/proof_context.ML Thu Mar 12 22:16:25 2009 +0100
@@ -301,7 +301,7 @@
in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
fun pretty_thm ctxt th =
- let val asms = map Thm.term_of (Assumption.assms_of ctxt)
+ let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
fun pretty_thms ctxt [th] = pretty_thm ctxt th
@@ -1370,7 +1370,7 @@
Pretty.commas (map prt_fix fixes))];
(*prems*)
- val prems = Assumption.prems_of ctxt;
+ val prems = Assumption.all_prems_of ctxt;
val len = length prems;
val suppressed = len - ! prems_limit;
val prt_prems = if null prems then []
--- a/src/Pure/Isar/spec_parse.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/spec_parse.ML Thu Mar 12 22:16:25 2009 +0100
@@ -13,10 +13,10 @@
val opt_attribs: Attrib.src list parser
val thm_name: string -> Attrib.binding parser
val opt_thm_name: string -> Attrib.binding parser
- val spec: (Attrib.binding * string list) parser
- val named_spec: (Attrib.binding * string list) parser
- val spec_name: ((binding * string) * Attrib.src list) parser
- val spec_opt_name: ((binding * string) * Attrib.src list) parser
+ val spec: (Attrib.binding * string) parser
+ val specs: (Attrib.binding * string list) parser
+ val alt_specs: (Attrib.binding * string) list parser
+ val where_alt_specs: (Attrib.binding * string) list parser
val xthm: (Facts.ref * Attrib.src list) parser
val xthms1: (Facts.ref * Attrib.src list) list parser
val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
@@ -30,8 +30,6 @@
val statement: (Attrib.binding * (string * string list) list) list parser
val general_statement: (Element.context list * Element.statement) parser
val statement_keyword: string parser
- val specification:
- (binding * ((Attrib.binding * string list) list * (binding * string option) list)) list parser
end;
structure SpecParse: SPEC_PARSE =
@@ -54,11 +52,13 @@
Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
Attrib.empty_binding;
-val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
-val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
+val spec = opt_thm_name ":" -- P.prop;
+val specs = opt_thm_name ":" -- Scan.repeat1 P.prop;
-val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
-val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
+val alt_specs =
+ P.enum1 "|" (spec --| Scan.option (Scan.ahead (P.name || P.$$$ "[") -- P.!!! (P.$$$ "|")));
+
+val where_alt_specs = P.where_ |-- P.!!! alt_specs;
val xthm =
P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
@@ -143,9 +143,4 @@
val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
-
-(* specifications *)
-
-val specification = P.enum1 "|" (P.parbinding -- (P.and_list1 spec -- P.for_simple_fixes));
-
end;
--- a/src/Pure/Isar/specification.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/specification.ML Thu Mar 12 22:16:25 2009 +0100
@@ -8,16 +8,22 @@
signature SPECIFICATION =
sig
val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
+ val check_spec:
+ (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
+ val read_spec:
+ (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
+ val check_free_spec:
+ (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
+ val read_free_spec:
+ (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
val check_specification: (binding * typ option * mixfix) list ->
- (Attrib.binding * term list) list list -> Proof.context ->
+ (Attrib.binding * term list) list -> Proof.context ->
(((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
val read_specification: (binding * string option * mixfix) list ->
- (Attrib.binding * string list) list list -> Proof.context ->
- (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val check_free_specification: (binding * typ option * mixfix) list ->
- (Attrib.binding * term list) list -> Proof.context ->
- (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val read_free_specification: (binding * string option * mixfix) list ->
(Attrib.binding * string list) list -> Proof.context ->
(((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
val axiomatization: (binding * typ option * mixfix) list ->
@@ -97,7 +103,7 @@
in fold_rev close bounds A end;
in map close_form As end;
-fun prep_spec prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
+fun prepare prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
let
val thy = ProofContext.theory_of ctxt;
@@ -122,15 +128,30 @@
val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
in ((params, name_atts ~~ specs), specs_ctxt) end;
-fun read_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src x;
-fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) x;
+
+fun single_spec (a, prop) = [(a, [prop])];
+fun the_spec (a, [prop]) = (a, prop);
+
+fun prep_spec prep_vars parse_prop prep_att do_close vars specs =
+ prepare prep_vars parse_prop prep_att do_close
+ vars (map single_spec specs) #>> apsnd (map the_spec);
+
+fun prep_specification prep_vars parse_prop prep_att vars specs =
+ prepare prep_vars parse_prop prep_att true [specs];
in
-fun read_specification x = read_spec true x;
-fun check_specification x = check_spec true x;
-fun read_free_specification vars specs = read_spec false vars [specs];
-fun check_free_specification vars specs = check_spec false vars [specs];
+fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) true x;
+fun read_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src true x;
+
+fun check_free_spec x = prep_spec ProofContext.cert_vars (K I) (K I) false x;
+fun read_free_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src false x;
+
+fun check_specification vars specs =
+ prepare ProofContext.cert_vars (K I) (K I) true vars [specs];
+
+fun read_specification vars specs =
+ prepare ProofContext.read_vars Syntax.parse_prop Attrib.intern_src true vars [specs];
end;
@@ -139,7 +160,7 @@
fun gen_axioms do_print prep raw_vars raw_specs thy =
let
- val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
+ val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy);
val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars;
(*consts*)
@@ -147,12 +168,16 @@
val subst = Term.subst_atomic (map Free xs ~~ consts);
(*axioms*)
- val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
- fold_map Thm.add_axiom (* FIXME proper use of binding!? *)
- ((map o apfst) Binding.name (PureThy.name_multi (Binding.name_of b) (map subst props)))
- #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
+ val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
+ fold_map Thm.add_axiom
+ (map (apfst (fn a => Binding.map_name (K a) b))
+ (PureThy.name_multi (Binding.name_of b) (map subst props)))
+ #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
+
+ (*facts*)
val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
(Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
+
val _ =
if not do_print then ()
else print_consts (ProofContext.init thy') (K false) xs;
@@ -164,10 +189,9 @@
(* definition *)
-fun gen_def do_print prep (raw_var, (raw_a, raw_prop)) lthy =
+fun gen_def do_print prep (raw_var, raw_spec) lthy =
let
- val (vars, [((raw_name, atts), [prop])]) =
- fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
+ val (vars, [((raw_name, atts), prop)]) = fst (prep (the_list raw_var) [raw_spec] lthy);
val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
val var as (b, _) =
(case vars of
@@ -193,16 +217,16 @@
else print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
in ((lhs, (def_name, th')), lthy3) end;
-val definition = gen_def false check_free_specification;
-val definition_cmd = gen_def true read_free_specification;
+val definition = gen_def false check_free_spec;
+val definition_cmd = gen_def true read_free_spec;
(* abbreviation *)
fun gen_abbrev do_print prep mode (raw_var, raw_prop) lthy =
let
- val ((vars, [(_, [prop])]), _) =
- prep (the_list raw_var) [(("", []), [raw_prop])]
+ val ((vars, [(_, prop)]), _) =
+ prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
(lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
val var =
@@ -223,8 +247,8 @@
val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
in lthy' end;
-val abbreviation = gen_abbrev false check_free_specification;
-val abbreviation_cmd = gen_abbrev true read_free_specification;
+val abbreviation = gen_abbrev false check_free_spec;
+val abbreviation_cmd = gen_abbrev true read_free_spec;
(* notation *)
@@ -256,15 +280,12 @@
local
-fun subtract_prems ctxt1 ctxt2 =
- Library.drop (length (Assumption.prems_of ctxt1), Assumption.prems_of ctxt2);
-
fun prep_statement prep_att prep_stmt elems concl ctxt =
(case concl of
Element.Shows shows =>
let
val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt;
- val prems = subtract_prems ctxt elems_ctxt;
+ val prems = Assumption.local_prems_of elems_ctxt ctxt;
val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
in ((prems, stmt, []), goal_ctxt) end
@@ -300,7 +321,7 @@
val atts = map (Attrib.internal o K)
[RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
- val prems = subtract_prems ctxt elems_ctxt;
+ val prems = Assumption.local_prems_of elems_ctxt ctxt;
val stmt = [((Binding.empty, atts), [(thesis, [])])];
val (facts, goal_ctxt) = elems_ctxt
--- a/src/Pure/Isar/theory_target.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Isar/theory_target.ML Thu Mar 12 22:16:25 2009 +0100
@@ -52,7 +52,7 @@
val fixes =
map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
val assumes =
- map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.assms_of ctxt);
+ map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.all_assms_of ctxt);
val elems =
(if null fixes then [] else [Element.Fixes fixes]) @
(if null assumes then [] else [Element.Assumes assumes]);
@@ -109,7 +109,7 @@
val th = Goal.norm_result raw_th;
val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
- val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
+ val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt);
val nprems = Thm.nprems_of th' - Thm.nprems_of th;
(*export fixes*)
--- a/src/Pure/Tools/find_theorems.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/Tools/find_theorems.ML Thu Mar 12 22:16:25 2009 +0100
@@ -336,7 +336,7 @@
fun find_theorems ctxt opt_goal rem_dups raw_criteria =
let
- val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.prems_of ctxt) 1));
+ val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.all_prems_of ctxt) 1));
val opt_goal' = Option.map add_prems opt_goal;
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
--- a/src/Pure/assumption.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/assumption.ML Thu Mar 12 22:16:25 2009 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/assumption.ML
Author: Makarius
-Local assumptions, parameterized by export rules.
+Context assumptions, parameterized by export rules.
*)
signature ASSUMPTION =
@@ -10,12 +10,13 @@
val assume_export: export
val presume_export: export
val assume: cterm -> thm
- val assms_of: Proof.context -> cterm list
- val prems_of: Proof.context -> thm list
+ val all_assms_of: Proof.context -> cterm list
+ val all_prems_of: Proof.context -> thm list
val extra_hyps: Proof.context -> thm -> term list
+ val local_assms_of: Proof.context -> Proof.context -> cterm list
+ val local_prems_of: Proof.context -> Proof.context -> thm list
val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
- val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context
val export: bool -> Proof.context -> Proof.context -> thm -> thm
val export_term: Proof.context -> Proof.context -> term -> term
val export_morphism: Proof.context -> Proof.context -> morphism
@@ -54,7 +55,7 @@
(** local context data **)
datatype data = Data of
- {assms: (export * cterm list) list, (*assumes and views: A ==> _*)
+ {assms: (export * cterm list) list, (*assumes: A ==> _*)
prems: thm list}; (*prems: A |- A*)
fun make_data (assms, prems) = Data {assms = assms, prems = prems};
@@ -68,18 +69,31 @@
fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
-val assumptions_of = #assms o rep_data;
-val assms_of = maps #2 o assumptions_of;
-val prems_of = #prems o rep_data;
+
+(* all assumptions *)
+
+val all_assumptions_of = #assms o rep_data;
+val all_assms_of = maps #2 o all_assumptions_of;
+val all_prems_of = #prems o rep_data;
-fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th);
+fun extra_hyps ctxt th =
+ subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
+
+(*named prems -- legacy feature*)
+val _ = Context.>>
+ (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
+ fn Context.Theory _ => [] | Context.Proof ctxt => all_prems_of ctxt)));
-(* named prems -- legacy feature *)
+(* local assumptions *)
+
+fun local_assumptions_of inner outer =
+ Library.drop (length (all_assumptions_of outer), all_assumptions_of inner);
-val _ = Context.>>
- (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
- fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
+val local_assms_of = maps #2 oo local_assumptions_of;
+
+fun local_prems_of inner outer =
+ Library.drop (length (all_prems_of outer), all_prems_of inner);
(* add assumptions *)
@@ -92,27 +106,16 @@
val add_assumes = add_assms assume_export;
-fun add_view outer view = map_data (fn (asms, prems) =>
- let
- val (asms1, asms2) = chop (length (assumptions_of outer)) asms;
- val asms' = asms1 @ [(assume_export, view)] @ asms2;
- in (asms', prems) end);
-
(* export *)
-fun diff_assms inner outer =
- Library.drop (length (assumptions_of outer), assumptions_of inner);
-
fun export is_goal inner outer =
- let val asms = diff_assms inner outer in
- MetaSimplifier.norm_hhf_protect
- #> fold_rev (fn (e, As) => #1 (e is_goal As)) asms
- #> MetaSimplifier.norm_hhf_protect
- end;
+ MetaSimplifier.norm_hhf_protect #>
+ fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
+ MetaSimplifier.norm_hhf_protect;
fun export_term inner outer =
- fold_rev (fn (e, As) => #2 (e false As)) (diff_assms inner outer);
+ fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
fun export_morphism inner outer =
let
--- a/src/Pure/goal.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Pure/goal.ML Thu Mar 12 22:16:25 2009 +0100
@@ -110,7 +110,7 @@
val cert = Thm.cterm_of thy;
val certT = Thm.ctyp_of thy;
- val assms = Assumption.assms_of ctxt;
+ val assms = Assumption.all_assms_of ctxt;
val As = map Thm.term_of assms;
val xs = map Free (fold Term.add_frees (prop :: As) []);
--- a/src/Tools/quickcheck.ML Thu Mar 12 09:27:23 2009 -0700
+++ b/src/Tools/quickcheck.ML Thu Mar 12 22:16:25 2009 +0100
@@ -144,7 +144,7 @@
fun test_goal_auto int state =
let
val ctxt = Proof.context_of state;
- val assms = map term_of (Assumption.assms_of ctxt);
+ val assms = map term_of (Assumption.all_assms_of ctxt);
val Test_Params { size, iterations, default_type } =
(snd o Data.get o Proof.theory_of) state;
fun test () =