# HG changeset patch # User wenzelm # Date 1321045747 -3600 # Node ID 98af01f897c98de7cf455063c18977bf7c70e673 # Parent 77c5b334a7ae607a151dd3e7d5b04c96d6ba2c37# Parent dcd02d1a25d7d495f5cb37d6e85be28167544c13 merged diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Fri Nov 11 22:05:18 2011 +0100 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Fri Nov 11 22:09:07 2011 +0100 @@ -100,12 +100,12 @@ val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio fun subtract_nat compfuns (_ : typ) = let - val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat} + val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat} in absdummy @{typ nat} (absdummy @{typ nat} (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $ (@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $ - Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $ + Predicate_Compile_Aux.mk_empty compfuns @{typ nat} $ Predicate_Compile_Aux.mk_single compfuns (@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1))) end @@ -118,7 +118,7 @@ fun enumerate_nats compfuns (_ : typ) = let val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"}) - val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat} + val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat} in absdummy @{typ nat} (absdummy @{typ nat} (Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Fri Nov 11 22:05:18 2011 +0100 +++ b/src/HOL/Numeral_Simprocs.thy Fri Nov 11 22:09:07 2011 +0100 @@ -202,6 +202,10 @@ use "Tools/nat_numeral_simprocs.ML" +simproc_setup nat_combine_numerals + ("(i::nat) + j" | "Suc (i + j)") = + {* fn phi => Nat_Numeral_Simprocs.combine_numerals *} + simproc_setup nateq_cancel_numerals ("(l::nat) + m = n" | "(l::nat) = m + n" | "(l::nat) * m = n" | "(l::nat) = m * n" | @@ -226,6 +230,46 @@ "Suc m - n" | "m - Suc n") = {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *} +simproc_setup nat_eq_cancel_numeral_factor + ("(l::nat) * m = n" | "(l::nat) = m * n") = + {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor *} + +simproc_setup nat_less_cancel_numeral_factor + ("(l::nat) * m < n" | "(l::nat) < m * n") = + {* fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor *} + +simproc_setup nat_le_cancel_numeral_factor + ("(l::nat) * m <= n" | "(l::nat) <= m * n") = + {* fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor *} + +simproc_setup nat_div_cancel_numeral_factor + ("((l::nat) * m) div n" | "(l::nat) div (m * n)") = + {* fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor *} + +simproc_setup nat_dvd_cancel_numeral_factor + ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = + {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor *} + +simproc_setup nat_eq_cancel_factor + ("(l::nat) * m = n" | "(l::nat) = m * n") = + {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *} + +simproc_setup nat_less_cancel_factor + ("(l::nat) * m < n" | "(l::nat) < m * n") = + {* fn phi => Nat_Numeral_Simprocs.less_cancel_factor *} + +simproc_setup nat_le_cancel_factor + ("(l::nat) * m <= n" | "(l::nat) <= m * n") = + {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *} + +simproc_setup nat_div_cancel_factor + ("((l::nat) * m) div n" | "(l::nat) div (m * n)") = + {* fn phi => Nat_Numeral_Simprocs.div_cancel_factor *} + +simproc_setup nat_dvd_cancel_factor + ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") = + {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *} + declaration {* K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]) #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @@ -247,7 +291,7 @@ @{simproc intless_cancel_numerals}, @{simproc intle_cancel_numerals}] #> Lin_Arith.add_simprocs - [Nat_Numeral_Simprocs.combine_numerals, + [@{simproc nat_combine_numerals}, @{simproc nateq_cancel_numerals}, @{simproc natless_cancel_numerals}, @{simproc natle_cancel_numerals}, diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Nov 11 22:05:18 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Nov 11 22:09:07 2011 +0100 @@ -66,23 +66,23 @@ val find_split_thm : theory -> term -> thm option (* datastructures and setup for generic compilation *) datatype compilation_funs = CompilationFuns of { - mk_predT : typ -> typ, - dest_predT : typ -> typ, - mk_bot : typ -> term, + mk_monadT : typ -> typ, + dest_monadT : typ -> typ, + mk_empty : typ -> term, mk_single : term -> term, mk_bind : term * term -> term, - mk_sup : term * term -> term, + mk_plus : term * term -> term, mk_if : term -> term, mk_iterate_upto : typ -> term * term * term -> term, mk_not : term -> term, mk_map : typ -> typ -> term -> term -> term }; - val mk_predT : compilation_funs -> typ -> typ - val dest_predT : compilation_funs -> typ -> typ - val mk_bot : compilation_funs -> typ -> term + val mk_monadT : compilation_funs -> typ -> typ + val dest_monadT : compilation_funs -> typ -> typ + val mk_empty : compilation_funs -> typ -> term val mk_single : compilation_funs -> term -> term val mk_bind : compilation_funs -> term * term -> term - val mk_sup : compilation_funs -> term * term -> term + val mk_plus : compilation_funs -> term * term -> term val mk_if : compilation_funs -> term -> term val mk_iterate_upto : compilation_funs -> typ -> term * term * term -> term val mk_not : compilation_funs -> term -> term @@ -699,24 +699,24 @@ (* datastructures and setup for generic compilation *) datatype compilation_funs = CompilationFuns of { - mk_predT : typ -> typ, - dest_predT : typ -> typ, - mk_bot : typ -> term, + mk_monadT : typ -> typ, + dest_monadT : typ -> typ, + mk_empty : typ -> term, mk_single : term -> term, mk_bind : term * term -> term, - mk_sup : term * term -> term, + mk_plus : term * term -> term, mk_if : term -> term, mk_iterate_upto : typ -> term * term * term -> term, mk_not : term -> term, mk_map : typ -> typ -> term -> term -> term }; -fun mk_predT (CompilationFuns funs) = #mk_predT funs -fun dest_predT (CompilationFuns funs) = #dest_predT funs -fun mk_bot (CompilationFuns funs) = #mk_bot funs +fun mk_monadT (CompilationFuns funs) = #mk_monadT funs +fun dest_monadT (CompilationFuns funs) = #dest_monadT funs +fun mk_empty (CompilationFuns funs) = #mk_empty funs fun mk_single (CompilationFuns funs) = #mk_single funs fun mk_bind (CompilationFuns funs) = #mk_bind funs -fun mk_sup (CompilationFuns funs) = #mk_sup funs +fun mk_plus (CompilationFuns funs) = #mk_plus funs fun mk_if (CompilationFuns funs) = #mk_if funs fun mk_iterate_upto (CompilationFuns funs) = #mk_iterate_upto funs fun mk_not (CompilationFuns funs) = #mk_not funs @@ -729,7 +729,7 @@ val Ts = binder_types T val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts in - inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs)) + inTs ---> (mk_monadT compfuns (HOLogic.mk_tupleT outTs)) end; (* Different options for compiler *) diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Fri Nov 11 22:05:18 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Fri Nov 11 22:09:07 2011 +0100 @@ -7,16 +7,16 @@ structure Predicate_Comp_Funs = struct -fun mk_predT T = Type (@{type_name Predicate.pred}, [T]) +fun mk_monadT T = Type (@{type_name Predicate.pred}, [T]) -fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T - | dest_predT T = raise TYPE ("dest_predT", [T], []); +fun dest_monadT (Type (@{type_name Predicate.pred}, [T])) = T + | dest_monadT T = raise TYPE ("dest_monadT", [T], []); -fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T); +fun mk_empty T = Const (@{const_name Orderings.bot}, mk_monadT T); fun mk_single t = let val T = fastype_of t - in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end; + in Const(@{const_name Predicate.single}, T --> mk_monadT T) $ t end; fun mk_bind (x, f) = let val T as Type ("fun", [_, U]) = fastype_of f @@ -24,42 +24,42 @@ Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f end; -val mk_sup = HOLogic.mk_binop @{const_name sup}; +val mk_plus = HOLogic.mk_binop @{const_name sup}; fun mk_if cond = Const (@{const_name Predicate.if_pred}, - HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond; + HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond; fun mk_iterate_upto T (f, from, to) = list_comb (Const (@{const_name Code_Numeral.iterate_upto}, - [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_predT T), + [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_monadT T), [f, from, to]) fun mk_not t = let - val T = mk_predT HOLogic.unitT + val T = mk_monadT HOLogic.unitT in Const (@{const_name Predicate.not_pred}, T --> T) $ t end fun mk_Enum f = let val T as Type ("fun", [T', _]) = fastype_of f in - Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f + Const (@{const_name Predicate.Pred}, T --> mk_monadT T') $ f end; fun mk_Eval (f, x) = let - val T = dest_predT (fastype_of f) + val T = dest_monadT (fastype_of f) in - Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x + Const (@{const_name Predicate.eval}, mk_monadT T --> T --> HOLogic.boolT) $ f $ x end; fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x) fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map}, - (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp; + (T1 --> T2) --> mk_monadT T1 --> mk_monadT T2) $ tf $ tp; val compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot, - mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty, + mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}; end; @@ -67,16 +67,16 @@ structure CPS_Comp_Funs = struct -fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"} +fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"} -fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T - | dest_predT T = raise TYPE ("dest_predT", [T], []); +fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T + | dest_monadT T = raise TYPE ("dest_monadT", [T], []); -fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_predT T); +fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_monadT T); fun mk_single t = let val T = fastype_of t - in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_predT T) $ t end; + in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_monadT T) $ t end; fun mk_bind (x, f) = let val T as Type ("fun", [_, U]) = fastype_of f @@ -84,16 +84,16 @@ Const (@{const_name Quickcheck_Exhaustive.cps_bind}, fastype_of x --> T --> U) $ x $ f end; -val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus}; +val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus}; fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if}, - HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond; + HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond; fun mk_iterate_upto T (f, from, to) = error "not implemented yet" fun mk_not t = let - val T = mk_predT HOLogic.unitT + val T = mk_monadT HOLogic.unitT in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end fun mk_Enum f = error "not implemented" @@ -105,8 +105,8 @@ fun mk_map T1 T2 tf tp = error "not implemented" val compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot, - mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty, + mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}; end; @@ -114,16 +114,16 @@ structure Pos_Bounded_CPS_Comp_Funs = struct -fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"} +fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"} -fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T - | dest_predT T = raise TYPE ("dest_predT", [T], []); +fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T + | dest_monadT T = raise TYPE ("dest_monadT", [T], []); -fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_predT T); +fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T); fun mk_single t = let val T = fastype_of t - in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_predT T) $ t end; + in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_monadT T) $ t end; fun mk_bind (x, f) = let val T as Type ("fun", [_, U]) = fastype_of f @@ -131,10 +131,10 @@ Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f end; -val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus}; +val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus}; fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if}, - HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond; + HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond; fun mk_iterate_upto T (f, from, to) = error "not implemented yet" @@ -143,7 +143,7 @@ val nT = @{typ "(unit Quickcheck_Exhaustive.unknown => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued) => code_numeral => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"} - val T = mk_predT HOLogic.unitT + val T = mk_monadT HOLogic.unitT in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end fun mk_Enum f = error "not implemented" @@ -155,8 +155,8 @@ fun mk_map T1 T2 tf tp = error "not implemented" val compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot, - mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty, + mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}; end; @@ -164,21 +164,21 @@ structure Neg_Bounded_CPS_Comp_Funs = struct -fun mk_predT T = +fun mk_monadT T = (Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]) --> @{typ "Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}) --> @{typ "code_numeral => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"} -fun dest_predT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]), +fun dest_monadT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]), @{typ "term list Quickcheck_Exhaustive.three_valued"}]), @{typ "code_numeral => term list Quickcheck_Exhaustive.three_valued"}])) = T - | dest_predT T = raise TYPE ("dest_predT", [T], []); + | dest_monadT T = raise TYPE ("dest_monadT", [T], []); -fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_predT T); +fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_monadT T); fun mk_single t = let val T = fastype_of t - in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_predT T) $ t end; + in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_monadT T) $ t end; fun mk_bind (x, f) = let val T as Type ("fun", [_, U]) = fastype_of f @@ -186,16 +186,16 @@ Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f end; -val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus}; +val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus}; fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if}, - HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond; + HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond; fun mk_iterate_upto T (f, from, to) = error "not implemented" fun mk_not t = let - val T = mk_predT HOLogic.unitT + val T = mk_monadT HOLogic.unitT val pT = @{typ "(unit => Code_Evaluation.term list option) => code_numeral => Code_Evaluation.term list option"} in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end @@ -208,8 +208,8 @@ fun mk_map T1 T2 tf tp = error "not implemented" val compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot, - mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty, + mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}; end; @@ -219,13 +219,13 @@ struct fun mk_randompredT T = - @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_predT T, @{typ Random.seed}) + @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_monadT T, @{typ Random.seed}) fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod}, [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []); -fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T) +fun mk_empty T = Const(@{const_name Quickcheck.empty}, mk_randompredT T) fun mk_single t = let @@ -241,7 +241,7 @@ Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f end -val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union} +val mk_plus = HOLogic.mk_binop @{const_name Quickcheck.union} fun mk_if cond = Const (@{const_name Quickcheck.if_randompred}, HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond; @@ -260,8 +260,8 @@ (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp val compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_randompredT, dest_predT = dest_randompredT, - mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_randompredT, dest_monadT = dest_randompredT, + mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}; end; @@ -276,7 +276,7 @@ Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []); -fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T); +fun mk_empty T = Const (@{const_name DSequence.empty}, mk_dseqT T); fun mk_single t = let val T = fastype_of t @@ -288,7 +288,7 @@ Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f end; -val mk_sup = HOLogic.mk_binop @{const_name DSequence.union}; +val mk_plus = HOLogic.mk_binop @{const_name DSequence.union}; fun mk_if cond = Const (@{const_name DSequence.if_seq}, HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond; @@ -302,8 +302,8 @@ (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp val compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_dseqT, dest_predT = dest_dseqT, - mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_dseqT, dest_monadT = dest_dseqT, + mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} end; @@ -318,7 +318,7 @@ Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []); -fun mk_bot T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T); +fun mk_empty T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T); fun mk_single t = let @@ -339,7 +339,7 @@ Const (@{const_name New_DSequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f end; -val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.pos_union}; +val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.pos_union}; fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq}, HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond; @@ -358,13 +358,13 @@ (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_pos_dseqT, dest_predT = dest_pos_dseqT, - mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT, + mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_pos_dseqT, dest_predT = dest_pos_dseqT, - mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT, + mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} end; @@ -379,7 +379,7 @@ Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []); -fun mk_bot T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T); +fun mk_empty T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T); fun mk_single t = let @@ -400,7 +400,7 @@ Const (@{const_name New_DSequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f end; -val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.neg_union}; +val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.neg_union}; fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq}, HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond; @@ -419,13 +419,13 @@ (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_neg_dseqT, dest_predT = dest_neg_dseqT, - mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT, + mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_neg_dseqT, dest_predT = dest_neg_dseqT, - mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT, + mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} end; @@ -442,7 +442,7 @@ Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); -fun mk_bot T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T); +fun mk_empty T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T); fun mk_single t = let @@ -463,7 +463,7 @@ Const (@{const_name New_Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f end; -val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union}; +val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union}; fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq}, HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond; @@ -487,13 +487,13 @@ (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT, - mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT, + mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT, - mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT, + mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} end; @@ -511,7 +511,7 @@ [Type (@{type_name Option.option}, [T])])])])])])) = T | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); -fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T); +fun mk_empty T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T); fun mk_single t = let @@ -532,7 +532,7 @@ Const (@{const_name New_Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f end; -val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union}; +val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union}; fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq}, HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond; @@ -554,13 +554,13 @@ (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT, - mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT, + mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT, - mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT, + mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} end; @@ -577,7 +577,7 @@ Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); -fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T); +fun mk_empty T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T); fun mk_single t = let @@ -591,7 +591,7 @@ Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f end; -val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union}; +val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.union}; fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq}, HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond; @@ -607,8 +607,8 @@ (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp val compfuns = Predicate_Compile_Aux.CompilationFuns - {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT, - mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, + {mk_monadT = mk_random_dseqT, dest_monadT = dest_random_dseqT, + mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if, mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} end; diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 11 22:05:18 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 11 22:09:07 2011 +0100 @@ -312,11 +312,11 @@ let val [depth] = additional_arguments val (_, Ts) = split_modeT mode (binder_types T) - val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts) + val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts) val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T') in if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"}) - $ mk_bot compfuns (dest_predT compfuns T') + $ mk_empty compfuns (dest_monadT compfuns T') $ compilation end, transform_additional_arguments = @@ -337,7 +337,7 @@ mk_random = (fn T => fn additional_arguments => list_comb (Const(@{const_name Quickcheck.iter}, [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> - Predicate_Comp_Funs.mk_predT T), additional_arguments)), + Predicate_Comp_Funs.mk_monadT T), additional_arguments)), modify_funT = (fn T => let val (Ts, U) = strip_type T @@ -363,7 +363,7 @@ mk_random = (fn T => fn additional_arguments => list_comb (Const(@{const_name Quickcheck.iter}, [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> - Predicate_Comp_Funs.mk_predT T), tl additional_arguments)), + Predicate_Comp_Funs.mk_monadT T), tl additional_arguments)), modify_funT = (fn T => let val (Ts, U) = strip_type T @@ -383,11 +383,11 @@ val depth = hd (additional_arguments) val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode (binder_types T) - val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts) + val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts) val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T') in if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"}) - $ mk_bot compfuns (dest_predT compfuns T') + $ mk_empty compfuns (dest_monadT compfuns T') $ compilation end, transform_additional_arguments = @@ -658,7 +658,7 @@ val name' = singleton (Name.variant_list (name :: names)) "y"; val T = HOLogic.mk_tupleT (map fastype_of out_ts); val U = fastype_of success_t; - val U' = dest_predT compfuns U; + val U' = dest_monadT compfuns U; val v = Free (name, T); val v' = Free (name', T); in @@ -667,8 +667,8 @@ if null eqs'' then success_t else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $ foldr1 HOLogic.mk_conj eqs'' $ success_t $ - mk_bot compfuns U'), - (v', mk_bot compfuns U')]) + mk_empty compfuns U'), + (v', mk_empty compfuns U')]) end; fun string_of_tderiv ctxt (t, deriv) = @@ -928,7 +928,7 @@ compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments inp (in_ts', out_ts') moded_ps' end - in SOME (foldr1 (mk_sup compfuns) (map compile_clause' moded_clauses)) end + in SOME (foldr1 (mk_plus compfuns) (map compile_clause' moded_clauses)) end | compile_switch_tree all_vs ctxt_eqs (Node ((position, switched_clauses), left_clauses)) = let val (i, is) = argument_position_of mode position @@ -943,18 +943,18 @@ val args = map2 (curry Free) argnames Ts val pattern = list_comb (Const (c, T), args) val ctxt_eqs' = (inp_var, pattern) :: ctxt_eqs - val compilation = the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs)) + val compilation = the_default (mk_empty compfuns (HOLogic.mk_tupleT outTs)) (compile_switch_tree (argnames @ x :: all_vs) ctxt_eqs' switched) in (pattern, compilation) end val switch = Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var ((map compile_single_case switched_clauses) @ - [(xt, mk_bot compfuns (HOLogic.mk_tupleT outTs))]) + [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))]) in case compile_switch_tree all_vs ctxt_eqs left_clauses of NONE => SOME switch - | SOME left_comp => SOME (mk_sup compfuns (switch, left_comp)) + | SOME left_comp => SOME (mk_plus compfuns (switch, left_comp)) end in compile_switch_tree all_vs [] switch_tree @@ -978,11 +978,11 @@ (all_vs @ param_vs) val compfuns = Comp_Mod.compfuns compilation_modifiers fun is_param_type (T as Type ("fun",[_ , T'])) = - is_some (try (dest_predT compfuns) T) orelse is_param_type T' - | is_param_type T = is_some (try (dest_predT compfuns) T) + is_some (try (dest_monadT compfuns) T) orelse is_param_type T' + | is_param_type T = is_some (try (dest_monadT compfuns) T) val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode (binder_types T) - val predT = mk_predT compfuns (HOLogic.mk_tupleT outTs) + val predT = mk_monadT compfuns (HOLogic.mk_tupleT outTs) val funT = Comp_Mod.funT_of compilation_modifiers mode T val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod) (fn T => fn (param_vs, names) => @@ -998,7 +998,7 @@ val param_modes = param_vs ~~ ho_arg_modes_of mode val compilation = if detect_switches options then - the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs)) + the_default (mk_empty compfuns (HOLogic.mk_tupleT outTs)) (compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode in_ts' outTs (mk_switch_tree ctxt mode moded_cls)) else @@ -1010,9 +1010,9 @@ in Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments (if null cl_ts then - mk_bot compfuns (HOLogic.mk_tupleT outTs) + mk_empty compfuns (HOLogic.mk_tupleT outTs) else - foldr1 (mk_sup compfuns) cl_ts) + foldr1 (mk_plus compfuns) cl_ts) end val fun_const = Const (function_name_of (Comp_Mod.compilation compilation_modifiers) @@ -1341,7 +1341,7 @@ (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) val args = map2 (curry Free) arg_names Ts val predfun = Const (function_name_of Pred ctxt predname full_mode, - Ts ---> Predicate_Comp_Funs.mk_predT @{typ unit}) + Ts ---> Predicate_Comp_Funs.mk_monadT @{typ unit}) val rhs = @{term Predicate.holds} $ (list_comb (predfun, args)) val eq_term = HOLogic.mk_Trueprop (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs)) @@ -1833,7 +1833,7 @@ val (_, outargs) = split_mode (head_mode_of deriv) all_args val t_pred = compile_expr comp_modifiers ctxt (body, deriv) [] additional_arguments; - val T_pred = dest_predT compfuns (fastype_of t_pred) + val T_pred = dest_monadT compfuns (fastype_of t_pred) val arrange = HOLogic.tupled_lambda (HOLogic.mk_tuple outargs) output in if null outargs then t_pred else mk_map compfuns T_pred T_compr arrange t_pred @@ -1876,7 +1876,7 @@ | New_Pos_Random_DSeq => [] | Pos_Generator_DSeq => [] val t = analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes options t_compr; - val T = dest_predT compfuns (fastype_of t); + val T = dest_monadT compfuns (fastype_of t); val t' = if stats andalso compilation = New_Pos_Random_DSeq then mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ code_numeral})) diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Nov 11 22:05:18 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Nov 11 22:09:07 2011 +0100 @@ -186,23 +186,23 @@ set_no_higher_order_predicate (!no_higher_order_predicate) (if !debug then debug_options else options) -val mk_predT = Predicate_Compile_Aux.mk_predT Predicate_Comp_Funs.compfuns +val mk_predT = Predicate_Compile_Aux.mk_monadT Predicate_Comp_Funs.compfuns val mk_return' = Predicate_Compile_Aux.mk_single Predicate_Comp_Funs.compfuns val mk_bind' = Predicate_Compile_Aux.mk_bind Predicate_Comp_Funs.compfuns -val mk_randompredT = Predicate_Compile_Aux.mk_predT RandomPredCompFuns.compfuns +val mk_randompredT = Predicate_Compile_Aux.mk_monadT RandomPredCompFuns.compfuns val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns val mk_bind = Predicate_Compile_Aux.mk_bind RandomPredCompFuns.compfuns val mk_new_randompredT = - Predicate_Compile_Aux.mk_predT New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns + Predicate_Compile_Aux.mk_monadT New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns val mk_new_return = Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns val mk_new_bind = Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns val mk_new_dseqT = - Predicate_Compile_Aux.mk_predT New_Pos_DSequence_CompFuns.depth_unlimited_compfuns + Predicate_Compile_Aux.mk_monadT New_Pos_DSequence_CompFuns.depth_unlimited_compfuns val mk_gen_return = Predicate_Compile_Aux.mk_single New_Pos_DSequence_CompFuns.depth_unlimited_compfuns val mk_gen_bind = @@ -210,7 +210,7 @@ val mk_cpsT = - Predicate_Compile_Aux.mk_predT Pos_Bounded_CPS_Comp_Funs.compfuns + Predicate_Compile_Aux.mk_monadT Pos_Bounded_CPS_Comp_Funs.compfuns val mk_cps_return = Predicate_Compile_Aux.mk_single Pos_Bounded_CPS_Comp_Funs.compfuns val mk_cps_bind = diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/abel_cancel.ML --- a/src/HOL/Tools/abel_cancel.ML Fri Nov 11 22:05:18 2011 +0100 +++ b/src/HOL/Tools/abel_cancel.ML Fri Nov 11 22:09:07 2011 +0100 @@ -24,6 +24,7 @@ add_atoms pos x #> add_atoms (not pos) y | add_atoms pos (Const (@{const_name Groups.uminus}, _) $ x) = add_atoms (not pos) x + | add_atoms pos (Const (@{const_name Groups.zero}, _)) = I | add_atoms pos x = cons (pos, x); fun atoms t = add_atoms true t []; diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Fri Nov 11 22:05:18 2011 +0100 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Fri Nov 11 22:09:07 2011 +0100 @@ -5,16 +5,24 @@ signature NAT_NUMERAL_SIMPROCS = sig - val combine_numerals: simproc + val combine_numerals: simpset -> cterm -> thm option val eq_cancel_numerals: simpset -> cterm -> thm option val less_cancel_numerals: simpset -> cterm -> thm option val le_cancel_numerals: simpset -> cterm -> thm option val diff_cancel_numerals: simpset -> cterm -> thm option - val cancel_factors: simproc list - val cancel_numeral_factors: simproc list + val eq_cancel_numeral_factor: simpset -> cterm -> thm option + val less_cancel_numeral_factor: simpset -> cterm -> thm option + val le_cancel_numeral_factor: simpset -> cterm -> thm option + val div_cancel_numeral_factor: simpset -> cterm -> thm option + val dvd_cancel_numeral_factor: simpset -> cterm -> thm option + val eq_cancel_factor: simpset -> cterm -> thm option + val less_cancel_factor: simpset -> cterm -> thm option + val le_cancel_factor: simpset -> cterm -> thm option + val div_cancel_factor: simpset -> cterm -> thm option + val dvd_cancel_factor: simpset -> cterm -> thm option end; -structure Nat_Numeral_Simprocs = +structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS = struct (*Maps n to #n for n = 0, 1, 2*) @@ -232,9 +240,7 @@ structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); -val combine_numerals = - Numeral_Simprocs.prep_simproc @{theory} - ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc); +fun combine_numerals ss ct = CombineNumerals.proc ss (term_of ct) (*** Applying CancelNumeralFactorFun ***) @@ -298,24 +304,11 @@ val neg_exchanges = true ) -val cancel_numeral_factors = - map (Numeral_Simprocs.prep_simproc @{theory}) - [("nateq_cancel_numeral_factors", - ["(l::nat) * m = n", "(l::nat) = m * n"], - K EqCancelNumeralFactor.proc), - ("natless_cancel_numeral_factors", - ["(l::nat) * m < n", "(l::nat) < m * n"], - K LessCancelNumeralFactor.proc), - ("natle_cancel_numeral_factors", - ["(l::nat) * m <= n", "(l::nat) <= m * n"], - K LeCancelNumeralFactor.proc), - ("natdiv_cancel_numeral_factors", - ["((l::nat) * m) div n", "(l::nat) div (m * n)"], - K DivCancelNumeralFactor.proc), - ("natdvd_cancel_numeral_factors", - ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], - K DvdCancelNumeralFactor.proc)]; - +fun eq_cancel_numeral_factor ss ct = EqCancelNumeralFactor.proc ss (term_of ct) +fun less_cancel_numeral_factor ss ct = LessCancelNumeralFactor.proc ss (term_of ct) +fun le_cancel_numeral_factor ss ct = LeCancelNumeralFactor.proc ss (term_of ct) +fun div_cancel_numeral_factor ss ct = DivCancelNumeralFactor.proc ss (term_of ct) +fun dvd_cancel_numeral_factor ss ct = DvdCancelNumeralFactor.proc ss (term_of ct) (*** Applying ExtractCommonTermFun ***) @@ -387,72 +380,10 @@ fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj} ); -val cancel_factor = - map (Numeral_Simprocs.prep_simproc @{theory}) - [("nat_eq_cancel_factor", - ["(l::nat) * m = n", "(l::nat) = m * n"], - K EqCancelFactor.proc), - ("nat_less_cancel_factor", - ["(l::nat) * m < n", "(l::nat) < m * n"], - K LessCancelFactor.proc), - ("nat_le_cancel_factor", - ["(l::nat) * m <= n", "(l::nat) <= m * n"], - K LeCancelFactor.proc), - ("nat_divide_cancel_factor", - ["((l::nat) * m) div n", "(l::nat) div (m * n)"], - K DivideCancelFactor.proc), - ("nat_dvd_cancel_factor", - ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], - K DvdCancelFactor.proc)]; +fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct) +fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct) +fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct) +fun div_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct) +fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct) end; - - -Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; -Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors; -Addsimprocs Nat_Numeral_Simprocs.cancel_factor; - - -(*examples: -print_depth 22; -set timing; -set simp_trace; -fun test s = (Goal s; by (Simp_tac 1)); - -(*combine_numerals*) -test "k + 3*k = (u::nat)"; -test "Suc (i + 3) = u"; -test "Suc (i + j + 3 + k) = u"; -test "k + j + 3*k + j = (u::nat)"; -test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)"; -test "(2*n*m) + (3*(m*n)) = (u::nat)"; -(*negative numerals: FAIL*) -test "Suc (i + j + -3 + k) = u"; - -(*cancel_numeral_factors*) -test "9*x = 12 * (y::nat)"; -test "(9*x) div (12 * (y::nat)) = z"; -test "9*x < 12 * (y::nat)"; -test "9*x <= 12 * (y::nat)"; - -(*cancel_factor*) -test "x*k = k*(y::nat)"; -test "k = k*(y::nat)"; -test "a*(b*c) = (b::nat)"; -test "a*(b*c) = d*(b::nat)*(x*a)"; - -test "x*k < k*(y::nat)"; -test "k < k*(y::nat)"; -test "a*(b*c) < (b::nat)"; -test "a*(b*c) < d*(b::nat)*(x*a)"; - -test "x*k <= k*(y::nat)"; -test "k <= k*(y::nat)"; -test "a*(b*c) <= (b::nat)"; -test "a*(b*c) <= d*(b::nat)*(x*a)"; - -test "(x*k) div (k*(y::nat)) = (uu::nat)"; -test "(k) div (k*(y::nat)) = (uu::nat)"; -test "(a*(b*c)) div ((b::nat)) = (uu::nat)"; -test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)"; -*) diff -r dcd02d1a25d7 -r 98af01f897c9 src/HOL/ex/Simproc_Tests.thy --- a/src/HOL/ex/Simproc_Tests.thy Fri Nov 11 22:05:18 2011 +0100 +++ b/src/HOL/ex/Simproc_Tests.thy Fri Nov 11 22:09:07 2011 +0100 @@ -5,7 +5,7 @@ header {* Testing of arithmetic simprocs *} theory Simproc_Tests -imports Rat +imports Main begin text {* @@ -21,12 +21,33 @@ fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1) *} +subsection {* Abelian group cancellation simprocs *} + +notepad begin + fix a b c u :: "'a::ab_group_add" + { + assume "(a + 0) - (b + 0) = u" have "(a + c) - (b + c) = u" + by (tactic {* test [@{simproc abel_cancel_sum}] *}) fact + next + assume "a + 0 = b + 0" have "a + c = b + c" + by (tactic {* test [@{simproc abel_cancel_relation}] *}) fact + } +end +(* TODO: more tests for Groups.abel_cancel_{sum,relation} *) subsection {* @{text int_combine_numerals} *} +(* FIXME: int_combine_numerals often unnecessarily regroups addition +and rewrites subtraction to negation. Ideally it should behave more +like Groups.abel_cancel_sum, preserving the shape of terms as much as +possible. *) + notepad begin fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring" { + assume "a + - b = u" have "(a + c) - (b + c) = u" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next assume "10 + (2 * l + oo) = uu" have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu" by (tactic {* test [@{simproc int_combine_numerals}] *}) fact @@ -324,10 +345,11 @@ } end -lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z" +lemma + fixes a b c d x y z :: "'a::linordered_field_inverse_zero" + shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z" oops -- "FIXME: need simproc to cover this case" - subsection {* @{text linordered_ring_less_cancel_factor} *} notepad begin @@ -384,16 +406,49 @@ } end -lemma "2/3 * (x::rat) + x / 3 = uu" +lemma + fixes x :: "'a::{linordered_field_inverse_zero,number_ring}" + shows "2/3 * x + x / 3 = uu" apply (tactic {* test [@{simproc field_combine_numerals}] *})? oops -- "FIXME: test fails" +subsection {* @{text nat_combine_numerals} *} + +notepad begin + fix i j k m n u :: nat + { + assume "4*k = u" have "k + 3*k = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + next + assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + next + assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + next + assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + next + assume "6 * Suc 0 + (5 * (i * j) + (4 * k + i)) = u" + have "Suc (j*i + i + k + 5 + 3*k + i*j*4) = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + next + assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u" + by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact + } +end + +(*negative numerals: FAIL*) +lemma "Suc (i + j + -3 + k) = u" +apply (tactic {* test [@{simproc nat_combine_numerals}] *})? +oops + subsection {* @{text nateq_cancel_numerals} *} notepad begin fix i j k l oo u uu vv w y z w' y' z' :: "nat" { - assume "Suc 0 * u = 0" have "2*u = (u::nat)" + assume "Suc 0 * u = 0" have "2*u = u" by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact next assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)" @@ -560,4 +615,101 @@ } end +subsection {* Factor-cancellation simprocs for type @{typ nat} *} + +text {* @{text nat_eq_cancel_factor}, @{text nat_less_cancel_factor}, +@{text nat_le_cancel_factor}, @{text nat_divide_cancel_factor}, and +@{text nat_dvd_cancel_factor}. *} + +notepad begin + fix a b c d k x y uu :: nat + { + assume "k = 0 \ x = y" have "x*k = k*y" + by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact + next + assume "k = 0 \ Suc 0 = y" have "k = k*y" + by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact + next + assume "b = 0 \ a * c = Suc 0" have "a*(b*c) = b" + by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact + next + assume "a = 0 \ b = 0 \ c = d * x" have "a*(b*c) = d*b*(x*a)" + by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact + next + assume "0 < k \ x < y" have "x*k < k*y" + by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact + next + assume "0 < k \ Suc 0 < y" have "k < k*y" + by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact + next + assume "0 < b \ a * c < Suc 0" have "a*(b*c) < b" + by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact + next + assume "0 < a \ 0 < b \ c < d * x" have "a*(b*c) < d*b*(x*a)" + by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact + next + assume "0 < k \ x \ y" have "x*k \ k*y" + by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact + next + assume "0 < k \ Suc 0 \ y" have "k \ k*y" + by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact + next + assume "0 < b \ a * c \ Suc 0" have "a*(b*c) \ b" + by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact + next + assume "0 < a \ 0 < b \ c \ d * x" have "a*(b*c) \ d*b*(x*a)" + by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact + next + assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu" + by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact + next + assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu" + by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact + next + assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu" + by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact + next + assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" + have "(a*(b*c)) div (d*b*(x*a)) = uu" + by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact + next + assume "k = 0 \ x dvd y" have "(x*k) dvd (k*y)" + by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact + next + assume "k = 0 \ Suc 0 dvd y" have "k dvd (k*y)" + by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact + next + assume "b = 0 \ a * c dvd Suc 0" have "(a*(b*c)) dvd (b)" + by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact + next + assume "b = 0 \ Suc 0 dvd a * c" have "b dvd (a*(b*c))" + by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact + next + assume "a = 0 \ b = 0 \ c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))" + by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact + } end + +subsection {* Numeral-cancellation simprocs for type @{typ nat} *} + +notepad begin + fix x y z :: nat + { + assume "3 * x = 4 * y" have "9*x = 12 * y" + by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact + next + assume "3 * x < 4 * y" have "9*x < 12 * y" + by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact + next + assume "3 * x \ 4 * y" have "9*x \ 12 * y" + by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact + next + assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z" + by (tactic {* test [@{simproc nat_div_cancel_numeral_factor}] *}) fact + next + assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)" + by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact + } +end + +end