# HG changeset patch # User haftmann # Date 1282212717 -7200 # Node ID 56965d8e4e1178c94ac3e206b6f754710922a98e # Parent 6c8806696bed2328bf7a360cb86b70bbb7151bb7 use HOLogic.boolT and @{typ bool} more pervasively diff -r 6c8806696bed -r 56965d8e4e11 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Thu Aug 19 11:19:24 2010 +0200 +++ b/src/HOL/Import/proof_kernel.ML Thu Aug 19 12:11:57 2010 +0200 @@ -388,7 +388,6 @@ val type_of = Term.type_of -val boolT = Type("bool",[]) val propT = Type("prop",[]) fun mk_defeq name rhs thy = @@ -1007,7 +1006,7 @@ local val th = thm "not_def" val thy = theory_of_thm th - val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},boolT-->propT))) + val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},HOLogic.boolT-->propT))) in val not_elim_thm = Thm.combination pp th end @@ -1773,7 +1772,7 @@ val (info',tm') = disamb_term_from info tm val th = norm_hyps th val ct = cterm_of thy tm' - val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name "Not"},boolT-->boolT) $ tm')) th + val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name "Not"},HOLogic.boolT-->HOLogic.boolT) $ tm')) th val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm' val res = HOLThm(rens_of info',res1) diff -r 6c8806696bed -r 56965d8e4e11 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Aug 19 11:19:24 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Aug 19 12:11:57 2010 +0200 @@ -52,7 +52,7 @@ fun transform_ho_typ (T as Type ("fun", _)) = let val (Ts, T') = strip_type T - in if T' = @{typ "bool"} then T else (Ts @ [T']) ---> HOLogic.boolT end + in if T' = HOLogic.boolT then T else (Ts @ [T']) ---> HOLogic.boolT end | transform_ho_typ t = t fun transform_ho_arg arg = diff -r 6c8806696bed -r 56965d8e4e11 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Thu Aug 19 11:19:24 2010 +0200 +++ b/src/HOL/Tools/cnf_funcs.ML Thu Aug 19 12:11:57 2010 +0200 @@ -98,7 +98,7 @@ | is_atom (Const (@{const_name "op &"}, _) $ _ $ _) = false | is_atom (Const (@{const_name "op |"}, _) $ _ $ _) = false | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _) = false - | is_atom (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false + | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false | is_atom (Const (@{const_name "Not"}, _) $ _) = false | is_atom _ = true; @@ -205,7 +205,7 @@ in make_nnf_imp OF [thm1, thm2] end - | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ x $ y) = + | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y) = let val thm1 = make_nnf_thm thy x val thm2 = make_nnf_thm thy (HOLogic.Not $ x) @@ -239,7 +239,7 @@ in make_nnf_not_imp OF [thm1, thm2] end - | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ x $ y)) = + | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) = let val thm1 = make_nnf_thm thy x val thm2 = make_nnf_thm thy (HOLogic.Not $ x) diff -r 6c8806696bed -r 56965d8e4e11 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Thu Aug 19 11:19:24 2010 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Thu Aug 19 12:11:57 2010 +0200 @@ -351,11 +351,11 @@ @{term "Pair :: term list option * (bool list * bool) => Random.seed => (term list option * (bool list * bool)) * Random.seed"}; fun mk_assms_report i = HOLogic.mk_prod (@{term "None :: term list option"}, - HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"} - (replicate i @{term "True"} @ replicate (length assms - i) @{term "False"}), - @{term "False"})) + HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT + (replicate i @{term True} @ replicate (length assms - i) @{term False}), + @{term False})) fun mk_concl_report b = - HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"} (replicate (length assms) @{term "True"}), + HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT (replicate (length assms) @{term True}), if b then @{term True} else @{term False}) val If = @{term "If :: bool => term list option * (bool list * bool) => term list option * (bool list * bool) => term list option * (bool list * bool)"} diff -r 6c8806696bed -r 56965d8e4e11 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Aug 19 11:19:24 2010 +0200 +++ b/src/HOL/Tools/refute.ML Thu Aug 19 12:11:57 2010 +0200 @@ -658,7 +658,7 @@ | Const (@{const_name Finite_Set.card}, _) => t | Const (@{const_name Finite_Set.finite}, _) => t | Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat}, - Type ("fun", [@{typ nat}, Type ("bool", [])])])) => t + Type ("fun", [@{typ nat}, @{typ bool}])])) => t | Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ nat}])])) => t | Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat}, @@ -835,7 +835,7 @@ | Const (@{const_name Finite_Set.finite}, T) => collect_type_axioms T axs | Const (@{const_name Orderings.less}, T as Type ("fun", [@{typ nat}, - Type ("fun", [@{typ nat}, Type ("bool", [])])])) => + Type ("fun", [@{typ nat}, @{typ bool}])])) => collect_type_axioms T axs | Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ nat}])])) => @@ -2653,7 +2653,7 @@ fun Finite_Set_card_interpreter thy model args t = case t of Const (@{const_name Finite_Set.card}, - Type ("fun", [Type ("fun", [T, Type ("bool", [])]), + Type ("fun", [Type ("fun", [T, @{typ bool}]), @{typ nat}])) => let (* interpretation -> int *) @@ -2685,7 +2685,7 @@ Leaf (replicate size_of_nat False) end val set_constants = - make_constants thy model (Type ("fun", [T, Type ("bool", [])])) + make_constants thy model (Type ("fun", [T, HOLogic.boolT])) in SOME (Node (map card set_constants), model, args) end @@ -2702,17 +2702,17 @@ fun Finite_Set_finite_interpreter thy model args t = case t of Const (@{const_name Finite_Set.finite}, - Type ("fun", [Type ("fun", [T, Type ("bool", [])]), - Type ("bool", [])])) $ _ => + Type ("fun", [Type ("fun", [T, @{typ bool}]), + @{typ bool}])) $ _ => (* we only consider finite models anyway, hence EVERY set is *) (* "finite" *) SOME (TT, model, args) | Const (@{const_name Finite_Set.finite}, - Type ("fun", [Type ("fun", [T, Type ("bool", [])]), - Type ("bool", [])])) => + Type ("fun", [Type ("fun", [T, @{typ bool}]), + @{typ bool}])) => let val size_of_set = - size_of_type thy model (Type ("fun", [T, Type ("bool", [])])) + size_of_type thy model (Type ("fun", [T, HOLogic.boolT])) in (* we only consider finite models anyway, hence EVERY set is *) (* "finite" *) @@ -2731,7 +2731,7 @@ fun Nat_less_interpreter thy model args t = case t of Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat}, - Type ("fun", [@{typ nat}, Type ("bool", [])])])) => + Type ("fun", [@{typ nat}, @{typ bool}])])) => let val size_of_nat = size_of_type thy model (@{typ nat}) (* the 'n'-th nat is not less than the first 'n' nats, while it *) @@ -2940,20 +2940,20 @@ fun lfp_interpreter thy model args t = case t of Const (@{const_name lfp}, Type ("fun", [Type ("fun", - [Type ("fun", [T, Type ("bool", [])]), - Type ("fun", [_, Type ("bool", [])])]), - Type ("fun", [_, Type ("bool", [])])])) => + [Type ("fun", [T, @{typ bool}]), + Type ("fun", [_, @{typ bool}])]), + Type ("fun", [_, @{typ bool}])])) => let val size_elem = size_of_type thy model T (* the universe (i.e. the set that contains every element) *) val i_univ = Node (replicate size_elem TT) (* all sets with elements from type 'T' *) val i_sets = - make_constants thy model (Type ("fun", [T, Type ("bool", [])])) + make_constants thy model (Type ("fun", [T, HOLogic.boolT])) (* all functions that map sets to sets *) val i_funs = make_constants thy model (Type ("fun", - [Type ("fun", [T, Type ("bool", [])]), - Type ("fun", [T, Type ("bool", [])])])) + [Type ("fun", [T, @{typ bool}]), + Type ("fun", [T, @{typ bool}])])) (* "lfp(f) == Inter({u. f(u) <= u})" *) (* interpretation * interpretation -> bool *) fun is_subset (Node subs, Node sups) = @@ -2995,20 +2995,20 @@ fun gfp_interpreter thy model args t = case t of Const (@{const_name gfp}, Type ("fun", [Type ("fun", - [Type ("fun", [T, Type ("bool", [])]), - Type ("fun", [_, Type ("bool", [])])]), - Type ("fun", [_, Type ("bool", [])])])) => + [Type ("fun", [T, @{typ bool}]), + Type ("fun", [_, @{typ bool}])]), + Type ("fun", [_, @{typ bool}])])) => let val size_elem = size_of_type thy model T (* the universe (i.e. the set that contains every element) *) val i_univ = Node (replicate size_elem TT) (* all sets with elements from type 'T' *) val i_sets = - make_constants thy model (Type ("fun", [T, Type ("bool", [])])) + make_constants thy model (Type ("fun", [T, HOLogic.boolT])) (* all functions that map sets to sets *) val i_funs = make_constants thy model (Type ("fun", - [Type ("fun", [T, Type ("bool", [])]), - Type ("fun", [T, Type ("bool", [])])])) + [Type ("fun", [T, HOLogic.boolT]), + Type ("fun", [T, HOLogic.boolT])])) (* "gfp(f) == Union({u. u <= f(u)})" *) (* interpretation * interpretation -> bool *) fun is_subset (Node subs, Node sups) =