balanced conjunctions;
authorwenzelm
Tue Jun 19 23:15:47 2007 +0200 (2007-06-19 ago)
changeset 23421c9007fc4a646
parent 23420 6f60a90e52e5
child 23422 4a368c087f58
balanced conjunctions;
added split_defined (from conjunction.ML);
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Tue Jun 19 23:15:43 2007 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Jun 19 23:15:47 2007 +0200
     1.3 @@ -263,6 +263,20 @@
     1.4  
     1.5  (** class definitions **)
     1.6  
     1.7 +fun split_defined n eq =
     1.8 +  let
     1.9 +    val intro =
    1.10 +      (eq RS Drule.equal_elim_rule2)
    1.11 +      |> Conjunction.curry_balanced n
    1.12 +      |> n = 0 ? Thm.eq_assumption 1;
    1.13 +    val dests =
    1.14 +      if n = 0 then []
    1.15 +      else
    1.16 +        (eq RS Drule.equal_elim_rule1)
    1.17 +        |> BalancedTree.dest (fn th =>
    1.18 +          (th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n;
    1.19 +  in (intro, dests) end;
    1.20 +
    1.21  fun define_class (bclass, raw_super) params raw_specs thy =
    1.22    let
    1.23      val ctxt = ProofContext.init thy;
    1.24 @@ -297,14 +311,14 @@
    1.25  
    1.26      val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss;
    1.27      val class_eq =
    1.28 -      Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_list conjs);
    1.29 +      Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_balanced conjs);
    1.30  
    1.31      val ([def], def_thy) =
    1.32        thy
    1.33        |> Sign.primitive_class (bclass, super)
    1.34        |> PureThy.add_defs_i false [((Thm.def_name bconst, class_eq), [])];
    1.35      val (raw_intro, (raw_classrel, raw_axioms)) =
    1.36 -      (Conjunction.split_defined (length conjs) def) ||> chop (length super);
    1.37 +      split_defined (length conjs) def ||> chop (length super);
    1.38  
    1.39  
    1.40      (* facts *)