--- 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.
--- 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 \
--- 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 \<Rightarrow> 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 \<le> sum n"
-proof -
- have "2 * n \<le> n * Suc n" by auto
- with sum2 have "2 * n \<le> 2 * sum n" by simp
- then show ?thesis by simp
-qed
-
-lemma sum_rest_aux:
- assumes "q \<le> n"
- assumes "sum m \<le> sum n + q"
- shows "m \<le> n"
-proof (rule ccontr)
- assume "\<not> m \<le> n"
- then have "n < m" by simp
- then have "m \<ge> 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 \<le> sum n + q` have "sum (Suc (n + r)) \<le> sum n + q" by simp
- then have "sum (n + r) + Suc (n + r) \<le> sum n + q" unfolding sum_Suc by simp
- with `m = Suc (n + r)` have "sum (n + r) + m \<le> sum n + q" by simp
- have "sum n \<le> sum (n + r)" unfolding strict_mono_less_eq [OF sum_strict_mono] by simp
- moreover from `q \<le> n` `n < m` have "q < m" by simp
- ultimately have "sum n + q < sum (n + r) + m" by auto
- with `sum (n + r) + m \<le> sum n + q` show False
- by auto
-qed
-
-lemma sum_rest:
- assumes "q \<le> n"
- shows "sum m \<le> sum n + q \<longleftrightarrow> m \<le> 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 \<Rightarrow> nat \<Rightarrow> 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 \<or> a + b \<ge> Suc (c + d) \<or> c + d \<ge> Suc (a + b)" by arith
- then have "a = c \<and> 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 \<ge> Suc (c + d)"
- with strict_mono_less_eq [OF sum_strict_mono]
- have "sum (a + b) \<ge> sum (Suc (c + d))" by simp
- with diageq show ?thesis by (simp add: sum_Suc)
- next
- assume "c + d \<ge> Suc (a + b)"
- with strict_mono_less_eq [OF sum_strict_mono]
- have "sum (c + d) \<ge> 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 \<Rightarrow> nat \<times> nat" where
- "tupelize q = (let d = Max {d. sum d \<le> q}; m = q - sum d
- in (m, d - m))"
-
-lemma tupelize_diagonalize:
- "tupelize (diagonalize m n) = (m, n)"
-proof -
- from sum_rest
- have "\<And>r. sum r \<le> sum (m + n) + m \<longleftrightarrow> r \<le> m + n" by simp
- then have "Max {d. sum d \<le> (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) \<le> n"
-proof -
- have "sum 0 \<le> n" by (simp add: sum_0)
- then have "Max {m \<Colon> nat. sum m \<le> n} \<le> Max {m \<Colon> nat. m \<le> n}"
- by (intro Max_mono [of "{m. sum m \<le> n}" "{m. m \<le> n}"])
- (auto intro: Max_mono order_trans sum_not_less_self)
- also have "Max {m \<Colon> nat. m \<le> n} \<le> n"
- by (subst Max_le_iff) auto
- finally have "Max {m. sum m \<le> n} \<le> n" .
- then show ?thesis by (simp add: tupelize_def Let_def)
-qed
-
-end
--- 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
--- 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
--- 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;
--- 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"
--- 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))))
--- 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