author wenzelm Tue Nov 21 18:07:31 2006 +0100 (2006-11-21) changeset 21435 883337ea2f3b parent 21434 944f80576be0 child 21436 5313a4cc3823
LocalTheory.axioms/notes/defs: proper kind;
simplified Proof.theorem(_i);
```     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 21 18:07:30 2006 +0100
1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 21 18:07:31 2006 +0100
1.3 @@ -38,6 +38,8 @@
1.4  open FundefLib
1.5  open FundefCommon
1.6
1.7 +val note_theorem = LocalTheory.note Thm.theoremK
1.8 +
1.9  fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
1.10      let val (xs, ys) = split_list ps
1.11      in xs ~~ f ys end
1.12 @@ -49,13 +51,16 @@
1.13      let
1.14        val fnames = map (fst o fst) fixes
1.15
1.16 -      val (saved_spec_psimps, lthy) = fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) lthy
1.17 +      val (saved_spec_psimps, lthy) =
1.18 +        fold_map (fold_map note_theorem) (restore_spec_structure psimps spec) lthy
1.19        val saved_psimps = flat (map snd (flat saved_spec_psimps))
1.20
1.21        val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
1.22
1.23        fun add_for_f fname psimps =
1.24 -          LocalTheory.note ((NameSpace.qualified fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd
1.25 +        note_theorem
1.26 +          ((NameSpace.qualified fname label, Attrib.internal Simplifier.simp_add :: moreatts),
1.27 +            psimps) #> snd
1.28      in
1.29        (saved_psimps,
1.30         fold2 add_for_f fnames psimps_by_f lthy)
1.31 @@ -73,10 +78,10 @@
1.32        val (((psimps', pinducts'), (_, [termination'])), lthy) =
1.33            lthy
1.35 -            ||>> PROFILE "adding pinduct" (LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
1.36 -            ||>> PROFILE "adding termination" (LocalTheory.note ((qualify "termination", []), [termination]))
1.37 -            ||> (snd o PROFILE "adding cases" (LocalTheory.note ((qualify "cases", []), [cases])))
1.38 -            ||> (snd o PROFILE "adding domintros" (LocalTheory.note ((qualify "domintros", []), domintros)))
1.39 +            ||>> PROFILE "adding pinduct" (note_theorem ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
1.40 +            ||>> PROFILE "adding termination" (note_theorem ((qualify "termination", []), [termination]))
1.41 +            ||> (snd o PROFILE "adding cases" (note_theorem ((qualify "cases", []), [cases])))
1.42 +            ||> (snd o PROFILE "adding domintros" (note_theorem ((qualify "domintros", []), domintros)))
1.43
1.44        val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
1.45                                    pinducts=snd pinducts', termination=termination', f=f, R=R }
1.46 @@ -121,7 +126,7 @@
1.47        val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
1.48      in
1.49        (name, lthy
1.50 -         |> Proof.theorem_i PureThy.internalK NONE afterqed [[(goal, [])]]
1.51 +         |> Proof.theorem_i NONE afterqed [[(goal, [])]]
1.52           |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
1.53      end
1.54
1.55 @@ -145,7 +150,7 @@
1.56      in
1.57          lthy
1.58            |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd
1.59 -          |> PROFILE "adding tinduct" (LocalTheory.note ((qualify "induct", []), tinduct)) |> snd
1.60 +          |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
1.61      end
1.62
1.63
1.64 @@ -159,11 +164,10 @@
1.65          val goal = FundefTermination.mk_total_termination_goal f R
1.66      in
1.67        lthy
1.68 -        |> ProofContext.note_thmss_i [(("termination",
1.69 +        |> ProofContext.note_thmss_i "" [(("termination",
1.70                                          [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
1.71          |> set_termination_rule termination
1.72 -        |> Proof.theorem_i PureThy.internalK NONE
1.73 -                           (total_termination_afterqed name data) [[(goal, [])]]
1.74 +        |> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]]
1.75      end
1.76
1.77
```
```     2.1 --- a/src/Pure/Isar/specification.ML	Tue Nov 21 18:07:30 2006 +0100
2.2 +++ b/src/Pure/Isar/specification.ML	Tue Nov 21 18:07:31 2006 +0100
2.3 @@ -102,7 +102,7 @@
2.4      val ((consts, axioms), lthy') = lthy
2.5        |> LocalTheory.consts spec_frees vars
2.6        ||> fold (fold Variable.auto_fixes o snd) specs   (* FIXME !? *)
2.7 -      ||>> LocalTheory.axioms specs;
2.8 +      ||>> LocalTheory.axioms Thm.axiomK specs;
2.9
2.10      (* FIXME generic target!? *)
2.11      val hs = map (Term.head_of o #2 o Logic.dest_equals o Thm.prop_of o #2) consts;
2.12 @@ -130,9 +130,9 @@
2.13            else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
2.14          val ((lhs, (_, th)), lthy2) = lthy1
2.15  (*          |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs));  FIXME *)
2.16 -          |> LocalTheory.def ((x, mx), ((name, []), rhs));
2.17 +          |> LocalTheory.def Thm.definitionK ((x, mx), ((name, []), rhs));
2.18          val ((b, [th']), lthy3) = lthy2
2.19 -          |> LocalTheory.note ((name, atts), [prove lthy2 th]);
2.20 +          |> LocalTheory.note Thm.definitionK ((name, atts), [prove lthy2 th]);
2.21        in (((x, T), (lhs, (b, th'))), LocalTheory.restore lthy3) end;
2.22
2.23      val ((cs, defs), lthy') = lthy |> fold_map define args |>> split_list;
2.24 @@ -185,12 +185,11 @@
2.25
2.26  fun gen_theorems prep_thms prep_att kind raw_facts lthy =
2.27    let
2.28 -    val k = if kind = "" then [] else [Attrib.kind kind];
2.29      val attrib = prep_att (ProofContext.theory_of lthy);
2.30      val facts = raw_facts |> map (fn ((name, atts), bs) =>
2.31        ((name, map attrib atts),
2.32 -        bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts @ k))));
2.33 -    val (res, lthy') = lthy |> LocalTheory.notes facts;
2.34 +        bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts))));
2.35 +    val (res, lthy') = lthy |> LocalTheory.notes kind facts;
2.36      val _ = present_results' lthy' kind res;
2.37    in (res, lthy') end;
2.38
2.39 @@ -246,8 +245,8 @@
2.40          val (facts, goal_ctxt) = elems_ctxt
2.41            |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
2.42            |> fold_map assume_case (obtains ~~ propp)
2.43 -          |-> (fn ths =>
2.44 -            ProofContext.note_thmss_i [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
2.45 +          |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
2.46 +                [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
2.47        in ((stmt, facts), goal_ctxt) end);
2.48
2.49  fun gen_theorem prep_att prep_stmt
2.50 @@ -255,7 +254,6 @@
2.51    let
2.52      val _ = LocalTheory.assert lthy0;
2.53      val thy = ProofContext.theory_of lthy0;
2.54 -    val attrib = prep_att thy;
2.55
2.56      val (loc, ctxt, lthy) =
2.57        (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
2.58 @@ -263,28 +261,26 @@
2.59            (SOME loc, ProofContext.init thy, LocalTheory.restore lthy0)
2.60        | _ => (NONE, lthy0, lthy0));
2.61
2.62 +    val attrib = prep_att thy;
2.63 +    val atts = map attrib raw_atts;
2.64 +
2.65      val elems = raw_elems |> (map o Locale.map_elem)
2.66        (Element.map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib});
2.67      val ((stmt, facts), goal_ctxt) = prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
2.68
2.69 -    val k = if kind = "" then [] else [Attrib.kind kind];
2.70 -    val names = map (fst o fst) stmt;
2.71 -    val attss = map (fn ((_, atts), _) => atts @ k) stmt;
2.72 -    val atts = map attrib raw_atts @ k;
2.73 -
2.74      fun after_qed' results goal_ctxt' =
2.75        let val results' = burrow (ProofContext.export_standard goal_ctxt' lthy) results in
2.76          lthy
2.77 -        |> LocalTheory.notes ((names ~~ attss) ~~ map (fn ths => [(ths, [])]) results')
2.78 +        |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
2.79          |> (fn (res, lthy') =>
2.80            (present_results lthy' ((kind, name), res);
2.81 -            if name = "" andalso null raw_atts then lthy'
2.82 -            else #2 (LocalTheory.notes [((name, atts), [(maps #2 res, [])])] lthy')))
2.83 +            if name = "" andalso null atts then lthy'
2.84 +            else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy')))
2.85          |> after_qed results'
2.86        end;
2.87    in
2.88      goal_ctxt
2.89 -    |> Proof.theorem_i kind before_qed after_qed' (map snd stmt)
2.90 +    |> Proof.theorem_i before_qed after_qed' (map snd stmt)
2.91      |> Proof.refine_insert facts
2.92    end;
2.93
```