theorem statements: incorporate Obtain.statement, tuned;
authorwenzelm
Tue Nov 07 19:39:52 2006 +0100 (2006-11-07)
changeset 21230abfdce60b371
parent 21229 9c96c1ec235f
child 21231 df149b8c86b8
theorem statements: incorporate Obtain.statement, tuned;
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Tue Nov 07 19:39:50 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Tue Nov 07 19:39:52 2006 +0100
     1.3 @@ -51,6 +51,7 @@
     1.4  structure Specification: SPECIFICATION =
     1.5  struct
     1.6  
     1.7 +
     1.8  (* diagnostics *)
     1.9  
    1.10  val quiet_mode = ref false;
    1.11 @@ -172,7 +173,7 @@
    1.12  val abbreviation_i = gen_abbrevs cert_specification;
    1.13  
    1.14  
    1.15 -(* const syntax *)
    1.16 +(* notation *)
    1.17  
    1.18  fun gen_notation prep_const mode args lthy =
    1.19    lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
    1.20 @@ -198,21 +199,53 @@
    1.21  val theorems_i = gen_theorems (K I) (K I);
    1.22  
    1.23  
    1.24 -(* goal statements *)
    1.25 +(* complex goal statements *)
    1.26  
    1.27  local
    1.28  
    1.29 -val global_goal =
    1.30 -  Proof.global_goal (K (K ())) Attrib.attribute_i ProofContext.bind_propp_schematic_i;
    1.31 +fun conclusion prep_att (Element.Shows concl) =
    1.32 +      let
    1.33 +        fun mk_stmt propp ctxt =
    1.34 +          ((Attrib.map_specs prep_att (map fst concl ~~ propp), []),
    1.35 +            fold (fold (Variable.fix_frees o fst)) propp ctxt);
    1.36 +      in (([], map snd concl), mk_stmt) end
    1.37 +  | conclusion _ (Element.Obtains cases) =
    1.38 +      let
    1.39 +        val names =
    1.40 +          cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
    1.41 +        val elems = cases |> map (fn (_, (vars, _)) =>
    1.42 +          Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
    1.43 +        val concl = cases |> map (fn (_, (_, props)) => map (rpair []) props);
    1.44  
    1.45 -fun mk_shows prep_att stmt ctxt =
    1.46 -  ((Attrib.map_specs prep_att stmt, []), fold (fold (Variable.fix_frees o fst) o snd) stmt ctxt);
    1.47 +        fun mk_stmt propp ctxt =
    1.48 +          let
    1.49 +            val thesis =
    1.50 +              ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
    1.51 +            val atts = map Attrib.internal
    1.52 +              [RuleCases.consumes (~ (length cases)), RuleCases.case_names names];
    1.53  
    1.54 -fun conclusion prep_att (Element.Shows concl) = (([], concl), mk_shows prep_att)
    1.55 -  | conclusion _ (Element.Obtains cases) =
    1.56 -      apfst (apfst (map Locale.Elem)) (Obtain.statement cases);
    1.57 -
    1.58 -in
    1.59 +            fun assume_case ((name, (vars, _)), asms) ctxt' =
    1.60 +              let
    1.61 +                val xs = map fst vars;
    1.62 +                val props = map fst asms;
    1.63 +                val (parms, _) = ctxt'
    1.64 +                  |> fold Variable.declare_term props
    1.65 +                  |> fold_map ProofContext.inferred_param xs;
    1.66 +                val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
    1.67 +              in
    1.68 +                ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
    1.69 +                ctxt' |> Variable.fix_frees asm
    1.70 +                |> ProofContext.add_assms_i Assumption.assume_export
    1.71 +                  [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
    1.72 +                |>> (fn [(_, [th])] => th)
    1.73 +              end;
    1.74 +            val (ths, ctxt') = ctxt
    1.75 +              |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
    1.76 +              |> fold_map assume_case (cases ~~ propp)
    1.77 +              |-> (fn ths =>
    1.78 +                ProofContext.note_thmss_i [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
    1.79 +          in (([(("", atts), [(thesis, [])])], ths), ctxt') end;
    1.80 +      in ((map Locale.Elem elems, concl), mk_stmt) end;
    1.81  
    1.82  fun gen_theorem prep_att prep_stmt
    1.83      kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 =
    1.84 @@ -223,8 +256,7 @@
    1.85      val (loc, ctxt, lthy) =
    1.86        (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
    1.87          (SOME loc, true) => (* workaround non-modularity of in/includes *)  (* FIXME *)
    1.88 -          (warning "Re-initializing theory target for locale inclusion";
    1.89 -            (SOME loc, ProofContext.init thy, LocalTheory.reinit lthy0))
    1.90 +          (SOME loc, ProofContext.init thy, LocalTheory.reinit lthy0)
    1.91        | _ => (NONE, lthy0, lthy0));
    1.92  
    1.93      val attrib = prep_att thy;
    1.94 @@ -234,12 +266,12 @@
    1.95      val ((concl_elems, concl), mk_stmt) = conclusion attrib raw_concl;
    1.96      val elems = map elem_attrib (raw_elems @ concl_elems);
    1.97  
    1.98 -    val (_, _, elems_ctxt, propp) = prep_stmt loc elems (map snd concl) ctxt;
    1.99 -    val ((stmt, facts), goal_ctxt) = mk_stmt (map (apsnd (K []) o fst) concl ~~ propp) elems_ctxt;
   1.100 +    val (_, _, elems_ctxt, propp) = prep_stmt loc elems concl ctxt;
   1.101 +    val ((stmt, facts), goal_ctxt) = mk_stmt propp elems_ctxt;
   1.102  
   1.103      val k = if kind = "" then [] else [Attrib.kind kind];
   1.104 -    val names = map (fst o fst) concl;
   1.105 -    val attss = map (fn ((_, atts), _) => map attrib atts @ k) concl;
   1.106 +    val names = map (fst o fst) stmt;
   1.107 +    val attss = map (fn ((_, atts), _) => map attrib atts @ k) stmt;
   1.108      val atts = map attrib raw_atts @ k;
   1.109  
   1.110      fun after_qed' results goal_ctxt' =
   1.111 @@ -254,10 +286,13 @@
   1.112        end;
   1.113    in
   1.114      goal_ctxt
   1.115 -    |> global_goal kind before_qed after_qed' NONE (name, []) stmt
   1.116 +    |> Proof.global_goal (K (K ())) Attrib.attribute_i ProofContext.bind_propp_schematic_i
   1.117 +      kind before_qed after_qed' NONE (name, []) stmt
   1.118      |> Proof.refine_insert facts
   1.119    end;
   1.120  
   1.121 +in
   1.122 +
   1.123  val theorem = gen_theorem Attrib.intern_src Locale.read_context_statement_i;
   1.124  val theorem_i = gen_theorem (K I) Locale.cert_context_statement;
   1.125