# HG changeset patch # User blanchet # Date 1236425246 -3600 # Node ID 5598523c482ac83e6ac2ce28866445b2b1a5398b # Parent e9971af27b110cfd9059202b6bf190fbd7237198# Parent 91f73b2997f947fbdb8c5de9cd49276b02a0dd42 merged diff -r 91f73b2997f9 -r 5598523c482a NEWS --- a/NEWS Sat Mar 07 12:26:56 2009 +0100 +++ b/NEWS Sat Mar 07 12:27:26 2009 +0100 @@ -220,6 +220,9 @@ *** HOL *** +* Theory Library/Diagonalize.thy provides constructive version of +Cantor's first diagonalization argument. + * New predicate "strict_mono" classifies strict functions on partial orders. With strict functions on linear orders, reasoning about (in)equalities is facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less". diff -r 91f73b2997f9 -r 5598523c482a src/HOL/Docs/MainDoc.thy --- a/src/HOL/Docs/MainDoc.thy Sat Mar 07 12:26:56 2009 +0100 +++ b/src/HOL/Docs/MainDoc.thy Sat Mar 07 12:27:26 2009 +0100 @@ -342,6 +342,36 @@ \end{supertabular} +\section{Set\_Interval} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const lessThan} & @{typeof lessThan}\\ +@{const atMost} & @{typeof atMost}\\ +@{const greaterThan} & @{typeof greaterThan}\\ +@{const atLeast} & @{typeof atLeast}\\ +@{const greaterThanLessThan} & @{typeof greaterThanLessThan}\\ +@{const atLeastLessThan} & @{typeof atLeastLessThan}\\ +@{const greaterThanAtMost} & @{typeof greaterThanAtMost}\\ +@{const atLeastAtMost} & @{typeof atLeastAtMost}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term "lessThan y"} & @{term[source] "lessThan y"}\\ +@{term "atMost y"} & @{term[source] "atMost y"}\\ +@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\ +@{term "atLeast x"} & @{term[source] "atLeast x"}\\ +@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\ +@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\ +@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\ +@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\ +@{term "UN i:{..n}. A"} & @{term[source] "\ i \ {..n}. A"}\\ +@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\x. t) {a..b}"}\\ +\end{supertabular} + +??????? + \section{Power} \begin{tabular}{@ {} l @ {~::~} l @ {}} diff -r 91f73b2997f9 -r 5598523c482a src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sat Mar 07 12:26:56 2009 +0100 +++ b/src/HOL/Finite_Set.thy Sat Mar 07 12:27:26 2009 +0100 @@ -3060,6 +3060,30 @@ by (simp add: Max fold1_strict_below_iff [folded dual_max]) qed +lemma Min_eqI: + assumes "finite A" + assumes "\y. y \ A \ y \ x" + and "x \ A" + shows "Min A = x" +proof (rule antisym) + from `x \ A` have "A \ {}" by auto + with assms show "Min A \ x" by simp +next + from assms show "x \ Min A" by simp +qed + +lemma Max_eqI: + assumes "finite A" + assumes "\y. y \ A \ y \ x" + and "x \ A" + shows "Max A = x" +proof (rule antisym) + from `x \ A` have "A \ {}" by auto + with assms show "Max A \ x" by simp +next + from assms show "x \ Max A" by simp +qed + lemma Min_antimono: assumes "M \ N" and "M \ {}" and "finite N" shows "Min N \ Min M" diff -r 91f73b2997f9 -r 5598523c482a src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Sat Mar 07 12:26:56 2009 +0100 +++ b/src/HOL/IntDiv.thy Sat Mar 07 12:27:26 2009 +0100 @@ -1025,9 +1025,12 @@ apply (auto simp add: div_eq_minus1) done -lemma div_nonneg_neg_le0: "[| (0::int) \ a; b < 0 |] ==> a div b \ 0" +lemma div_nonneg_neg_le0: "[| (0::int) \ a; b < 0 |] ==> a div b \ 0" by (drule zdiv_mono1_neg, auto) +lemma div_nonpos_pos_le0: "[| (a::int) \ 0; b > 0 |] ==> a div b \ 0" +by (drule zdiv_mono1, auto) + lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \ a div b) = (0 \ a)" apply auto apply (drule_tac [2] zdiv_mono1) diff -r 91f73b2997f9 -r 5598523c482a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Mar 07 12:26:56 2009 +0100 +++ b/src/HOL/IsaMakefile Sat Mar 07 12:27:26 2009 +0100 @@ -318,7 +318,7 @@ Library/Finite_Cartesian_Product.thy \ Library/FrechetDeriv.thy \ Library/Fundamental_Theorem_Algebra.thy \ - Library/Inner_Product.thy \ + Library/Inner_Product.thy Library/Lattice_Syntax.thy \ Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy \ Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy \ Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy \ @@ -332,13 +332,13 @@ Library/List_lexord.thy Library/Commutative_Ring.thy \ Library/comm_ring.ML Library/Coinductive_List.thy \ Library/AssocList.thy Library/Formal_Power_Series.thy \ - Library/Binomial.thy Library/Eval_Witness.thy \ + Library/Binomial.thy Library/Eval_Witness.thy \ Library/Code_Index.thy Library/Code_Char.thy \ Library/Code_Char_chr.thy Library/Code_Integer.thy \ - Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy \ - Library/Boolean_Algebra.thy Library/Countable.thy \ - Library/RBT.thy Library/Univ_Poly.thy \ - Library/Random.thy Library/Quickcheck.thy \ + Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy \ + Library/Boolean_Algebra.thy Library/Countable.thy \ + Library/Diagonalize.thy Library/RBT.thy Library/Univ_Poly.thy \ + Library/Random.thy Library/Quickcheck.thy \ Library/Poly_Deriv.thy \ Library/Polynomial.thy \ Library/Product_plus.thy \ diff -r 91f73b2997f9 -r 5598523c482a src/HOL/Library/Diagonalize.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Diagonalize.thy Sat Mar 07 12:27:26 2009 +0100 @@ -0,0 +1,149 @@ +(* 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 91f73b2997f9 -r 5598523c482a src/HOL/Library/Lattice_Syntax.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Lattice_Syntax.thy Sat Mar 07 12:27:26 2009 +0100 @@ -0,0 +1,17 @@ +(* Author: Florian Haftmann, TU Muenchen *) + +header {* Pretty syntax for lattice operations *} + +(*<*) +theory Lattice_Syntax +imports Set +begin + +notation + inf (infixl "\" 70) and + sup (infixl "\" 65) and + Inf ("\_" [900] 900) and + Sup ("\_" [900] 900) + +end +(*>*) \ No newline at end of file diff -r 91f73b2997f9 -r 5598523c482a src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Sat Mar 07 12:26:56 2009 +0100 +++ b/src/HOL/Library/Library.thy Sat Mar 07 12:27:26 2009 +0100 @@ -17,6 +17,7 @@ ContNotDenum Countable Determinants + Diagonalize Efficient_Nat Enum Eval_Witness @@ -28,6 +29,7 @@ Fundamental_Theorem_Algebra Infinite_Set Inner_Product + Lattice_Syntax ListVector Mapping Multiset diff -r 91f73b2997f9 -r 5598523c482a src/HOL/Option.thy --- a/src/HOL/Option.thy Sat Mar 07 12:26:56 2009 +0100 +++ b/src/HOL/Option.thy Sat Mar 07 12:27:26 2009 +0100 @@ -5,7 +5,7 @@ header {* Datatype option *} theory Option -imports Datatype +imports Datatype Finite_Set begin datatype 'a option = None | Some 'a @@ -30,6 +30,9 @@ lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV" by (rule set_ext, case_tac x) auto +instance option :: (finite) finite proof +qed (simp add: insert_None_conv_UNIV [symmetric]) + lemma inj_Some [simp]: "inj_on Some A" by (rule inj_onI) simp diff -r 91f73b2997f9 -r 5598523c482a src/HOL/Plain.thy --- a/src/HOL/Plain.thy Sat Mar 07 12:26:56 2009 +0100 +++ b/src/HOL/Plain.thy Sat Mar 07 12:27:26 2009 +0100 @@ -9,9 +9,6 @@ include @{text Hilbert_Choice}. *} -instance option :: (finite) finite - by default (simp add: insert_None_conv_UNIV [symmetric]) - ML {* path_add "~~/src/HOL/Library" *} end diff -r 91f73b2997f9 -r 5598523c482a src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Sat Mar 07 12:26:56 2009 +0100 +++ b/src/HOL/Predicate.thy Sat Mar 07 12:27:26 2009 +0100 @@ -1,15 +1,40 @@ (* Title: HOL/Predicate.thy - ID: $Id$ - Author: Stefan Berghofer, TU Muenchen + Author: Stefan Berghofer and Lukas Bulwahn and Florian Haftmann, TU Muenchen *) -header {* Predicates *} +header {* Predicates as relations and enumerations *} theory Predicate imports Inductive Relation begin -subsection {* Equality and Subsets *} +notation + inf (infixl "\" 70) and + sup (infixl "\" 65) and + Inf ("\_" [900] 900) and + Sup ("\_" [900] 900) and + top ("\") and + bot ("\") + + +subsection {* Predicates as (complete) lattices *} + +subsubsection {* @{const sup} on @{typ bool} *} + +lemma sup_boolI1: + "P \ P \ Q" + by (simp add: sup_bool_eq) + +lemma sup_boolI2: + "Q \ P \ Q" + by (simp add: sup_bool_eq) + +lemma sup_boolE: + "P \ Q \ (P \ R) \ (Q \ R) \ R" + by (auto simp add: sup_bool_eq) + + +subsubsection {* Equality and Subsets *} lemma pred_equals_eq: "((\x. x \ R) = (\x. x \ S)) = (R = S)" by (simp add: mem_def) @@ -24,7 +49,7 @@ by fast -subsection {* Top and bottom elements *} +subsubsection {* Top and bottom elements *} lemma top1I [intro!]: "top x" by (simp add: top_fun_eq top_bool_eq) @@ -39,7 +64,7 @@ by (simp add: bot_fun_eq bot_bool_eq) -subsection {* The empty set *} +subsubsection {* The empty set *} lemma bot_empty_eq: "bot = (\x. x \ {})" by (auto simp add: expand_fun_eq) @@ -48,7 +73,7 @@ by (auto simp add: expand_fun_eq) -subsection {* Binary union *} +subsubsection {* Binary union *} lemma sup1_iff [simp]: "sup A B x \ A x | B x" by (simp add: sup_fun_eq sup_bool_eq) @@ -92,7 +117,7 @@ by simp iprover -subsection {* Binary intersection *} +subsubsection {* Binary intersection *} lemma inf1_iff [simp]: "inf A B x \ A x \ B x" by (simp add: inf_fun_eq inf_bool_eq) @@ -131,7 +156,7 @@ by simp -subsection {* Unions of families *} +subsubsection {* Unions of families *} lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)" by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast @@ -158,7 +183,7 @@ by (simp add: expand_fun_eq) -subsection {* Intersections of families *} +subsubsection {* Intersections of families *} lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)" by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast @@ -191,7 +216,9 @@ by (simp add: expand_fun_eq) -subsection {* Composition of two relations *} +subsection {* Predicates as relations *} + +subsubsection {* Composition *} inductive pred_comp :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool" @@ -207,7 +234,7 @@ by (auto simp add: expand_fun_eq elim: pred_compE) -subsection {* Converse *} +subsubsection {* Converse *} inductive conversep :: "('a => 'b => bool) => 'b => 'a => bool" @@ -253,7 +280,7 @@ by (auto simp add: expand_fun_eq) -subsection {* Domain *} +subsubsection {* Domain *} inductive DomainP :: "('a => 'b => bool) => 'a => bool" @@ -267,7 +294,7 @@ by (blast intro!: Orderings.order_antisym predicate1I) -subsection {* Range *} +subsubsection {* Range *} inductive RangeP :: "('a => 'b => bool) => 'b => bool" @@ -281,7 +308,7 @@ by (blast intro!: Orderings.order_antisym predicate1I) -subsection {* Inverse image *} +subsubsection {* Inverse image *} definition inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where @@ -294,7 +321,7 @@ by (simp add: inv_imagep_def) -subsection {* The Powerset operator *} +subsubsection {* Powerset *} definition Powp :: "('a \ bool) \ 'a set \ bool" where "Powp A == \B. \x \ B. A x" @@ -305,7 +332,7 @@ lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq] -subsection {* Properties of relations - predicate versions *} +subsubsection {* Properties of relations *} abbreviation antisymP :: "('a => 'a => bool) => bool" where "antisymP r == antisym {(x, y). r x y}" @@ -316,4 +343,264 @@ abbreviation single_valuedP :: "('a => 'b => bool) => bool" where "single_valuedP r == single_valued {(x, y). r x y}" + +subsection {* Predicates as enumerations *} + +subsubsection {* The type of predicate enumerations (a monad) *} + +datatype 'a pred = Pred "'a \ bool" + +primrec eval :: "'a pred \ 'a \ bool" where + eval_pred: "eval (Pred f) = f" + +lemma Pred_eval [simp]: + "Pred (eval x) = x" + by (cases x) simp + +lemma eval_inject: "eval x = eval y \ x = y" + by (cases x) auto + +definition single :: "'a \ 'a pred" where + "single x = Pred ((op =) x)" + +definition bind :: "'a pred \ ('a \ 'b pred) \ 'b pred" (infixl "\=" 70) where + "P \= f = Pred (\x. (\y. eval P y \ eval (f y) x))" + +instantiation pred :: (type) complete_lattice +begin + +definition + "P \ Q \ eval P \ eval Q" + +definition + "P < Q \ eval P < eval Q" + +definition + "\ = Pred \" + +definition + "\ = Pred \" + +definition + "P \ Q = Pred (eval P \ eval Q)" + +definition + "P \ Q = Pred (eval P \ eval Q)" + +definition + "\A = Pred (INFI A eval)" + +definition + "\A = Pred (SUPR A eval)" + +instance by default + (auto simp add: less_eq_pred_def less_pred_def + inf_pred_def sup_pred_def bot_pred_def top_pred_def + Inf_pred_def Sup_pred_def, + auto simp add: le_fun_def less_fun_def le_bool_def less_bool_def + eval_inject mem_def) + end + +lemma bind_bind: + "(P \= Q) \= R = P \= (\x. Q x \= R)" + by (auto simp add: bind_def expand_fun_eq) + +lemma bind_single: + "P \= single = P" + by (simp add: bind_def single_def) + +lemma single_bind: + "single x \= P = P x" + by (simp add: bind_def single_def) + +lemma bottom_bind: + "\ \= P = \" + by (auto simp add: bot_pred_def bind_def expand_fun_eq) + +lemma sup_bind: + "(P \ Q) \= R = P \= R \ Q \= R" + by (auto simp add: bind_def sup_pred_def expand_fun_eq) + +lemma Sup_bind: "(\A \= f) = \((\x. x \= f) ` A)" + by (auto simp add: bind_def Sup_pred_def expand_fun_eq) + +lemma pred_iffI: + assumes "\x. eval A x \ eval B x" + and "\x. eval B x \ eval A x" + shows "A = B" +proof - + from assms have "\x. eval A x \ eval B x" by blast + then show ?thesis by (cases A, cases B) (simp add: expand_fun_eq) +qed + +lemma singleI: "eval (single x) x" + unfolding single_def by simp + +lemma singleI_unit: "eval (single ()) x" + by simp (rule singleI) + +lemma singleE: "eval (single x) y \ (y = x \ P) \ P" + unfolding single_def by simp + +lemma singleE': "eval (single x) y \ (x = y \ P) \ P" + by (erule singleE) simp + +lemma bindI: "eval P x \ eval (Q x) y \ eval (P \= Q) y" + unfolding bind_def by auto + +lemma bindE: "eval (R \= Q) y \ (\x. eval R x \ eval (Q x) y \ P) \ P" + unfolding bind_def by auto + +lemma botE: "eval \ x \ P" + unfolding bot_pred_def by auto + +lemma supI1: "eval A x \ eval (A \ B) x" + unfolding sup_pred_def by simp + +lemma supI2: "eval B x \ eval (A \ B) x" + unfolding sup_pred_def by simp + +lemma supE: "eval (A \ B) x \ (eval A x \ P) \ (eval B x \ P) \ P" + unfolding sup_pred_def by auto + + +subsubsection {* Derived operations *} + +definition if_pred :: "bool \ unit pred" where + if_pred_eq: "if_pred b = (if b then single () else \)" + +definition eq_pred :: "'a \ 'a \ unit pred" where + eq_pred_eq: "eq_pred a b = if_pred (a = b)" + +definition not_pred :: "unit pred \ unit pred" where + not_pred_eq: "not_pred P = (if eval P () then \ else single ())" + +lemma if_predI: "P \ eval (if_pred P) ()" + unfolding if_pred_eq by (auto intro: singleI) + +lemma if_predE: "eval (if_pred b) x \ (b \ x = () \ P) \ P" + unfolding if_pred_eq by (cases b) (auto elim: botE) + +lemma eq_predI: "eval (eq_pred a a) ()" + unfolding eq_pred_eq if_pred_eq by (auto intro: singleI) + +lemma eq_predE: "eval (eq_pred a b) x \ (a = b \ x = () \ P) \ P" + unfolding eq_pred_eq by (erule if_predE) + +lemma not_predI: "\ P \ eval (not_pred (Pred (\u. P))) ()" + unfolding not_pred_eq eval_pred by (auto intro: singleI) + +lemma not_predI': "\ eval P () \ eval (not_pred P) ()" + unfolding not_pred_eq by (auto intro: singleI) + +lemma not_predE: "eval (not_pred (Pred (\u. P))) x \ (\ P \ thesis) \ thesis" + unfolding not_pred_eq + by (auto split: split_if_asm elim: botE) + +lemma not_predE': "eval (not_pred P) x \ (\ eval P x \ thesis) \ thesis" + unfolding not_pred_eq + by (auto split: split_if_asm elim: botE) + + +subsubsection {* Implementation *} + +datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq" + +primrec pred_of_seq :: "'a seq \ 'a pred" where + "pred_of_seq Empty = \" + | "pred_of_seq (Insert x P) = single x \ P" + | "pred_of_seq (Join P xq) = P \ pred_of_seq xq" + +definition Seq :: "(unit \ 'a seq) \ 'a pred" where + "Seq f = pred_of_seq (f ())" + +code_datatype Seq + +primrec member :: "'a seq \ 'a \ bool" where + "member Empty x \ False" + | "member (Insert y P) x \ x = y \ eval P x" + | "member (Join P xq) x \ eval P x \ member xq x" + +lemma eval_member: + "member xq = eval (pred_of_seq xq)" +proof (induct xq) + case Empty show ?case + by (auto simp add: expand_fun_eq elim: botE) +next + case Insert show ?case + by (auto simp add: expand_fun_eq elim: supE singleE intro: supI1 supI2 singleI) +next + case Join then show ?case + by (auto simp add: expand_fun_eq elim: supE intro: supI1 supI2) +qed + +lemma eval_code [code]: "eval (Seq f) = member (f ())" + unfolding Seq_def by (rule sym, rule eval_member) + +lemma single_code [code]: + "single x = Seq (\u. Insert x \)" + unfolding Seq_def by simp + +primrec "apply" :: "('a \ 'b Predicate.pred) \ 'a seq \ 'b seq" where + "apply f Empty = Empty" + | "apply f (Insert x P) = Join (f x) (Join (P \= f) Empty)" + | "apply f (Join P xq) = Join (P \= f) (apply f xq)" + +lemma apply_bind: + "pred_of_seq (apply f xq) = pred_of_seq xq \= f" +proof (induct xq) + case Empty show ?case + by (simp add: bottom_bind) +next + case Insert show ?case + by (simp add: single_bind sup_bind) +next + case Join then show ?case + by (simp add: sup_bind) +qed + +lemma bind_code [code]: + "Seq g \= f = Seq (\u. apply f (g ()))" + unfolding Seq_def by (rule sym, rule apply_bind) + +lemma bot_set_code [code]: + "\ = Seq (\u. Empty)" + unfolding Seq_def by simp + +lemma sup_code [code]: + "Seq f \ Seq g = Seq (\u. case f () + of Empty \ g () + | Insert x P \ Insert x (P \ Seq g) + | Join P xq \ Join (Seq g) (Join P xq))" (*FIXME order!?*) +proof (cases "f ()") + case Empty + thus ?thesis + unfolding Seq_def by (simp add: sup_commute [of "\"] sup_bot) +next + case Insert + thus ?thesis + unfolding Seq_def by (simp add: sup_assoc) +next + case Join + thus ?thesis + unfolding Seq_def by (simp add: sup_commute [of "pred_of_seq (g ())"] sup_assoc) +qed + + +declare eq_pred_def [code, code del] + +no_notation + inf (infixl "\" 70) and + sup (infixl "\" 65) and + Inf ("\_" [900] 900) and + Sup ("\_" [900] 900) and + top ("\") and + bot ("\") and + bind (infixl "\=" 70) + +hide (open) type pred seq +hide (open) const Pred eval single bind if_pred eq_pred not_pred + Empty Insert Join Seq member "apply" + +end diff -r 91f73b2997f9 -r 5598523c482a src/HOL/document/root.tex --- a/src/HOL/document/root.tex Sat Mar 07 12:26:56 2009 +0100 +++ b/src/HOL/document/root.tex Sat Mar 07 12:27:26 2009 +0100 @@ -1,9 +1,8 @@ - -% $Id$ \documentclass[11pt,a4paper]{article} \usepackage{graphicx,isabelle,isabellesym,latexsym} \usepackage{amssymb} +\usepackage[english]{babel} \usepackage[only,bigsqcap]{stmaryrd} \usepackage[latin1]{inputenc} \usepackage{pdfsetup} diff -r 91f73b2997f9 -r 5598523c482a src/HOL/ex/ExecutableContent.thy --- a/src/HOL/ex/ExecutableContent.thy Sat Mar 07 12:26:56 2009 +0100 +++ b/src/HOL/ex/ExecutableContent.thy Sat Mar 07 12:27:26 2009 +0100 @@ -24,6 +24,19 @@ "~~/src/HOL/ex/Records" begin +lemma [code, code del]: + "(size :: 'a::size Predicate.pred => nat) = size" .. +lemma [code, code del]: + "pred_size = pred_size" .. +lemma [code, code del]: + "pred_case = pred_case" .. +lemma [code, code del]: + "pred_rec = pred_rec" .. +lemma [code, code del]: + "(Code_Eval.term_of \ 'a::{type, term_of} Predicate.pred \ Code_Eval.term) = Code_Eval.term_of" .. +lemma [code, code del]: + "(Code_Eval.term_of \ 'a::{type, term_of} Predicate.seq \ Code_Eval.term) = Code_Eval.term_of" .. + text {* However, some aren't executable *} declare pair_leq_def[code del] diff -r 91f73b2997f9 -r 5598523c482a src/Provers/blast.ML --- a/src/Provers/blast.ML Sat Mar 07 12:26:56 2009 +0100 +++ b/src/Provers/blast.ML Sat Mar 07 12:27:26 2009 +0100 @@ -643,13 +643,13 @@ (*Print tracing information at each iteration of prover*) fun tracing (State {thy, fullTrace, ...}) brs = - let fun printPairs (((G,_)::_,_)::_) = Output.immediate_output(traceTerm thy G) - | printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm thy H ^ "\t (Unsafe)") + let fun printPairs (((G,_)::_,_)::_) = Output.tracing (traceTerm thy G) + | printPairs (([],(H,_)::_)::_) = Output.tracing (traceTerm thy H ^ "\t (Unsafe)") | printPairs _ = () fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = (fullTrace := brs0 :: !fullTrace; - List.app (fn _ => Output.immediate_output "+") brs; - Output.immediate_output (" [" ^ Int.toString lim ^ "] "); + List.app (fn _ => Output.tracing "+") brs; + Output.tracing (" [" ^ Int.toString lim ^ "] "); printPairs pairs; writeln"") in if !trace then printBrs (map normBr brs) else () @@ -662,10 +662,10 @@ if !trace then (case !ntrail-ntrl of 0 => () - | 1 => Output.immediate_output"\t1 variable UPDATED:" - | n => Output.immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:"); + | 1 => Output.tracing "\t1 variable UPDATED:" + | n => Output.tracing ("\t" ^ Int.toString n ^ " variables UPDATED:"); (*display the instantiations themselves, though no variable names*) - List.app (fn v => Output.immediate_output(" " ^ string_of thy 4 (the (!v)))) + List.app (fn v => Output.tracing (" " ^ string_of thy 4 (the (!v)))) (List.take(!trail, !ntrail-ntrl)); writeln"") else (); @@ -674,9 +674,9 @@ fun traceNew prems = if !trace then case length prems of - 0 => Output.immediate_output"branch closed by rule" - | 1 => Output.immediate_output"branch extended (1 new subgoal)" - | n => Output.immediate_output("branch split: "^ Int.toString n ^ " new subgoals") + 0 => Output.tracing "branch closed by rule" + | 1 => Output.tracing "branch extended (1 new subgoal)" + | n => Output.tracing ("branch split: "^ Int.toString n ^ " new subgoals") else (); @@ -1005,7 +1005,7 @@ NONE => closeF Ls | SOME tac => let val choices' = - (if !trace then (Output.immediate_output"branch closed"; + (if !trace then (Output.tracing "branch closed"; traceVars state ntrl) else (); prune state (nbrs, nxtVars, @@ -1136,9 +1136,9 @@ clearTo state ntrl; raise NEWBRANCHES) else traceNew prems; - if !trace andalso dup then Output.immediate_output" (duplicating)" + if !trace andalso dup then Output.tracing " (duplicating)" else (); - if !trace andalso recur then Output.immediate_output" (recursive)" + if !trace andalso recur then Output.tracing " (recursive)" else (); traceVars state ntrl; if null prems then nclosed := !nclosed + 1 diff -r 91f73b2997f9 -r 5598523c482a src/Pure/General/output.ML --- a/src/Pure/General/output.ML Sat Mar 07 12:26:56 2009 +0100 +++ b/src/Pure/General/output.ML Sat Mar 07 12:27:26 2009 +0100 @@ -32,7 +32,6 @@ val escape: output -> string val std_output: output -> unit val std_error: output -> unit - val immediate_output: string -> unit val writeln_default: output -> unit val writeln_fn: (output -> unit) ref val priority_fn: (output -> unit) ref @@ -89,8 +88,6 @@ fun std_error s = NAMED_CRITICAL "IO" (fn () => (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr)); -val immediate_output = std_output o output; - fun writeln_default "" = () | writeln_default s = std_output (suffix "\n" s); diff -r 91f73b2997f9 -r 5598523c482a src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sat Mar 07 12:26:56 2009 +0100 +++ b/src/Pure/Thy/thy_info.ML Sat Mar 07 12:27:26 2009 +0100 @@ -383,7 +383,12 @@ fun schedule_seq tasks = Graph.topological_order tasks - |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () () | _ => ())); + |> List.app (fn name => + (case Graph.get_node tasks name of + Task body => + let val after_load = body () + in after_load () handle exn => (kill_thy name; raise exn) end + | _ => ())); in diff -r 91f73b2997f9 -r 5598523c482a src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sat Mar 07 12:26:56 2009 +0100 +++ b/src/Pure/Thy/thy_output.ML Sat Mar 07 12:27:26 2009 +0100 @@ -78,8 +78,12 @@ fun command src = let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup (! global_commands) name of - NONE => error ("Unknown document antiquotation command: " ^ quote name ^ Position.str_of pos) - | SOME f => (Position.report (Markup.doc_antiq name) pos; f src)) + NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos) + | SOME f => + (Position.report (Markup.doc_antiq name) pos; + (fn node => f src node handle ERROR msg => + cat_error msg ("The error(s) above occurred in document antiquotation: " ^ + quote name ^ Position.str_of pos)))) end; fun option (name, s) f () = diff -r 91f73b2997f9 -r 5598523c482a src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Sat Mar 07 12:26:56 2009 +0100 +++ b/src/Pure/Tools/find_theorems.ML Sat Mar 07 12:27:26 2009 +0100 @@ -168,8 +168,7 @@ fun etacn thm i = Seq.take (! tac_limit) o etac thm i; fun try_thm thm = if Thm.no_prems thm then rtac thm 1 goal - else (etacn thm THEN_ALL_NEW - (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; + else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; in fn (_, thm) => if (is_some o Seq.pull o try_thm) thm @@ -181,11 +180,10 @@ fun filter_simp ctxt t (_, thm) = let - val (_, {mk_rews = {mk, ...}, ...}) = - Simplifier.rep_ss (Simplifier.local_simpset_of ctxt); + val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt); val extract_simp = - (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl); - val ss = is_matching_thm extract_simp ctxt false t thm + (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); + val ss = is_matching_thm extract_simp ctxt false t thm; in if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE end; diff -r 91f73b2997f9 -r 5598523c482a src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Sat Mar 07 12:26:56 2009 +0100 +++ b/src/Pure/meta_simplifier.ML Sat Mar 07 12:27:26 2009 +0100 @@ -59,6 +59,7 @@ val delcongs: simpset * thm list -> simpset val addsimprocs: simpset * simproc list -> simpset val delsimprocs: simpset * simproc list -> simpset + val mksimps: simpset -> thm -> thm list val setmksimps: simpset * (thm -> thm list) -> simpset val setmkcong: simpset * (thm -> thm) -> simpset val setmksym: simpset * (thm -> thm option) -> simpset @@ -547,6 +548,7 @@ fun add_simp thm ss = ss addsimps [thm]; fun del_simp thm ss = ss delsimps [thm]; + (* congs *) fun cong_name (Const (a, _)) = SOME a @@ -694,6 +696,8 @@ in +val mksimps = #mk o #mk_rews o #2 o rep_ss; + fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) => (mk, mk_cong, mk_sym, mk_eq_True, reorient)); diff -r 91f73b2997f9 -r 5598523c482a src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Sat Mar 07 12:26:56 2009 +0100 +++ b/src/Tools/eqsubst.ML Sat Mar 07 12:27:26 2009 +0100 @@ -128,8 +128,7 @@ (* changes object "=" to meta "==" which prepares a given rewrite rule *) fun prep_meta_eq ctxt = - let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt) - in mk #> map Drule.zero_var_indexes end; + Simplifier.mksimps (Simplifier.local_simpset_of ctxt) #> map Drule.zero_var_indexes; (* a type abriviation for match information *)