Added mk_int and mk_list.
authorberghofe
Mon Dec 16 13:43:11 2002 +0100 (2002-12-16)
changeset 13755a9bb54a3cfb7
parent 13754 021cf00435a9
child 13756 41abb61ecce9
Added mk_int and mk_list.
src/HOL/Main.thy
src/HOL/hologic.ML
     1.1 --- a/src/HOL/Main.thy	Mon Dec 16 11:18:35 2002 +0100
     1.2 +++ b/src/HOL/Main.thy	Mon Dec 16 13:43:11 2002 +0100
     1.3 @@ -39,7 +39,12 @@
     1.4  
     1.5    "wfrec"   ("wf'_rec?")
     1.6  
     1.7 -ML {* fun wf_rec f x = f (wf_rec f) x; *}
     1.8 +ML {*
     1.9 +fun wf_rec f x = f (wf_rec f) x;
    1.10 +
    1.11 +val term_of_list = HOLogic.mk_list;
    1.12 +val term_of_int = HOLogic.mk_int;
    1.13 +*}
    1.14  
    1.15  lemma [code]: "((n::nat) < 0) = False" by simp
    1.16  declare less_Suc_eq [code]
     2.1 --- a/src/HOL/hologic.ML	Mon Dec 16 11:18:35 2002 +0100
     2.2 +++ b/src/HOL/hologic.ML	Mon Dec 16 13:43:11 2002 +0100
     2.3 @@ -66,6 +66,7 @@
     2.4    val mk_nat: int -> term
     2.5    val dest_nat: term -> int
     2.6    val intT: typ
     2.7 +  val mk_int: int -> term
     2.8    val realT: typ
     2.9    val binT: typ
    2.10    val pls_const: term
    2.11 @@ -74,7 +75,8 @@
    2.12    val number_of_const: typ -> term
    2.13    val int_of: int list -> int
    2.14    val dest_binum: term -> int
    2.15 -  val mk_bin   : int -> term
    2.16 +  val mk_bin: int -> term
    2.17 +  val mk_list: ('a -> term) -> typ -> 'a list -> term
    2.18  end;
    2.19  
    2.20  
    2.21 @@ -271,11 +273,6 @@
    2.22    | dest_nat t = raise TERM ("dest_nat", [t]);
    2.23  
    2.24  
    2.25 -val intT = Type ("IntDef.int", []);
    2.26 -
    2.27 -val realT = Type("RealDef.real",[]);
    2.28 -
    2.29 -
    2.30  (* binary numerals *)
    2.31  
    2.32  val binT = Type ("Numeral.bin", []);
    2.33 @@ -316,4 +313,24 @@
    2.34        | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
    2.35      in term_of (bin_of n) end;
    2.36  
    2.37 +
    2.38 +(* int *)
    2.39 +
    2.40 +val intT = Type ("IntDef.int", []);
    2.41 +
    2.42 +fun mk_int i = number_of_const intT $ mk_bin i;
    2.43 +
    2.44 +
    2.45 +(* real *)
    2.46 +
    2.47 +val realT = Type("RealDef.real", []);
    2.48 +
    2.49 +
    2.50 +(* list *)
    2.51 +
    2.52 +fun mk_list f T [] = Const ("List.list.Nil", Type ("List.list", [T]))
    2.53 +  | mk_list f T (x :: xs) = Const ("List.list.Cons",
    2.54 +      T --> Type ("List.list", [T]) --> Type ("List.list", [T])) $ f x $
    2.55 +        mk_list f T xs;
    2.56 +
    2.57  end;