46 val _ = thm_antiq "thms" Attrib.thms; |
46 val _ = thm_antiq "thms" Attrib.thms; |
47 |
47 |
48 |
48 |
49 (* ad-hoc goals *) |
49 (* ad-hoc goals *) |
50 |
50 |
|
51 val and_ = Args.$$$ "and"; |
51 val by = Args.$$$ "by"; |
52 val by = Args.$$$ "by"; |
52 val goal = Scan.unless (Scan.lift by) Args.prop; |
53 val goal = Scan.unless (by || and_) Args.name; |
53 |
54 |
54 val _ = ML_Context.add_antiq "lemma" |
55 val _ = ML_Context.add_antiq "lemma" |
55 (fn pos => Args.context -- Args.mode "open" -- Scan.repeat1 goal -- |
56 (fn pos => Args.context -- Args.mode "open" -- |
56 Scan.lift (by |-- Method.parse -- Scan.option Method.parse) >> |
57 Scan.lift (OuterParse.and_list1 (Scan.repeat1 goal) -- |
57 (fn (((ctxt, is_open), props), methods) => fn {struct_name, background} => |
58 (by |-- Method.parse -- Scan.option Method.parse)) >> |
|
59 (fn ((ctxt, is_open), (raw_propss, methods)) => fn {struct_name, background} => |
58 let |
60 let |
|
61 val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; |
59 val i = serial (); |
62 val i = serial (); |
60 val prep_result = |
63 val prep_result = |
61 Goal.norm_result #> Thm.default_position pos #> not is_open ? Thm.close_derivation; |
64 Goal.norm_result #> Thm.default_position pos #> not is_open ? Thm.close_derivation; |
62 fun after_qed [res] goal_ctxt = |
65 fun after_qed res goal_ctxt = |
63 put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt res)) goal_ctxt; |
66 put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt; |
64 val ctxt' = ctxt |
67 val ctxt' = ctxt |
65 |> Proof.theorem_i NONE after_qed [map (rpair []) props] |
68 |> Proof.theorem_i NONE after_qed propss |
66 |> Proof.global_terminal_proof methods; |
69 |> Proof.global_terminal_proof methods; |
67 val (a, background') = background |
70 val (a, background') = background |
68 |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i); |
71 |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i); |
69 val ml = (thm_bind (if length props = 1 then "thm" else "thms") a i, struct_name ^ "." ^ a); |
72 val ml = |
|
73 (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, |
|
74 struct_name ^ "." ^ a); |
70 in (K ml, background') end)); |
75 in (K ml, background') end)); |
71 |
76 |
72 end; |
77 end; |
73 |
78 |