1.1 --- a/src/Pure/Isar/specification.ML Tue Nov 07 21:28:14 2006 +0100
1.2 +++ b/src/Pure/Isar/specification.ML Tue Nov 07 21:30:03 2006 +0100
1.3 @@ -203,55 +203,60 @@
1.4
1.5 local
1.6
1.7 -fun conclusion prep_att (Element.Shows concl) =
1.8 +fun prep_statement prep_att prep_stmt elems concl ctxt =
1.9 + (case concl of
1.10 + Element.Shows shows =>
1.11 let
1.12 - fun mk_stmt propp ctxt =
1.13 - ((Attrib.map_specs prep_att (map fst concl ~~ propp), []),
1.14 - fold (fold (Variable.fix_frees o fst)) propp ctxt);
1.15 - in (([], map snd concl), mk_stmt) end
1.16 - | conclusion _ (Element.Obtains cases) =
1.17 + val (_, _, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
1.18 + val goal_ctxt = fold (fold (Variable.fix_frees o fst)) propp elems_ctxt;
1.19 + val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
1.20 + in ((stmt, []), goal_ctxt) end
1.21 + | Element.Obtains obtains =>
1.22 let
1.23 - val names =
1.24 - cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
1.25 - val elems = cases |> map (fn (_, (vars, _)) =>
1.26 - Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
1.27 - val concl = cases |> map (fn (_, (_, props)) => map (rpair []) props);
1.28 + val case_names = obtains |> map_index
1.29 + (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
1.30 + val constraints = obtains |> map (fn (_, (vars, _)) =>
1.31 + Locale.Elem (Element.Constrains
1.32 + (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))));
1.33
1.34 - fun mk_stmt propp ctxt =
1.35 - let
1.36 - val thesis =
1.37 - ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
1.38 - val atts = map Attrib.internal
1.39 - [RuleCases.consumes (~ (length cases)), RuleCases.case_names names];
1.40 + val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
1.41 + val (_, _, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
1.42 +
1.43 + val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
1.44
1.45 - fun assume_case ((name, (vars, _)), asms) ctxt' =
1.46 - let
1.47 - val xs = map fst vars;
1.48 - val props = map fst asms;
1.49 - val (parms, _) = ctxt'
1.50 - |> fold Variable.declare_term props
1.51 - |> fold_map ProofContext.inferred_param xs;
1.52 - val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
1.53 - in
1.54 - ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
1.55 - ctxt' |> Variable.fix_frees asm
1.56 - |> ProofContext.add_assms_i Assumption.assume_export
1.57 - [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
1.58 - |>> (fn [(_, [th])] => th)
1.59 - end;
1.60 - val (ths, ctxt') = ctxt
1.61 - |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
1.62 - |> fold_map assume_case (cases ~~ propp)
1.63 - |-> (fn ths =>
1.64 - ProofContext.note_thmss_i [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
1.65 - in (([(("", atts), [(thesis, [])])], ths), ctxt') end;
1.66 - in ((map Locale.Elem elems, concl), mk_stmt) end;
1.67 + fun assume_case ((name, (vars, _)), asms) ctxt' =
1.68 + let
1.69 + val xs = map fst vars;
1.70 + val props = map fst asms;
1.71 + val (parms, _) = ctxt'
1.72 + |> fold Variable.declare_term props
1.73 + |> fold_map ProofContext.inferred_param xs;
1.74 + val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
1.75 + in
1.76 + ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
1.77 + ctxt' |> Variable.fix_frees asm
1.78 + |> ProofContext.add_assms_i Assumption.assume_export
1.79 + [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
1.80 + |>> (fn [(_, [th])] => th)
1.81 + end;
1.82 +
1.83 + val atts = map Attrib.internal
1.84 + [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
1.85 + val stmt = [(("", atts), [(thesis, [])])];
1.86 +
1.87 + val (facts, goal_ctxt) = elems_ctxt
1.88 + |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
1.89 + |> fold_map assume_case (obtains ~~ propp)
1.90 + |-> (fn ths =>
1.91 + ProofContext.note_thmss_i [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
1.92 + in ((stmt, facts), goal_ctxt) end);
1.93
1.94 fun gen_theorem prep_att prep_stmt
1.95 kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 =
1.96 let
1.97 val _ = LocalTheory.assert lthy0;
1.98 val thy = ProofContext.theory_of lthy0;
1.99 + val attrib = prep_att thy;
1.100
1.101 val (loc, ctxt, lthy) =
1.102 (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
1.103 @@ -259,19 +264,13 @@
1.104 (SOME loc, ProofContext.init thy, LocalTheory.reinit lthy0)
1.105 | _ => (NONE, lthy0, lthy0));
1.106
1.107 - val attrib = prep_att thy;
1.108 - val elem_attrib = Locale.map_elem
1.109 + val elems = raw_elems |> (map o Locale.map_elem)
1.110 (Element.map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib});
1.111 -
1.112 - val ((concl_elems, concl), mk_stmt) = conclusion attrib raw_concl;
1.113 - val elems = map elem_attrib (raw_elems @ concl_elems);
1.114 -
1.115 - val (_, _, elems_ctxt, propp) = prep_stmt loc elems concl ctxt;
1.116 - val ((stmt, facts), goal_ctxt) = mk_stmt propp elems_ctxt;
1.117 + val ((stmt, facts), goal_ctxt) = prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
1.118
1.119 val k = if kind = "" then [] else [Attrib.kind kind];
1.120 val names = map (fst o fst) stmt;
1.121 - val attss = map (fn ((_, atts), _) => map attrib atts @ k) stmt;
1.122 + val attss = map (fn ((_, atts), _) => atts @ k) stmt;
1.123 val atts = map attrib raw_atts @ k;
1.124
1.125 fun after_qed' results goal_ctxt' =