abstract size function in hologic.ML
authorhaftmann
Thu May 17 19:49:17 2007 +0200 (2007-05-17)
changeset 2299402440636214f
parent 22993 838c66e760b5
child 22995 d8b4f2dc2b1d
abstract size function in hologic.ML
src/HOL/List.thy
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/hologic.ML
     1.1 --- a/src/HOL/List.thy	Thu May 17 19:49:16 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Thu May 17 19:49:17 2007 +0200
     1.3 @@ -320,7 +320,7 @@
     1.4      fun prove_neq() =
     1.5        let
     1.6          val Type(_,listT::_) = eqT;
     1.7 -        val size = Const("Nat.size", listT --> HOLogic.natT);
     1.8 +        val size = HOLogic.size_const listT;
     1.9          val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
    1.10          val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
    1.11          val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len
     2.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu May 17 19:49:16 2007 +0200
     2.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu May 17 19:49:17 2007 +0200
     2.3 @@ -399,14 +399,15 @@
     2.4      val descr' = flat descr;
     2.5      val recTs = get_rec_types descr' sorts;
     2.6  
     2.7 -    val size_name = "Nat.size";
     2.8 +    val Const (size_name, _) = HOLogic.size_const dummyT;
     2.9      val size_names = replicate (length (hd descr)) size_name @
    2.10        map (Sign.full_name thy1) (DatatypeProp.indexify_names
    2.11          (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
    2.12      val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
    2.13        (map (fn T => name_of_typ T ^ "_size") recTs));
    2.14  
    2.15 -    fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
    2.16 +    fun plus (t1, t2) =
    2.17 +      Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
    2.18  
    2.19      fun make_sizefun (_, cargs) =
    2.20        let
    2.21 @@ -423,11 +424,10 @@
    2.22  
    2.23      fun instance_size_class tyco thy =
    2.24        let
    2.25 -        val size_sort = ["Nat.size"];
    2.26          val n = Sign.arity_number thy tyco;
    2.27        in
    2.28          thy
    2.29 -        |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, size_sort)
    2.30 +        |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size])
    2.31               (ClassPackage.intro_classes_tac [])
    2.32        end
    2.33  
     3.1 --- a/src/HOL/Tools/datatype_package.ML	Thu May 17 19:49:16 2007 +0200
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu May 17 19:49:17 2007 +0200
     3.3 @@ -562,11 +562,10 @@
     3.4  
     3.5      fun instance_size_class tyco thy =
     3.6        let
     3.7 -        val size_sort = ["Nat.size"];
     3.8          val n = Sign.arity_number thy tyco;
     3.9        in
    3.10          thy
    3.11 -        |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, size_sort)
    3.12 +        |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size])
    3.13               (ClassPackage.intro_classes_tac [])
    3.14        end
    3.15  
     4.1 --- a/src/HOL/Tools/datatype_prop.ML	Thu May 17 19:49:16 2007 +0200
     4.2 +++ b/src/HOL/Tools/datatype_prop.ML	Thu May 17 19:49:17 2007 +0200
     4.3 @@ -353,26 +353,26 @@
     4.4  
     4.5  fun make_size descr sorts thy =
     4.6    let
     4.7 -    val descr' = List.concat descr;
     4.8 +    val descr' = flat descr;
     4.9      val recTs = get_rec_types descr' sorts;
    4.10  
    4.11 -    val size_name = "Nat.size";
    4.12 +    val Const (size_name, _) = HOLogic.size_const dummyT;
    4.13      val size_names = replicate (length (hd descr)) size_name @
    4.14        map (Sign.intern_const thy) (indexify_names
    4.15          (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
    4.16      val size_consts = map (fn (s, T) =>
    4.17        Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
    4.18  
    4.19 -    fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
    4.20 +    fun plus (t1, t2) = Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
    4.21  
    4.22      fun make_size_eqn size_const T (cname, cargs) =
    4.23        let
    4.24 -        val recs = List.filter is_rec_type cargs;
    4.25 +        val recs = filter is_rec_type cargs;
    4.26          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    4.27          val recTs = map (typ_of_dtyp descr' sorts) recs;
    4.28          val tnames = make_tnames Ts;
    4.29 -        val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
    4.30 -        val ts = map (fn ((r, s), T) => List.nth (size_consts, dest_DtRec r) $
    4.31 +        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
    4.32 +        val ts = map (fn ((r, s), T) => nth size_consts (dest_DtRec r) $
    4.33            Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
    4.34          val t = if ts = [] then HOLogic.zero else
    4.35            foldl1 plus (ts @ [HOLogic.Suc_zero])
     5.1 --- a/src/HOL/hologic.ML	Thu May 17 19:49:16 2007 +0200
     5.2 +++ b/src/HOL/hologic.ML	Thu May 17 19:49:17 2007 +0200
     5.3 @@ -73,6 +73,8 @@
     5.4    val Suc_zero: term
     5.5    val mk_nat: IntInf.int -> term
     5.6    val dest_nat: term -> IntInf.int
     5.7 +  val class_size: string
     5.8 +  val size_const: typ -> term
     5.9    val bitT: typ
    5.10    val B0_const: term
    5.11    val B1_const: term
    5.12 @@ -281,9 +283,9 @@
    5.13  
    5.14  val natT = Type ("nat", []);
    5.15  
    5.16 -val zero = Const ("HOL.zero", natT);
    5.17 +val zero = Const ("HOL.zero_class.zero", natT);
    5.18  
    5.19 -fun is_zero (Const ("HOL.zero", _)) = true
    5.20 +fun is_zero (Const ("HOL.zero_class.zero", _)) = true
    5.21    | is_zero _ = false;
    5.22  
    5.23  fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
    5.24 @@ -293,13 +295,23 @@
    5.25  
    5.26  val Suc_zero = mk_Suc zero;
    5.27  
    5.28 -fun mk_nat 0 = zero
    5.29 -  | mk_nat n = mk_Suc (mk_nat (IntInf.- (n, 1)));
    5.30 +fun mk_nat n =
    5.31 +  let
    5.32 +    fun mk 0 = zero
    5.33 +      | mk n = mk_Suc (mk (IntInf.- (n, 1)));
    5.34 +  in if IntInf.< (n, 0)
    5.35 +    then error "mk_nat: negative numeral"
    5.36 +    else mk n
    5.37 +  end;
    5.38  
    5.39 -fun dest_nat (Const ("HOL.zero", _)) = 0
    5.40 +fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
    5.41    | dest_nat (Const ("Suc", _) $ t) = IntInf.+ (dest_nat t, 1)
    5.42    | dest_nat t = raise TERM ("dest_nat", [t]);
    5.43  
    5.44 +val class_size = "Nat.size";
    5.45 +
    5.46 +fun size_const T = Const ("Nat.size_class.size", T --> natT);
    5.47 +
    5.48  
    5.49  (* bit *)
    5.50  
    5.51 @@ -337,7 +349,7 @@
    5.52        2 * dest_numeral bs + IntInf.fromInt (dest_bit b)
    5.53    | dest_numeral t = raise TERM ("dest_numeral", [t]);
    5.54  
    5.55 -fun number_of_const T = Const ("Numeral.number_of", intT --> T);
    5.56 +fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T);
    5.57  
    5.58  fun add_numerals_of (Const _) =
    5.59        I
    5.60 @@ -351,17 +363,18 @@
    5.61        add_numerals_of t
    5.62    | add_numerals_of (t as _ $ _) =
    5.63        case strip_comb t
    5.64 -       of (Const ("Numeral.number_of",
    5.65 +       of (Const ("Numeral.number_class.number_of",
    5.66             Type (_, [_, T])), ts) => fold (cons o rpair T) ts
    5.67          | (t', ts) => add_numerals_of t' #> fold add_numerals_of ts;
    5.68  
    5.69 -fun mk_number T 0 = Const ("HOL.zero", T)
    5.70 -  | mk_number T 1 = Const ("HOL.one", T)
    5.71 +fun mk_number T 0 = Const ("HOL.zero_class.zero", T)
    5.72 +  | mk_number T 1 = Const ("HOL.one_class.one", T)
    5.73    | mk_number T i = number_of_const T $ mk_numeral i;
    5.74  
    5.75 -fun dest_number (Const ("HOL.zero", T)) = (T, 0)
    5.76 -  | dest_number (Const ("HOL.one", T)) = (T, 1)
    5.77 -  | dest_number (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) = (T, dest_numeral t)
    5.78 +fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0)
    5.79 +  | dest_number (Const ("HOL.one_class.one", T)) = (T, 1)
    5.80 +  | dest_number (Const ("Numeral.number_class.number_of", Type ("fun", [_, T])) $ t) =
    5.81 +      (T, dest_numeral t)
    5.82    | dest_number t = raise TERM ("dest_number", [t]);
    5.83  
    5.84