# HG changeset patch # User wenzelm # Date 1236892585 -3600 # Node ID d09b7f0c2c140549cb87ac916400e68df0d33c47 # Parent 5d7d0add17410719bd8a27bb0659ed116550f3f2# Parent a14ff49d30830b7b7349e2b49fc30e172acc912a merged diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/FunDef.thy --- 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 diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Import/shuffler.ML --- 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 diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Nominal/nominal_primrec.ML --- 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; diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Statespace/state_space.ML --- 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; diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Tools/function_package/fundef_common.ML --- 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 diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Tools/function_package/fundef_package.ML --- 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" *) diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Tools/inductive_package.ML --- 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; diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOL/Tools/primrec_package.ML --- 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; diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOLCF/Tools/domain/domain_axioms.ML --- 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; diff -r 5d7d0add1741 -r d09b7f0c2c14 src/HOLCF/Tools/fixrec_package.ML --- 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; diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/args.ML --- 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) || diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/isar_syn.ML --- 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))); diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/local_defs.ML --- 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; diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/proof_context.ML --- 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 [] diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/spec_parse.ML --- 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; diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/specification.ML --- 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 diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Isar/theory_target.ML --- 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*) diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/Tools/find_theorems.ML --- 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; diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/assumption.ML --- 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 diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Pure/goal.ML --- 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) []); diff -r 5d7d0add1741 -r d09b7f0c2c14 src/Tools/quickcheck.ML --- 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 () =