# HG changeset patch # User nipkow # Date 1323066671 -3600 # Node ID b5db02fa9536b1cf2650a6a865f8a32b03c0be3a # Parent 17100f4ce0b5d7977d4570337592f7bd0610723a# Parent f8723843c29e6357db3214da172805ad24d0958f merged diff -r f8723843c29e -r b5db02fa9536 NEWS --- a/NEWS Mon Dec 05 07:31:00 2011 +0100 +++ b/NEWS Mon Dec 05 07:31:11 2011 +0100 @@ -53,6 +53,9 @@ *** HOL *** +* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, use +theory HOL/Library/Nat_Bijection instead. + * Session HOL-Word: Discontinued many redundant theorems specific to type 'a word. INCOMPATIBILITY, use the corresponding generic theorems instead. diff -r f8723843c29e -r b5db02fa9536 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Dec 05 07:31:00 2011 +0100 +++ b/src/HOL/IsaMakefile Mon Dec 05 07:31:11 2011 +0100 @@ -438,7 +438,7 @@ Library/Code_Real_Approx_By_Float.thy \ Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \ Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy \ - Library/Convex.thy Library/Countable.thy Library/Diagonalize.thy \ + Library/Convex.thy Library/Countable.thy \ Library/Dlist.thy Library/Dlist_Cset.thy Library/Efficient_Nat.thy \ Library/Eval_Witness.thy Library/Executable_Set.thy \ Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy \ diff -r f8723843c29e -r b5db02fa9536 src/HOL/Library/Diagonalize.thy --- a/src/HOL/Library/Diagonalize.thy Mon Dec 05 07:31:00 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,149 +0,0 @@ -(* Author: Florian Haftmann, TU Muenchen *) - -header {* A constructive version of Cantor's first diagonalization argument. *} - -theory Diagonalize -imports Main -begin - -subsection {* Summation from @{text "0"} to @{text "n"} *} - -definition sum :: "nat \ nat" where - "sum n = n * Suc n div 2" - -lemma sum_0: - "sum 0 = 0" - unfolding sum_def by simp - -lemma sum_Suc: - "sum (Suc n) = Suc n + sum n" - unfolding sum_def by simp - -lemma sum2: - "2 * sum n = n * Suc n" -proof - - have "2 dvd n * Suc n" - proof (cases "2 dvd n") - case True then show ?thesis by simp - next - case False then have "2 dvd Suc n" by arith - then show ?thesis by (simp del: mult_Suc_right) - qed - then have "n * Suc n div 2 * 2 = n * Suc n" - by (rule dvd_div_mult_self [of "2::nat"]) - then show ?thesis by (simp add: sum_def) -qed - -lemma sum_strict_mono: - "strict_mono sum" -proof (rule strict_monoI) - fix m n :: nat - assume "m < n" - then have "m * Suc m < n * Suc n" by (intro mult_strict_mono) simp_all - then have "2 * sum m < 2 * sum n" by (simp add: sum2) - then show "sum m < sum n" by auto -qed - -lemma sum_not_less_self: - "n \ sum n" -proof - - have "2 * n \ n * Suc n" by auto - with sum2 have "2 * n \ 2 * sum n" by simp - then show ?thesis by simp -qed - -lemma sum_rest_aux: - assumes "q \ n" - assumes "sum m \ sum n + q" - shows "m \ n" -proof (rule ccontr) - assume "\ m \ n" - then have "n < m" by simp - then have "m \ Suc n" by simp - then have "m = m - Suc n + Suc n" by simp - then have "m = Suc (n + (m - Suc n))" by simp - then obtain r where "m = Suc (n + r)" by auto - with `sum m \ sum n + q` have "sum (Suc (n + r)) \ sum n + q" by simp - then have "sum (n + r) + Suc (n + r) \ sum n + q" unfolding sum_Suc by simp - with `m = Suc (n + r)` have "sum (n + r) + m \ sum n + q" by simp - have "sum n \ sum (n + r)" unfolding strict_mono_less_eq [OF sum_strict_mono] by simp - moreover from `q \ n` `n < m` have "q < m" by simp - ultimately have "sum n + q < sum (n + r) + m" by auto - with `sum (n + r) + m \ sum n + q` show False - by auto -qed - -lemma sum_rest: - assumes "q \ n" - shows "sum m \ sum n + q \ m \ n" -using assms apply (auto intro: sum_rest_aux) -apply (simp add: strict_mono_less_eq [OF sum_strict_mono, symmetric, of m n]) -done - - -subsection {* Diagonalization: an injective embedding of two @{typ nat}s to one @{typ nat} *} - -definition diagonalize :: "nat \ nat \ nat" where - "diagonalize m n = sum (m + n) + m" - -lemma diagonalize_inject: - assumes "diagonalize a b = diagonalize c d" - shows "a = c" and "b = d" -proof - - from assms have diageq: "sum (a + b) + a = sum (c + d) + c" - by (simp add: diagonalize_def) - have "a + b = c + d \ a + b \ Suc (c + d) \ c + d \ Suc (a + b)" by arith - then have "a = c \ b = d" - proof (elim disjE) - assume sumeq: "a + b = c + d" - then have "a = c" using diageq by auto - moreover from sumeq this have "b = d" by auto - ultimately show ?thesis .. - next - assume "a + b \ Suc (c + d)" - with strict_mono_less_eq [OF sum_strict_mono] - have "sum (a + b) \ sum (Suc (c + d))" by simp - with diageq show ?thesis by (simp add: sum_Suc) - next - assume "c + d \ Suc (a + b)" - with strict_mono_less_eq [OF sum_strict_mono] - have "sum (c + d) \ sum (Suc (a + b))" by simp - with diageq show ?thesis by (simp add: sum_Suc) - qed - then show "a = c" and "b = d" by auto -qed - - -subsection {* The reverse diagonalization: reconstruction a pair of @{typ nat}s from one @{typ nat} *} - -text {* The inverse of the @{const sum} function *} - -definition tupelize :: "nat \ nat \ nat" where - "tupelize q = (let d = Max {d. sum d \ q}; m = q - sum d - in (m, d - m))" - -lemma tupelize_diagonalize: - "tupelize (diagonalize m n) = (m, n)" -proof - - from sum_rest - have "\r. sum r \ sum (m + n) + m \ r \ m + n" by simp - then have "Max {d. sum d \ (sum (m + n) + m)} = m + n" - by (auto intro: Max_eqI) - then show ?thesis - by (simp add: tupelize_def diagonalize_def) -qed - -lemma snd_tupelize: - "snd (tupelize n) \ n" -proof - - have "sum 0 \ n" by (simp add: sum_0) - then have "Max {m \ nat. sum m \ n} \ Max {m \ nat. m \ n}" - by (intro Max_mono [of "{m. sum m \ n}" "{m. m \ n}"]) - (auto intro: Max_mono order_trans sum_not_less_self) - also have "Max {m \ nat. m \ n} \ n" - by (subst Max_le_iff) auto - finally have "Max {m. sum m \ n} \ n" . - then show ?thesis by (simp add: tupelize_def Let_def) -qed - -end diff -r f8723843c29e -r b5db02fa9536 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon Dec 05 07:31:00 2011 +0100 +++ b/src/HOL/Library/Library.thy Mon Dec 05 07:31:11 2011 +0100 @@ -13,7 +13,6 @@ Convex Countable Cset_Monad - Diagonalize Dlist_Cset Eval_Witness Extended_Nat diff -r f8723843c29e -r b5db02fa9536 src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Mon Dec 05 07:31:00 2011 +0100 +++ b/src/HOL/Quickcheck_Exhaustive.thy Mon Dec 05 07:31:11 2011 +0100 @@ -466,7 +466,7 @@ where "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)" -type_synonym 'a pos_bound_cps = "('a => term list option) => code_numeral => term list option" +type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => code_numeral => (bool * term list) option" definition pos_bound_cps_empty :: "'a pos_bound_cps" where @@ -515,7 +515,7 @@ definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps" where - "neg_bound_cps_not n = (%c i. case n (%u. Some []) i of None => c (Known ()) | Some _ => No_value)" + "neg_bound_cps_not n = (%c i. case n (%u. Some (True, [])) i of None => c (Known ()) | Some _ => No_value)" definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps" where diff -r f8723843c29e -r b5db02fa9536 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Dec 05 07:31:00 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Dec 05 07:31:11 2011 +0100 @@ -1039,7 +1039,7 @@ | _ => NONE in Quickcheck.Result - {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample, + {counterexample = Option.map (pair true o curry (op ~~) (Term.add_free_names t [])) counterexample, evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []} end; diff -r f8723843c29e -r b5db02fa9536 src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Mon Dec 05 07:31:00 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Mon Dec 05 07:31:11 2011 +0100 @@ -114,9 +114,11 @@ structure Pos_Bounded_CPS_Comp_Funs = struct -fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"} +val resultT = @{typ "(bool * Code_Evaluation.term list) option"} +fun mk_monadT T = (T --> resultT) --> @{typ "code_numeral"} --> resultT -fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T +fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "(bool * term list) option"}]), + @{typ "code_numeral => (bool * term list) option"}])) = T | dest_monadT T = raise TYPE ("dest_monadT", [T], []); fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T); @@ -196,7 +198,8 @@ fun mk_not t = let val T = mk_monadT HOLogic.unitT - val pT = @{typ "(unit => Code_Evaluation.term list option) => code_numeral => Code_Evaluation.term list option"} + val pT = @{typ "(unit => (bool * Code_Evaluation.term list) option)"} + --> @{typ "code_numeral => (bool * Code_Evaluation.term list) option"} in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end fun mk_Enum f = error "not implemented" diff -r f8723843c29e -r b5db02fa9536 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Dec 05 07:31:00 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Dec 05 07:31:11 2011 +0100 @@ -550,7 +550,8 @@ mk_random = (fn T => fn additional_arguments => Const (@{const_name "Quickcheck_Exhaustive.exhaustive"}, - (T --> @{typ "term list option"}) --> @{typ "code_numeral => term list option"})), + (T --> @{typ "(bool * term list) option"}) --> + @{typ "code_numeral => (bool * term list) option"})), modify_funT = I, additional_arguments = K [], wrap_compilation = K (K (K (K (K I)))) diff -r f8723843c29e -r b5db02fa9536 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Dec 05 07:31:00 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Dec 05 07:31:11 2011 +0100 @@ -18,7 +18,7 @@ Proof.context -> Proof.context; val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) -> Proof.context -> Proof.context - val put_cps_result : (unit -> int -> term list option) -> + val put_cps_result : (unit -> int -> (bool * term list) option) -> Proof.context -> Proof.context val test_goals : (Predicate_Compile_Aux.compilation * bool) -> Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list @@ -70,7 +70,7 @@ structure CPS_Result = Proof_Data ( - type T = unit -> int -> term list option + type T = unit -> int -> (bool * term list) option (* FIXME avoid user error with non-user text *) fun init _ () = error "CPS_Result" ); @@ -278,8 +278,9 @@ mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))) | Pos_Generator_CPS => prog $ - mk_split_lambda (map Free vs') (mk_Some @{typ "term list"} $ (HOLogic.mk_list @{typ term} - (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))) + mk_split_lambda (map Free vs') (mk_Some @{typ "bool * term list"} $ + HOLogic.mk_prod (@{term "True"}, HOLogic.mk_list @{typ term} + (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))) | Depth_Limited_Random => fold_rev absdummy [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}] @@ -333,10 +334,10 @@ Code_Runtime.dynamic_value_strict (CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result") thy4 (SOME target) - (fn proc => fn g => fn depth => g depth |> Option.map (map proc)) + (fn proc => fn g => fn depth => g depth |> Option.map (apsnd (map proc))) qc_term [] in - fn size => fn nrandom => compiled_term + fn size => fn nrandom => Option.map snd o compiled_term end | Depth_Limited_Random => let @@ -385,7 +386,7 @@ val counterexample = try_upto_depth ctxt (c size (!nrandom)) in Quickcheck.Result - {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample, + {counterexample = Option.map (pair true o (curry (op ~~)) (Term.add_free_names t [])) counterexample, evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []} end