# HG changeset patch # User wenzelm # Date 1320411139 -3600 # Node ID 2838109364f0f974990c1ffc61594fa0980603be # Parent f502f439305435023f77dac7e0b8b993ffda8f60# Parent 6e0a8aba99ec4d96638f72ea91ed9ac8c40ef7bd merged diff -r f502f4393054 -r 2838109364f0 src/HOL/Nominal/nominal_induct.ML --- a/src/HOL/Nominal/nominal_induct.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/HOL/Nominal/nominal_induct.ML Fri Nov 04 13:52:19 2011 +0100 @@ -72,7 +72,7 @@ val ys = if p < n then [] else map (tune o #1) (take (p - n) ps) @ xs; - in Logic.list_rename_params (ys, prem) end; + in Logic.list_rename_params ys prem end; fun rename_prems prop = let val (As, C) = Logic.strip_horn prop in Logic.list_implies (map rename As, C) end; diff -r f502f4393054 -r 2838109364f0 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/Pure/Isar/element.ML Fri Nov 04 13:52:19 2011 +0100 @@ -294,9 +294,9 @@ in proof after_qed' propss #> refine_witness #> Seq.hd end; fun proof_local cmd goal_ctxt int after_qed' propss = - Proof.map_context (K goal_ctxt) - #> Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i - cmd NONE after_qed' (map (pair Thm.empty_binding) propss); + Proof.map_context (K goal_ctxt) #> + Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i + cmd NONE after_qed' (map (pair Thm.empty_binding) propss); in diff -r f502f4393054 -r 2838109364f0 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/Pure/Isar/obtain.ML Fri Nov 04 13:52:19 2011 +0100 @@ -123,7 +123,8 @@ val xs = map (Variable.check_name o #1) vars; (*obtain asms*) - val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); + val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt; + val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt; val asm_props = maps (map fst) proppss; val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss; @@ -138,11 +139,11 @@ val that_name = if name = "" then thatN else name; val that_prop = - Term.list_all_free (parms, Logic.list_implies (asm_props, thesis)) - |> Library.curry Logic.list_rename_params xs; + Logic.list_rename_params xs + (Term.list_all_free (parms, Logic.list_implies (asm_props, thesis))); val obtain_prop = - Logic.list_rename_params ([Auto_Bind.thesisN], - Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis))); + Logic.list_rename_params [Auto_Bind.thesisN] + (Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis))); fun after_qed _ = Proof.local_qed (NONE, false) @@ -153,6 +154,7 @@ state |> Proof.enter_forward |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int + |> Proof.map_context bind_ctxt |> Proof.proof (SOME Method.succeed_text) |> Seq.hd |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)] |> Proof.assume @@ -308,7 +310,7 @@ |> Proof.begin_block |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] |> Proof.chain_facts chain_facts - |> Proof.local_goal print_result (K I) (apsnd (rpair I)) + |> Proof.local_goal print_result (K I) (pair o rpair I) "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])] |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd end; diff -r f502f4393054 -r 2838109364f0 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/Pure/Isar/parse.ML Fri Nov 04 13:52:19 2011 +0100 @@ -322,7 +322,7 @@ val simple_fixes = and_list1 params >> flat; val fixes = - and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) || + and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1) || params >> map (fn (x, y) => (x, y, NoSyn))) >> flat; val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) []; diff -r f502f4393054 -r 2838109364f0 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/Pure/Isar/proof.ML Fri Nov 04 13:52:19 2011 +0100 @@ -84,7 +84,7 @@ val apply_end: Method.text -> state -> state Seq.seq val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) -> (theory -> 'a -> attribute) -> - (context * 'b list -> context * (term list list * (context -> context))) -> + ('b list -> context -> (term list list * (context -> context)) * context) -> string -> Method.text option -> (thm list list -> state -> state) -> ((binding * 'a list) * 'b) list -> state -> state val local_qed: Method.text option * bool -> state -> state @@ -863,7 +863,7 @@ |> assert_forward_or_chain |> enter_forward |> open_block - |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp))); + |> map_context_result (prepp raw_propp); val props = flat propss; val vars = implicit_vars props; @@ -938,9 +938,13 @@ (* global goals *) -fun global_goal prepp before_qed after_qed propp ctxt = - init ctxt - |> generic_goal (prepp #> Proof_Context.auto_fixes) "" before_qed (K I, after_qed) propp; +fun prepp_auto_fixes prepp args = + prepp args #> + (fn ((propss, a), ctxt) => ((propss, a), (fold o fold) Variable.auto_fixes propss ctxt)); + +fun global_goal prepp before_qed after_qed propp = + init #> + generic_goal (prepp_auto_fixes prepp) "" before_qed (K I, after_qed) propp; val theorem = global_goal Proof_Context.bind_propp_schematic_i; val theorem_cmd = global_goal Proof_Context.bind_propp_schematic; diff -r f502f4393054 -r 2838109364f0 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Nov 04 13:52:19 2011 +0100 @@ -93,22 +93,22 @@ val auto_bind_facts: term list -> Proof.context -> Proof.context val match_bind: bool -> (string list * string) list -> Proof.context -> term list * Proof.context val match_bind_i: bool -> (term list * term) list -> Proof.context -> term list * Proof.context - val read_propp: Proof.context * (string * string list) list list - -> Proof.context * (term * term list) list list - val cert_propp: Proof.context * (term * term list) list list - -> Proof.context * (term * term list) list list - val read_propp_schematic: Proof.context * (string * string list) list list - -> Proof.context * (term * term list) list list - val cert_propp_schematic: Proof.context * (term * term list) list list - -> Proof.context * (term * term list) list list - val bind_propp: Proof.context * (string * string list) list list - -> Proof.context * (term list list * (Proof.context -> Proof.context)) - val bind_propp_i: Proof.context * (term * term list) list list - -> Proof.context * (term list list * (Proof.context -> Proof.context)) - val bind_propp_schematic: Proof.context * (string * string list) list list - -> Proof.context * (term list list * (Proof.context -> Proof.context)) - val bind_propp_schematic_i: Proof.context * (term * term list) list list - -> Proof.context * (term list list * (Proof.context -> Proof.context)) + val read_propp: (string * string list) list list -> Proof.context -> + (term * term list) list list * Proof.context + val cert_propp: (term * term list) list list -> Proof.context -> + (term * term list) list list * Proof.context + val read_propp_schematic: (string * string list) list list -> Proof.context -> + (term * term list) list list * Proof.context + val cert_propp_schematic: (term * term list) list list -> Proof.context -> + (term * term list) list list * Proof.context + val bind_propp: (string * string list) list list -> Proof.context -> + (term list list * (Proof.context -> Proof.context)) * Proof.context + val bind_propp_i: (term * term list) list list -> Proof.context -> + (term list list * (Proof.context -> Proof.context)) * Proof.context + val bind_propp_schematic: (string * string list) list list -> Proof.context -> + (term list list * (Proof.context -> Proof.context)) * Proof.context + val bind_propp_schematic_i: (term * term list) list list -> Proof.context -> + (term list list * (Proof.context -> Proof.context)) * Proof.context val fact_tac: thm list -> int -> tactic val some_fact_tac: Proof.context -> int -> tactic val get_fact: Proof.context -> Facts.ref -> thm list @@ -124,7 +124,6 @@ (binding * typ option * mixfix) list * Proof.context 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 add_assms: Assumption.export -> (Thm.binding * (string * string list) list) list -> Proof.context -> (string * thm list) list * Proof.context @@ -778,26 +777,26 @@ local -fun prep_propp mode prep_props (context, args) = +fun prep_propp mode prep_props args context = let fun prep (_, raw_pats) (ctxt, prop :: props) = let val ctxt' = Variable.declare_term prop ctxt in ((prop, prep_props (set_mode mode_pattern ctxt') raw_pats), (ctxt', props)) end; - val (propp, (context', _)) = (fold_map o fold_map) prep args - (context, prep_props (set_mode mode context) (maps (map fst) args)); - in (context', propp) end; + val (propp, (context', _)) = + (fold_map o fold_map) prep args + (context, prep_props (set_mode mode context) (maps (map fst) args)); + in (propp, context') end; -fun gen_bind_propp mode parse_prop (ctxt, raw_args) = +fun gen_bind_propp mode parse_prop raw_args ctxt = let - val (ctxt', args) = prep_propp mode parse_prop (ctxt, raw_args); + val (args, ctxt') = prep_propp mode parse_prop raw_args ctxt; val binds = flat (flat (map (map (simult_matches ctxt')) args)); val propss = map (map #1) args; - - (*generalize result: context evaluated now, binds added later*) - val gen = Variable.exportT_terms ctxt' ctxt; - fun gen_binds c = c |> bind_terms (map #1 binds ~~ map SOME (gen (map #2 binds))); - in (ctxt' |> bind_terms (map (apsnd SOME) binds), (propss, gen_binds)) end; + fun gen_binds ctxt0 = ctxt0 + |> bind_terms (map #1 binds ~~ + map (SOME o Term.close_schematic_term) (Variable.export_terms ctxt' ctxt0 (map #2 binds))); + in ((propss, gen_binds), ctxt' |> bind_terms (map (apsnd SOME) binds)) end; in @@ -1038,9 +1037,6 @@ #> pair xs) end; -fun auto_fixes (ctxt, (propss, x)) = - ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x)); - (** assumptions **) @@ -1050,7 +1046,7 @@ fun gen_assms prepp exp args ctxt = let val cert = Thm.cterm_of (theory_of ctxt); - val (propss, ctxt1) = swap (prepp (ctxt, map snd args)); + val ((propss, _), ctxt1) = prepp (map snd args) ctxt; val _ = Variable.warn_extra_tfrees ctxt ctxt1; val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1; in @@ -1061,8 +1057,8 @@ in -val add_assms = gen_assms (apsnd #1 o bind_propp); -val add_assms_i = gen_assms (apsnd #1 o bind_propp_i); +val add_assms = gen_assms bind_propp; +val add_assms_i = gen_assms bind_propp_i; end; diff -r f502f4393054 -r 2838109364f0 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/Pure/Isar/rule_cases.ML Fri Nov 04 13:52:19 2011 +0100 @@ -403,7 +403,7 @@ fun rename prem = let val xs = map (Name.internal o Name.clean o fst) (Logic.strip_params prem) - in Logic.list_rename_params (xs, prem) end; + in Logic.list_rename_params xs prem end; fun rename_prems prop = let val (As, C) = Logic.strip_horn prop in Logic.list_implies (map rename As, C) end; diff -r f502f4393054 -r 2838109364f0 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/Pure/Isar/specification.ML Fri Nov 04 13:52:19 2011 +0100 @@ -308,7 +308,7 @@ val (propp, elems_ctxt) = prep_stmt elems (map snd shows) 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; + val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt; in ((prems, stmt, NONE), goal_ctxt) end | Element.Obtains obtains => let diff -r f502f4393054 -r 2838109364f0 src/Pure/logic.ML --- a/src/Pure/logic.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/Pure/logic.ML Fri Nov 04 13:52:19 2011 +0100 @@ -46,7 +46,7 @@ val name_arity: string * sort list * class -> string val mk_arities: arity -> term list val dest_arity: term -> string * sort list * class - val unconstrainT: sort list -> term -> + val unconstrainT: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term val protectC: term val protect: term -> term @@ -68,8 +68,8 @@ val strip_params: term -> (string * typ) list val has_meta_prems: term -> bool val flatten_params: int -> term -> term - val list_rename_params: string list * term -> term - val assum_pairs: int * term -> (term*term)list + val list_rename_params: string list -> term -> term + val assum_pairs: int * term -> (term * term) list val assum_problems: int * term -> (term -> term) * term list * term val varifyT_global: typ -> typ val unvarifyT_global: typ -> typ @@ -453,11 +453,11 @@ end; (*Makes parameters in a goal have the names supplied by the list cs.*) -fun list_rename_params (cs, Const("==>", _) $ A $ B) = - implies $ A $ list_rename_params (cs, B) - | list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) = - a $ Abs(c, T, list_rename_params (cs, t)) - | list_rename_params (cs, B) = B; +fun list_rename_params cs (Const ("==>", _) $ A $ B) = + implies $ A $ list_rename_params cs B + | list_rename_params (c :: cs) ((a as Const ("all", _)) $ Abs (_, T, t)) = + a $ Abs (c, T, list_rename_params cs t) + | list_rename_params cs B = B; diff -r f502f4393054 -r 2838109364f0 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/Pure/simplifier.ML Fri Nov 04 13:52:19 2011 +0100 @@ -184,9 +184,7 @@ lhss = let val lhss' = prep lthy lhss; - val ctxt' = lthy - |> fold Variable.declare_term lhss' - |> fold Variable.auto_fixes lhss'; + val ctxt' = fold Variable.auto_fixes lhss' lthy; in Variable.export_terms ctxt' lthy lhss' end |> map (Thm.cterm_of (Proof_Context.theory_of lthy)), proc = proc, diff -r f502f4393054 -r 2838109364f0 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/Pure/thm.ML Fri Nov 04 13:52:19 2011 +0100 @@ -1494,7 +1494,7 @@ if short < 0 then error "More names than abstractions!" else Name.variant_list cs (take short iparams) @ cs; val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi []; - val newBi = Logic.list_rename_params (newnames, Bi); + val newBi = Logic.list_rename_params newnames Bi; in (case duplicates (op =) cs of a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); state) diff -r f502f4393054 -r 2838109364f0 src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Nov 04 08:19:24 2011 +0100 +++ b/src/Tools/induct.ML Fri Nov 04 13:52:19 2011 +0100 @@ -627,7 +627,7 @@ val xs' = (case filter (fn x' => x' = x) xs of [] => xs | [_] => xs | _ => index 1 xs); - in Logic.list_rename_params (xs', A) end; + in Logic.list_rename_params xs' A end; fun rename_prop p = let val (As, C) = Logic.strip_horn p in Logic.list_implies (map rename_asm As, C) end;