# HG changeset patch # User paulson # Date 1433803941 -3600 # Node ID a58c48befade61a038186af3402bf128d2155413 # Parent b699cedd04e8154514b818fe229832c8b65f51b1# Parent b640770117fd727155d73f3b41b9a9bf546594a6 tidying messy proofs diff -r b699cedd04e8 -r a58c48befade NEWS --- a/NEWS Mon Jun 08 23:51:08 2015 +0100 +++ b/NEWS Mon Jun 08 23:52:21 2015 +0100 @@ -9,6 +9,9 @@ *** Pure *** +* Isar command 'obtain' binds term abbreviations (via 'is' patterns) in +the proof body as well, abstracted over the hypothetical parameters. + * New Isar command 'supply' supports fact definitions during goal refinement ('apply' scripts). diff -r b699cedd04e8 -r a58c48befade src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Mon Jun 08 23:51:08 2015 +0100 +++ b/src/Pure/Isar/element.ML Mon Jun 08 23:52:21 2015 +0100 @@ -278,10 +278,10 @@ in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end; in proof after_qed' propss #> refine_witness #> Seq.hd end; -fun proof_local cmd goal_ctxt int after_qed' propss = +fun proof_local cmd goal_ctxt int after_qed' propp = Proof.map_context (K goal_ctxt) #> - Proof.local_goal (K (K ())) (K I) Proof_Context.bind_propp cmd NONE - after_qed' (map (pair Thm.empty_binding) propss); + Proof.local_goal (K (K ())) (K I) Proof_Context.cert_propp cmd NONE + after_qed' (map (pair Thm.empty_binding) propp); in diff -r b699cedd04e8 -r a58c48befade src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Mon Jun 08 23:51:08 2015 +0100 +++ b/src/Pure/Isar/obtain.ML Mon Jun 08 23:52:21 2015 +0100 @@ -71,13 +71,13 @@ space_implode " " (map (Syntax.string_of_term ctxt) bads)); in tm end; -fun eliminate fix_ctxt rule xs As thm = +fun eliminate ctxt rule xs As thm = let - val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm); - val _ = Object_Logic.is_judgment fix_ctxt (Thm.concl_of thm) orelse + val _ = eliminate_term ctxt xs (Thm.full_prop_of thm); + val _ = Object_Logic.is_judgment ctxt (Thm.concl_of thm) orelse error "Conclusion in obtained context must be object-logic judgment"; - val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt; + val ((_, [thm']), ctxt') = Variable.import true [thm] ctxt; val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm')); in ((Drule.implies_elim_list thm' (map Thm.assume prems) @@ -85,7 +85,7 @@ |> Drule.forall_intr_list xs) COMP rule) |> Drule.implies_intr_list prems - |> singleton (Variable.export ctxt' fix_ctxt) + |> singleton (Variable.export ctxt' ctxt) end; fun obtain_export ctxt rule xs _ As = @@ -113,30 +113,37 @@ val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; (*obtain vars*) - val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt; - val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars; + val ((xs', vars), fix_ctxt) = ctxt + |> fold_map prep_var raw_vars + |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars); val xs = map (Variable.check_name o #1) vars; (*obtain asms*) - val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt; - val ((_, binds), binds_ctxt) = Proof_Context.bind_propp proppss asms_ctxt; - val asm_props = maps (map fst) proppss; - val asms = map fst (Attrib.map_specs (map (prep_att ctxt)) raw_asms) ~~ proppss; + val (asm_propss, binds) = prep_propp fix_ctxt (map snd raw_asms); + val asm_props = flat asm_propss; + val declare_asms = fold Variable.declare_term asm_props #> Proof_Context.bind_terms binds; + val asms = + map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~ + map (map (rpair [])) asm_propss; - (*obtain parms*) - val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt; - val parms = map Free (xs' ~~ Ts); - val cparms = map (Thm.cterm_of ctxt) parms; - val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt; + (*obtain params*) + val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' (declare_asms fix_ctxt); + val params = map Free (xs' ~~ Ts); + val cparams = map (Thm.cterm_of params_ctxt) params; + val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt; + + (*abstracted term bindings*) + val abs_term = Term.close_schematic_term o fold_rev Term.lambda_name (xs ~~ params); + val binds' = map (apsnd abs_term) binds; (*obtain statements*) val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN; - val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN); + val (thesis_var, thesis) = #1 (bind_judgment params_ctxt thesisN); val that_name = if name = "" then thatN else name; val that_prop = Logic.list_rename_params xs - (fold_rev Logic.all parms (Logic.list_implies (asm_props, thesis))); + (fold_rev Logic.all params (Logic.list_implies (asm_props, thesis))); val obtain_prop = Logic.list_rename_params [Auto_Bind.thesisN] (Logic.all (Free thesis_var) (Logic.mk_implies (that_prop, thesis))); @@ -145,12 +152,13 @@ Proof.local_qed (NONE, false) #> `Proof.the_fact #-> (fn rule => Proof.fix vars - #> Proof.assm (obtain_export fix_ctxt rule cparms) asms); + #> Proof.map_context declare_asms + #> Proof.assm (obtain_export params_ctxt rule cparams) asms); in state |> Proof.enter_forward |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int - |> Proof.map_context (Proof_Context.export_bind_terms binds binds_ctxt) + |> Proof.map_context (Proof_Context.bind_terms binds') |> Proof.proof (SOME Method.succeed_text) |> Seq.hd |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)] |> Proof.assume @@ -308,7 +316,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) (pair o rpair []) + |> Proof.local_goal print_result (K I) (K (rpair [])) "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])] |> Proof.refine (Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis))) |> Seq.hd diff -r b699cedd04e8 -r a58c48befade src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Jun 08 23:51:08 2015 +0100 +++ b/src/Pure/Isar/proof.ML Mon Jun 08 23:52:21 2015 +0100 @@ -91,7 +91,7 @@ val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) -> (context -> 'a -> attribute) -> - ('b list -> context -> (term list list * (indexname * term) list) * context) -> + (context -> 'b list -> (term list list * (indexname * term) list)) -> string -> Method.text option -> (thm list list -> state -> state) -> ((binding * 'a list) * 'b) list -> state -> state val local_qed: Method.text_range option * bool -> state -> state @@ -910,19 +910,21 @@ in -fun generic_goal prepp kind before_qed after_qed raw_propp state = +fun generic_goal prep_propp kind before_qed after_qed propp state = let val ctxt = context_of state; val chaining = can assert_chain state; val pos = Position.thread_data (); - val ((propss, binds), goal_state) = + val (propss, binds) = prep_propp ctxt propp; + val props = flat propss; + + val goal_state = state |> assert_forward_or_chain |> enter_forward |> open_block - |> map_context_result (prepp raw_propp); - val props = flat propss; + |> map_context (fold Variable.auto_fixes props #> Proof_Context.bind_terms binds); val goal_ctxt = context_of goal_state; val vars = implicit_vars props; @@ -972,7 +974,7 @@ (* local goals *) -fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state = +fun local_goal print_results prep_att prep_propp kind before_qed after_qed stmt state = let val ((names, attss), propp) = Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list; @@ -983,7 +985,8 @@ #> after_qed results; in state - |> generic_goal prepp kind before_qed (after_qed', K I) propp + |> map_context (Variable.set_body true) + |> generic_goal prep_propp kind before_qed (after_qed', K I) propp |> tap (Variable.warn_extra_tfrees (context_of state) o context_of) end; @@ -998,16 +1001,13 @@ (* global goals *) -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 prep_propp before_qed after_qed propp = + init + #> generic_goal (prep_propp o Proof_Context.set_mode Proof_Context.mode_schematic) "" + before_qed (K I, after_qed) propp; -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; -val theorem_cmd = global_goal Proof_Context.bind_propp_schematic_cmd; +val theorem = global_goal Proof_Context.cert_propp; +val theorem_cmd = global_goal Proof_Context.read_propp; fun global_qeds arg = end_proof true arg @@ -1056,11 +1056,11 @@ local -fun gen_have prep_att prepp before_qed after_qed stmt int = +fun gen_have prep_att prep_propp before_qed after_qed stmt int = local_goal (Proof_Display.print_results int (Position.thread_data ())) - prep_att prepp "have" before_qed after_qed stmt; + prep_att prep_propp "have" before_qed after_qed stmt; -fun gen_show prep_att prepp before_qed after_qed stmt int state = +fun gen_show prep_att prep_propp before_qed after_qed stmt int state = let val testing = Unsynchronized.ref false; val rule = Unsynchronized.ref (NONE: thm option); @@ -1091,7 +1091,7 @@ #> after_qed results; in state - |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt + |> local_goal print_results prep_att prep_propp "show" before_qed after_qed' stmt |> int ? (fn goal_state => (case test_proof (map_context (Context_Position.set_visible false) goal_state) of Exn.Res _ => goal_state @@ -1100,10 +1100,10 @@ in -val have = gen_have (K I) Proof_Context.bind_propp; -val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp_cmd; -val show = gen_show (K I) Proof_Context.bind_propp; -val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp_cmd; +val have = gen_have (K I) Proof_Context.cert_propp; +val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp; +val show = gen_show (K I) Proof_Context.cert_propp; +val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp; end; diff -r b699cedd04e8 -r a58c48befade src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Jun 08 23:51:08 2015 +0100 +++ b/src/Pure/Isar/proof_context.ML Mon Jun 08 23:52:21 2015 +0100 @@ -114,18 +114,10 @@ term list * Proof.context val match_bind_cmd: bool -> (string list * string) list -> Proof.context -> term list * 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 bind_propp: (term * term list) list list -> Proof.context -> - (term list list * (indexname * term) list) * Proof.context - val bind_propp_cmd: (string * string list) list list -> Proof.context -> - (term list list * (indexname * term) list) * Proof.context - val bind_propp_schematic: (term * term list) list list -> Proof.context -> - (term list list * (indexname * term) list) * Proof.context - val bind_propp_schematic_cmd: (string * string list) list list -> Proof.context -> - (term list list * (indexname * term) list) * Proof.context + val cert_propp: Proof.context -> (term * term list) list list -> + (term list list * (indexname * term) list) + val read_propp: Proof.context -> (string * string list) list list -> + (term list list * (indexname * term) list) val fact_tac: Proof.context -> thm list -> int -> tactic val some_fact_tac: Proof.context -> int -> tactic val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list @@ -892,30 +884,20 @@ local -fun prep_propp mode prep_props raw_args ctxt = +fun prep_propp prep_props ctxt raw_args = let - val props = prep_props (set_mode mode ctxt) (maps (map fst) raw_args); - val ctxt' = fold Variable.declare_term props ctxt; - val patss = maps (map (prep_props (set_mode mode_pattern ctxt') o snd)) raw_args; - val propp = unflat raw_args (props ~~ patss); - in (propp, ctxt') end; + val props = prep_props ctxt (maps (map fst) raw_args); + val props_ctxt = fold Variable.declare_term props ctxt; + val patss = maps (map (prep_props (set_mode mode_pattern props_ctxt) o snd)) raw_args; -fun gen_bind_propp mode parse_prop raw_args ctxt = - let - val (args, ctxt') = prep_propp mode parse_prop raw_args ctxt; - val propss = map (map fst) args; - val binds = (maps o maps) (simult_matches ctxt') args; - in ((propss, binds), bind_terms binds ctxt') end; + val propps = unflat raw_args (props ~~ patss); + val binds = (maps o maps) (simult_matches props_ctxt) propps; + in (map (map fst) propps, binds) end; in -val read_propp = prep_propp mode_default Syntax.read_props; -val cert_propp = prep_propp mode_default (map o cert_prop); - -val bind_propp = gen_bind_propp mode_default (map o cert_prop); -val bind_propp_cmd = gen_bind_propp mode_default Syntax.read_props; -val bind_propp_schematic = gen_bind_propp mode_schematic (map o cert_prop); -val bind_propp_schematic_cmd = gen_bind_propp mode_schematic Syntax.read_props; +val cert_propp = prep_propp (map o cert_prop); +val read_propp = prep_propp Syntax.read_props; end; @@ -1176,22 +1158,25 @@ local -fun gen_assms prepp exp args ctxt = +fun gen_assms prep_propp exp args ctxt = let - 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 (Thm.cterm_of ctxt)) propss ctxt1; + val (propss, binds) = prep_propp ctxt (map snd args); + val props = flat propss; in - ctxt2 - |> auto_bind_facts (flat propss) - |> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss) + ctxt + |> fold Variable.declare_term props + |> tap (Variable.warn_extra_tfrees ctxt) + |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss + |-> (fn premss => + auto_bind_facts props + #> bind_terms binds + #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss)) end; in -val add_assms = gen_assms bind_propp; -val add_assms_cmd = gen_assms bind_propp_cmd; +val add_assms = gen_assms cert_propp; +val add_assms_cmd = gen_assms read_propp; end;