# HG changeset patch # User haftmann # Date 1179424157 -7200 # Node ID 02440636214f8b67e693df17afa07559d93d3709 # Parent 838c66e760b550dbb39eec2830fb4bb0bae7aca1 abstract size function in hologic.ML diff -r 838c66e760b5 -r 02440636214f src/HOL/List.thy --- a/src/HOL/List.thy Thu May 17 19:49:16 2007 +0200 +++ b/src/HOL/List.thy Thu May 17 19:49:17 2007 +0200 @@ -320,7 +320,7 @@ fun prove_neq() = let val Type(_,listT::_) = eqT; - val size = Const("Nat.size", listT --> HOLogic.natT); + val size = HOLogic.size_const listT; val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs); val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len); val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len diff -r 838c66e760b5 -r 02440636214f src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Thu May 17 19:49:16 2007 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu May 17 19:49:17 2007 +0200 @@ -399,14 +399,15 @@ val descr' = flat descr; val recTs = get_rec_types descr' sorts; - val size_name = "Nat.size"; + val Const (size_name, _) = HOLogic.size_const dummyT; val size_names = replicate (length (hd descr)) size_name @ map (Sign.full_name thy1) (DatatypeProp.indexify_names (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs)))); val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names (map (fn T => name_of_typ T ^ "_size") recTs)); - fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2; + fun plus (t1, t2) = + Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; fun make_sizefun (_, cargs) = let @@ -423,11 +424,10 @@ fun instance_size_class tyco thy = let - val size_sort = ["Nat.size"]; val n = Sign.arity_number thy tyco; in thy - |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, size_sort) + |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size]) (ClassPackage.intro_classes_tac []) end diff -r 838c66e760b5 -r 02440636214f src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Thu May 17 19:49:16 2007 +0200 +++ b/src/HOL/Tools/datatype_package.ML Thu May 17 19:49:17 2007 +0200 @@ -562,11 +562,10 @@ fun instance_size_class tyco thy = let - val size_sort = ["Nat.size"]; val n = Sign.arity_number thy tyco; in thy - |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, size_sort) + |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size]) (ClassPackage.intro_classes_tac []) end diff -r 838c66e760b5 -r 02440636214f src/HOL/Tools/datatype_prop.ML --- a/src/HOL/Tools/datatype_prop.ML Thu May 17 19:49:16 2007 +0200 +++ b/src/HOL/Tools/datatype_prop.ML Thu May 17 19:49:17 2007 +0200 @@ -353,26 +353,26 @@ fun make_size descr sorts thy = let - val descr' = List.concat descr; + val descr' = flat descr; val recTs = get_rec_types descr' sorts; - val size_name = "Nat.size"; + val Const (size_name, _) = HOLogic.size_const dummyT; val size_names = replicate (length (hd descr)) size_name @ map (Sign.intern_const thy) (indexify_names (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs)))); val size_consts = map (fn (s, T) => Const (s, T --> HOLogic.natT)) (size_names ~~ recTs); - fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2; + fun plus (t1, t2) = Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; fun make_size_eqn size_const T (cname, cargs) = let - val recs = List.filter is_rec_type cargs; + val recs = filter is_rec_type cargs; val Ts = map (typ_of_dtyp descr' sorts) cargs; val recTs = map (typ_of_dtyp descr' sorts) recs; val tnames = make_tnames Ts; - val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs)); - val ts = map (fn ((r, s), T) => List.nth (size_consts, dest_DtRec r) $ + val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs)); + val ts = map (fn ((r, s), T) => nth size_consts (dest_DtRec r) $ Free (s, T)) (recs ~~ rec_tnames ~~ recTs); val t = if ts = [] then HOLogic.zero else foldl1 plus (ts @ [HOLogic.Suc_zero]) diff -r 838c66e760b5 -r 02440636214f src/HOL/hologic.ML --- a/src/HOL/hologic.ML Thu May 17 19:49:16 2007 +0200 +++ b/src/HOL/hologic.ML Thu May 17 19:49:17 2007 +0200 @@ -73,6 +73,8 @@ val Suc_zero: term val mk_nat: IntInf.int -> term val dest_nat: term -> IntInf.int + val class_size: string + val size_const: typ -> term val bitT: typ val B0_const: term val B1_const: term @@ -281,9 +283,9 @@ val natT = Type ("nat", []); -val zero = Const ("HOL.zero", natT); +val zero = Const ("HOL.zero_class.zero", natT); -fun is_zero (Const ("HOL.zero", _)) = true +fun is_zero (Const ("HOL.zero_class.zero", _)) = true | is_zero _ = false; fun mk_Suc t = Const ("Suc", natT --> natT) $ t; @@ -293,13 +295,23 @@ val Suc_zero = mk_Suc zero; -fun mk_nat 0 = zero - | mk_nat n = mk_Suc (mk_nat (IntInf.- (n, 1))); +fun mk_nat n = + let + fun mk 0 = zero + | mk n = mk_Suc (mk (IntInf.- (n, 1))); + in if IntInf.< (n, 0) + then error "mk_nat: negative numeral" + else mk n + end; -fun dest_nat (Const ("HOL.zero", _)) = 0 +fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0 | dest_nat (Const ("Suc", _) $ t) = IntInf.+ (dest_nat t, 1) | dest_nat t = raise TERM ("dest_nat", [t]); +val class_size = "Nat.size"; + +fun size_const T = Const ("Nat.size_class.size", T --> natT); + (* bit *) @@ -337,7 +349,7 @@ 2 * dest_numeral bs + IntInf.fromInt (dest_bit b) | dest_numeral t = raise TERM ("dest_numeral", [t]); -fun number_of_const T = Const ("Numeral.number_of", intT --> T); +fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T); fun add_numerals_of (Const _) = I @@ -351,17 +363,18 @@ add_numerals_of t | add_numerals_of (t as _ $ _) = case strip_comb t - of (Const ("Numeral.number_of", + of (Const ("Numeral.number_class.number_of", Type (_, [_, T])), ts) => fold (cons o rpair T) ts | (t', ts) => add_numerals_of t' #> fold add_numerals_of ts; -fun mk_number T 0 = Const ("HOL.zero", T) - | mk_number T 1 = Const ("HOL.one", T) +fun mk_number T 0 = Const ("HOL.zero_class.zero", T) + | mk_number T 1 = Const ("HOL.one_class.one", T) | mk_number T i = number_of_const T $ mk_numeral i; -fun dest_number (Const ("HOL.zero", T)) = (T, 0) - | dest_number (Const ("HOL.one", T)) = (T, 1) - | dest_number (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) = (T, dest_numeral t) +fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0) + | dest_number (Const ("HOL.one_class.one", T)) = (T, 1) + | dest_number (Const ("Numeral.number_class.number_of", Type ("fun", [_, T])) $ t) = + (T, dest_numeral t) | dest_number t = raise TERM ("dest_number", [t]);