# HG changeset patch # User nipkow # Date 1312780396 -7200 # Node ID 18a0aef2af808289f7b16921ba4c682fc117fd65 # Parent 919e2bde720236784d9d66ce8544169453a6a530# Parent a43ca8ed65645c3aaf78432d6e751e9e67ff3e59 merged diff -r a43ca8ed6564 -r 18a0aef2af80 NEWS --- a/NEWS Sat Aug 06 14:16:23 2011 +0200 +++ b/NEWS Mon Aug 08 07:13:16 2011 +0200 @@ -65,8 +65,9 @@ * Class complete_lattice: generalized a couple of lemmas from sets; generalized theorems INF_cong and SUP_cong. New type classes for complete -boolean algebras and complete linear orderes. Lemmas Inf_less_iff, +boolean algebras and complete linear orders. Lemmas Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder. +Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply. More consistent and less misunderstandable names: INFI_def ~> INF_def SUPR_def ~> SUP_def @@ -83,7 +84,7 @@ to UNION any longer; these have been moved to collection UN_ball_bex_simps. INCOMPATIBILITY. -* Archimedian_Field.thy: +* Archimedean_Field.thy: floor now is defined as parameter of a separate type class floor_ceiling. * Finite_Set.thy: more coherent development of fold_set locales: @@ -98,9 +99,11 @@ - theory Library/Code_Char_ord provides native ordering of characters in the target language. - commands code_module and code_library are legacy, use export_code instead. - - evaluator "SML" and method evaluation are legacy, use evaluator "code" - and method eval instead. - + - method evaluation is legacy, use method eval instead. + - legacy evaluator "SML" is deactivated by default. To activate it, add the following + line in your theory: + setup {* Value.add_evaluator ("SML", Codegen.eval_term) *} + * Declare ext [intro] by default. Rare INCOMPATIBILITY. * Nitpick: @@ -151,6 +154,22 @@ - Use extended reals instead of positive extended reals. INCOMPATIBILITY. +* Old recdef package has been moved to Library/Old_Recdef.thy, where it +must be loaded explicitly. INCOMPATIBILITY. + +* Well-founded recursion combinator "wfrec" has been moved to +Library/Wfrec.thy. INCOMPATIBILITY. + +* Theory Library/Nat_Infinity has been renamed to Library/Extended_Nat. +The names of the following types and constants have changed: + inat (type) ~> enat + Fin ~> enat + Infty ~> infinity (overloaded) + iSuc ~> eSuc + the_Fin ~> the_enat +Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has +been renamed accordingly. + *** Document preparation *** diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Bali/Basis.thy Mon Aug 08 07:13:16 2011 +0200 @@ -3,13 +3,11 @@ *) header {* Definitions extending HOL as logical basis of Bali *} -theory Basis imports Main begin +theory Basis imports Main "~~/src/HOL/Library/Old_Recdef" begin section "misc" -declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *) - declare split_if_asm [split] option.split [split] option.split_asm [split] declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} declare if_weak_cong [cong del] option.weak_case_cong [cong del] diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Bali/Decl.thy --- a/src/HOL/Bali/Decl.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Bali/Decl.thy Mon Aug 08 07:13:16 2011 +0200 @@ -5,7 +5,8 @@ *} theory Decl -imports Term Table (** order is significant, because of clash for "var" **) +imports Term Table + (** order is significant, because of clash for "var" **) begin text {* diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Complete_Lattice.thy Mon Aug 08 07:13:16 2011 +0200 @@ -38,156 +38,11 @@ (unfold_locales, (fact bot_least top_greatest Sup_upper Sup_least Inf_lower Inf_greatest)+) -lemma Inf_Sup: "\A = \{b. \a \ A. b \ a}" - by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) - -lemma Sup_Inf: "\A = \{b. \a \ A. a \ b}" - by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) - -lemma Inf_empty [simp]: - "\{} = \" - by (auto intro: antisym Inf_greatest) - -lemma Sup_empty [simp]: - "\{} = \" - by (auto intro: antisym Sup_least) - -lemma Inf_UNIV [simp]: - "\UNIV = \" - by (simp add: Sup_Inf Sup_empty [symmetric]) - -lemma Sup_UNIV [simp]: - "\UNIV = \" - by (simp add: Inf_Sup Inf_empty [symmetric]) - -lemma Inf_insert: "\insert a A = a \ \A" - by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower) - -lemma Sup_insert: "\insert a A = a \ \A" - by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper) - -lemma Inf_singleton [simp]: - "\{a} = a" - by (auto intro: antisym Inf_lower Inf_greatest) - -lemma Sup_singleton [simp]: - "\{a} = a" - by (auto intro: antisym Sup_upper Sup_least) - -lemma Inf_binary: - "\{a, b} = a \ b" - by (simp add: Inf_insert) - -lemma Sup_binary: - "\{a, b} = a \ b" - by (simp add: Sup_insert) - -lemma le_Inf_iff: "b \ \A \ (\a\A. b \ a)" - by (auto intro: Inf_greatest dest: Inf_lower) - -lemma Sup_le_iff: "\A \ b \ (\a\A. a \ b)" - by (auto intro: Sup_least dest: Sup_upper) - -lemma Inf_superset_mono: "B \ A \ \A \ \B" - by (auto intro: Inf_greatest Inf_lower) - -lemma Sup_subset_mono: "A \ B \ \A \ \B" - by (auto intro: Sup_least Sup_upper) - -lemma Inf_mono: - assumes "\b. b \ B \ \a\A. a \ b" - shows "\A \ \B" -proof (rule Inf_greatest) - fix b assume "b \ B" - with assms obtain a where "a \ A" and "a \ b" by blast - from `a \ A` have "\A \ a" by (rule Inf_lower) - with `a \ b` show "\A \ b" by auto -qed - -lemma Sup_mono: - assumes "\a. a \ A \ \b\B. a \ b" - shows "\A \ \B" -proof (rule Sup_least) - fix a assume "a \ A" - with assms obtain b where "b \ B" and "a \ b" by blast - from `b \ B` have "b \ \B" by (rule Sup_upper) - with `a \ b` show "a \ \B" by auto -qed - -lemma Sup_upper2: "u \ A \ v \ u \ v \ \A" - using Sup_upper [of u A] by auto - -lemma Inf_lower2: "u \ A \ u \ v \ \A \ v" - using Inf_lower [of u A] by auto - -lemma Inf_less_eq: - assumes "\v. v \ A \ v \ u" - and "A \ {}" - shows "\A \ u" -proof - - from `A \ {}` obtain v where "v \ A" by blast - moreover with assms have "v \ u" by blast - ultimately show ?thesis by (rule Inf_lower2) -qed - -lemma less_eq_Sup: - assumes "\v. v \ A \ u \ v" - and "A \ {}" - shows "u \ \A" -proof - - from `A \ {}` obtain v where "v \ A" by blast - moreover with assms have "u \ v" by blast - ultimately show ?thesis by (rule Sup_upper2) -qed - -lemma less_eq_Inf_inter: "\A \ \B \ \(A \ B)" - by (auto intro: Inf_greatest Inf_lower) - -lemma Sup_inter_less_eq: "\(A \ B) \ \A \ \B " - by (auto intro: Sup_least Sup_upper) - -lemma Inf_union_distrib: "\(A \ B) = \A \ \B" - by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2) - -lemma Sup_union_distrib: "\(A \ B) = \A \ \B" - by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2) - -lemma Inf_top_conv [no_atp]: - "\A = \ \ (\x\A. x = \)" - "\ = \A \ (\x\A. x = \)" -proof - - show "\A = \ \ (\x\A. x = \)" - proof - assume "\x\A. x = \" - then have "A = {} \ A = {\}" by auto - then show "\A = \" by auto - next - assume "\A = \" - show "\x\A. x = \" - proof (rule ccontr) - assume "\ (\x\A. x = \)" - then obtain x where "x \ A" and "x \ \" by blast - then obtain B where "A = insert x B" by blast - with `\A = \` `x \ \` show False by (simp add: Inf_insert) - qed - qed - then show "\ = \A \ (\x\A. x = \)" by auto -qed - -lemma Sup_bot_conv [no_atp]: - "\A = \ \ (\x\A. x = \)" (is ?P) - "\ = \A \ (\x\A. x = \)" (is ?Q) -proof - - interpret dual: complete_lattice Sup Inf "op \" "op >" sup inf \ \ - by (fact dual_complete_lattice) - from dual.Inf_top_conv show ?P and ?Q by simp_all -qed - definition INFI :: "'b set \ ('b \ 'a) \ 'a" where - INF_def: "INFI A f = \ (f ` A)" + INF_def: "INFI A f = \(f ` A)" definition SUPR :: "'b set \ ('b \ 'a) \ 'a" where - SUP_def: "SUPR A f = \ (f ` A)" + SUP_def: "SUPR A f = \(f ` A)" text {* Note: must use names @{const INFI} and @{const SUPR} here instead of @@ -227,17 +82,25 @@ context complete_lattice begin -lemma INF_empty: "(\x\{}. f x) = \" - by (simp add: INF_def) - -lemma SUP_empty: "(\x\{}. f x) = \" - by (simp add: SUP_def) +lemma INF_foundation_dual [no_atp]: + "complete_lattice.SUPR Inf = INFI" +proof (rule ext)+ + interpret dual: complete_lattice Sup Inf "op \" "op >" sup inf \ \ + by (fact dual_complete_lattice) + fix f :: "'b \ 'a" and A + show "complete_lattice.SUPR Inf A f = (\a\A. f a)" + by (simp only: dual.SUP_def INF_def) +qed -lemma INF_insert: "(\x\insert a A. f x) = f a \ INFI A f" - by (simp add: INF_def Inf_insert) - -lemma SUP_insert: "(\x\insert a A. f x) = f a \ SUPR A f" - by (simp add: SUP_def Sup_insert) +lemma SUP_foundation_dual [no_atp]: + "complete_lattice.INFI Sup = SUPR" +proof (rule ext)+ + interpret dual: complete_lattice Sup Inf "op \" "op >" sup inf \ \ + by (fact dual_complete_lattice) + fix f :: "'b \ 'a" and A + show "complete_lattice.INFI Sup A f = (\a\A. f a)" + by (simp only: dual.INF_def SUP_def) +qed lemma INF_leI: "i \ A \ (\i\A. f i) \ f i" by (auto simp add: INF_def intro: Inf_lower) @@ -245,35 +108,97 @@ lemma le_SUP_I: "i \ A \ f i \ (\i\A. f i)" by (auto simp add: SUP_def intro: Sup_upper) -lemma INF_leI2: "i \ A \ f i \ u \ (\i\A. f i) \ u" - using INF_leI [of i A f] by auto - -lemma le_SUP_I2: "i \ A \ u \ f i \ u \ (\i\A. f i)" - using le_SUP_I [of i A f] by auto - lemma le_INF_I: "(\i. i \ A \ u \ f i) \ u \ (\i\A. f i)" by (auto simp add: INF_def intro: Inf_greatest) lemma SUP_leI: "(\i. i \ A \ f i \ u) \ (\i\A. f i) \ u" by (auto simp add: SUP_def intro: Sup_least) +lemma Inf_lower2: "u \ A \ u \ v \ \A \ v" + using Inf_lower [of u A] by auto + +lemma INF_leI2: "i \ A \ f i \ u \ (\i\A. f i) \ u" + using INF_leI [of i A f] by auto + +lemma Sup_upper2: "u \ A \ v \ u \ v \ \A" + using Sup_upper [of u A] by auto + +lemma le_SUP_I2: "i \ A \ u \ f i \ u \ (\i\A. f i)" + using le_SUP_I [of i A f] by auto + +lemma le_Inf_iff: "b \ \A \ (\a\A. b \ a)" + by (auto intro: Inf_greatest dest: Inf_lower) + lemma le_INF_iff: "u \ (\i\A. f i) \ (\i \ A. u \ f i)" by (auto simp add: INF_def le_Inf_iff) +lemma Sup_le_iff: "\A \ b \ (\a\A. a \ b)" + by (auto intro: Sup_least dest: Sup_upper) + lemma SUP_le_iff: "(\i\A. f i) \ u \ (\i \ A. f i \ u)" by (auto simp add: SUP_def Sup_le_iff) -lemma INF_const [simp]: "A \ {} \ (\i\A. f) = f" - by (auto intro: antisym INF_leI le_INF_I) +lemma Inf_empty [simp]: + "\{} = \" + by (auto intro: antisym Inf_greatest) + +lemma INF_empty: "(\x\{}. f x) = \" + by (simp add: INF_def) + +lemma Sup_empty [simp]: + "\{} = \" + by (auto intro: antisym Sup_least) + +lemma SUP_empty: "(\x\{}. f x) = \" + by (simp add: SUP_def) -lemma SUP_const [simp]: "A \ {} \ (\i\A. f) = f" - by (auto intro: antisym SUP_leI le_SUP_I) +lemma Inf_UNIV [simp]: + "\UNIV = \" + by (auto intro!: antisym Inf_lower) + +lemma Sup_UNIV [simp]: + "\UNIV = \" + by (auto intro!: antisym Sup_upper) + +lemma Inf_insert: "\insert a A = a \ \A" + by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower) + +lemma INF_insert: "(\x\insert a A. f x) = f a \ INFI A f" + by (simp add: INF_def Inf_insert) + +lemma Sup_insert: "\insert a A = a \ \A" + by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper) -lemma INF_top: "(\x\A. \) = \" - by (cases "A = {}") (simp_all add: INF_empty) +lemma SUP_insert: "(\x\insert a A. f x) = f a \ SUPR A f" + by (simp add: SUP_def Sup_insert) + +lemma Inf_Sup: "\A = \{b. \a \ A. b \ a}" + by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) + +lemma Sup_Inf: "\A = \{b. \a \ A. a \ b}" + by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) + +lemma Inf_singleton [simp]: + "\{a} = a" + by (auto intro: antisym Inf_lower Inf_greatest) -lemma SUP_bot: "(\x\A. \) = \" - by (cases "A = {}") (simp_all add: SUP_empty) +lemma Sup_singleton [simp]: + "\{a} = a" + by (auto intro: antisym Sup_upper Sup_least) + +lemma Inf_binary: + "\{a, b} = a \ b" + by (simp add: Inf_insert) + +lemma Sup_binary: + "\{a, b} = a \ b" + by (simp add: Sup_insert) + +lemma Inf_superset_mono: "B \ A \ \A \ \B" + by (auto intro: Inf_greatest Inf_lower) + +lemma Sup_subset_mono: "A \ B \ \A \ \B" + by (auto intro: Sup_least Sup_upper) lemma INF_cong: "A = B \ (\x. x \ B \ C x = D x) \ (\x\A. C x) = (\x\B. D x)" @@ -283,10 +208,30 @@ "A = B \ (\x. x \ B \ C x = D x) \ (\x\A. C x) = (\x\B. D x)" by (simp add: SUP_def image_def) +lemma Inf_mono: + assumes "\b. b \ B \ \a\A. a \ b" + shows "\A \ \B" +proof (rule Inf_greatest) + fix b assume "b \ B" + with assms obtain a where "a \ A" and "a \ b" by blast + from `a \ A` have "\A \ a" by (rule Inf_lower) + with `a \ b` show "\A \ b" by auto +qed + lemma INF_mono: "(\m. m \ B \ \n\A. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)" by (force intro!: Inf_mono simp: INF_def) +lemma Sup_mono: + assumes "\a. a \ A \ \b\B. a \ b" + shows "\A \ \B" +proof (rule Sup_least) + fix a assume "a \ A" + with assms obtain b where "b \ B" and "a \ b" by blast + from `b \ B` have "b \ \B" by (rule Sup_upper) + with `a \ b` show "a \ \B" by auto +qed + lemma SUP_mono: "(\n. n \ A \ \m\B. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)" by (force intro!: Sup_mono simp: SUP_def) @@ -300,6 +245,106 @@ "A \ B \ (\x. x \ A \ f x \ g x) \ (\x\A. f x) \ (\x\B. g x)" by (blast intro: SUP_mono dest: subsetD) +lemma Inf_less_eq: + assumes "\v. v \ A \ v \ u" + and "A \ {}" + shows "\A \ u" +proof - + from `A \ {}` obtain v where "v \ A" by blast + moreover with assms have "v \ u" by blast + ultimately show ?thesis by (rule Inf_lower2) +qed + +lemma less_eq_Sup: + assumes "\v. v \ A \ u \ v" + and "A \ {}" + shows "u \ \A" +proof - + from `A \ {}` obtain v where "v \ A" by blast + moreover with assms have "u \ v" by blast + ultimately show ?thesis by (rule Sup_upper2) +qed + +lemma less_eq_Inf_inter: "\A \ \B \ \(A \ B)" + by (auto intro: Inf_greatest Inf_lower) + +lemma Sup_inter_less_eq: "\(A \ B) \ \A \ \B " + by (auto intro: Sup_least Sup_upper) + +lemma Inf_union_distrib: "\(A \ B) = \A \ \B" + by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2) + +lemma INF_union: + "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)" + by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INF_I INF_leI) + +lemma Sup_union_distrib: "\(A \ B) = \A \ \B" + by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2) + +lemma SUP_union: + "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)" + by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUP_I) + +lemma INF_inf_distrib: "(\a\A. f a) \ (\a\A. g a) = (\a\A. f a \ g a)" + by (rule antisym) (rule le_INF_I, auto intro: le_infI1 le_infI2 INF_leI INF_mono) + +lemma SUP_sup_distrib: "(\a\A. f a) \ (\a\A. g a) = (\a\A. f a \ g a)" + by (rule antisym) (auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono, + rule SUP_leI, auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono) + +lemma Inf_top_conv [no_atp]: + "\A = \ \ (\x\A. x = \)" + "\ = \A \ (\x\A. x = \)" +proof - + show "\A = \ \ (\x\A. x = \)" + proof + assume "\x\A. x = \" + then have "A = {} \ A = {\}" by auto + then show "\A = \" by auto + next + assume "\A = \" + show "\x\A. x = \" + proof (rule ccontr) + assume "\ (\x\A. x = \)" + then obtain x where "x \ A" and "x \ \" by blast + then obtain B where "A = insert x B" by blast + with `\A = \` `x \ \` show False by (simp add: Inf_insert) + qed + qed + then show "\ = \A \ (\x\A. x = \)" by auto +qed + +lemma INF_top_conv: + "(\x\A. B x) = \ \ (\x\A. B x = \)" + "\ = (\x\A. B x) \ (\x\A. B x = \)" + by (auto simp add: INF_def Inf_top_conv) + +lemma Sup_bot_conv [no_atp]: + "\A = \ \ (\x\A. x = \)" (is ?P) + "\ = \A \ (\x\A. x = \)" (is ?Q) +proof - + interpret dual: complete_lattice Sup Inf "op \" "op >" sup inf \ \ + by (fact dual_complete_lattice) + from dual.Inf_top_conv show ?P and ?Q by simp_all +qed + +lemma SUP_bot_conv: + "(\x\A. B x) = \ \ (\x\A. B x = \)" + "\ = (\x\A. B x) \ (\x\A. B x = \)" + by (auto simp add: SUP_def Sup_bot_conv) + +lemma INF_const [simp]: "A \ {} \ (\i\A. f) = f" + by (auto intro: antisym INF_leI le_INF_I) + +lemma SUP_const [simp]: "A \ {} \ (\i\A. f) = f" + by (auto intro: antisym SUP_leI le_SUP_I) + +lemma INF_top: "(\x\A. \) = \" + by (cases "A = {}") (simp_all add: INF_empty) + +lemma SUP_bot: "(\x\A. \) = \" + by (cases "A = {}") (simp_all add: SUP_empty) + lemma INF_commute: "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)" by (iprover intro: INF_leI le_INF_I order_trans antisym) @@ -322,14 +367,6 @@ then show ?thesis by (simp add: SUP_insert) qed -lemma INF_union: - "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)" - by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INF_I INF_leI) - -lemma SUP_union: - "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)" - by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUP_I) - lemma INF_constant: "(\y\A. c) = (if A = {} then \ else c)" by (simp add: INF_empty) @@ -346,16 +383,6 @@ "(\x\A. B x) = \({Y. \x\A. Y = B x})" by (simp add: SUP_def image_def) -lemma INF_top_conv: - "\ = (\x\A. B x) \ (\x\A. B x = \)" - "(\x\A. B x) = \ \ (\x\A. B x = \)" - by (auto simp add: INF_def Inf_top_conv) - -lemma SUP_bot_conv: - "\ = (\x\A. B x) \ (\x\A. B x = \)" - "(\x\A. B x) = \ \ (\x\A. B x = \)" - by (auto simp add: SUP_def Sup_bot_conv) - lemma less_INF_D: assumes "y < (\i\A. f i)" "i \ A" shows "y < f i" proof - @@ -392,12 +419,74 @@ end -class complete_boolean_algebra = boolean_algebra + complete_lattice +class complete_distrib_lattice = complete_lattice + + assumes sup_Inf: "a \ \B = (\b\B. a \ b)" + assumes inf_Sup: "a \ \B = (\b\B. a \ b)" +begin + +lemma sup_INF: + "a \ (\b\B. f b) = (\b\B. a \ f b)" + by (simp add: INF_def sup_Inf image_image) + +lemma inf_SUP: + "a \ (\b\B. f b) = (\b\B. a \ f b)" + by (simp add: SUP_def inf_Sup image_image) + +lemma dual_complete_distrib_lattice: + "class.complete_distrib_lattice Sup Inf (op \) (op >) sup inf \ \" + apply (rule class.complete_distrib_lattice.intro) + apply (fact dual_complete_lattice) + apply (rule class.complete_distrib_lattice_axioms.intro) + apply (simp_all only: INF_foundation_dual SUP_foundation_dual inf_Sup sup_Inf) + done + +subclass distrib_lattice proof -- {* Question: is it sufficient to include @{class distrib_lattice} + and prove @{text inf_Sup} and @{text sup_Inf} from that? *} + fix a b c + from sup_Inf have "a \ \{b, c} = (\d\{b, c}. a \ d)" . + then show "a \ b \ c = (a \ b) \ (a \ c)" by (simp add: INF_def Inf_binary) +qed + +lemma Inf_sup: + "\B \ a = (\b\B. b \ a)" + by (simp add: sup_Inf sup_commute) + +lemma Sup_inf: + "\B \ a = (\b\B. b \ a)" + by (simp add: inf_Sup inf_commute) + +lemma INF_sup: + "(\b\B. f b) \ a = (\b\B. f b \ a)" + by (simp add: sup_INF sup_commute) + +lemma SUP_inf: + "(\b\B. f b) \ a = (\b\B. f b \ a)" + by (simp add: inf_SUP inf_commute) + +lemma Inf_sup_eq_top_iff: + "(\B \ a = \) \ (\b\B. b \ a = \)" + by (simp only: Inf_sup INF_top_conv) + +lemma Sup_inf_eq_bot_iff: + "(\B \ a = \) \ (\b\B. b \ a = \)" + by (simp only: Sup_inf SUP_bot_conv) + +lemma INF_sup_distrib2: + "(\a\A. f a) \ (\b\B. g b) = (\a\A. \b\B. f a \ g b)" + by (subst INF_commute) (simp add: sup_INF INF_sup) + +lemma SUP_inf_distrib2: + "(\a\A. f a) \ (\b\B. g b) = (\a\A. \b\B. f a \ g b)" + by (subst SUP_commute) (simp add: inf_SUP SUP_inf) + +end + +class complete_boolean_algebra = boolean_algebra + complete_distrib_lattice begin lemma dual_complete_boolean_algebra: "class.complete_boolean_algebra Sup Inf (op \) (op >) sup inf \ \ (\x y. x \ - y) uminus" - by (rule class.complete_boolean_algebra.intro, rule dual_complete_lattice, rule dual_boolean_algebra) + by (rule class.complete_boolean_algebra.intro, rule dual_complete_distrib_lattice, rule dual_boolean_algebra) lemma uminus_Inf: "- (\A) = \(uminus ` A)" @@ -408,6 +497,9 @@ by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto qed +lemma uminus_INF: "- (\x\A. B x) = (\x\A. - B x)" + by (simp add: INF_def SUP_def uminus_Inf image_image) + lemma uminus_Sup: "- (\A) = \(uminus ` A)" proof - @@ -415,9 +507,6 @@ then show ?thesis by simp qed -lemma uminus_INF: "- (\x\A. B x) = (\x\A. - B x)" - by (simp add: INF_def SUP_def uminus_Inf image_image) - lemma uminus_SUP: "- (\x\A. B x) = (\x\A. - B x)" by (simp add: INF_def SUP_def uminus_Sup image_image) @@ -434,14 +523,14 @@ "\S \ a \ (\x\S. x \ a)" unfolding not_le [symmetric] le_Inf_iff by auto +lemma INF_less_iff: + "(\i\A. f i) \ a \ (\x\A. f x \ a)" + unfolding INF_def Inf_less_iff by auto + lemma less_Sup_iff: "a \ \S \ (\x\S. a \ x)" unfolding not_le [symmetric] Sup_le_iff by auto -lemma INF_less_iff: - "(\i\A. f i) \ a \ (\x\A. f x \ a)" - unfolding INF_def Inf_less_iff by auto - lemma less_SUP_iff: "a \ (\i\A. f i) \ (\x\A. a \ f x)" unfolding SUP_def less_Sup_iff by auto @@ -468,6 +557,10 @@ qed qed +lemma SUP_eq_top_iff: + "(\i\A. f i) = \ \ (\x<\. \i\A. x < f i)" + unfolding SUP_def Sup_eq_top_iff by auto + lemma Inf_eq_bot_iff: "\A = \ \ (\x>\. \i\A. i < x)" proof - @@ -480,16 +573,12 @@ "(\i\A. f i) = \ \ (\x>\. \i\A. f i < x)" unfolding INF_def Inf_eq_bot_iff by auto -lemma SUP_eq_top_iff: - "(\i\A. f i) = \ \ (\x<\. \i\A. x < f i)" - unfolding SUP_def Sup_eq_top_iff by auto - end subsection {* @{typ bool} and @{typ "_ \ _"} as complete lattice *} -instantiation bool :: complete_boolean_algebra +instantiation bool :: complete_lattice begin definition @@ -521,26 +610,28 @@ by (auto simp add: Bex_def SUP_def Sup_bool_def) qed +instance bool :: complete_boolean_algebra proof +qed (auto simp add: Inf_bool_def Sup_bool_def) + instantiation "fun" :: (type, complete_lattice) complete_lattice begin definition - "\A = (\x. \{y. \f\A. y = f x})" + "\A = (\x. \f\A. f x)" lemma Inf_apply: - "(\A) x = \{y. \f\A. y = f x}" + "(\A) x = (\f\A. f x)" by (simp add: Inf_fun_def) definition - "\A = (\x. \{y. \f\A. y = f x})" + "\A = (\x. \f\A. f x)" lemma Sup_apply: - "(\A) x = \{y. \f\A. y = f x}" + "(\A) x = (\f\A. f x)" by (simp add: Sup_fun_def) instance proof -qed (auto simp add: le_fun_def Inf_apply Sup_apply - intro: Inf_lower Sup_upper Inf_greatest Sup_least) +qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_leI le_SUP_I le_INF_I SUP_leI) end @@ -552,6 +643,9 @@ "(\y\A. f y) x = (\y\A. f y x)" by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply) +instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof +qed (auto simp add: inf_apply sup_apply Inf_apply Sup_apply INF_def SUP_def inf_Sup sup_Inf image_image) + instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra .. @@ -815,9 +909,6 @@ lemma empty_Union_conv [simp,no_atp]: "({} = \A) \ (\x\A. x = {})" by (fact Sup_bot_conv) -lemma Union_disjoint: "(\C \ A = {}) \ (\B\C. B \ A = {})" -- "FIXME generalize" - by blast - lemma subset_Pow_Union: "A \ Pow (\A)" by blast @@ -997,42 +1088,43 @@ subsection {* Distributive laws *} lemma Int_Union: "A \ \B = (\C\B. A \ C)" - by blast + by (fact inf_Sup) + +lemma Un_Inter: "A \ \B = (\C\B. A \ C)" + by (fact sup_Inf) lemma Int_Union2: "\B \ A = (\C\B. C \ A)" - by blast + by (fact Sup_inf) + +lemma INT_Int_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)" + by (rule sym) (rule INF_inf_distrib) + +lemma UN_Un_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)" + by (rule sym) (rule SUP_sup_distrib) + +lemma Int_Inter_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)" + by (simp only: INT_Int_distrib INF_def) lemma Un_Union_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)" -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *} -- {* Union of a family of unions *} - by blast - -lemma UN_Un_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)" - -- {* Equivalent version *} - by blast + by (simp only: UN_Un_distrib SUP_def) -lemma Un_Inter: "A \ \B = (\C\B. A \ C)" - by blast - -lemma Int_Inter_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)" - by blast - -lemma INT_Int_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)" - -- {* Equivalent version *} - by blast +lemma Un_INT_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)" + by (fact sup_INF) lemma Int_UN_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)" -- {* Halmos, Naive Set Theory, page 35. *} - by blast - -lemma Un_INT_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)" - by blast + by (fact inf_SUP) lemma Int_UN_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)" - by blast + by (fact SUP_inf_distrib2) lemma Un_INT_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)" - by blast + by (fact INF_sup_distrib2) + +lemma Union_disjoint: "(\C \ A = {}) \ (\B\C. B \ A = {})" + by (fact Sup_inf_eq_bot_iff) subsection {* Complement *} @@ -1051,9 +1143,9 @@ lemma UN_simps [simp]: "\a B C. (\x\C. insert a (B x)) = (if C={} then {} else insert a (\x\C. B x))" - "\A B C. (\x\C. A x \ B) = ((if C={} then {} else (\x\C. A x) \ B))" + "\A B C. (\x\C. A x \ B) = ((if C={} then {} else (\x\C. A x) \ B))" "\A B C. (\x\C. A \ B x) = ((if C={} then {} else A \ (\x\C. B x)))" - "\A B C. (\x\C. A x \ B) = ((\x\C. A x) \B)" + "\A B C. (\x\C. A x \ B) = ((\x\C. A x) \ B)" "\A B C. (\x\C. A \ B x) = (A \(\x\C. B x))" "\A B C. (\x\C. A x - B) = ((\x\C. A x) - B)" "\A B C. (\x\C. A - B x) = (A - (\x\C. B x))" @@ -1063,7 +1155,7 @@ by auto lemma INT_simps [simp]: - "\A B C. (\x\C. A x \ B) = (if C={} then UNIV else (\x\C. A x) \B)" + "\A B C. (\x\C. A x \ B) = (if C={} then UNIV else (\x\C. A x) \ B)" "\A B C. (\x\C. A \ B x) = (if C={} then UNIV else A \(\x\C. B x))" "\A B C. (\x\C. A x - B) = (if C={} then UNIV else (\x\C. A x) - B)" "\A B C. (\x\C. A - B x) = (if C={} then UNIV else A - (\x\C. B x))" @@ -1087,7 +1179,7 @@ lemma UN_extend_simps: "\a B C. insert a (\x\C. B x) = (if C={} then {a} else (\x\C. insert a (B x)))" - "\A B C. (\x\C. A x) \ B = (if C={} then B else (\x\C. A x \ B))" + "\A B C. (\x\C. A x) \ B = (if C={} then B else (\x\C. A x \ B))" "\A B C. A \ (\x\C. B x) = (if C={} then A else (\x\C. A \ B x))" "\A B C. ((\x\C. A x) \ B) = (\x\C. A x \ B)" "\A B C. (A \ (\x\C. B x)) = (\x\C. A \ B x)" diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Mon Aug 08 07:13:16 2011 +0200 @@ -3,7 +3,7 @@ *) theory Cooper -imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" +imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef" uses ("cooper_tac.ML") begin diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Decision_Procs/Ferrack.thy Mon Aug 08 07:13:16 2011 +0200 @@ -4,7 +4,7 @@ theory Ferrack imports Complex_Main Dense_Linear_Order DP_Library - "~~/src/HOL/Library/Efficient_Nat" + "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef" uses ("ferrack_tac.ML") begin diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Decision_Procs/MIR.thy Mon Aug 08 07:13:16 2011 +0200 @@ -4,7 +4,7 @@ theory MIR imports Complex_Main Dense_Linear_Order DP_Library - "~~/src/HOL/Library/Efficient_Nat" + "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef" uses ("mir_tac.ML") begin diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Aug 08 07:13:16 2011 +0200 @@ -6,7 +6,7 @@ theory Parametric_Ferrante_Rackoff imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library - "~~/src/HOL/Library/Efficient_Nat" + "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef" begin subsection {* Terms *} diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/HOL.thy Mon Aug 08 07:13:16 2011 +0200 @@ -1962,10 +1962,6 @@ subsubsection {* Evaluation and normalization by evaluation *} -setup {* - Value.add_evaluator ("SML", Codegen.eval_term) -*} - ML {* fun gen_eval_method conv ctxt = SIMPLE_METHOD' (CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 (conv ctxt))) ctxt) diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/HOLCF/FOCUS/Fstream.thy --- a/src/HOL/HOLCF/FOCUS/Fstream.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy Mon Aug 08 07:13:16 2011 +0200 @@ -140,7 +140,7 @@ section "slen" -lemma slen_fscons: "#(m~> s) = iSuc (#s)" +lemma slen_fscons: "#(m~> s) = eSuc (#s)" by (simp add: fscons_def) lemma slen_fscons_eq: diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/HOLCF/FOCUS/Fstreams.thy --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy Mon Aug 08 07:13:16 2011 +0200 @@ -57,12 +57,12 @@ lemma slen_fsingleton[simp]: "#() = enat 1" by (simp add: fsingleton_def2 enat_defs) -lemma slen_fstreams[simp]: "#( ooo s) = iSuc (#s)" +lemma slen_fstreams[simp]: "#( ooo s) = eSuc (#s)" by (simp add: fsingleton_def2) -lemma slen_fstreams2[simp]: "#(s ooo ) = iSuc (#s)" +lemma slen_fstreams2[simp]: "#(s ooo ) = eSuc (#s)" apply (cases "#s") -apply (auto simp add: iSuc_enat) +apply (auto simp add: eSuc_enat) apply (insert slen_sconc [of _ s "Suc 0" ""], auto) by (simp add: sconc_def) diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/HOLCF/FOCUS/Stream_adm.thy --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy Mon Aug 08 07:13:16 2011 +0200 @@ -132,8 +132,8 @@ apply (erule allE, erule allE, drule mp) (* stream_monoP *) apply ( drule ileI1) apply ( drule order_trans) -apply ( rule ile_iSuc) -apply ( drule iSuc_ile_mono [THEN iffD1]) +apply ( rule ile_eSuc) +apply ( drule eSuc_ile_mono [THEN iffD1]) apply ( assumption) apply (drule mp) apply ( erule is_ub_thelub) diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/HOLCF/Library/Stream.thy --- a/src/HOL/HOLCF/Library/Stream.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/HOLCF/Library/Stream.thy Mon Aug 08 07:13:16 2011 +0200 @@ -329,10 +329,10 @@ lemma slen_empty [simp]: "#\ = 0" by (simp add: slen_def stream.finite_def zero_enat_def Least_equality) -lemma slen_scons [simp]: "x ~= \ ==> #(x&&xs) = iSuc (#xs)" +lemma slen_scons [simp]: "x ~= \ ==> #(x&&xs) = eSuc (#xs)" apply (case_tac "stream_finite (x && xs)") apply (simp add: slen_def, auto) -apply (simp add: stream.finite_def, auto simp add: iSuc_enat) +apply (simp add: stream.finite_def, auto simp add: eSuc_enat) apply (rule Least_Suc2, auto) (*apply (drule sym)*) (*apply (drule sym scons_eq_UU [THEN iffD1],simp)*) @@ -341,7 +341,7 @@ by (drule stream_finite_lemma1,auto) lemma slen_less_1_eq: "(#x < enat (Suc 0)) = (x = \)" -by (cases x, auto simp add: enat_0 iSuc_enat[THEN sym]) +by (cases x, auto simp add: enat_0 eSuc_enat[THEN sym]) lemma slen_empty_eq: "(#x = 0) = (x = \)" by (cases x, auto) @@ -353,7 +353,7 @@ apply (case_tac "#y") apply simp_all done -lemma slen_iSuc: "#x = iSuc n --> (? a y. x = a&&y & a ~= \ & #y = n)" +lemma slen_eSuc: "#x = eSuc n --> (? a y. x = a&&y & a ~= \ & #y = n)" by (cases x, auto) lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \" @@ -362,15 +362,15 @@ lemma slen_scons_eq_rev: "(#x < enat (Suc (Suc n))) = (!a y. x ~= a && y | a = \ | #y < enat (Suc n))" apply (cases x, auto) apply (simp add: zero_enat_def) - apply (case_tac "#stream") apply (simp_all add: iSuc_enat) - apply (case_tac "#stream") apply (simp_all add: iSuc_enat) + apply (case_tac "#stream") apply (simp_all add: eSuc_enat) + apply (case_tac "#stream") apply (simp_all add: eSuc_enat) done lemma slen_take_lemma4 [rule_format]: "!s. stream_take n$s ~= s --> #(stream_take n$s) = enat n" apply (induct n, auto simp add: enat_0) apply (case_tac "s=UU", simp) -by (drule stream_exhaust_eq [THEN iffD1], auto simp add: iSuc_enat) +by (drule stream_exhaust_eq [THEN iffD1], auto simp add: eSuc_enat) (* lemma stream_take_idempotent [simp]: @@ -398,7 +398,7 @@ apply (case_tac "x=UU", simp) apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) apply (erule_tac x="y" in allE, auto) -apply (simp_all add: not_less iSuc_enat) +apply (simp_all add: not_less eSuc_enat) apply (case_tac "#y") apply simp_all apply (case_tac "x=UU", simp) apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) @@ -448,7 +448,7 @@ apply (case_tac "x=UU", auto simp add: zero_enat_def) apply (drule stream_exhaust_eq [THEN iffD1], auto) apply (erule_tac x="y" in allE, auto) -apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_enat) +apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: eSuc_enat) by (simp add: iterate_lemma) lemma slen_take_lemma3 [rule_format]: @@ -478,7 +478,7 @@ apply (subgoal_tac "stream_take n$s ~=s") apply (insert slen_take_lemma4 [of n s],auto) apply (cases s, simp) -by (simp add: slen_take_lemma4 iSuc_enat) +by (simp add: slen_take_lemma4 eSuc_enat) (* ----------------------------------------------------------------------- *) (* theorems about smap *) @@ -593,12 +593,12 @@ apply (erule_tac x="k" in allE) apply (erule_tac x="y" in allE,auto) apply (erule_tac x="THE p. Suc p = t" in allE,auto) - apply (simp add: iSuc_def split: enat.splits) - apply (simp add: iSuc_def split: enat.splits) + apply (simp add: eSuc_def split: enat.splits) + apply (simp add: eSuc_def split: enat.splits) apply (simp only: the_equality) - apply (simp add: iSuc_def split: enat.splits) + apply (simp add: eSuc_def split: enat.splits) apply force -apply (simp add: iSuc_def split: enat.splits) +apply (simp add: eSuc_def split: enat.splits) done lemma take_i_rt_len: @@ -696,7 +696,7 @@ by auto lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y" -apply (simp add: sconc_def zero_enat_def iSuc_def split: enat.splits, auto) +apply (simp add: sconc_def zero_enat_def eSuc_def split: enat.splits, auto) apply (rule someI2_ex,auto) apply (rule_tac x="x && y" in exI,auto) apply (simp add: i_rt_Suc_forw) @@ -709,7 +709,7 @@ apply (rule stream_finite_ind [of x],auto) apply (simp add: stream.finite_def) apply (drule slen_take_lemma1,blast) - apply (simp_all add: zero_enat_def iSuc_def split: enat.splits) + apply (simp_all add: zero_enat_def eSuc_def split: enat.splits) apply (erule_tac x="y" in allE,auto) by (rule_tac x="a && w" in exI,auto) @@ -743,7 +743,7 @@ lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y" apply (cases "#x",auto) - apply (simp add: sconc_def iSuc_enat) + apply (simp add: sconc_def eSuc_enat) apply (rule someI2_ex) apply (drule ex_sconc, simp) apply (rule someI2_ex, auto) @@ -870,9 +870,9 @@ lemma sconc_finite: "(#x~=\ & #y~=\) = (#(x ooo y)~=\)" apply auto - apply (metis not_Infty_eq slen_sconc_finite1) - apply (metis not_Infty_eq slen_sconc_infinite1) -apply (metis not_Infty_eq slen_sconc_infinite2) + apply (metis not_infinity_eq slen_sconc_finite1) + apply (metis not_infinity_eq slen_sconc_infinite1) +apply (metis not_infinity_eq slen_sconc_infinite2) done (* ----------------------------------------------------------------------- *) @@ -956,7 +956,7 @@ defer 1 apply (simp add: constr_sconc_def del: scons_sconc) apply (case_tac "#s") - apply (simp add: iSuc_enat) + apply (simp add: eSuc_enat) apply (case_tac "a=UU",auto simp del: scons_sconc) apply (simp) apply (simp add: sconc_def) diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/IMP/AExp.thy --- a/src/HOL/IMP/AExp.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/IMP/AExp.thy Mon Aug 08 07:13:16 2011 +0200 @@ -23,40 +23,25 @@ text {* A little syntax magic to write larger states compactly: *} -nonterminal funlets and funlet - -syntax - "_funlet" :: "['a, 'a] => funlet" ("_ /->/ _") - "" :: "funlet => funlets" ("_") - "_Funlets" :: "[funlet, funlets] => funlets" ("_,/ _") - "_Fun" :: "funlets => 'a => 'b" ("(1[_])") - "_FunUpd" :: "['a => 'b, funlets] => 'a => 'b" ("_/'(_')" [900,0]900) - -syntax (xsymbols) - "_funlet" :: "['a, 'a] => funlet" ("_ /\/ _") - definition "null_heap \ \x. 0" - +syntax + "_State" :: "updbinds => 'a" ("<_>") translations - "_FunUpd m (_Funlets xy ms)" == "_FunUpd (_FunUpd m xy) ms" - "_FunUpd m (_funlet x y)" == "m(x := y)" - "_Fun ms" == "_FunUpd (CONST null_heap) ms" - "_Fun (_Funlets ms1 ms2)" <= "_FunUpd (_Fun ms1) ms2" - "_Funlets ms1 (_Funlets ms2 ms3)" <= "_Funlets (_Funlets ms1 ms2) ms3" + "_State ms" => "_Update (CONST null_heap) ms" text {* We can now write a series of updates to the function @{text "\x. 0"} compactly: *} -lemma "[a \ Suc 0, b \ 2] = (null_heap (a := Suc 0)) (b := 2)" +lemma " = (null_heap (a := Suc 0)) (b := 2)" by (rule refl) -value "aval (Plus (V ''x'') (N 5)) [''x'' \ 7]" +value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>" text {* Variables that are not mentioned in the state are 0 by default in - the @{term "[a \ b::int]"} syntax: + the @{term ""} syntax: *} -value "aval (Plus (V ''x'') (N 5)) [''y'' \ 7]" +value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>" subsection "Optimization" diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/IMP/ASM.thy --- a/src/HOL/IMP/ASM.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/IMP/ASM.thy Mon Aug 08 07:13:16 2011 +0200 @@ -25,7 +25,7 @@ "aexec (i#is) s stk = aexec is s (aexec1 i s stk)" value "aexec [LOADI 5, LOAD ''y'', ADD] - [''x'' \ 42, ''y'' \ 43] [50]" + <''x'' := 42, ''y'' := 43> [50]" lemma aexec_append[simp]: "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)" diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/IMP/BExp.thy --- a/src/HOL/IMP/BExp.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/IMP/BExp.thy Mon Aug 08 07:13:16 2011 +0200 @@ -11,7 +11,7 @@ "bval (Less a1 a2) s = (aval a1 s < aval a2 s)" value "bval (Less (V ''x'') (Plus (N 3) (V ''y''))) - [''x'' \ 3, ''y'' \ 1]" + <''x'' := 3, ''y'' := 1>" subsection "Optimization" diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/IMP/Big_Step.thy --- a/src/HOL/IMP/Big_Step.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/IMP/Big_Step.thy Mon Aug 08 07:13:16 2011 +0200 @@ -42,13 +42,13 @@ text{* We need to translate the result state into a list to display it. *} -values "{map t [''x''] |t. (SKIP, [''x'' \ 42]) \ t}" +values "{map t [''x''] |t. (SKIP, <''x'' := 42>) \ t}" -values "{map t [''x''] |t. (''x'' ::= N 2, [''x'' \ 42]) \ t}" +values "{map t [''x''] |t. (''x'' ::= N 2, <''x'' := 42>) \ t}" values "{map t [''x'',''y''] |t. (WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)), - [''x'' \ 0, ''y'' \ 13]) \ t}" + <''x'' := 0, ''y'' := 13>) \ t}" text{* Proof automation: *} diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/IMP/Comp_Rev.thy --- a/src/HOL/IMP/Comp_Rev.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/IMP/Comp_Rev.thy Mon Aug 08 07:13:16 2011 +0200 @@ -188,7 +188,7 @@ "1 \ isize (acomp a)" by (induct a) auto -lemma exits_acomp [simp]: +lemma acomp_exits [simp]: "exits (acomp a) = {isize (acomp a)}" by (auto simp: exits_def acomp_size) diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/IMP/Compiler.thy --- a/src/HOL/IMP/Compiler.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/IMP/Compiler.thy Mon Aug 08 07:13:16 2011 +0200 @@ -88,7 +88,7 @@ values "{(i,map t [''x'',''y''],stk) | i t stk. [LOAD ''y'', STORE ''x''] \ - (0, [''x'' \ 3, ''y'' \ 4], []) \* (i,t,stk)}" + (0, <''x'' := 3, ''y'' := 4>, []) \* (i,t,stk)}" subsection{* Verification infrastructure *} @@ -112,7 +112,7 @@ "ADD \i c \ c' = (\i s stk. c = (i, s, stk) \ c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))" "STORE x \i c \ c' = - (\i s stk. c = (i, s, stk) \ c' = (i + 1, s(x \ hd stk), tl stk))" + (\i s stk. c = (i, s, stk) \ c' = (i + 1, s(x := hd stk), tl stk))" "JMP n \i c \ c' = (\i s stk. c = (i, s, stk) \ c' = (i + 1 + n, s, stk))" "JMPFLESS n \i c \ c' = (\i s stk. c = (i, s, stk) \ diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/IMP/Small_Step.thy --- a/src/HOL/IMP/Small_Step.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/IMP/Small_Step.thy Mon Aug 08 07:13:16 2011 +0200 @@ -27,7 +27,7 @@ values "{(c',map t [''x'',''y'',''z'']) |c' t. (''x'' ::= V ''z''; ''y'' ::= V ''x'', - [''x'' \ 3, ''y'' \ 7, ''z'' \ 5]) \* (c',t)}" + <''x'' := 3, ''y'' := 7, ''z'' := 5>) \* (c',t)}" subsection{* Proof infrastructure *} diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/IMP/Types.thy --- a/src/HOL/IMP/Types.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/IMP/Types.thy Mon Aug 08 07:13:16 2011 +0200 @@ -17,7 +17,7 @@ "taval (V x) s (s x)" | "taval a1 s (Iv i1) \ taval a2 s (Iv i2) \ taval (Plus a1 a2) s (Iv(i1+i2))" | -"taval a\<^isub>1 s (Rv r1) \ taval a2 s (Rv r2) +"taval a1 s (Rv r1) \ taval a2 s (Rv r2) \ taval (Plus a1 a2) s (Rv(r1+r2))" inductive_cases [elim!]: @@ -32,9 +32,9 @@ inductive tbval :: "bexp \ state \ bool \ bool" where "tbval (B bv) s bv" | "tbval b s bv \ tbval (Not b) s (\ bv)" | -"tbval b\<^isub>1 s bv1 \ tbval b2 s bv2 \ tbval (And b1 b2) s (bv1 & bv2)" | -"taval a\<^isub>1 s (Iv i1) \ taval a2 s (Iv i2) \ tbval (Less a1 a2) s (i1 < i2)" | -"taval a\<^isub>1 s (Rv r1) \ taval a2 s (Rv r2) \ tbval (Less a1 a2) s (r1 < r2)" +"tbval b1 s bv1 \ tbval b2 s bv2 \ tbval (And b1 b2) s (bv1 & bv2)" | +"taval a1 s (Iv i1) \ taval a2 s (Iv i2) \ tbval (Less a1 a2) s (i1 < i2)" | +"taval a1 s (Rv r1) \ taval a2 s (Rv r2) \ tbval (Less a1 a2) s (r1 < r2)" subsection "Syntax of Commands" (* a copy of Com.thy - keep in sync! *) diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Induct/Sexp.thy --- a/src/HOL/Induct/Sexp.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Induct/Sexp.thy Mon Aug 08 07:13:16 2011 +0200 @@ -6,7 +6,7 @@ structures by hand. *) -theory Sexp imports Main begin +theory Sexp imports Main "~~/src/HOL/Library/Wfrec" begin type_synonym 'a item = "'a Datatype.item" abbreviation "Leaf == Datatype.Leaf" diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/IsaMakefile Mon Aug 08 07:13:16 2011 +0200 @@ -292,7 +292,6 @@ Quotient.thy \ Random.thy \ Random_Sequence.thy \ - Recdef.thy \ Record.thy \ Refute.thy \ Semiring_Normalization.thy \ @@ -359,7 +358,6 @@ Tools/Quotient/quotient_tacs.ML \ Tools/Quotient/quotient_term.ML \ Tools/Quotient/quotient_typ.ML \ - Tools/recdef.ML \ Tools/record.ML \ Tools/semiring_normalizer.ML \ Tools/Sledgehammer/async_manager.ML \ @@ -389,15 +387,6 @@ Tools/string_code.ML \ Tools/string_syntax.ML \ Tools/transfer.ML \ - Tools/TFL/casesplit.ML \ - Tools/TFL/dcterm.ML \ - Tools/TFL/post.ML \ - Tools/TFL/rules.ML \ - Tools/TFL/tfl.ML \ - Tools/TFL/thms.ML \ - Tools/TFL/thry.ML \ - Tools/TFL/usyntax.ML \ - Tools/TFL/utils.ML $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES) @$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main @@ -464,12 +453,14 @@ Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy \ Library/More_List.thy Library/More_Set.thy Library/Multiset.thy \ Library/Nat_Bijection.thy Library/Nested_Environment.thy \ - Library/Numeral_Type.thy Library/OptionalSugar.thy \ + Library/Numeral_Type.thy Library/Old_Recdef.thy \ + Library/OptionalSugar.thy \ Library/Order_Relation.thy Library/Permutation.thy \ Library/Permutations.thy Library/Poly_Deriv.thy \ Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \ Library/Preorder.thy Library/Product_Vector.thy \ Library/Product_ord.thy Library/Product_plus.thy \ + Library/Product_Lattice.thy \ Library/Quickcheck_Types.thy \ Library/Quotient_List.thy Library/Quotient_Option.thy \ Library/Quotient_Product.thy Library/Quotient_Sum.thy \ @@ -482,10 +473,14 @@ Library/Sum_of_Squares/sos_wrapper.ML \ Library/Sum_of_Squares/sum_of_squares.ML \ Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \ - Library/While_Combinator.thy Library/Zorn.thy \ + Library/Wfrec.thy Library/While_Combinator.thy Library/Zorn.thy \ $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ Library/reflection.ML Library/reify_data.ML \ - Library/document/root.bib Library/document/root.tex + Library/document/root.bib Library/document/root.tex \ + Tools/TFL/casesplit.ML Tools/TFL/dcterm.ML Tools/TFL/post.ML \ + Tools/TFL/rules.ML Tools/TFL/tfl.ML Tools/TFL/thms.ML \ + Tools/TFL/thry.ML Tools/TFL/usyntax.ML Tools/TFL/utils.ML \ + Tools/recdef.ML @cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Library/Extended_Nat.thy --- a/src/HOL/Library/Extended_Nat.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Library/Extended_Nat.thy Mon Aug 08 07:13:16 2011 +0200 @@ -49,14 +49,14 @@ declare [[coercion "enat::nat\enat"]] -lemma not_Infty_eq[iff]: "(x \ \) = (EX i. x = enat i)" -by (cases x) auto +lemma not_infinity_eq [iff]: "(x \ \) = (EX i. x = enat i)" + by (cases x) auto lemma not_enat_eq [iff]: "(ALL y. x ~= enat y) = (x = \)" -by (cases x) auto + by (cases x) auto primrec the_enat :: "enat \ nat" -where "the_enat (enat n) = n" + where "the_enat (enat n) = n" subsection {* Constructors and numbers *} @@ -76,8 +76,8 @@ end -definition iSuc :: "enat \ enat" where - "iSuc i = (case i of enat n \ enat (Suc n) | \ \ \)" +definition eSuc :: "enat \ enat" where + "eSuc i = (case i of enat n \ enat (Suc n) | \ \ \)" lemma enat_0: "enat 0 = 0" by (simp add: zero_enat_def) @@ -88,13 +88,13 @@ lemma enat_number: "enat (number_of k) = number_of k" by (simp add: number_of_enat_def) -lemma one_iSuc: "1 = iSuc 0" - by (simp add: zero_enat_def one_enat_def iSuc_def) +lemma one_eSuc: "1 = eSuc 0" + by (simp add: zero_enat_def one_enat_def eSuc_def) -lemma Infty_ne_i0 [simp]: "(\::enat) \ 0" +lemma infinity_ne_i0 [simp]: "(\::enat) \ 0" by (simp add: zero_enat_def) -lemma i0_ne_Infty [simp]: "0 \ (\::enat)" +lemma i0_ne_infinity [simp]: "0 \ (\::enat)" by (simp add: zero_enat_def) lemma zero_enat_eq [simp]: @@ -112,35 +112,35 @@ "\ 1 = (0\enat)" unfolding zero_enat_def one_enat_def by simp_all -lemma Infty_ne_i1 [simp]: "(\::enat) \ 1" +lemma infinity_ne_i1 [simp]: "(\::enat) \ 1" by (simp add: one_enat_def) -lemma i1_ne_Infty [simp]: "1 \ (\::enat)" +lemma i1_ne_infinity [simp]: "1 \ (\::enat)" by (simp add: one_enat_def) -lemma Infty_ne_number [simp]: "(\::enat) \ number_of k" +lemma infinity_ne_number [simp]: "(\::enat) \ number_of k" by (simp add: number_of_enat_def) -lemma number_ne_Infty [simp]: "number_of k \ (\::enat)" +lemma number_ne_infinity [simp]: "number_of k \ (\::enat)" by (simp add: number_of_enat_def) -lemma iSuc_enat: "iSuc (enat n) = enat (Suc n)" - by (simp add: iSuc_def) +lemma eSuc_enat: "eSuc (enat n) = enat (Suc n)" + by (simp add: eSuc_def) -lemma iSuc_number_of: "iSuc (number_of k) = enat (Suc (number_of k))" - by (simp add: iSuc_enat number_of_enat_def) +lemma eSuc_number_of: "eSuc (number_of k) = enat (Suc (number_of k))" + by (simp add: eSuc_enat number_of_enat_def) -lemma iSuc_Infty [simp]: "iSuc \ = \" - by (simp add: iSuc_def) +lemma eSuc_infinity [simp]: "eSuc \ = \" + by (simp add: eSuc_def) -lemma iSuc_ne_0 [simp]: "iSuc n \ 0" - by (simp add: iSuc_def zero_enat_def split: enat.splits) +lemma eSuc_ne_0 [simp]: "eSuc n \ 0" + by (simp add: eSuc_def zero_enat_def split: enat.splits) -lemma zero_ne_iSuc [simp]: "0 \ iSuc n" - by (rule iSuc_ne_0 [symmetric]) +lemma zero_ne_eSuc [simp]: "0 \ eSuc n" + by (rule eSuc_ne_0 [symmetric]) -lemma iSuc_inject [simp]: "iSuc m = iSuc n \ m = n" - by (simp add: iSuc_def split: enat.splits) +lemma eSuc_inject [simp]: "eSuc m = eSuc n \ m = n" + by (simp add: eSuc_def split: enat.splits) lemma number_of_enat_inject [simp]: "(number_of k \ enat) = number_of l \ (number_of k \ nat) = number_of l" @@ -184,28 +184,28 @@ else if l < Int.Pls then number_of k else number_of (k + l))" unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ enat] .. -lemma iSuc_number [simp]: - "iSuc (number_of k) = (if neg (number_of k \ int) then 1 else number_of (Int.succ k))" - unfolding iSuc_number_of +lemma eSuc_number [simp]: + "eSuc (number_of k) = (if neg (number_of k \ int) then 1 else number_of (Int.succ k))" + unfolding eSuc_number_of unfolding one_enat_def number_of_enat_def Suc_nat_number_of if_distrib [symmetric] .. -lemma iSuc_plus_1: - "iSuc n = n + 1" - by (cases n) (simp_all add: iSuc_enat one_enat_def) +lemma eSuc_plus_1: + "eSuc n = n + 1" + by (cases n) (simp_all add: eSuc_enat one_enat_def) -lemma plus_1_iSuc: - "1 + q = iSuc q" - "q + 1 = iSuc q" -by (simp_all add: iSuc_plus_1 add_ac) +lemma plus_1_eSuc: + "1 + q = eSuc q" + "q + 1 = eSuc q" + by (simp_all add: eSuc_plus_1 add_ac) -lemma iadd_Suc: "iSuc m + n = iSuc (m + n)" -by (simp_all add: iSuc_plus_1 add_ac) +lemma iadd_Suc: "eSuc m + n = eSuc (m + n)" + by (simp_all add: eSuc_plus_1 add_ac) -lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)" -by (simp only: add_commute[of m] iadd_Suc) +lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)" + by (simp only: add_commute[of m] iadd_Suc) lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \ n = 0)" -by (cases m, cases n, simp_all add: zero_enat_def) + by (cases m, cases n, simp_all add: zero_enat_def) subsection {* Multiplication *} @@ -251,16 +251,16 @@ end -lemma mult_iSuc: "iSuc m * n = n + m * n" - unfolding iSuc_plus_1 by (simp add: algebra_simps) +lemma mult_eSuc: "eSuc m * n = n + m * n" + unfolding eSuc_plus_1 by (simp add: algebra_simps) -lemma mult_iSuc_right: "m * iSuc n = m + m * n" - unfolding iSuc_plus_1 by (simp add: algebra_simps) +lemma mult_eSuc_right: "m * eSuc n = m + m * n" + unfolding eSuc_plus_1 by (simp add: algebra_simps) lemma of_nat_eq_enat: "of_nat n = enat n" apply (induct n) apply (simp add: enat_0) - apply (simp add: plus_1_iSuc iSuc_enat) + apply (simp add: plus_1_eSuc eSuc_enat) done instance enat :: number_semiring @@ -274,11 +274,11 @@ then show "inj (\n. of_nat n :: enat)" by (simp add: of_nat_eq_enat) qed -lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \ n = 0)" -by(auto simp add: times_enat_def zero_enat_def split: enat.split) +lemma imult_is_0 [simp]: "((m::enat) * n = 0) = (m = 0 \ n = 0)" + by (auto simp add: times_enat_def zero_enat_def split: enat.split) -lemma imult_is_Infty: "((a::enat) * b = \) = (a = \ \ b \ 0 \ b = \ \ a \ 0)" -by(auto simp add: times_enat_def zero_enat_def split: enat.split) +lemma imult_is_infinity: "((a::enat) * b = \) = (a = \ \ b \ 0 \ b = \ \ a \ 0)" + by (auto simp add: times_enat_def zero_enat_def split: enat.split) subsection {* Subtraction *} @@ -294,33 +294,33 @@ end -lemma idiff_enat_enat[simp,code]: "enat a - enat b = enat (a - b)" -by(simp add: diff_enat_def) +lemma idiff_enat_enat [simp,code]: "enat a - enat b = enat (a - b)" + by (simp add: diff_enat_def) -lemma idiff_Infty[simp,code]: "\ - n = (\::enat)" -by(simp add: diff_enat_def) +lemma idiff_infinity [simp,code]: "\ - n = (\::enat)" + by (simp add: diff_enat_def) -lemma idiff_Infty_right[simp,code]: "enat a - \ = 0" -by(simp add: diff_enat_def) +lemma idiff_infinity_right [simp,code]: "enat a - \ = 0" + by (simp add: diff_enat_def) -lemma idiff_0[simp]: "(0::enat) - n = 0" -by (cases n, simp_all add: zero_enat_def) +lemma idiff_0 [simp]: "(0::enat) - n = 0" + by (cases n, simp_all add: zero_enat_def) -lemmas idiff_enat_0[simp] = idiff_0[unfolded zero_enat_def] +lemmas idiff_enat_0 [simp] = idiff_0 [unfolded zero_enat_def] -lemma idiff_0_right[simp]: "(n::enat) - 0 = n" -by (cases n) (simp_all add: zero_enat_def) +lemma idiff_0_right [simp]: "(n::enat) - 0 = n" + by (cases n) (simp_all add: zero_enat_def) -lemmas idiff_enat_0_right[simp] = idiff_0_right[unfolded zero_enat_def] +lemmas idiff_enat_0_right [simp] = idiff_0_right [unfolded zero_enat_def] -lemma idiff_self[simp]: "n \ \ \ (n::enat) - n = 0" -by(auto simp: zero_enat_def) +lemma idiff_self [simp]: "n \ \ \ (n::enat) - n = 0" + by (auto simp: zero_enat_def) -lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m" -by(simp add: iSuc_def split: enat.split) +lemma eSuc_minus_eSuc [simp]: "eSuc n - eSuc m = n - m" + by (simp add: eSuc_def split: enat.split) -lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n" -by(simp add: one_enat_def iSuc_enat[symmetric] zero_enat_def[symmetric]) +lemma eSuc_minus_1 [simp]: "eSuc n - 1 = n" + by (simp add: one_enat_def eSuc_enat[symmetric] zero_enat_def[symmetric]) (*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*) @@ -378,58 +378,58 @@ by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) lemma ile0_eq [simp]: "n \ (0\enat) \ n = 0" -by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) - -lemma Infty_ileE [elim!]: "\ \ enat m \ R" by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) -lemma Infty_ilessE [elim!]: "\ < enat m \ R" +lemma infinity_ileE [elim!]: "\ \ enat m \ R" + by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) + +lemma infinity_ilessE [elim!]: "\ < enat m \ R" by simp lemma not_iless0 [simp]: "\ n < (0\enat)" by (simp add: zero_enat_def less_enat_def split: enat.splits) lemma i0_less [simp]: "(0\enat) < n \ n \ 0" -by (simp add: zero_enat_def less_enat_def split: enat.splits) + by (simp add: zero_enat_def less_enat_def split: enat.splits) -lemma iSuc_ile_mono [simp]: "iSuc n \ iSuc m \ n \ m" - by (simp add: iSuc_def less_eq_enat_def split: enat.splits) +lemma eSuc_ile_mono [simp]: "eSuc n \ eSuc m \ n \ m" + by (simp add: eSuc_def less_eq_enat_def split: enat.splits) -lemma iSuc_mono [simp]: "iSuc n < iSuc m \ n < m" - by (simp add: iSuc_def less_enat_def split: enat.splits) +lemma eSuc_mono [simp]: "eSuc n < eSuc m \ n < m" + by (simp add: eSuc_def less_enat_def split: enat.splits) -lemma ile_iSuc [simp]: "n \ iSuc n" - by (simp add: iSuc_def less_eq_enat_def split: enat.splits) +lemma ile_eSuc [simp]: "n \ eSuc n" + by (simp add: eSuc_def less_eq_enat_def split: enat.splits) -lemma not_iSuc_ilei0 [simp]: "\ iSuc n \ 0" - by (simp add: zero_enat_def iSuc_def less_eq_enat_def split: enat.splits) +lemma not_eSuc_ilei0 [simp]: "\ eSuc n \ 0" + by (simp add: zero_enat_def eSuc_def less_eq_enat_def split: enat.splits) -lemma i0_iless_iSuc [simp]: "0 < iSuc n" - by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.splits) +lemma i0_iless_eSuc [simp]: "0 < eSuc n" + by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.splits) -lemma iless_iSuc0[simp]: "(n < iSuc 0) = (n = 0)" -by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.split) +lemma iless_eSuc0[simp]: "(n < eSuc 0) = (n = 0)" + by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.split) -lemma ileI1: "m < n \ iSuc m \ n" - by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits) +lemma ileI1: "m < n \ eSuc m \ n" + by (simp add: eSuc_def less_eq_enat_def less_enat_def split: enat.splits) lemma Suc_ile_eq: "enat (Suc m) \ n \ enat m < n" by (cases n) auto -lemma iless_Suc_eq [simp]: "enat m < iSuc n \ enat m \ n" - by (auto simp add: iSuc_def less_enat_def split: enat.splits) +lemma iless_Suc_eq [simp]: "enat m < eSuc n \ enat m \ n" + by (auto simp add: eSuc_def less_enat_def split: enat.splits) -lemma imult_Infty: "(0::enat) < n \ \ * n = \" -by (simp add: zero_enat_def less_enat_def split: enat.splits) +lemma imult_infinity: "(0::enat) < n \ \ * n = \" + by (simp add: zero_enat_def less_enat_def split: enat.splits) -lemma imult_Infty_right: "(0::enat) < n \ n * \ = \" -by (simp add: zero_enat_def less_enat_def split: enat.splits) +lemma imult_infinity_right: "(0::enat) < n \ n * \ = \" + by (simp add: zero_enat_def less_enat_def split: enat.splits) lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \ 0 < n)" -by (simp only: i0_less imult_is_0, simp) + by (simp only: i0_less imult_is_0, simp) -lemma mono_iSuc: "mono iSuc" -by(simp add: mono_def) +lemma mono_eSuc: "mono eSuc" + by (simp add: mono_def) lemma min_enat_simps [simp]: @@ -462,7 +462,7 @@ apply (drule spec) apply (erule exE) apply (drule ileI1) -apply (rule iSuc_enat [THEN subst]) +apply (rule eSuc_enat [THEN subst]) apply (rule exI) apply (erule (1) le_less_trans) done @@ -500,7 +500,7 @@ "[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P" by (induct n) auto -lemma less_InftyE: +lemma less_infinityE: "[| n < \; !!k. n = enat k ==> P |] ==> P" by (induct n) auto @@ -519,7 +519,7 @@ next show "P \" apply (rule prem, clarify) - apply (erule less_InftyE) + apply (erule less_infinityE) apply (simp add: P_enat) done qed @@ -568,7 +568,7 @@ subsection {* Traditional theorem names *} -lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def iSuc_def +lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def eSuc_def plus_enat_def less_eq_enat_def less_enat_def end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Library/Library.thy Mon Aug 08 07:13:16 2011 +0200 @@ -39,6 +39,7 @@ Multiset Nested_Environment Numeral_Type + Old_Recdef OptionalSugar Option_ord Permutation @@ -60,6 +61,7 @@ Sum_of_Squares Transitive_Closure_Table Univ_Poly + Wfrec While_Combinator Zorn begin diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Library/More_List.thy --- a/src/HOL/Library/More_List.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Library/More_List.thy Mon Aug 08 07:13:16 2011 +0200 @@ -35,7 +35,7 @@ "fold f (rev xs) = foldr f xs" by (simp add: foldr_fold_rev) -lemma fold_cong [fundef_cong, recdef_cong]: +lemma fold_cong [fundef_cong]: "a = b \ xs = ys \ (\x. x \ set xs \ f x = g x) \ fold f xs a = fold g ys b" by (induct ys arbitrary: a b xs) simp_all diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Library/Old_Recdef.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Old_Recdef.thy Mon Aug 08 07:13:16 2011 +0200 @@ -0,0 +1,101 @@ +(* Title: HOL/Library/Old_Recdef.thy + Author: Konrad Slind and Markus Wenzel, TU Muenchen +*) + +header {* TFL: recursive function definitions *} + +theory Old_Recdef +imports Wfrec +uses + ("~~/src/HOL/Tools/TFL/casesplit.ML") + ("~~/src/HOL/Tools/TFL/utils.ML") + ("~~/src/HOL/Tools/TFL/usyntax.ML") + ("~~/src/HOL/Tools/TFL/dcterm.ML") + ("~~/src/HOL/Tools/TFL/thms.ML") + ("~~/src/HOL/Tools/TFL/rules.ML") + ("~~/src/HOL/Tools/TFL/thry.ML") + ("~~/src/HOL/Tools/TFL/tfl.ML") + ("~~/src/HOL/Tools/TFL/post.ML") + ("~~/src/HOL/Tools/recdef.ML") +begin + +subsection {* Lemmas for TFL *} + +lemma tfl_wf_induct: "ALL R. wf R --> + (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))" +apply clarify +apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast) +done + +lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)" +apply clarify +apply (rule cut_apply, assumption) +done + +lemma tfl_wfrec: + "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)" +apply clarify +apply (erule wfrec) +done + +lemma tfl_eq_True: "(x = True) --> x" + by blast + +lemma tfl_rev_eq_mp: "(x = y) --> y --> x"; + by blast + +lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)" + by blast + +lemma tfl_P_imp_P_iff_True: "P ==> P = True" + by blast + +lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)" + by blast + +lemma tfl_disj_assoc: "(a \ b) \ c == a \ (b \ c)" + by simp + +lemma tfl_disjE: "P \ Q ==> P --> R ==> Q --> R ==> R" + by blast + +lemma tfl_exE: "\x. P x ==> \x. P x --> Q ==> Q" + by blast + +use "~~/src/HOL/Tools/TFL/casesplit.ML" +use "~~/src/HOL/Tools/TFL/utils.ML" +use "~~/src/HOL/Tools/TFL/usyntax.ML" +use "~~/src/HOL/Tools/TFL/dcterm.ML" +use "~~/src/HOL/Tools/TFL/thms.ML" +use "~~/src/HOL/Tools/TFL/rules.ML" +use "~~/src/HOL/Tools/TFL/thry.ML" +use "~~/src/HOL/Tools/TFL/tfl.ML" +use "~~/src/HOL/Tools/TFL/post.ML" +use "~~/src/HOL/Tools/recdef.ML" +setup Recdef.setup + +subsection {* Rule setup *} + +lemmas [recdef_simp] = + inv_image_def + measure_def + lex_prod_def + same_fst_def + less_Suc_eq [THEN iffD2] + +lemmas [recdef_cong] = + if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong + map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong + +lemmas [recdef_wf] = + wf_trancl + wf_less_than + wf_lex_prod + wf_inv_image + wf_measure + wf_measures + wf_pred_nat + wf_same_fst + wf_empty + +end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Library/Product_Lattice.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Product_Lattice.thy Mon Aug 08 07:13:16 2011 +0200 @@ -0,0 +1,198 @@ +(* Title: Product_Lattice.thy + Author: Brian Huffman +*) + +header {* Lattice operations on product types *} + +theory Product_Lattice +imports "~~/src/HOL/Library/Product_plus" +begin + +subsection {* Pointwise ordering *} + +instantiation prod :: (ord, ord) ord +begin + +definition + "x \ y \ fst x \ fst y \ snd x \ snd y" + +definition + "(x::'a \ 'b) < y \ x \ y \ \ y \ x" + +instance .. + +end + +lemma fst_mono: "x \ y \ fst x \ fst y" + unfolding less_eq_prod_def by simp + +lemma snd_mono: "x \ y \ snd x \ snd y" + unfolding less_eq_prod_def by simp + +lemma Pair_mono: "x \ x' \ y \ y' \ (x, y) \ (x', y')" + unfolding less_eq_prod_def by simp + +lemma Pair_le [simp]: "(a, b) \ (c, d) \ a \ c \ b \ d" + unfolding less_eq_prod_def by simp + +instance prod :: (preorder, preorder) preorder +proof + fix x y z :: "'a \ 'b" + show "x < y \ x \ y \ \ y \ x" + by (rule less_prod_def) + show "x \ x" + unfolding less_eq_prod_def + by fast + assume "x \ y" and "y \ z" thus "x \ z" + unfolding less_eq_prod_def + by (fast elim: order_trans) +qed + +instance prod :: (order, order) order + by default auto + + +subsection {* Binary infimum and supremum *} + +instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf +begin + +definition + "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))" + +lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)" + unfolding inf_prod_def by simp + +lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)" + unfolding inf_prod_def by simp + +lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)" + unfolding inf_prod_def by simp + +instance + by default auto + +end + +instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup +begin + +definition + "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))" + +lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)" + unfolding sup_prod_def by simp + +lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)" + unfolding sup_prod_def by simp + +lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)" + unfolding sup_prod_def by simp + +instance + by default auto + +end + +instance prod :: (lattice, lattice) lattice .. + +instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice + by default (auto simp add: sup_inf_distrib1) + + +subsection {* Top and bottom elements *} + +instantiation prod :: (top, top) top +begin + +definition + "top = (top, top)" + +lemma fst_top [simp]: "fst top = top" + unfolding top_prod_def by simp + +lemma snd_top [simp]: "snd top = top" + unfolding top_prod_def by simp + +lemma Pair_top_top: "(top, top) = top" + unfolding top_prod_def by simp + +instance + by default (auto simp add: top_prod_def) + +end + +instantiation prod :: (bot, bot) bot +begin + +definition + "bot = (bot, bot)" + +lemma fst_bot [simp]: "fst bot = bot" + unfolding bot_prod_def by simp + +lemma snd_bot [simp]: "snd bot = bot" + unfolding bot_prod_def by simp + +lemma Pair_bot_bot: "(bot, bot) = bot" + unfolding bot_prod_def by simp + +instance + by default (auto simp add: bot_prod_def) + +end + +instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice .. + +instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra + by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq) + + +subsection {* Complete lattice operations *} + +instantiation prod :: (complete_lattice, complete_lattice) complete_lattice +begin + +definition + "Sup A = (SUP x:A. fst x, SUP x:A. snd x)" + +definition + "Inf A = (INF x:A. fst x, INF x:A. snd x)" + +instance + by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def + INF_leI le_SUPI le_INF_iff SUP_le_iff) + +end + +lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)" + unfolding Sup_prod_def by simp + +lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)" + unfolding Sup_prod_def by simp + +lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)" + unfolding Inf_prod_def by simp + +lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)" + unfolding Inf_prod_def by simp + +lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))" + by (simp add: SUPR_def fst_Sup image_image) + +lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))" + by (simp add: SUPR_def snd_Sup image_image) + +lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))" + by (simp add: INFI_def fst_Inf image_image) + +lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))" + by (simp add: INFI_def snd_Inf image_image) + +lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)" + by (simp add: SUPR_def Sup_prod_def image_image) + +lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)" + by (simp add: INFI_def Inf_prod_def image_image) + +end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Library/ROOT.ML --- a/src/HOL/Library/ROOT.ML Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Library/ROOT.ML Mon Aug 08 07:13:16 2011 +0200 @@ -2,4 +2,5 @@ (* Classical Higher-order Logic -- batteries included *) use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order", + "Product_Lattice", "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)]; diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Library/Wfrec.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Wfrec.thy Mon Aug 08 07:13:16 2011 +0200 @@ -0,0 +1,121 @@ +(* Title: HOL/Library/Wfrec.thy + Author: Tobias Nipkow + Author: Lawrence C Paulson + Author: Konrad Slind +*) + +header {* Well-Founded Recursion Combinator *} + +theory Wfrec +imports Main +begin + +inductive + wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool" + for R :: "('a * 'a) set" + and F :: "('a => 'b) => 'a => 'b" +where + wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==> + wfrec_rel R F x (F g x)" + +definition + cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where + "cut f r x == (%y. if (y,x):r then f y else undefined)" + +definition + adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where + "adm_wf R F == ALL f g x. + (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x" + +definition + wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where + "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" + +lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))" +by (simp add: fun_eq_iff cut_def) + +lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)" +by (simp add: cut_def) + +text{*Inductive characterization of wfrec combinator; for details see: +John Harrison, "Inductive definitions: automation and application"*} + +lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y" +apply (simp add: adm_wf_def) +apply (erule_tac a=x in wf_induct) +apply (rule ex1I) +apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI) +apply (fast dest!: theI') +apply (erule wfrec_rel.cases, simp) +apply (erule allE, erule allE, erule allE, erule mp) +apply (fast intro: the_equality [symmetric]) +done + +lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)" +apply (simp add: adm_wf_def) +apply (intro strip) +apply (rule cuts_eq [THEN iffD2, THEN subst], assumption) +apply (rule refl) +done + +lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a" +apply (simp add: wfrec_def) +apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption) +apply (rule wfrec_rel.wfrecI) +apply (intro strip) +apply (erule adm_lemma [THEN wfrec_unique, THEN theI']) +done + + +text{** This form avoids giant explosions in proofs. NOTE USE OF ==*} +lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a" +apply auto +apply (blast intro: wfrec) +done + + +subsection {* Nitpick setup *} + +axiomatization wf_wfrec :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" + +definition wf_wfrec' :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where +[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x" + +definition wfrec' :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where +"wfrec' R F x \ if wf R then wf_wfrec' R F x + else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" + +setup {* + Nitpick_HOL.register_ersatz_global + [(@{const_name wf_wfrec}, @{const_name wf_wfrec'}), + (@{const_name wfrec}, @{const_name wfrec'})] +*} + +hide_const (open) wf_wfrec wf_wfrec' wfrec' +hide_fact (open) wf_wfrec'_def wfrec'_def + +subsection {* Wellfoundedness of @{text same_fst} *} + +definition + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set" +where + "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}" + --{*For @{text rec_def} declarations where the first n parameters + stay unchanged in the recursive call. *} + +lemma same_fstI [intro!]: + "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R" +by (simp add: same_fst_def) + +lemma wf_same_fst: + assumes prem: "(!!x. P x ==> wf(R x))" + shows "wf(same_fst P R)" +apply (simp cong del: imp_cong add: wf_def same_fst_def) +apply (intro strip) +apply (rename_tac a b) +apply (case_tac "wf (R a)") + apply (erule_tac a = b in wf_induct, blast) +apply (blast intro: prem) +done + +end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/List.thy --- a/src/HOL/List.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/List.thy Mon Aug 08 07:13:16 2011 +0200 @@ -5,7 +5,7 @@ header {* The datatype of finite lists *} theory List -imports Plain Presburger Recdef Code_Numeral Quotient ATP +imports Plain Presburger Code_Numeral Quotient ATP uses ("Tools/list_code.ML") ("Tools/list_to_set_comprehension.ML") @@ -800,7 +800,7 @@ lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)" by (induct xs) auto -lemma map_cong [fundef_cong, recdef_cong]: +lemma map_cong [fundef_cong]: "xs = ys \ (\x. x \ set ys \ f x = g x) \ map f xs = map g ys" by simp @@ -1237,7 +1237,7 @@ (\us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs)" by(auto dest:Cons_eq_filterD) -lemma filter_cong[fundef_cong, recdef_cong]: +lemma filter_cong[fundef_cong]: "xs = ys \ (\x. x \ set ys \ P x = Q x) \ filter P xs = filter Q ys" apply simp apply(erule thin_rl) @@ -2003,12 +2003,12 @@ apply(auto) done -lemma takeWhile_cong [fundef_cong, recdef_cong]: +lemma takeWhile_cong [fundef_cong]: "[| l = k; !!x. x : set l ==> P x = Q x |] ==> takeWhile P l = takeWhile Q k" by (induct k arbitrary: l) (simp_all) -lemma dropWhile_cong [fundef_cong, recdef_cong]: +lemma dropWhile_cong [fundef_cong]: "[| l = k; !!x. x : set l ==> P x = Q x |] ==> dropWhile P l = dropWhile Q k" by (induct k arbitrary: l, simp_all) @@ -2349,12 +2349,12 @@ shows "foldl (\s x. f x s) (h s) xs = h (foldl (\s x. g x s) s xs)" by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_iff) -lemma foldl_cong [fundef_cong, recdef_cong]: +lemma foldl_cong [fundef_cong]: "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] ==> foldl f a l = foldl g b k" by (induct k arbitrary: a b l) simp_all -lemma foldr_cong [fundef_cong, recdef_cong]: +lemma foldr_cong [fundef_cong]: "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] ==> foldr f l a = foldr g k b" by (induct k arbitrary: a b l) simp_all @@ -4586,7 +4586,7 @@ definition "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)" -lemma wf_measures[recdef_wf, simp]: "wf (measures fs)" +lemma wf_measures[simp]: "wf (measures fs)" unfolding measures_def by blast diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/MicroJava/BV/BVExample.thy --- a/src/HOL/MicroJava/BV/BVExample.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Aug 08 07:13:16 2011 +0200 @@ -21,13 +21,6 @@ *} section "Setup" -text {* - Since the types @{typ cnam}, @{text vnam}, and @{text mname} are - anonymous, we describe distinctness of names in the example by axioms: -*} -axioms - distinct_classes: "list_nam \ test_nam" - distinct_fields: "val_nam \ next_nam" text {* Abbreviations for definitions we will have to use often in the proofs below: *} @@ -415,35 +408,45 @@ in kiljvm G mxs (1+size pTs+mxl) rT et instr start)" lemma [code]: - "unstables r step ss = (UN p:{..stable r step ss p then {p} else {})" - apply (unfold unstables_def) - apply (rule equalityI) - apply (rule subsetI) - apply (erule CollectE) - apply (erule conjE) - apply (rule UN_I) - apply simp - apply simp - apply (rule subsetI) - apply (erule UN_E) - apply (case_tac "\ stable r step ss p") - apply simp+ - done + "unstables r step ss = + foldr (\p A. if \stable r step ss p then insert p A else A) [0..stable r step ss p then {p} else {})" + apply (unfold unstables_def) + apply (rule equalityI) + apply (rule subsetI) + apply (erule CollectE) + apply (erule conjE) + apply (rule UN_I) + apply simp + apply simp + apply (rule subsetI) + apply (erule UN_E) + apply (case_tac "\ stable r step ss p") + apply simp+ + done + also have "\f. (UN p:{.. \ (\p. if \ stable r step ss p then {p} else {}) = + (\p A. if \stable r step ss p then insert p A else A)" + by(auto simp add: fun_eq_iff) + finally show ?thesis . +qed -definition some_elem :: "'a set \ 'a" where +definition some_elem :: "'a set \ 'a" where [code del]: "some_elem = (%S. SOME x. x : S)" - -consts_code - "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)") +code_const some_elem + (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)") +setup {* Code.add_signature_cmd ("some_elem", "'a set \ 'a") *} text {* This code setup is just a demonstration and \emph{not} sound! *} lemma False proof - have "some_elem (set [False, True]) = False" - by evaluation + by eval moreover have "some_elem (set [True, False]) = True" - by evaluation + by eval ultimately show False by (simp add: some_elem_def) qed @@ -465,15 +468,35 @@ by simp lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold +lemmas [code] = lesub_def plussub_def -lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp +setup {* + Code.add_signature_cmd ("More_Set.is_empty", "'a set \ bool") + #> Code.add_signature_cmd ("propa", "('s \ 's \ 's) \ (nat \ 's) list \ 's list \ nat set \ 's list * nat set") + #> Code.add_signature_cmd + ("iter", "('s \ 's \ 's) \ (nat \ 's \ (nat \ 's) list) \ 's list \ nat set \ 's list * nat set") + #> Code.add_signature_cmd ("unstables", "('s \ 's \ bool) \ (nat \ 's \ (nat \ 's) list) \ 's list \ nat set") +*} + +definition [code del]: "mem2 = op :" +lemma [code]: "mem2 x A = A x" + by(simp add: mem2_def mem_def) -code_module BV -contains - test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0 +lemmas [folded mem2_def, code] = + JType.sup_def[unfolded exec_lub_def] + wf_class_code + widen.equation + match_exception_entry_def + +definition test1 where + "test1 = test_kil E list_name [Class list_name] (PrimT Void) 3 0 [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins" - test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins" -ML BV.test1 -ML BV.test2 +definition test2 where + "test2 = test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins" + +ML {* + @{code test1}; + @{code test2}; +*} end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/MicroJava/J/Eval.thy --- a/src/HOL/MicroJava/J/Eval.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/MicroJava/J/Eval.thy Mon Aug 08 07:13:16 2011 +0200 @@ -189,4 +189,55 @@ apply (fast) done + +lemma eval_LAcc_code: "G\Norm (h, l) -LAcc v\the (l v)-> Norm (h, l)" +using LAcc[of G "(h, l)" v] by simp + +lemma eval_Call_code: + "[| G\Norm s0 -e\a'-> s1; a = the_Addr a'; + G\s1 -ps[\]pvs-> (x,(h,l)); dynT = fst (the (h a)); + (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs)); + G\(np a' x,(h,(init_vars lvars)(pns[\]pvs)(This\a'))) -blk-> s3; + G\ s3 -res\v -> (x4,(h4, l4)) |] ==> + G\Norm s0 -{C}e..mn({pTs}ps)\v-> (x4,(h4,l))" +using Call[of G s0 e a' s1 a ps pvs x h l dynT md rT pns lvars blk res mn pTs s3 v x4 "(h4, l4)" C] +by simp + +lemmas [code_pred_intro] = XcptE NewC Cast Lit BinOp +lemmas [code_pred_intro LAcc_code] = eval_LAcc_code +lemmas [code_pred_intro] = LAss FAcc FAss +lemmas [code_pred_intro Call_code] = eval_Call_code +lemmas [code_pred_intro] = XcptEs Nil Cons XcptS Skip Expr Comp Cond LoopF +lemmas [code_pred_intro LoopT_code] = LoopT + +code_pred + (modes: + eval: i \ i \ i \ o \ o \ bool + and + evals: i \ i \ i \ o \ o \ bool + and + exec: i \ i \ i \ o \ bool) + eval +proof - + case eval + from eval.prems show thesis + proof(cases (no_simp)) + case LAcc with LAcc_code show ?thesis by auto + next + case (Call a b c d e f g h i j k l m n o p q r s t u v s4) + with Call_code show ?thesis + by(cases "s4")(simp, (erule meta_allE meta_impE|rule conjI refl| assumption)+) + qed(erule (3) that[OF refl]|assumption)+ +next + case evals + from evals.prems show thesis + by(cases (no_simp))(erule (3) that[OF refl]|assumption)+ +next + case exec + from exec.prems show thesis + proof(cases (no_simp)) + case LoopT thus ?thesis by(rule LoopT_code[OF refl]) + qed(erule (2) that[OF refl]|assumption)+ +qed + end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/MicroJava/J/JBasis.thy --- a/src/HOL/MicroJava/J/JBasis.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/MicroJava/J/JBasis.thy Mon Aug 08 07:13:16 2011 +0200 @@ -7,7 +7,7 @@ \isaheader{Some Auxiliary Definitions} *} -theory JBasis imports Main begin +theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin lemmas [simp] = Let_def diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/MicroJava/J/JListExample.thy --- a/src/HOL/MicroJava/J/JListExample.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/MicroJava/J/JListExample.thy Mon Aug 08 07:13:16 2011 +0200 @@ -11,15 +11,19 @@ declare [[syntax_ambiguity_level = 100000]] consts - list_name :: cname + list_nam :: cnam append_name :: mname - val_nam :: vnam - next_nam :: vnam - l_nam :: vnam - l1_nam :: vnam - l2_nam :: vnam - l3_nam :: vnam - l4_nam :: vnam + +axiomatization val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam :: vnam +where distinct_fields: "val_name \ next_name" + and distinct_vars: + "l_nam \ l1_nam" "l_nam \ l2_nam" "l_nam \ l3_nam" "l_nam \ l4_nam" + "l1_nam \ l2_nam" "l1_nam \ l3_nam" "l1_nam \ l4_nam" + "l2_nam \ l3_nam" "l2_nam \ l4_nam" + "l3_nam \ l4_nam" + +definition list_name :: cname where + "list_name = Cname list_nam" definition val_name :: vname where "val_name == VName val_nam" @@ -58,71 +62,119 @@ definition example_prg :: "java_mb prog" where "example_prg == [ObjectC, (list_name, list_class)]" -types_code - cname ("string") - vnam ("string") - mname ("string") - loc' ("int") +code_datatype list_nam +lemma equal_cnam_code [code]: + "HOL.equal list_nam list_nam \ True" + by(simp add: equal_cnam_def) + +code_datatype append_name +lemma equal_mname_code [code]: + "HOL.equal append_name append_name \ True" + by(simp add: equal_mname_def) -consts_code - "new_Addr" ("\new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}") -attach {* -fun new_addr p none loc hp = - let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1); - in nr 0 end; -*} +code_datatype val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam +lemma equal_vnam_code [code]: + "HOL.equal val_nam val_nam \ True" + "HOL.equal next_nam next_nam \ True" + "HOL.equal l_nam l_nam \ True" + "HOL.equal l1_nam l1_nam \ True" + "HOL.equal l2_nam l2_nam \ True" + "HOL.equal l3_nam l3_nam \ True" + "HOL.equal l4_nam l4_nam \ True" + + "HOL.equal val_nam next_nam \ False" + "HOL.equal next_nam val_nam \ False" - "undefined" ("(raise Match)") - "undefined :: val" ("{* Unit *}") - "undefined :: cname" ("\"\"") + "HOL.equal l_nam l1_nam \ False" + "HOL.equal l_nam l2_nam \ False" + "HOL.equal l_nam l3_nam \ False" + "HOL.equal l_nam l4_nam \ False" + + "HOL.equal l1_nam l_nam \ False" + "HOL.equal l1_nam l2_nam \ False" + "HOL.equal l1_nam l3_nam \ False" + "HOL.equal l1_nam l4_nam \ False" + + "HOL.equal l2_nam l_nam \ False" + "HOL.equal l2_nam l1_nam \ False" + "HOL.equal l2_nam l3_nam \ False" + "HOL.equal l2_nam l4_nam \ False" - "Object" ("\"Object\"") - "list_name" ("\"list\"") - "append_name" ("\"append\"") - "val_nam" ("\"val\"") - "next_nam" ("\"next\"") - "l_nam" ("\"l\"") - "l1_nam" ("\"l1\"") - "l2_nam" ("\"l2\"") - "l3_nam" ("\"l3\"") - "l4_nam" ("\"l4\"") + "HOL.equal l3_nam l_nam \ False" + "HOL.equal l3_nam l1_nam \ False" + "HOL.equal l3_nam l2_nam \ False" + "HOL.equal l3_nam l4_nam \ False" + + "HOL.equal l4_nam l_nam \ False" + "HOL.equal l4_nam l1_nam \ False" + "HOL.equal l4_nam l2_nam \ False" + "HOL.equal l4_nam l3_nam \ False" + by(simp_all add: distinct_fields distinct_fields[symmetric] distinct_vars distinct_vars[symmetric] equal_vnam_def) + +axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \ l = l'" +lemma equal_loc'_code [code]: + "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \ l = l'" + by(simp add: equal_loc'_def nat_to_loc'_inject) -code_module J -contains - test = "example_prg\Norm (empty, empty) - -(Expr (l1_name::=NewC list_name);; - Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));; - Expr (l2_name::=NewC list_name);; - Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));; - Expr (l3_name::=NewC list_name);; - Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));; - Expr (l4_name::=NewC list_name);; - Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));; - Expr ({list_name}(LAcc l1_name).. - append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));; - Expr ({list_name}(LAcc l1_name).. - append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));; - Expr ({list_name}(LAcc l1_name).. - append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _" +definition undefined_cname :: cname + where [code del]: "undefined_cname = undefined" +declare undefined_cname_def[symmetric, code_inline] +code_datatype Object Xcpt Cname undefined_cname + +definition undefined_val :: val + where [code del]: "undefined_val = undefined" +declare undefined_val_def[symmetric, code_inline] +code_datatype Unit Null Bool Intg Addr undefined_val + +definition E where + "E = Expr (l1_name::=NewC list_name);; + Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));; + Expr (l2_name::=NewC list_name);; + Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));; + Expr (l3_name::=NewC list_name);; + Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));; + Expr (l4_name::=NewC list_name);; + Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));; + Expr ({list_name}(LAcc l1_name).. + append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));; + Expr ({list_name}(LAcc l1_name).. + append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));; + Expr ({list_name}(LAcc l1_name).. + append_name({[RefT (ClassT list_name)]}[LAcc l4_name]))" + +definition test where + "test = Predicate.Pred (\s. example_prg\Norm (empty, empty) -E-> s)" -section {* Big step execution *} +lemma test_code [code]: + "test = exec_i_i_i_o example_prg (Norm (empty, empty)) E" +by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def) -ML {* +ML {* + val SOME ((_, (heap, locs)), _) = Predicate.yield @{code test}; + locs @{code l1_name}; + locs @{code l2_name}; + locs @{code l3_name}; + locs @{code l4_name}; -val SOME ((_, (heap, locs)), _) = DSeq.pull J.test; -locs J.l1_name; -locs J.l2_name; -locs J.l3_name; -locs J.l4_name; -snd (J.the (heap (J.Loc 0))) (J.val_name, "list"); -snd (J.the (heap (J.Loc 0))) (J.next_name, "list"); -snd (J.the (heap (J.Loc 1))) (J.val_name, "list"); -snd (J.the (heap (J.Loc 1))) (J.next_name, "list"); -snd (J.the (heap (J.Loc 2))) (J.val_name, "list"); -snd (J.the (heap (J.Loc 2))) (J.next_name, "list"); -snd (J.the (heap (J.Loc 3))) (J.val_name, "list"); -snd (J.the (heap (J.Loc 3))) (J.next_name, "list"); + fun list_fields n = + @{code snd} (@{code the} (heap (@{code Loc} (@{code "nat_to_loc'"} n)))); + fun val_field n = + list_fields n (@{code val_name}, @{code "list_name"}); + fun next_field n = + list_fields n (@{code next_name}, @{code "list_name"}); + val Suc = @{code Suc}; + val_field @{code "0 :: nat"}; + next_field @{code "0 :: nat"}; + + val_field @{code "1 :: nat"}; + next_field @{code "1 :: nat"}; + + val_field (Suc (Suc @{code "0 :: nat"})); + next_field (Suc (Suc @{code "0 :: nat"})); + + val_field (Suc (Suc (Suc @{code "0 :: nat"}))); + next_field (Suc (Suc (Suc @{code "0 :: nat"}))); *} end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/MicroJava/J/State.thy --- a/src/HOL/MicroJava/J/State.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/MicroJava/J/State.thy Mon Aug 08 07:13:16 2011 +0200 @@ -52,8 +52,18 @@ definition raise_if :: "bool \ xcpt \ val option \ val option" where "raise_if b x xo \ if b \ (xo = None) then Some (Addr (XcptRef x)) else xo" +text {* Make @{text new_Addr} completely specified (at least for the code generator) *} +(* definition new_Addr :: "aheap => loc \ val option" where "new_Addr h \ SOME (a,x). (h a = None \ x = None) | x = Some (Addr (XcptRef OutOfMemory))" +*) +consts nat_to_loc' :: "nat => loc'" +code_datatype nat_to_loc' +definition new_Addr :: "aheap => loc \ val option" where + "new_Addr h \ + if \n. h (Loc (nat_to_loc' n)) = None + then (Loc (nat_to_loc' (LEAST n. h (Loc (nat_to_loc' n)) = None)), None) + else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))" definition np :: "val => val option => val option" where "np v == raise_if (v = Null) NullPointer" @@ -74,11 +84,8 @@ hp ref = None \ xcp = None \ xcp = Some (Addr (XcptRef OutOfMemory))" apply (drule sym) apply (unfold new_Addr_def) -apply(simp add: Pair_fst_snd_eq Eps_split) -apply(rule someI) -apply(rule disjI2) -apply(rule_tac r = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans) -apply auto +apply (simp split: split_if_asm) +apply (erule LeastI) done lemma raise_if_True [simp]: "raise_if True x y \ None" @@ -150,4 +157,42 @@ lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x" by (simp add: c_hupd_def split_beta) +text {* Naive implementation for @{term "new_Addr"} by exhaustive search *} + +definition gen_new_Addr :: "aheap => nat \ loc \ val option" where + "gen_new_Addr h n \ + if \a. a \ n \ h (Loc (nat_to_loc' a)) = None + then (Loc (nat_to_loc' (LEAST a. a \ n \ h (Loc (nat_to_loc' a)) = None)), None) + else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))" + +lemma new_Addr_code_code [code]: + "new_Addr h = gen_new_Addr h 0" +by(simp only: new_Addr_def gen_new_Addr_def split: split_if) simp + +lemma gen_new_Addr_code [code]: + "gen_new_Addr h n = (if h (Loc (nat_to_loc' n)) = None then (Loc (nat_to_loc' n), None) else gen_new_Addr h (Suc n))" +apply(simp add: gen_new_Addr_def) +apply(rule impI) +apply(rule conjI) + apply safe[1] + apply(auto intro: arg_cong[where f=nat_to_loc'] Least_equality)[1] + apply(rule arg_cong[where f=nat_to_loc']) + apply(rule arg_cong[where f=Least]) + apply(rule ext) + apply(safe, simp_all)[1] + apply(rename_tac "n'") + apply(case_tac "n = n'", simp_all)[1] +apply clarify +apply(subgoal_tac "a = n") + apply(auto intro: Least_equality arg_cong[where f=nat_to_loc'])[1] +apply(rule ccontr) +apply(erule_tac x="a" in allE) +apply simp +done + +instantiation loc' :: equal begin +definition "HOL.equal (l :: loc') l' \ l = l'" +instance proof qed(simp add: equal_loc'_def) end + +end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/MicroJava/J/SystemClasses.thy --- a/src/HOL/MicroJava/J/SystemClasses.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/MicroJava/J/SystemClasses.thy Mon Aug 08 07:13:16 2011 +0200 @@ -13,18 +13,18 @@ *} definition ObjectC :: "'c cdecl" where - "ObjectC \ (Object, (undefined,[],[]))" + [code_inline]: "ObjectC \ (Object, (undefined,[],[]))" definition NullPointerC :: "'c cdecl" where - "NullPointerC \ (Xcpt NullPointer, (Object,[],[]))" + [code_inline]: "NullPointerC \ (Xcpt NullPointer, (Object,[],[]))" definition ClassCastC :: "'c cdecl" where - "ClassCastC \ (Xcpt ClassCast, (Object,[],[]))" + [code_inline]: "ClassCastC \ (Xcpt ClassCast, (Object,[],[]))" definition OutOfMemoryC :: "'c cdecl" where - "OutOfMemoryC \ (Xcpt OutOfMemory, (Object,[],[]))" + [code_inline]: "OutOfMemoryC \ (Xcpt OutOfMemory, (Object,[],[]))" definition SystemClasses :: "'c cdecl list" where - "SystemClasses \ [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" + [code_inline]: "SystemClasses \ [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/MicroJava/J/Type.thy --- a/src/HOL/MicroJava/J/Type.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/MicroJava/J/Type.thy Mon Aug 08 07:13:16 2011 +0200 @@ -8,6 +8,24 @@ theory Type imports JBasis begin typedecl cnam +instantiation cnam :: equal begin +definition "HOL.equal (cn :: cnam) cn' \ cn = cn'" +instance proof qed(simp add: equal_cnam_def) +end +text {* These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME *} +instantiation cnam :: typerep begin +definition "typerep_class.typerep \ \_ :: cnam itself. Typerep.Typerep (STR ''Type.cnam'') []" +instance proof qed +end +instantiation cnam :: term_of begin +definition "term_of_class.term_of (C :: cnam) \ + Code_Evaluation.Const (STR ''dummy_cnam'') (Typerep.Typerep (STR ''Type.cnam'') [])" +instance proof qed +end +instantiation cnam :: partial_term_of begin +definition "partial_term_of_class.partial_term_of (C :: cnam itself) n = undefined" +instance proof qed +end -- "exceptions" datatype @@ -23,7 +41,42 @@ | Cname cnam typedecl vnam -- "variable or field name" +instantiation vnam :: equal begin +definition "HOL.equal (vn :: vnam) vn' \ vn = vn'" +instance proof qed(simp add: equal_vnam_def) +end +instantiation vnam :: typerep begin +definition "typerep_class.typerep \ \_ :: vnam itself. Typerep.Typerep (STR ''Type.vnam'') []" +instance proof qed +end +instantiation vnam :: term_of begin +definition "term_of_class.term_of (V :: vnam) \ + Code_Evaluation.Const (STR ''dummy_vnam'') (Typerep.Typerep (STR ''Type.vnam'') [])" +instance proof qed +end +instantiation vnam :: partial_term_of begin +definition "partial_term_of_class.partial_term_of (V :: vnam itself) n = undefined" +instance proof qed +end + typedecl mname -- "method name" +instantiation mname :: equal begin +definition "HOL.equal (M :: mname) M' \ M = M'" +instance proof qed(simp add: equal_mname_def) +end +instantiation mname :: typerep begin +definition "typerep_class.typerep \ \_ :: mname itself. Typerep.Typerep (STR ''Type.mname'') []" +instance proof qed +end +instantiation mname :: term_of begin +definition "term_of_class.term_of (M :: mname) \ + Code_Evaluation.Const (STR ''dummy_mname'') (Typerep.Typerep (STR ''Type.mname'') [])" +instance proof qed +end +instantiation mname :: partial_term_of begin +definition "partial_term_of_class.partial_term_of (M :: mname itself) n = undefined" +instance proof qed +end -- "names for @{text This} pointer and local/field variables" datatype vname diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/MicroJava/J/TypeRel.thy --- a/src/HOL/MicroJava/J/TypeRel.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/MicroJava/J/TypeRel.thy Mon Aug 08 07:13:16 2011 +0200 @@ -4,7 +4,7 @@ header {* \isaheader{Relations between Java Types} *} -theory TypeRel imports Decl begin +theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin -- "direct subclass, cf. 8.1.3" @@ -77,22 +77,112 @@ "wf_class G = wf ((subcls1 G)^-1)" -text {* Code generator setup (FIXME!) *} + +text {* Code generator setup *} + +code_pred + (modes: i \ i \ o \ bool, i \ i \ i \ bool) + subcls1p + . +declare subcls1_def[unfolded Collect_def, code_pred_def] +code_pred + (modes: i \ i \ o \ bool, i \ i \ i \ bool) + [inductify] + subcls1 + . + +definition subcls' where "subcls' G = (subcls1p G)^**" +code_pred + (modes: i \ i \ i \ bool, i \ i \ o \ bool) + [inductify] + subcls' +. +lemma subcls_conv_subcls' [code_inline]: + "(subcls1 G)^* = (\(C, D). subcls' G C D)" +by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def) + +lemma class_rec_code [code]: + "class_rec G C t f = + (if wf_class G then + (case class G C of + None \ class_rec G C t f + | Some (D, fs, ms) \ + if C = Object then f Object fs ms t else f C fs ms (class_rec G D t f)) + else class_rec G C t f)" +apply(cases "wf_class G") + apply(unfold class_rec_def wf_class_def) + apply(subst wfrec, assumption) + apply(cases "class G C") + apply(simp add: wfrec) + apply clarsimp + apply(rename_tac D fs ms) + apply(rule_tac f="f C fs ms" in arg_cong) + apply(clarsimp simp add: cut_def) + apply(blast intro: subcls1I) +apply simp +done -consts_code - "wfrec" ("\wfrec?") -attach {* -fun wfrec f x = f (wfrec f) x; -*} +lemma wf_class_code [code]: + "wf_class G \ (\(C, rest) \ set G. C \ Object \ \ G \ fst (the (class G C)) \C C)" +proof + assume "wf_class G" + hence wf: "wf (((subcls1 G)^+)^-1)" unfolding wf_class_def by(rule wf_converse_trancl) + hence acyc: "acyclic ((subcls1 G)^+)" by(auto dest: wf_acyclic) + show "\(C, rest) \ set G. C \ Object \ \ G \ fst (the (class G C)) \C C" + proof(safe) + fix C D fs ms + assume "(C, D, fs, ms) \ set G" + and "C \ Object" + and subcls: "G \ fst (the (class G C)) \C C" + from `(C, D, fs, ms) \ set G` obtain D' fs' ms' + where "class": "class G C = Some (D', fs', ms')" + unfolding class_def by(auto dest!: weak_map_of_SomeI) + hence "G \ C \C1 D'" using `C \ Object` .. + hence "(C, D') \ (subcls1 G)^+" .. + also with acyc have "C \ D'" by(auto simp add: acyclic_def) + with subcls "class" have "(D', C) \ (subcls1 G)^+" by(auto dest: rtranclD) + finally show False using acyc by(auto simp add: acyclic_def) + qed +next + assume rhs[rule_format]: "\(C, rest) \ set G. C \ Object \ \ G \ fst (the (class G C)) \C C" + have "acyclic (subcls1 G)" + proof(intro acyclicI strip notI) + fix C + assume "(C, C) \ (subcls1 G)\<^sup>+" + thus False + proof(cases) + case base + then obtain rest where "class G C = Some (C, rest)" + and "C \ Object" by cases + from `class G C = Some (C, rest)` have "(C, C, rest) \ set G" + unfolding class_def by(rule map_of_SomeD) + with `C \ Object` `class G C = Some (C, rest)` + have "\ G \ C \C C" by(auto dest: rhs) + thus False by simp + next + case (step D) + from `G \ D \C1 C` obtain rest where "class G D = Some (C, rest)" + and "D \ Object" by cases + from `class G D = Some (C, rest)` have "(D, C, rest) \ set G" + unfolding class_def by(rule map_of_SomeD) + with `D \ Object` `class G D = Some (C, rest)` + have "\ G \ C \C D" by(auto dest: rhs) + moreover from `(C, D) \ (subcls1 G)\<^sup>+` + have "G \ C \C D" by(rule trancl_into_rtrancl) + ultimately show False by contradiction + qed + qed + thus "wf_class G" unfolding wf_class_def + by(rule finite_acyclic_wf_converse[OF finite_subcls1]) +qed consts - method :: "'c prog \ cname => ( sig \ cname \ ty \ 'c)" (* ###curry *) field :: "'c prog \ cname => ( vname \ cname \ ty )" (* ###curry *) fields :: "'c prog \ cname => ((vname \ cname) \ ty) list" (* ###curry *) -- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6" -defs method_def: "method \ \(G,C). class_rec G C empty (\C fs ms ts. +defs method_def [code]: "method \ \(G,C). class_rec G C empty (\C fs ms ts. ts ++ map_of (map (\(s,m). (s,(C,m))) ms))" lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==> @@ -106,7 +196,7 @@ -- "list of fields of a class, including inherited and hidden ones" -defs fields_def: "fields \ \(G,C). class_rec G C [] (\C fs ms ts. +defs fields_def [code]: "fields \ \(G,C). class_rec G C [] (\C fs ms ts. map (\(fn,ft). ((fn,C),ft)) fs @ ts)" lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==> @@ -119,7 +209,7 @@ done -defs field_def: "field == map_of o (map (\((fn,fd),ft). (fn,(fd,ft)))) o fields" +defs field_def [code]: "field == map_of o (map (\((fn,fd),ft). (fn,(fd,ft)))) o fields" lemma field_fields: "field (G,C) fn = Some (fd, fT) \ map_of (fields (G,C)) (fn, fd) = Some fT" @@ -138,6 +228,8 @@ | subcls : "G\C\C D ==> G\Class C \ Class D" | null [intro!]: "G\ NT \ RefT R" +code_pred widen . + lemmas refl = HOL.refl -- "casting conversion, cf. 5.5 / 5.1.5" diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/MicroJava/JVM/JVMListExample.thy --- a/src/HOL/MicroJava/JVM/JVMListExample.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Mon Aug 08 07:13:16 2011 +0200 @@ -8,13 +8,20 @@ imports "../J/SystemClasses" JVMExec begin -consts - list_nam :: cnam - test_nam :: cnam - append_name :: mname - makelist_name :: mname - val_nam :: vnam - next_nam :: vnam +text {* + Since the types @{typ cnam}, @{text vnam}, and @{text mname} are + anonymous, we describe distinctness of names in the example by axioms: +*} +axiomatization list_nam test_nam :: cnam +where distinct_classes: "list_nam \ test_nam" + +axiomatization append_name makelist_name :: mname +where distinct_methods: "append_name \ makelist_name" + +axiomatization val_nam next_nam :: vnam +where distinct_fields: "val_nam \ next_nam" + +axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \ l = l'" definition list_name :: cname where "list_name == Cname list_nam" @@ -86,96 +93,103 @@ definition E :: jvm_prog where "E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]" +code_datatype list_nam test_nam +lemma equal_cnam_code [code]: + "HOL.equal list_nam list_nam \ True" + "HOL.equal test_nam test_nam \ True" + "HOL.equal list_nam test_nam \ False" + "HOL.equal test_nam list_nam \ False" + by(simp_all add: distinct_classes distinct_classes[symmetric] equal_cnam_def) -types_code - cnam ("string") - vnam ("string") - mname ("string") - loc' ("int") +code_datatype append_name makelist_name +lemma equal_mname_code [code]: + "HOL.equal append_name append_name \ True" + "HOL.equal makelist_name makelist_name \ True" + "HOL.equal append_name makelist_name \ False" + "HOL.equal makelist_name append_name \ False" + by(simp_all add: distinct_methods distinct_methods[symmetric] equal_mname_def) -consts_code - "new_Addr" ("\new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}") -attach {* -fun new_addr p none loc hp = - let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1); - in nr 0 end; -*} +code_datatype val_nam next_nam +lemma equal_vnam_code [code]: + "HOL.equal val_nam val_nam \ True" + "HOL.equal next_nam next_nam \ True" + "HOL.equal val_nam next_nam \ False" + "HOL.equal next_nam val_nam \ False" + by(simp_all add: distinct_fields distinct_fields[symmetric] equal_vnam_def) + - "undefined" ("(raise Match)") - "undefined :: val" ("{* Unit *}") - "undefined :: cname" ("{* Object *}") +lemma equal_loc'_code [code]: + "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \ l = l'" + by(simp add: equal_loc'_def nat_to_loc'_inject) - "list_nam" ("\"list\"") - "test_nam" ("\"test\"") - "append_name" ("\"append\"") - "makelist_name" ("\"makelist\"") - "val_nam" ("\"val\"") - "next_nam" ("\"next\"") +definition undefined_cname :: cname + where [code del]: "undefined_cname = undefined" +code_datatype Object Xcpt Cname undefined_cname +declare undefined_cname_def[symmetric, code_inline] + +definition undefined_val :: val + where [code del]: "undefined_val = undefined" +declare undefined_val_def[symmetric, code_inline] +code_datatype Unit Null Bool Intg Addr undefined_val definition "test = exec (E, start_state E test_name makelist_name)" - -subsection {* Single step execution *} - -code_module JVM -contains - exec = exec - test = test - -ML {* JVM.test *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} -ML {* JVM.exec (JVM.E, JVM.the it) *} +ML {* + @{code test}; + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); + @{code exec} (@{code E}, @{code the} it); +*} end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Aug 08 07:13:16 2011 +0200 @@ -397,10 +397,6 @@ lemma affine_hull_eq[simp]: "(affine hull s = s) \ affine s" by (metis affine_affine_hull hull_same mem_def) -lemma setsum_restrict_set'': assumes "finite A" - shows "setsum f {x \ A. P x} = (\x\A. if P x then f x else 0)" - unfolding mem_def[of _ P, symmetric] unfolding setsum_restrict_set'[OF assms] .. - subsection {* Some explicit formulations (from Lars Schewe). *} lemma affine: fixes V::"'a::real_vector set" diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/NanoJava/TypeRel.thy --- a/src/HOL/NanoJava/TypeRel.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/NanoJava/TypeRel.thy Mon Aug 08 07:13:16 2011 +0200 @@ -4,7 +4,7 @@ header "Type relations" -theory TypeRel imports Decl begin +theory TypeRel imports Decl "~~/src/HOL/Library/Old_Recdef" begin consts subcls1 :: "(cname \ cname) set" --{* subclass *} diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Nitpick.thy Mon Aug 08 07:13:16 2011 +0200 @@ -82,15 +82,6 @@ definition wf' :: "('a \ 'a \ bool) \ bool" where "wf' r \ acyclic r \ (finite r \ unknown)" -axiomatization wf_wfrec :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" - -definition wf_wfrec' :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where -[nitpick_simp]: "wf_wfrec' R F x = F (Recdef.cut (wf_wfrec R F) R x) x" - -definition wfrec' :: "('a \ 'a \ bool) \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where -"wfrec' R F x \ if wf R then wf_wfrec' R F x - else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y" - definition card' :: "('a \ bool) \ nat" where "card' A \ if finite A then length (SOME xs. set xs = A \ distinct xs) else 0" @@ -235,17 +226,24 @@ use "Tools/Nitpick/nitpick_tests.ML" use "Tools/Nitpick/nitrox.ML" -setup {* Nitpick_Isar.setup *} +setup {* + Nitpick_Isar.setup #> + Nitpick_HOL.register_ersatz_global + [(@{const_name card}, @{const_name card'}), + (@{const_name setsum}, @{const_name setsum'}), + (@{const_name fold_graph}, @{const_name fold_graph'}), + (@{const_name wf}, @{const_name wf'})] +*} hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The - FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum' + FunBox PairBox Word prod refl' wf' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac less_frac less_eq_frac of_frac hide_type (open) iota bisim_iterator fun_box pair_box unsigned_bit signed_bit word hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold - prod_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def + prod_def refl'_def wf'_def card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Orderings.thy Mon Aug 08 07:13:16 2011 +0200 @@ -1246,7 +1246,7 @@ subsection {* Order on bool *} -instantiation bool :: "{order, bot, top}" +instantiation bool :: "{bot, top}" begin definition diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Predicate.thy Mon Aug 08 07:13:16 2011 +0200 @@ -431,7 +431,7 @@ "x \ (op =) y \ x = y" by (auto simp add: mem_def) -instantiation pred :: (type) "{complete_lattice, boolean_algebra}" +instantiation pred :: (type) complete_lattice begin definition @@ -482,6 +482,22 @@ "eval (\A) = SUPR A eval" by (simp add: Sup_pred_def) +instance proof +qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def) + +end + +lemma eval_INFI [simp]: + "eval (INFI A f) = INFI A (eval \ f)" + by (unfold INFI_def) simp + +lemma eval_SUPR [simp]: + "eval (SUPR A f) = SUPR A (eval \ f)" + by (unfold SUPR_def) simp + +instantiation pred :: (type) complete_boolean_algebra +begin + definition "- P = Pred (- eval P)" @@ -497,18 +513,10 @@ by (simp add: minus_pred_def) instance proof -qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def uminus_apply minus_apply) +qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply) end -lemma eval_INFI [simp]: - "eval (INFI A f) = INFI A (eval \ f)" - by (unfold INFI_def) simp - -lemma eval_SUPR [simp]: - "eval (SUPR A f) = SUPR A (eval \ f)" - by (unfold SUPR_def) simp - definition single :: "'a \ 'a pred" where "single x = Pred ((op =) x)" @@ -741,11 +749,12 @@ by simp lemma closure_of_bool_cases [no_atp]: -assumes "(f :: unit \ bool) = (%u. False) \ P f" -assumes "f = (%u. True) \ P f" -shows "P f" + fixes f :: "unit \ bool" + assumes "f = (\u. False) \ P f" + assumes "f = (\u. True) \ P f" + shows "P f" proof - - have "f = (%u. False) \ f = (%u. True)" + have "f = (\u. False) \ f = (\u. True)" apply (cases "f ()") apply (rule disjI2) apply (rule ext) @@ -758,19 +767,18 @@ qed lemma unit_pred_cases: -assumes "P \" -assumes "P (single ())" -shows "P Q" -using assms -unfolding bot_pred_def Collect_def empty_def single_def -apply (cases Q) -apply simp -apply (rule_tac f="fun" in closure_of_bool_cases) -apply auto -apply (subgoal_tac "(%x. () = x) = (%x. True)") -apply auto -done - + assumes "P \" + assumes "P (single ())" + shows "P Q" +using assms unfolding bot_pred_def Collect_def empty_def single_def proof (cases Q) + fix f + assume "P (Pred (\u. False))" "P (Pred (\u. () = u))" + then have "P (Pred f)" + by (cases _ f rule: closure_of_bool_cases) simp_all + moreover assume "Q = Pred f" + ultimately show "P Q" by simp +qed + lemma holds_if_pred: "holds (if_pred b) = b" unfolding if_pred_eq holds_eq diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Recdef.thy --- a/src/HOL/Recdef.thy Sat Aug 06 14:16:23 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,189 +0,0 @@ -(* Title: HOL/Recdef.thy - Author: Konrad Slind and Markus Wenzel, TU Muenchen -*) - -header {* TFL: recursive function definitions *} - -theory Recdef -imports Plain Hilbert_Choice -uses - ("Tools/TFL/casesplit.ML") - ("Tools/TFL/utils.ML") - ("Tools/TFL/usyntax.ML") - ("Tools/TFL/dcterm.ML") - ("Tools/TFL/thms.ML") - ("Tools/TFL/rules.ML") - ("Tools/TFL/thry.ML") - ("Tools/TFL/tfl.ML") - ("Tools/TFL/post.ML") - ("Tools/recdef.ML") -begin - -inductive - wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool" - for R :: "('a * 'a) set" - and F :: "('a => 'b) => 'a => 'b" -where - wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==> - wfrec_rel R F x (F g x)" - -definition - cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where - "cut f r x == (%y. if (y,x):r then f y else undefined)" - -definition - adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where - "adm_wf R F == ALL f g x. - (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x" - -definition - wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where - "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" - -subsection{*Well-Founded Recursion*} - -text{*cut*} - -lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))" -by (simp add: fun_eq_iff cut_def) - -lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)" -by (simp add: cut_def) - -text{*Inductive characterization of wfrec combinator; for details see: -John Harrison, "Inductive definitions: automation and application"*} - -lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y" -apply (simp add: adm_wf_def) -apply (erule_tac a=x in wf_induct) -apply (rule ex1I) -apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI) -apply (fast dest!: theI') -apply (erule wfrec_rel.cases, simp) -apply (erule allE, erule allE, erule allE, erule mp) -apply (fast intro: the_equality [symmetric]) -done - -lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)" -apply (simp add: adm_wf_def) -apply (intro strip) -apply (rule cuts_eq [THEN iffD2, THEN subst], assumption) -apply (rule refl) -done - -lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a" -apply (simp add: wfrec_def) -apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption) -apply (rule wfrec_rel.wfrecI) -apply (intro strip) -apply (erule adm_lemma [THEN wfrec_unique, THEN theI']) -done - - -text{** This form avoids giant explosions in proofs. NOTE USE OF ==*} -lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a" -apply auto -apply (blast intro: wfrec) -done - - -lemma tfl_wf_induct: "ALL R. wf R --> - (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))" -apply clarify -apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast) -done - -lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)" -apply clarify -apply (rule cut_apply, assumption) -done - -lemma tfl_wfrec: - "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)" -apply clarify -apply (erule wfrec) -done - -lemma tfl_eq_True: "(x = True) --> x" - by blast - -lemma tfl_rev_eq_mp: "(x = y) --> y --> x"; - by blast - -lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)" - by blast - -lemma tfl_P_imp_P_iff_True: "P ==> P = True" - by blast - -lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)" - by blast - -lemma tfl_disj_assoc: "(a \ b) \ c == a \ (b \ c)" - by simp - -lemma tfl_disjE: "P \ Q ==> P --> R ==> Q --> R ==> R" - by blast - -lemma tfl_exE: "\x. P x ==> \x. P x --> Q ==> Q" - by blast - -use "Tools/TFL/casesplit.ML" -use "Tools/TFL/utils.ML" -use "Tools/TFL/usyntax.ML" -use "Tools/TFL/dcterm.ML" -use "Tools/TFL/thms.ML" -use "Tools/TFL/rules.ML" -use "Tools/TFL/thry.ML" -use "Tools/TFL/tfl.ML" -use "Tools/TFL/post.ML" -use "Tools/recdef.ML" -setup Recdef.setup - -text {*Wellfoundedness of @{text same_fst}*} - -definition - same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set" -where - "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}" - --{*For @{text rec_def} declarations where the first n parameters - stay unchanged in the recursive call. *} - -lemma same_fstI [intro!]: - "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R" -by (simp add: same_fst_def) - -lemma wf_same_fst: - assumes prem: "(!!x. P x ==> wf(R x))" - shows "wf(same_fst P R)" -apply (simp cong del: imp_cong add: wf_def same_fst_def) -apply (intro strip) -apply (rename_tac a b) -apply (case_tac "wf (R a)") - apply (erule_tac a = b in wf_induct, blast) -apply (blast intro: prem) -done - -text {*Rule setup*} - -lemmas [recdef_simp] = - inv_image_def - measure_def - lex_prod_def - same_fst_def - less_Suc_eq [THEN iffD2] - -lemmas [recdef_cong] = - if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong - -lemmas [recdef_wf] = - wf_trancl - wf_less_than - wf_lex_prod - wf_inv_image - wf_measure - wf_pred_nat - wf_same_fst - wf_empty - -end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Aug 08 07:13:16 2011 +0200 @@ -372,8 +372,11 @@ end) | add_type_def prfx (s, Pending_Type) (ids, thy) = - (check_no_assoc thy prfx s; - (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd)); + (ids, + case get_type thy prfx s of + SOME _ => thy + | NONE => Typedecl.typedecl_global + (Binding.name s, [], NoSyn) thy |> snd); fun term_of_expr thy prfx types pfuns = diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/SetInterval.thy Mon Aug 08 07:13:16 2011 +0200 @@ -14,6 +14,7 @@ context ord begin + definition lessThan :: "'a => 'a set" ("(1{..<_})") where "{.. setsum f {x \ A. x \ B} = (\x\A. if x \ B then f x else 0)" + by (simp add: setsum_restrict_set [symmetric] Int_def) + +lemma setsum_restrict_set'': + "finite A \ setsum f {x \ A. P x} = (\x\A. if P x then f x else 0)" + by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq]) lemma setsum_setsum_restrict: - "finite S \ finite T \ setsum (\x. setsum (\y. f x y) {y. y\ T \ R x y}) S = setsum (\y. setsum (\x. f x y) {x. x \ S \ R x y}) T" - by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def) - (rule setsum_commute) + "finite S \ finite T \ + setsum (\x. setsum (\y. f x y) {y. y \ T \ R x y}) S = setsum (\y. setsum (\x. f x y) {x. x \ S \ R x y}) T" + by (simp add: setsum_restrict_set'') (rule setsum_commute) lemma setsum_image_gen: assumes fS: "finite S" shows "setsum g S = setsum (\y. setsum g {x. x \ S \ f x = y}) (f ` S)" diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Subst/Unify.thy --- a/src/HOL/Subst/Unify.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Subst/Unify.thy Mon Aug 08 07:13:16 2011 +0200 @@ -6,7 +6,7 @@ header {* Unification Algorithm *} theory Unify -imports Unifier +imports Unifier "~~/src/HOL/Library/Old_Recdef" begin subsection {* Substitution and Unification in Higher-Order Logic. *} diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 08 07:13:16 2011 +0200 @@ -148,6 +148,9 @@ val unregister_frac_type : string -> morphism -> Context.generic -> Context.generic val unregister_frac_type_global : string -> theory -> theory + val register_ersatz : + (string * string) list -> morphism -> Context.generic -> Context.generic + val register_ersatz_global : (string * string) list -> theory -> theory val register_codatatype : typ -> string -> styp list -> morphism -> Context.generic -> Context.generic val register_codatatype_global : @@ -287,12 +290,14 @@ structure Data = Generic_Data ( type T = {frac_types: (string * (string * string) list) list, + ersatz_table: (string * string) list, codatatypes: (string * (string * styp list)) list} - val empty = {frac_types = [], codatatypes = []} + val empty = {frac_types = [], ersatz_table = [], codatatypes = []} val extend = I - fun merge ({frac_types = fs1, codatatypes = cs1}, - {frac_types = fs2, codatatypes = cs2}) : T = + fun merge ({frac_types = fs1, ersatz_table = et1, codatatypes = cs1}, + {frac_types = fs2, ersatz_table = et2, codatatypes = cs2}) : T = {frac_types = AList.merge (op =) (K true) (fs1, fs2), + ersatz_table = AList.merge (op =) (K true) (et1, et2), codatatypes = AList.merge (op =) (K true) (cs1, cs2)} ) @@ -491,8 +496,7 @@ val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type val is_record_type = not o null o Record.dest_recTs fun is_frac_type ctxt (Type (s, [])) = - s |> AList.lookup (op =) (#frac_types (Data.get (Context.Proof ctxt))) - |> these |> null |> not + s |> AList.defined (op =) (#frac_types (Data.get (Context.Proof ctxt))) | is_frac_type _ _ = false fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt fun is_higher_order_type (Type (@{type_name fun}, _)) = true @@ -575,9 +579,10 @@ fun register_frac_type_generic frac_s ersaetze generic = let - val {frac_types, codatatypes} = Data.get generic + val {frac_types, ersatz_table, codatatypes} = Data.get generic val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types - in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end + in Data.put {frac_types = frac_types, ersatz_table = ersatz_table, + codatatypes = codatatypes} generic end (* TODO: Consider morphism. *) fun register_frac_type frac_s ersaetze (_ : morphism) = register_frac_type_generic frac_s ersaetze @@ -590,11 +595,22 @@ val unregister_frac_type_global = Context.theory_map o unregister_frac_type_generic +fun register_ersatz_generic ersatz generic = + let + val {frac_types, ersatz_table, codatatypes} = Data.get generic + val ersatz_table = AList.merge (op =) (K true) (ersatz_table, ersatz) + in Data.put {frac_types = frac_types, ersatz_table = ersatz_table, + codatatypes = codatatypes} generic end +(* TODO: Consider morphism. *) +fun register_ersatz ersatz (_ : morphism) = + register_ersatz_generic ersatz +val register_ersatz_global = Context.theory_map o register_ersatz_generic + fun register_codatatype_generic co_T case_name constr_xs generic = let val ctxt = Context.proof_of generic val thy = Context.theory_of generic - val {frac_types, codatatypes} = Data.get generic + val {frac_types, ersatz_table, codatatypes} = Data.get generic val constr_xs = map (apsnd (repair_constr_type ctxt co_T)) constr_xs val (co_s, co_Ts) = dest_Type co_T val _ = @@ -606,7 +622,8 @@ raise TYPE ("Nitpick_HOL.register_codatatype_generic", [co_T], []) val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) codatatypes - in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end + in Data.put {frac_types = frac_types, ersatz_table = ersatz_table, + codatatypes = codatatypes} generic end (* TODO: Consider morphism. *) fun register_codatatype co_T case_name constr_xs (_ : morphism) = register_codatatype_generic co_T case_name constr_xs @@ -1762,7 +1779,7 @@ "too many nested definitions (" ^ string_of_int depth ^ ") while expanding " ^ quote s) - else if s = @{const_name wfrec'} then + else if s = "Wfrec.wfrec'" (* FIXME unchecked! *) then (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), []) else if not unfold andalso size_of_term def > def_inline_threshold () then @@ -1851,17 +1868,8 @@ is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1) | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy) Inttab.empty -(* TODO: Move to "Nitpick.thy" *) -val basic_ersatz_table = - [(@{const_name card}, @{const_name card'}), - (@{const_name setsum}, @{const_name setsum'}), - (@{const_name fold_graph}, @{const_name fold_graph'}), - (@{const_name wf}, @{const_name wf'}), - (@{const_name wf_wfrec}, @{const_name wf_wfrec'}), - (@{const_name wfrec}, @{const_name wfrec'})] - fun ersatz_table ctxt = - basic_ersatz_table + #ersatz_table (Data.get (Context.Proof ctxt)) |> fold (append o snd) (#frac_types (Data.get (Context.Proof ctxt))) fun add_simps simp_table s eqs = diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Mon Aug 08 07:13:16 2011 +0200 @@ -445,7 +445,7 @@ fun is_cong thm = case (Thm.prop_of thm) of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $ - (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false + (Const("==",_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) => false | _ => true; @@ -645,7 +645,7 @@ end; fun restricted t = is_some (USyntax.find_term - (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false) + (fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false) t) fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th = diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/Tools/recdef.ML Mon Aug 08 07:13:16 2011 +0200 @@ -182,7 +182,7 @@ (** add_recdef(_i) **) -fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions"; +fun requires_recdef thy = Theory.requires thy "Old_Recdef" "recursive functions"; fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy = let diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/ZF/Games.thy --- a/src/HOL/ZF/Games.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/ZF/Games.thy Mon Aug 08 07:13:16 2011 +0200 @@ -320,7 +320,7 @@ apply (simp add: wfzf_is_option_of) done -lemma wf_option_of[recdef_wf, simp, intro]: "wf option_of" +lemma wf_option_of[simp, intro]: "wf option_of" proof - have option_of: "option_of = inv_image is_option_of Rep_game" apply (rule set_eqI) diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/ZF/LProd.thy --- a/src/HOL/ZF/LProd.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/ZF/LProd.thy Mon Aug 08 07:13:16 2011 +0200 @@ -82,7 +82,7 @@ qed qed -lemma wf_lprod[recdef_wf,simp,intro]: +lemma wf_lprod[simp,intro]: assumes wf_R: "wf R" shows "wf (lprod R)" proof - @@ -116,7 +116,7 @@ by (auto intro: lprod_list[where a=c and b=c and ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified]) -lemma [recdef_wf, simp, intro]: +lemma [simp, intro]: assumes wfR: "wf R" shows "wf (gprod_2_1 R)" proof - have "gprod_2_1 R \ inv_image (lprod R) (\ (a,b). [a,b])" @@ -125,7 +125,7 @@ by (rule_tac wf_subset, auto) qed -lemma [recdef_wf, simp, intro]: +lemma [simp, intro]: assumes wfR: "wf R" shows "wf (gprod_2_2 R)" proof - have "gprod_2_2 R \ inv_image (lprod R) (\ (a,b). [a,b])" diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/ZF/Zet.thy --- a/src/HOL/ZF/Zet.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/ZF/Zet.thy Mon Aug 08 07:13:16 2011 +0200 @@ -196,7 +196,7 @@ lemma zimage_id[simp]: "zimage id A = A" by (simp add: zet_ext_eq zimage_iff) -lemma zimage_cong[recdef_cong, fundef_cong]: "\ M = N; !! x. zin x N \ f x = g x \ \ zimage f M = zimage g N" +lemma zimage_cong[fundef_cong]: "\ M = N; !! x. zin x N \ f x = g x \ \ zimage f M = zimage g N" by (auto simp add: zet_ext_eq zimage_iff) end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/ex/Eval_Examples.thy --- a/src/HOL/ex/Eval_Examples.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/ex/Eval_Examples.thy Mon Aug 08 07:13:16 2011 +0200 @@ -34,42 +34,34 @@ value "(Suc 2 + 1) * 4" value [code] "(Suc 2 + 1) * 4" -value [SML] "(Suc 2 + 1) * 4" value [nbe] "(Suc 2 + 1) * 4" value "(Suc 2 + Suc 0) * Suc 3" value [code] "(Suc 2 + Suc 0) * Suc 3" -value [SML] "(Suc 2 + Suc 0) * Suc 3" value [nbe] "(Suc 2 + Suc 0) * Suc 3" value "nat 100" value [code] "nat 100" -value [SML] "nat 100" value [nbe] "nat 100" value "(10::int) \ 12" value [code] "(10::int) \ 12" -value [SML] "(10::int) \ 12" value [nbe] "(10::int) \ 12" value "max (2::int) 4" value [code] "max (2::int) 4" -value [SML] "max (2::int) 4" value [nbe] "max (2::int) 4" value "of_int 2 / of_int 4 * (1::rat)" value [code] "of_int 2 / of_int 4 * (1::rat)" -value [SML] "of_int 2 / of_int 4 * (1::rat)" value [nbe] "of_int 2 / of_int 4 * (1::rat)" value "[] :: nat list" value [code] "[] :: nat list" -value [SML] "[] :: nat list" value [nbe] "[] :: nat list" value "[(nat 100, ())]" value [code] "[(nat 100, ())]" -value [SML] "[(nat 100, ())]" value [nbe] "[(nat 100, ())]" text {* a fancy datatype *} @@ -84,7 +76,6 @@ value "Bla (Bar (4::nat) [Suc 0])" value [code] "Bla (Bar (4::nat) [Suc 0])" -value [SML] "Bla (Bar (4::nat) [Suc 0])" value [nbe] "Bla (Bar (4::nat) [Suc 0])" end diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/ex/InductiveInvariant.thy --- a/src/HOL/ex/InductiveInvariant.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/ex/InductiveInvariant.thy Mon Aug 08 07:13:16 2011 +0200 @@ -4,7 +4,7 @@ header {* Some of the results in Inductive Invariants for Nested Recursion *} -theory InductiveInvariant imports Main begin +theory InductiveInvariant imports "~~/src/HOL/Library/Old_Recdef" begin text {* A formalization of some of the results in \emph{Inductive Invariants for Nested Recursion}, by Sava Krsti\'{c} and John diff -r a43ca8ed6564 -r 18a0aef2af80 src/HOL/ex/Recdefs.thy --- a/src/HOL/ex/Recdefs.thy Sat Aug 06 14:16:23 2011 +0200 +++ b/src/HOL/ex/Recdefs.thy Mon Aug 08 07:13:16 2011 +0200 @@ -7,7 +7,7 @@ header {* Examples of recdef definitions *} -theory Recdefs imports Main begin +theory Recdefs imports "~~/src/HOL/Library/Old_Recdef" begin consts fact :: "nat => nat" recdef fact less_than diff -r a43ca8ed6564 -r 18a0aef2af80 src/Tools/jEdit/README_BUILD --- a/src/Tools/jEdit/README_BUILD Sat Aug 06 14:16:23 2011 +0200 +++ b/src/Tools/jEdit/README_BUILD Mon Aug 08 07:13:16 2011 +0200 @@ -1,7 +1,7 @@ Requirements for instantaneous build from sources ================================================= -* Proper Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_24 or 1.6.0_25 +* Official Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_26 http://java.sun.com/javase/downloads/index.jsp * Scala Compiler 2.8.1.final diff -r a43ca8ed6564 -r 18a0aef2af80 src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Sat Aug 06 14:16:23 2011 +0200 +++ b/src/Tools/jEdit/src/isabelle_options.scala Mon Aug 08 07:13:16 2011 +0200 @@ -27,7 +27,8 @@ override def _init() { - addComponent(Isabelle.Property("logic.title"), logic_selector.peer) + addComponent(Isabelle.Property("logic.title"), + logic_selector.peer.asInstanceOf[java.awt.Component]) addComponent(Isabelle.Property("auto-start.title"), auto_start.peer) auto_start.selected = Isabelle.Boolean_Property("auto-start")