complex goal statements: misc cleanup;
authorwenzelm
Tue Nov 07 21:30:03 2006 +0100 (2006-11-07)
changeset 21236890fafbcf8b0
parent 21235 674e2731b519
child 21237 b803f9870e97
complex goal statements: misc cleanup;
src/Pure/Isar/specification.ML
     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' =