--- 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 ***
--- 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]
--- 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 {*
--- 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: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
- by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
-
-lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
- by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
-
-lemma Inf_empty [simp]:
- "\<Sqinter>{} = \<top>"
- by (auto intro: antisym Inf_greatest)
-
-lemma Sup_empty [simp]:
- "\<Squnion>{} = \<bottom>"
- by (auto intro: antisym Sup_least)
-
-lemma Inf_UNIV [simp]:
- "\<Sqinter>UNIV = \<bottom>"
- by (simp add: Sup_Inf Sup_empty [symmetric])
-
-lemma Sup_UNIV [simp]:
- "\<Squnion>UNIV = \<top>"
- by (simp add: Inf_Sup Inf_empty [symmetric])
-
-lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
- by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
-
-lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
- by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
-
-lemma Inf_singleton [simp]:
- "\<Sqinter>{a} = a"
- by (auto intro: antisym Inf_lower Inf_greatest)
-
-lemma Sup_singleton [simp]:
- "\<Squnion>{a} = a"
- by (auto intro: antisym Sup_upper Sup_least)
-
-lemma Inf_binary:
- "\<Sqinter>{a, b} = a \<sqinter> b"
- by (simp add: Inf_insert)
-
-lemma Sup_binary:
- "\<Squnion>{a, b} = a \<squnion> b"
- by (simp add: Sup_insert)
-
-lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
- by (auto intro: Inf_greatest dest: Inf_lower)
-
-lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
- by (auto intro: Sup_least dest: Sup_upper)
-
-lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
- by (auto intro: Inf_greatest Inf_lower)
-
-lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
- by (auto intro: Sup_least Sup_upper)
-
-lemma Inf_mono:
- assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
- shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
-proof (rule Inf_greatest)
- fix b assume "b \<in> B"
- with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
- from `a \<in> A` have "\<Sqinter>A \<sqsubseteq> a" by (rule Inf_lower)
- with `a \<sqsubseteq> b` show "\<Sqinter>A \<sqsubseteq> b" by auto
-qed
-
-lemma Sup_mono:
- assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
- shows "\<Squnion>A \<sqsubseteq> \<Squnion>B"
-proof (rule Sup_least)
- fix a assume "a \<in> A"
- with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
- from `b \<in> B` have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper)
- with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
-qed
-
-lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
- using Sup_upper [of u A] by auto
-
-lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
- using Inf_lower [of u A] by auto
-
-lemma Inf_less_eq:
- assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
- and "A \<noteq> {}"
- shows "\<Sqinter>A \<sqsubseteq> u"
-proof -
- from `A \<noteq> {}` obtain v where "v \<in> A" by blast
- moreover with assms have "v \<sqsubseteq> u" by blast
- ultimately show ?thesis by (rule Inf_lower2)
-qed
-
-lemma less_eq_Sup:
- assumes "\<And>v. v \<in> A \<Longrightarrow> u \<sqsubseteq> v"
- and "A \<noteq> {}"
- shows "u \<sqsubseteq> \<Squnion>A"
-proof -
- from `A \<noteq> {}` obtain v where "v \<in> A" by blast
- moreover with assms have "u \<sqsubseteq> v" by blast
- ultimately show ?thesis by (rule Sup_upper2)
-qed
-
-lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
- by (auto intro: Inf_greatest Inf_lower)
-
-lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
- by (auto intro: Sup_least Sup_upper)
-
-lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
- by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
-
-lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
- by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
-
-lemma Inf_top_conv [no_atp]:
- "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
- "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
-proof -
- show "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
- proof
- assume "\<forall>x\<in>A. x = \<top>"
- then have "A = {} \<or> A = {\<top>}" by auto
- then show "\<Sqinter>A = \<top>" by auto
- next
- assume "\<Sqinter>A = \<top>"
- show "\<forall>x\<in>A. x = \<top>"
- proof (rule ccontr)
- assume "\<not> (\<forall>x\<in>A. x = \<top>)"
- then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
- then obtain B where "A = insert x B" by blast
- with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
- qed
- qed
- then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
-qed
-
-lemma Sup_bot_conv [no_atp]:
- "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
- "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
-proof -
- interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
- by (fact dual_complete_lattice)
- from dual.Inf_top_conv show ?P and ?Q by simp_all
-qed
-
definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
- INF_def: "INFI A f = \<Sqinter> (f ` A)"
+ INF_def: "INFI A f = \<Sqinter>(f ` A)"
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
- SUP_def: "SUPR A f = \<Squnion> (f ` A)"
+ SUP_def: "SUPR A f = \<Squnion>(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: "(\<Sqinter>x\<in>{}. f x) = \<top>"
- by (simp add: INF_def)
-
-lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
- 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 \<ge>" "op >" sup inf \<top> \<bottom>
+ by (fact dual_complete_lattice)
+ fix f :: "'b \<Rightarrow> 'a" and A
+ show "complete_lattice.SUPR Inf A f = (\<Sqinter>a\<in>A. f a)"
+ by (simp only: dual.SUP_def INF_def)
+qed
-lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
- by (simp add: INF_def Inf_insert)
-
-lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> 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 \<ge>" "op >" sup inf \<top> \<bottom>
+ by (fact dual_complete_lattice)
+ fix f :: "'b \<Rightarrow> 'a" and A
+ show "complete_lattice.INFI Sup A f = (\<Squnion>a\<in>A. f a)"
+ by (simp only: dual.INF_def SUP_def)
+qed
lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
by (auto simp add: INF_def intro: Inf_lower)
@@ -245,35 +108,97 @@
lemma le_SUP_I: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
by (auto simp add: SUP_def intro: Sup_upper)
-lemma INF_leI2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
- using INF_leI [of i A f] by auto
-
-lemma le_SUP_I2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
- using le_SUP_I [of i A f] by auto
-
lemma le_INF_I: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
by (auto simp add: INF_def intro: Inf_greatest)
lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
by (auto simp add: SUP_def intro: Sup_least)
+lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
+ using Inf_lower [of u A] by auto
+
+lemma INF_leI2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
+ using INF_leI [of i A f] by auto
+
+lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
+ using Sup_upper [of u A] by auto
+
+lemma le_SUP_I2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+ using le_SUP_I [of i A f] by auto
+
+lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
+ by (auto intro: Inf_greatest dest: Inf_lower)
+
lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> f i)"
by (auto simp add: INF_def le_Inf_iff)
+lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
+ by (auto intro: Sup_least dest: Sup_upper)
+
lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
by (auto simp add: SUP_def Sup_le_iff)
-lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
- by (auto intro: antisym INF_leI le_INF_I)
+lemma Inf_empty [simp]:
+ "\<Sqinter>{} = \<top>"
+ by (auto intro: antisym Inf_greatest)
+
+lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
+ by (simp add: INF_def)
+
+lemma Sup_empty [simp]:
+ "\<Squnion>{} = \<bottom>"
+ by (auto intro: antisym Sup_least)
+
+lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
+ by (simp add: SUP_def)
-lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
- by (auto intro: antisym SUP_leI le_SUP_I)
+lemma Inf_UNIV [simp]:
+ "\<Sqinter>UNIV = \<bottom>"
+ by (auto intro!: antisym Inf_lower)
+
+lemma Sup_UNIV [simp]:
+ "\<Squnion>UNIV = \<top>"
+ by (auto intro!: antisym Sup_upper)
+
+lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
+ by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
+
+lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
+ by (simp add: INF_def Inf_insert)
+
+lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
+ by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
-lemma INF_top: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
- by (cases "A = {}") (simp_all add: INF_empty)
+lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
+ by (simp add: SUP_def Sup_insert)
+
+lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
+ by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
+
+lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
+ by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
+
+lemma Inf_singleton [simp]:
+ "\<Sqinter>{a} = a"
+ by (auto intro: antisym Inf_lower Inf_greatest)
-lemma SUP_bot: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
- by (cases "A = {}") (simp_all add: SUP_empty)
+lemma Sup_singleton [simp]:
+ "\<Squnion>{a} = a"
+ by (auto intro: antisym Sup_upper Sup_least)
+
+lemma Inf_binary:
+ "\<Sqinter>{a, b} = a \<sqinter> b"
+ by (simp add: Inf_insert)
+
+lemma Sup_binary:
+ "\<Squnion>{a, b} = a \<squnion> b"
+ by (simp add: Sup_insert)
+
+lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
+ by (auto intro: Inf_greatest Inf_lower)
+
+lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
+ by (auto intro: Sup_least Sup_upper)
lemma INF_cong:
"A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Sqinter>x\<in>A. C x) = (\<Sqinter>x\<in>B. D x)"
@@ -283,10 +208,30 @@
"A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Squnion>x\<in>A. C x) = (\<Squnion>x\<in>B. D x)"
by (simp add: SUP_def image_def)
+lemma Inf_mono:
+ assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
+ shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
+proof (rule Inf_greatest)
+ fix b assume "b \<in> B"
+ with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
+ from `a \<in> A` have "\<Sqinter>A \<sqsubseteq> a" by (rule Inf_lower)
+ with `a \<sqsubseteq> b` show "\<Sqinter>A \<sqsubseteq> b" by auto
+qed
+
lemma INF_mono:
"(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<sqsubseteq> (\<Sqinter>n\<in>B. g n)"
by (force intro!: Inf_mono simp: INF_def)
+lemma Sup_mono:
+ assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
+ shows "\<Squnion>A \<sqsubseteq> \<Squnion>B"
+proof (rule Sup_least)
+ fix a assume "a \<in> A"
+ with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
+ from `b \<in> B` have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper)
+ with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
+qed
+
lemma SUP_mono:
"(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)"
by (force intro!: Sup_mono simp: SUP_def)
@@ -300,6 +245,106 @@
"A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
by (blast intro: SUP_mono dest: subsetD)
+lemma Inf_less_eq:
+ assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
+ and "A \<noteq> {}"
+ shows "\<Sqinter>A \<sqsubseteq> u"
+proof -
+ from `A \<noteq> {}` obtain v where "v \<in> A" by blast
+ moreover with assms have "v \<sqsubseteq> u" by blast
+ ultimately show ?thesis by (rule Inf_lower2)
+qed
+
+lemma less_eq_Sup:
+ assumes "\<And>v. v \<in> A \<Longrightarrow> u \<sqsubseteq> v"
+ and "A \<noteq> {}"
+ shows "u \<sqsubseteq> \<Squnion>A"
+proof -
+ from `A \<noteq> {}` obtain v where "v \<in> A" by blast
+ moreover with assms have "u \<sqsubseteq> v" by blast
+ ultimately show ?thesis by (rule Sup_upper2)
+qed
+
+lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
+ by (auto intro: Inf_greatest Inf_lower)
+
+lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
+ by (auto intro: Sup_least Sup_upper)
+
+lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
+ by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
+
+lemma INF_union:
+ "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
+ by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INF_I INF_leI)
+
+lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
+ by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
+
+lemma SUP_union:
+ "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
+ by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUP_I)
+
+lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)"
+ by (rule antisym) (rule le_INF_I, auto intro: le_infI1 le_infI2 INF_leI INF_mono)
+
+lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> 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]:
+ "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
+ "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
+proof -
+ show "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
+ proof
+ assume "\<forall>x\<in>A. x = \<top>"
+ then have "A = {} \<or> A = {\<top>}" by auto
+ then show "\<Sqinter>A = \<top>" by auto
+ next
+ assume "\<Sqinter>A = \<top>"
+ show "\<forall>x\<in>A. x = \<top>"
+ proof (rule ccontr)
+ assume "\<not> (\<forall>x\<in>A. x = \<top>)"
+ then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
+ then obtain B where "A = insert x B" by blast
+ with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
+ qed
+ qed
+ then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
+qed
+
+lemma INF_top_conv:
+ "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
+ "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
+ by (auto simp add: INF_def Inf_top_conv)
+
+lemma Sup_bot_conv [no_atp]:
+ "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
+ "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
+proof -
+ interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
+ by (fact dual_complete_lattice)
+ from dual.Inf_top_conv show ?P and ?Q by simp_all
+qed
+
+lemma SUP_bot_conv:
+ "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
+ "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
+ by (auto simp add: SUP_def Sup_bot_conv)
+
+lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
+ by (auto intro: antisym INF_leI le_INF_I)
+
+lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
+ by (auto intro: antisym SUP_leI le_SUP_I)
+
+lemma INF_top: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
+ by (cases "A = {}") (simp_all add: INF_empty)
+
+lemma SUP_bot: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
+ by (cases "A = {}") (simp_all add: SUP_empty)
+
lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>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:
- "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
- by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INF_I INF_leI)
-
-lemma SUP_union:
- "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
- by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUP_I)
-
lemma INF_constant:
"(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
by (simp add: INF_empty)
@@ -346,16 +383,6 @@
"(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
by (simp add: SUP_def image_def)
-lemma INF_top_conv:
- "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
- "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
- by (auto simp add: INF_def Inf_top_conv)
-
-lemma SUP_bot_conv:
- "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
- "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
- by (auto simp add: SUP_def Sup_bot_conv)
-
lemma less_INF_D:
assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> 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 \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
+ assumes inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
+begin
+
+lemma sup_INF:
+ "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
+ by (simp add: INF_def sup_Inf image_image)
+
+lemma inf_SUP:
+ "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
+ by (simp add: SUP_def inf_Sup image_image)
+
+lemma dual_complete_distrib_lattice:
+ "class.complete_distrib_lattice Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
+ 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 \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
+ then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_binary)
+qed
+
+lemma Inf_sup:
+ "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
+ by (simp add: sup_Inf sup_commute)
+
+lemma Sup_inf:
+ "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
+ by (simp add: inf_Sup inf_commute)
+
+lemma INF_sup:
+ "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
+ by (simp add: sup_INF sup_commute)
+
+lemma SUP_inf:
+ "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
+ by (simp add: inf_SUP inf_commute)
+
+lemma Inf_sup_eq_top_iff:
+ "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
+ by (simp only: Inf_sup INF_top_conv)
+
+lemma Sup_inf_eq_bot_iff:
+ "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
+ by (simp only: Sup_inf SUP_bot_conv)
+
+lemma INF_sup_distrib2:
+ "(\<Sqinter>a\<in>A. f a) \<squnion> (\<Sqinter>b\<in>B. g b) = (\<Sqinter>a\<in>A. \<Sqinter>b\<in>B. f a \<squnion> g b)"
+ by (subst INF_commute) (simp add: sup_INF INF_sup)
+
+lemma SUP_inf_distrib2:
+ "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> 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 \<ge>) (op >) sup inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - 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:
"- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
@@ -408,6 +497,9 @@
by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto
qed
+lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
+ by (simp add: INF_def SUP_def uminus_Inf image_image)
+
lemma uminus_Sup:
"- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
proof -
@@ -415,9 +507,6 @@
then show ?thesis by simp
qed
-lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
- by (simp add: INF_def SUP_def uminus_Inf image_image)
-
lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
by (simp add: INF_def SUP_def uminus_Sup image_image)
@@ -434,14 +523,14 @@
"\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
unfolding not_le [symmetric] le_Inf_iff by auto
+lemma INF_less_iff:
+ "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
+ unfolding INF_def Inf_less_iff by auto
+
lemma less_Sup_iff:
"a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
unfolding not_le [symmetric] Sup_le_iff by auto
-lemma INF_less_iff:
- "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
- unfolding INF_def Inf_less_iff by auto
-
lemma less_SUP_iff:
"a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
unfolding SUP_def less_Sup_iff by auto
@@ -468,6 +557,10 @@
qed
qed
+lemma SUP_eq_top_iff:
+ "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
+ unfolding SUP_def Sup_eq_top_iff by auto
+
lemma Inf_eq_bot_iff:
"\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
proof -
@@ -480,16 +573,12 @@
"(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
unfolding INF_def Inf_eq_bot_iff by auto
-lemma SUP_eq_top_iff:
- "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
- unfolding SUP_def Sup_eq_top_iff by auto
-
end
subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} 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
- "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+ "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
lemma Inf_apply:
- "(\<Sqinter>A) x = \<Sqinter>{y. \<exists>f\<in>A. y = f x}"
+ "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
by (simp add: Inf_fun_def)
definition
- "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+ "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
lemma Sup_apply:
- "(\<Squnion>A) x = \<Squnion>{y. \<exists>f\<in>A. y = f x}"
+ "(\<Squnion>A) x = (\<Squnion>f\<in>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 @@
"(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>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]: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
by (fact Sup_bot_conv)
-lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})" -- "FIXME generalize"
- by blast
-
lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
by blast
@@ -997,42 +1088,43 @@
subsection {* Distributive laws *}
lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
- by blast
+ by (fact inf_Sup)
+
+lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)"
+ by (fact sup_Inf)
lemma Int_Union2: "\<Union>B \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
- by blast
+ by (fact Sup_inf)
+
+lemma INT_Int_distrib: "(\<Inter>i\<in>I. A i \<inter> B i) = (\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i)"
+ by (rule sym) (rule INF_inf_distrib)
+
+lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)"
+ by (rule sym) (rule SUP_sup_distrib)
+
+lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"
+ by (simp only: INT_Int_distrib INF_def)
lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)"
-- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}
-- {* Union of a family of unions *}
- by blast
-
-lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)"
- -- {* Equivalent version *}
- by blast
+ by (simp only: UN_Un_distrib SUP_def)
-lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)"
- by blast
-
-lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"
- by blast
-
-lemma INT_Int_distrib: "(\<Inter>i\<in>I. A i \<inter> B i) = (\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i)"
- -- {* Equivalent version *}
- by blast
+lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
+ by (fact sup_INF)
lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. B \<inter> A i)"
-- {* Halmos, Naive Set Theory, page 35. *}
- by blast
-
-lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
- by blast
+ by (fact inf_SUP)
lemma Int_UN_distrib2: "(\<Union>i\<in>I. A i) \<inter> (\<Union>j\<in>J. B j) = (\<Union>i\<in>I. \<Union>j\<in>J. A i \<inter> B j)"
- by blast
+ by (fact SUP_inf_distrib2)
lemma Un_INT_distrib2: "(\<Inter>i\<in>I. A i) \<union> (\<Inter>j\<in>J. B j) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A i \<union> B j)"
- by blast
+ by (fact INF_sup_distrib2)
+
+lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})"
+ by (fact Sup_inf_eq_bot_iff)
subsection {* Complement *}
@@ -1051,9 +1143,9 @@
lemma UN_simps [simp]:
"\<And>a B C. (\<Union>x\<in>C. insert a (B x)) = (if C={} then {} else insert a (\<Union>x\<in>C. B x))"
- "\<And>A B C. (\<Union>x\<in>C. A x \<union> B) = ((if C={} then {} else (\<Union>x\<in>C. A x) \<union> B))"
+ "\<And>A B C. (\<Union>x\<in>C. A x \<union> B) = ((if C={} then {} else (\<Union>x\<in>C. A x) \<union> B))"
"\<And>A B C. (\<Union>x\<in>C. A \<union> B x) = ((if C={} then {} else A \<union> (\<Union>x\<in>C. B x)))"
- "\<And>A B C. (\<Union>x\<in>C. A x \<inter> B) = ((\<Union>x\<in>C. A x) \<inter>B)"
+ "\<And>A B C. (\<Union>x\<in>C. A x \<inter> B) = ((\<Union>x\<in>C. A x) \<inter> B)"
"\<And>A B C. (\<Union>x\<in>C. A \<inter> B x) = (A \<inter>(\<Union>x\<in>C. B x))"
"\<And>A B C. (\<Union>x\<in>C. A x - B) = ((\<Union>x\<in>C. A x) - B)"
"\<And>A B C. (\<Union>x\<in>C. A - B x) = (A - (\<Inter>x\<in>C. B x))"
@@ -1063,7 +1155,7 @@
by auto
lemma INT_simps [simp]:
- "\<And>A B C. (\<Inter>x\<in>C. A x \<inter> B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) \<inter>B)"
+ "\<And>A B C. (\<Inter>x\<in>C. A x \<inter> B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) \<inter> B)"
"\<And>A B C. (\<Inter>x\<in>C. A \<inter> B x) = (if C={} then UNIV else A \<inter>(\<Inter>x\<in>C. B x))"
"\<And>A B C. (\<Inter>x\<in>C. A x - B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) - B)"
"\<And>A B C. (\<Inter>x\<in>C. A - B x) = (if C={} then UNIV else A - (\<Union>x\<in>C. B x))"
@@ -1087,7 +1179,7 @@
lemma UN_extend_simps:
"\<And>a B C. insert a (\<Union>x\<in>C. B x) = (if C={} then {a} else (\<Union>x\<in>C. insert a (B x)))"
- "\<And>A B C. (\<Union>x\<in>C. A x) \<union> B = (if C={} then B else (\<Union>x\<in>C. A x \<union> B))"
+ "\<And>A B C. (\<Union>x\<in>C. A x) \<union> B = (if C={} then B else (\<Union>x\<in>C. A x \<union> B))"
"\<And>A B C. A \<union> (\<Union>x\<in>C. B x) = (if C={} then A else (\<Union>x\<in>C. A \<union> B x))"
"\<And>A B C. ((\<Union>x\<in>C. A x) \<inter> B) = (\<Union>x\<in>C. A x \<inter> B)"
"\<And>A B C. (A \<inter> (\<Union>x\<in>C. B x)) = (\<Union>x\<in>C. A \<inter> B x)"
--- 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
--- 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
--- 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
--- 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 *}
--- 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)
--- 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:
--- 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]: "#(<a>) = enat 1"
by (simp add: fsingleton_def2 enat_defs)
-lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)"
+lemma slen_fstreams[simp]: "#(<a> ooo s) = eSuc (#s)"
by (simp add: fsingleton_def2)
-lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)"
+lemma slen_fstreams2[simp]: "#(s ooo <a>) = 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" "<a>"], auto)
by (simp add: sconc_def)
--- 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)
--- 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]: "#\<bottom> = 0"
by (simp add: slen_def stream.finite_def zero_enat_def Least_equality)
-lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = iSuc (#xs)"
+lemma slen_scons [simp]: "x ~= \<bottom> ==> #(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 = \<bottom>)"
-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 = \<bottom>)"
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 ~= \<bottom> & #y = n)"
+lemma slen_eSuc: "#x = eSuc n --> (? a y. x = a&&y & a ~= \<bottom> & #y = n)"
by (cases x, auto)
lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>"
@@ -362,15 +362,15 @@
lemma slen_scons_eq_rev: "(#x < enat (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #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~=\<infinity> & #y~=\<infinity>) = (#(x ooo y)~=\<infinity>)"
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)
--- 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" ("_ /\<rightarrow>/ _")
-
definition
"null_heap \<equiv> \<lambda>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 "\<lambda>x. 0"} compactly:
*}
-lemma "[a \<rightarrow> Suc 0, b \<rightarrow> 2] = (null_heap (a := Suc 0)) (b := 2)"
+lemma "<a := Suc 0, b := 2> = (null_heap (a := Suc 0)) (b := 2)"
by (rule refl)
-value "aval (Plus (V ''x'') (N 5)) [''x'' \<rightarrow> 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 \<rightarrow> b::int]"} syntax:
+ the @{term "<a := b::int>"} syntax:
*}
-value "aval (Plus (V ''x'') (N 5)) [''y'' \<rightarrow> 7]"
+value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
subsection "Optimization"
--- 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'' \<rightarrow> 42, ''y'' \<rightarrow> 43] [50]"
+ <''x'' := 42, ''y'' := 43> [50]"
lemma aexec_append[simp]:
"aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
--- 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'' \<rightarrow> 3, ''y'' \<rightarrow> 1]"
+ <''x'' := 3, ''y'' := 1>"
subsection "Optimization"
--- 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'' \<rightarrow> 42]) \<Rightarrow> t}"
+values "{map t [''x''] |t. (SKIP, <''x'' := 42>) \<Rightarrow> t}"
-values "{map t [''x''] |t. (''x'' ::= N 2, [''x'' \<rightarrow> 42]) \<Rightarrow> t}"
+values "{map t [''x''] |t. (''x'' ::= N 2, <''x'' := 42>) \<Rightarrow> t}"
values "{map t [''x'',''y''] |t.
(WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
- [''x'' \<rightarrow> 0, ''y'' \<rightarrow> 13]) \<Rightarrow> t}"
+ <''x'' := 0, ''y'' := 13>) \<Rightarrow> t}"
text{* Proof automation: *}
--- 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 \<le> 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)
--- 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''] \<turnstile>
- (0, [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 4], []) \<rightarrow>* (i,t,stk)}"
+ (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
subsection{* Verification infrastructure *}
@@ -112,7 +112,7 @@
"ADD \<turnstile>i c \<rightarrow> c' =
(\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))"
"STORE x \<turnstile>i c \<rightarrow> c' =
- (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x \<rightarrow> hd stk), tl stk))"
+ (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x := hd stk), tl stk))"
"JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))"
"JMPFLESS n \<turnstile>i c \<rightarrow> c' =
(\<exists>i s stk. c = (i, s, stk) \<and>
--- 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'' \<rightarrow> 3, ''y'' \<rightarrow> 7, ''z'' \<rightarrow> 5]) \<rightarrow>* (c',t)}"
+ <''x'' := 3, ''y'' := 7, ''z'' := 5>) \<rightarrow>* (c',t)}"
subsection{* Proof infrastructure *}
--- 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) \<Longrightarrow> taval a2 s (Iv i2)
\<Longrightarrow> taval (Plus a1 a2) s (Iv(i1+i2))" |
-"taval a\<^isub>1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
+"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
\<Longrightarrow> taval (Plus a1 a2) s (Rv(r1+r2))"
inductive_cases [elim!]:
@@ -32,9 +32,9 @@
inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
"tbval (B bv) s bv" |
"tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
-"tbval b\<^isub>1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
-"taval a\<^isub>1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
-"taval a\<^isub>1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
+"tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
+"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
+"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
subsection "Syntax of Commands"
(* a copy of Com.thy - keep in sync! *)
--- 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"
--- 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
--- 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\<Rightarrow>enat"]]
-lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
-by (cases x) auto
+lemma not_infinity_eq [iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
+ by (cases x) auto
lemma not_enat_eq [iff]: "(ALL y. x ~= enat y) = (x = \<infinity>)"
-by (cases x) auto
+ by (cases x) auto
primrec the_enat :: "enat \<Rightarrow> 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 \<Rightarrow> enat" where
- "iSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
+definition eSuc :: "enat \<Rightarrow> enat" where
+ "eSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
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]: "(\<infinity>::enat) \<noteq> 0"
+lemma infinity_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0"
by (simp add: zero_enat_def)
-lemma i0_ne_Infty [simp]: "0 \<noteq> (\<infinity>::enat)"
+lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)"
by (simp add: zero_enat_def)
lemma zero_enat_eq [simp]:
@@ -112,35 +112,35 @@
"\<not> 1 = (0\<Colon>enat)"
unfolding zero_enat_def one_enat_def by simp_all
-lemma Infty_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
+lemma infinity_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
by (simp add: one_enat_def)
-lemma i1_ne_Infty [simp]: "1 \<noteq> (\<infinity>::enat)"
+lemma i1_ne_infinity [simp]: "1 \<noteq> (\<infinity>::enat)"
by (simp add: one_enat_def)
-lemma Infty_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
+lemma infinity_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
by (simp add: number_of_enat_def)
-lemma number_ne_Infty [simp]: "number_of k \<noteq> (\<infinity>::enat)"
+lemma number_ne_infinity [simp]: "number_of k \<noteq> (\<infinity>::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 \<infinity> = \<infinity>"
- by (simp add: iSuc_def)
+lemma eSuc_infinity [simp]: "eSuc \<infinity> = \<infinity>"
+ by (simp add: eSuc_def)
-lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
- by (simp add: iSuc_def zero_enat_def split: enat.splits)
+lemma eSuc_ne_0 [simp]: "eSuc n \<noteq> 0"
+ by (simp add: eSuc_def zero_enat_def split: enat.splits)
-lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n"
- by (rule iSuc_ne_0 [symmetric])
+lemma zero_ne_eSuc [simp]: "0 \<noteq> eSuc n"
+ by (rule eSuc_ne_0 [symmetric])
-lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n"
- by (simp add: iSuc_def split: enat.splits)
+lemma eSuc_inject [simp]: "eSuc m = eSuc n \<longleftrightarrow> m = n"
+ by (simp add: eSuc_def split: enat.splits)
lemma number_of_enat_inject [simp]:
"(number_of k \<Colon> enat) = number_of l \<longleftrightarrow> (number_of k \<Colon> 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 \<Colon> 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 \<Colon> 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 \<and> 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 (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
qed
-lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \<or> 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 \<or> n = 0)"
+ by (auto simp add: times_enat_def zero_enat_def split: enat.split)
-lemma imult_is_Infty: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
-by(auto simp add: times_enat_def zero_enat_def split: enat.split)
+lemma imult_is_infinity: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 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]: "\<infinity> - n = (\<infinity>::enat)"
-by(simp add: diff_enat_def)
+lemma idiff_infinity [simp,code]: "\<infinity> - n = (\<infinity>::enat)"
+ by (simp add: diff_enat_def)
-lemma idiff_Infty_right[simp,code]: "enat a - \<infinity> = 0"
-by(simp add: diff_enat_def)
+lemma idiff_infinity_right [simp,code]: "enat a - \<infinity> = 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 \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
-by(auto simp: zero_enat_def)
+lemma idiff_self [simp]: "n \<noteq> \<infinity> \<Longrightarrow> (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 \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0"
-by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
-
-lemma Infty_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
-lemma Infty_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
+lemma infinity_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
+ by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
+
+lemma infinity_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
by simp
lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)"
by (simp add: zero_enat_def less_enat_def split: enat.splits)
lemma i0_less [simp]: "(0\<Colon>enat) < n \<longleftrightarrow> n \<noteq> 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 \<le> iSuc m \<longleftrightarrow> n \<le> m"
- by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
+lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m"
+ by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
-lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m"
- by (simp add: iSuc_def less_enat_def split: enat.splits)
+lemma eSuc_mono [simp]: "eSuc n < eSuc m \<longleftrightarrow> n < m"
+ by (simp add: eSuc_def less_enat_def split: enat.splits)
-lemma ile_iSuc [simp]: "n \<le> iSuc n"
- by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
+lemma ile_eSuc [simp]: "n \<le> eSuc n"
+ by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
-lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
- by (simp add: zero_enat_def iSuc_def less_eq_enat_def split: enat.splits)
+lemma not_eSuc_ilei0 [simp]: "\<not> eSuc n \<le> 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 \<Longrightarrow> iSuc m \<le> n"
- by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits)
+lemma ileI1: "m < n \<Longrightarrow> eSuc m \<le> n"
+ by (simp add: eSuc_def less_eq_enat_def less_enat_def split: enat.splits)
lemma Suc_ile_eq: "enat (Suc m) \<le> n \<longleftrightarrow> enat m < n"
by (cases n) auto
-lemma iless_Suc_eq [simp]: "enat m < iSuc n \<longleftrightarrow> enat m \<le> n"
- by (auto simp add: iSuc_def less_enat_def split: enat.splits)
+lemma iless_Suc_eq [simp]: "enat m < eSuc n \<longleftrightarrow> enat m \<le> n"
+ by (auto simp add: eSuc_def less_enat_def split: enat.splits)
-lemma imult_Infty: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
-by (simp add: zero_enat_def less_enat_def split: enat.splits)
+lemma imult_infinity: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
+ by (simp add: zero_enat_def less_enat_def split: enat.splits)
-lemma imult_Infty_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
-by (simp add: zero_enat_def less_enat_def split: enat.splits)
+lemma imult_infinity_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
+ by (simp add: zero_enat_def less_enat_def split: enat.splits)
lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 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 < \<infinity>; !!k. n = enat k ==> P |] ==> P"
by (induct n) auto
@@ -519,7 +519,7 @@
next
show "P \<infinity>"
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
--- 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
--- 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 \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
\<Longrightarrow> fold f xs a = fold g ys b"
by (induct ys arbitrary: a b xs) simp_all
--- /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 \<or> b) \<or> c == a \<or> (b \<or> c)"
+ by simp
+
+lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
+ by blast
+
+lemma tfl_exE: "\<exists>x. P x ==> \<forall>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
--- /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 \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y"
+
+definition
+ "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+
+instance ..
+
+end
+
+lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y"
+ unfolding less_eq_prod_def by simp
+
+lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y"
+ unfolding less_eq_prod_def by simp
+
+lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')"
+ unfolding less_eq_prod_def by simp
+
+lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
+ unfolding less_eq_prod_def by simp
+
+instance prod :: (preorder, preorder) preorder
+proof
+ fix x y z :: "'a \<times> 'b"
+ show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+ by (rule less_prod_def)
+ show "x \<le> x"
+ unfolding less_eq_prod_def
+ by fast
+ assume "x \<le> y" and "y \<le> z" thus "x \<le> 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
--- 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"*)];
--- /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 \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+
+definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
+
+definition wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+"wfrec' R F x \<equiv> 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
--- 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 \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys"
by simp
@@ -1237,7 +1237,7 @@
(\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
by(auto dest:Cons_eq_filterD)
-lemma filter_cong[fundef_cong, recdef_cong]:
+lemma filter_cong[fundef_cong]:
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> 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 (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>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
--- 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 \<noteq> test_nam"
- distinct_fields: "val_nam \<noteq> 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:{..<size ss}. if \<not>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 "\<not> stable r step ss p")
- apply simp+
- done
+ "unstables r step ss =
+ foldr (\<lambda>p A. if \<not>stable r step ss p then insert p A else A) [0..<size ss] {}"
+proof -
+ have "unstables r step ss = (UN p:{..<size ss}. if \<not>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 "\<not> stable r step ss p")
+ apply simp+
+ done
+ also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
+ also note Sup_set_foldr also note foldr_map
+ also have "op \<union> \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) =
+ (\<lambda>p A. if \<not>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 \<Rightarrow> 'a" where
+definition some_elem :: "'a set \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("propa", "('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set")
+ #> Code.add_signature_cmd
+ ("iter", "('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list) \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set")
+ #> Code.add_signature_cmd ("unstables", "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list) \<Rightarrow> 's list \<Rightarrow> 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
--- 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\<turnstile>Norm (h, l) -LAcc v\<succ>the (l v)-> Norm (h, l)"
+using LAcc[of G "(h, l)" v] by simp
+
+lemma eval_Call_code:
+ "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
+ G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
+ (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
+ G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) -blk-> s3;
+ G\<turnstile> s3 -res\<succ>v -> (x4,(h4, l4)) |] ==>
+ G\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\<succ>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 \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> o \<Rightarrow> bool
+ and
+ evals: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> o \<Rightarrow> bool
+ and
+ exec: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> 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
--- 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
--- 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 \<noteq> next_name"
+ and distinct_vars:
+ "l_nam \<noteq> l1_nam" "l_nam \<noteq> l2_nam" "l_nam \<noteq> l3_nam" "l_nam \<noteq> l4_nam"
+ "l1_nam \<noteq> l2_nam" "l1_nam \<noteq> l3_nam" "l1_nam \<noteq> l4_nam"
+ "l2_nam \<noteq> l3_nam" "l2_nam \<noteq> l4_nam"
+ "l3_nam \<noteq> 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 \<longleftrightarrow> True"
+ by(simp add: equal_cnam_def)
+
+code_datatype append_name
+lemma equal_mname_code [code]:
+ "HOL.equal append_name append_name \<longleftrightarrow> True"
+ by(simp add: equal_mname_def)
-consts_code
- "new_Addr" ("\<module>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 \<longleftrightarrow> True"
+ "HOL.equal next_nam next_nam \<longleftrightarrow> True"
+ "HOL.equal l_nam l_nam \<longleftrightarrow> True"
+ "HOL.equal l1_nam l1_nam \<longleftrightarrow> True"
+ "HOL.equal l2_nam l2_nam \<longleftrightarrow> True"
+ "HOL.equal l3_nam l3_nam \<longleftrightarrow> True"
+ "HOL.equal l4_nam l4_nam \<longleftrightarrow> True"
+
+ "HOL.equal val_nam next_nam \<longleftrightarrow> False"
+ "HOL.equal next_nam val_nam \<longleftrightarrow> False"
- "undefined" ("(raise Match)")
- "undefined :: val" ("{* Unit *}")
- "undefined :: cname" ("\"\"")
+ "HOL.equal l_nam l1_nam \<longleftrightarrow> False"
+ "HOL.equal l_nam l2_nam \<longleftrightarrow> False"
+ "HOL.equal l_nam l3_nam \<longleftrightarrow> False"
+ "HOL.equal l_nam l4_nam \<longleftrightarrow> False"
+
+ "HOL.equal l1_nam l_nam \<longleftrightarrow> False"
+ "HOL.equal l1_nam l2_nam \<longleftrightarrow> False"
+ "HOL.equal l1_nam l3_nam \<longleftrightarrow> False"
+ "HOL.equal l1_nam l4_nam \<longleftrightarrow> False"
+
+ "HOL.equal l2_nam l_nam \<longleftrightarrow> False"
+ "HOL.equal l2_nam l1_nam \<longleftrightarrow> False"
+ "HOL.equal l2_nam l3_nam \<longleftrightarrow> False"
+ "HOL.equal l2_nam l4_nam \<longleftrightarrow> 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 \<longleftrightarrow> False"
+ "HOL.equal l3_nam l1_nam \<longleftrightarrow> False"
+ "HOL.equal l3_nam l2_nam \<longleftrightarrow> False"
+ "HOL.equal l3_nam l4_nam \<longleftrightarrow> False"
+
+ "HOL.equal l4_nam l_nam \<longleftrightarrow> False"
+ "HOL.equal l4_nam l1_nam \<longleftrightarrow> False"
+ "HOL.equal l4_nam l2_nam \<longleftrightarrow> False"
+ "HOL.equal l4_nam l3_nam \<longleftrightarrow> 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' \<longleftrightarrow> l = l'"
+lemma equal_loc'_code [code]:
+ "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'"
+ by(simp add: equal_loc'_def nat_to_loc'_inject)
-code_module J
-contains
- test = "example_prg\<turnstile>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 (\<lambda>s. example_prg\<turnstile>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
--- 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 \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where
"raise_if b x xo \<equiv> if b \<and> (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 \<times> val option" where
"new_Addr h \<equiv> SOME (a,x). (h a = None \<and> x = None) | x = Some (Addr (XcptRef OutOfMemory))"
+*)
+consts nat_to_loc' :: "nat => loc'"
+code_datatype nat_to_loc'
+definition new_Addr :: "aheap => loc \<times> val option" where
+ "new_Addr h \<equiv>
+ if \<exists>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 \<and> xcp = None \<or> 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 \<noteq> 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 \<Rightarrow> loc \<times> val option" where
+ "gen_new_Addr h n \<equiv>
+ if \<exists>a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None
+ then (Loc (nat_to_loc' (LEAST a. a \<ge> n \<and> 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' \<longleftrightarrow> l = l'"
+instance proof qed(simp add: equal_loc'_def)
end
+
+end
--- 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 \<equiv> (Object, (undefined,[],[]))"
+ [code_inline]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
definition NullPointerC :: "'c cdecl" where
- "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
+ [code_inline]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
definition ClassCastC :: "'c cdecl" where
- "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
+ [code_inline]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
definition OutOfMemoryC :: "'c cdecl" where
- "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
+ [code_inline]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
definition SystemClasses :: "'c cdecl list" where
- "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
+ [code_inline]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
end
--- 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' \<longleftrightarrow> 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 \<equiv> \<lambda>_ :: cnam itself. Typerep.Typerep (STR ''Type.cnam'') []"
+instance proof qed
+end
+instantiation cnam :: term_of begin
+definition "term_of_class.term_of (C :: cnam) \<equiv>
+ 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' \<longleftrightarrow> vn = vn'"
+instance proof qed(simp add: equal_vnam_def)
+end
+instantiation vnam :: typerep begin
+definition "typerep_class.typerep \<equiv> \<lambda>_ :: vnam itself. Typerep.Typerep (STR ''Type.vnam'') []"
+instance proof qed
+end
+instantiation vnam :: term_of begin
+definition "term_of_class.term_of (V :: vnam) \<equiv>
+ 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' \<longleftrightarrow> M = M'"
+instance proof qed(simp add: equal_mname_def)
+end
+instantiation mname :: typerep begin
+definition "typerep_class.typerep \<equiv> \<lambda>_ :: mname itself. Typerep.Typerep (STR ''Type.mname'') []"
+instance proof qed
+end
+instantiation mname :: term_of begin
+definition "term_of_class.term_of (M :: mname) \<equiv>
+ 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
--- 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 \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
+ subcls1p
+ .
+declare subcls1_def[unfolded Collect_def, code_pred_def]
+code_pred
+ (modes: i \<Rightarrow> i \<times> o \<Rightarrow> bool, i \<Rightarrow> i \<times> i \<Rightarrow> bool)
+ [inductify]
+ subcls1
+ .
+
+definition subcls' where "subcls' G = (subcls1p G)^**"
+code_pred
+ (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
+ [inductify]
+ subcls'
+.
+lemma subcls_conv_subcls' [code_inline]:
+ "(subcls1 G)^* = (\<lambda>(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 \<Rightarrow> class_rec G C t f
+ | Some (D, fs, ms) \<Rightarrow>
+ 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" ("\<module>wfrec?")
-attach {*
-fun wfrec f x = f (wfrec f) x;
-*}
+lemma wf_class_code [code]:
+ "wf_class G \<longleftrightarrow> (\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>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 "\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C"
+ proof(safe)
+ fix C D fs ms
+ assume "(C, D, fs, ms) \<in> set G"
+ and "C \<noteq> Object"
+ and subcls: "G \<turnstile> fst (the (class G C)) \<preceq>C C"
+ from `(C, D, fs, ms) \<in> 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 \<turnstile> C \<prec>C1 D'" using `C \<noteq> Object` ..
+ hence "(C, D') \<in> (subcls1 G)^+" ..
+ also with acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
+ with subcls "class" have "(D', C) \<in> (subcls1 G)^+" by(auto dest: rtranclD)
+ finally show False using acyc by(auto simp add: acyclic_def)
+ qed
+next
+ assume rhs[rule_format]: "\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C"
+ have "acyclic (subcls1 G)"
+ proof(intro acyclicI strip notI)
+ fix C
+ assume "(C, C) \<in> (subcls1 G)\<^sup>+"
+ thus False
+ proof(cases)
+ case base
+ then obtain rest where "class G C = Some (C, rest)"
+ and "C \<noteq> Object" by cases
+ from `class G C = Some (C, rest)` have "(C, C, rest) \<in> set G"
+ unfolding class_def by(rule map_of_SomeD)
+ with `C \<noteq> Object` `class G C = Some (C, rest)`
+ have "\<not> G \<turnstile> C \<preceq>C C" by(auto dest: rhs)
+ thus False by simp
+ next
+ case (step D)
+ from `G \<turnstile> D \<prec>C1 C` obtain rest where "class G D = Some (C, rest)"
+ and "D \<noteq> Object" by cases
+ from `class G D = Some (C, rest)` have "(D, C, rest) \<in> set G"
+ unfolding class_def by(rule map_of_SomeD)
+ with `D \<noteq> Object` `class G D = Some (C, rest)`
+ have "\<not> G \<turnstile> C \<preceq>C D" by(auto dest: rhs)
+ moreover from `(C, D) \<in> (subcls1 G)\<^sup>+`
+ have "G \<turnstile> C \<preceq>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 \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
field :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty )" (* ###curry *)
fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
-- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
-defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
+defs method_def [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
ts ++ map_of (map (\<lambda>(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 \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts.
+defs fields_def [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts.
map (\<lambda>(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 (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
+defs field_def [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
lemma field_fields:
"field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
@@ -138,6 +228,8 @@
| subcls : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
| null [intro!]: "G\<turnstile> NT \<preceq> RefT R"
+code_pred widen .
+
lemmas refl = HOL.refl
-- "casting conversion, cf. 5.5 / 5.1.5"
--- 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 \<noteq> test_nam"
+
+axiomatization append_name makelist_name :: mname
+where distinct_methods: "append_name \<noteq> makelist_name"
+
+axiomatization val_nam next_nam :: vnam
+where distinct_fields: "val_nam \<noteq> next_nam"
+
+axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> 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 \<longleftrightarrow> True"
+ "HOL.equal test_nam test_nam \<longleftrightarrow> True"
+ "HOL.equal list_nam test_nam \<longleftrightarrow> False"
+ "HOL.equal test_nam list_nam \<longleftrightarrow> 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 \<longleftrightarrow> True"
+ "HOL.equal makelist_name makelist_name \<longleftrightarrow> True"
+ "HOL.equal append_name makelist_name \<longleftrightarrow> False"
+ "HOL.equal makelist_name append_name \<longleftrightarrow> False"
+ by(simp_all add: distinct_methods distinct_methods[symmetric] equal_mname_def)
-consts_code
- "new_Addr" ("\<module>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 \<longleftrightarrow> True"
+ "HOL.equal next_nam next_nam \<longleftrightarrow> True"
+ "HOL.equal val_nam next_nam \<longleftrightarrow> False"
+ "HOL.equal next_nam val_nam \<longleftrightarrow> 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') \<longleftrightarrow> 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
--- 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) \<longleftrightarrow> affine s"
by (metis affine_affine_hull hull_same mem_def)
-lemma setsum_restrict_set'': assumes "finite A"
- shows "setsum f {x \<in> A. P x} = (\<Sum>x\<in>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"
--- 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 \<times> cname) set" --{* subclass *}
--- 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 \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
"wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
-axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-
-definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
-[nitpick_simp]: "wf_wfrec' R F x = F (Recdef.cut (wf_wfrec R F) R x) x"
-
-definition wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
-"wfrec' R F x \<equiv> 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 \<Rightarrow> bool) \<Rightarrow> nat" where
"card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> 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
--- 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
--- 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 \<in> (op =) y \<longleftrightarrow> 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 (\<Squnion>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 \<circ> f)"
+ by (unfold INFI_def) simp
+
+lemma eval_SUPR [simp]:
+ "eval (SUPR A f) = SUPR A (eval \<circ> 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 \<circ> f)"
- by (unfold INFI_def) simp
-
-lemma eval_SUPR [simp]:
- "eval (SUPR A f) = SUPR A (eval \<circ> f)"
- by (unfold SUPR_def) simp
-
definition single :: "'a \<Rightarrow> 'a pred" where
"single x = Pred ((op =) x)"
@@ -741,11 +749,12 @@
by simp
lemma closure_of_bool_cases [no_atp]:
-assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
-assumes "f = (%u. True) \<Longrightarrow> P f"
-shows "P f"
+ fixes f :: "unit \<Rightarrow> bool"
+ assumes "f = (\<lambda>u. False) \<Longrightarrow> P f"
+ assumes "f = (\<lambda>u. True) \<Longrightarrow> P f"
+ shows "P f"
proof -
- have "f = (%u. False) \<or> f = (%u. True)"
+ have "f = (\<lambda>u. False) \<or> f = (\<lambda>u. True)"
apply (cases "f ()")
apply (rule disjI2)
apply (rule ext)
@@ -758,19 +767,18 @@
qed
lemma unit_pred_cases:
-assumes "P \<bottom>"
-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 \<bottom>"
+ 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 (\<lambda>u. False))" "P (Pred (\<lambda>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
--- 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 \<or> b) \<or> c == a \<or> (b \<or> c)"
- by simp
-
-lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
- by blast
-
-lemma tfl_exE: "\<exists>x. P x ==> \<forall>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
--- 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 =
--- 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
"{..<u} == {x. x < u}"
@@ -1162,12 +1163,18 @@
(if m <= n then f m - f(n + 1) else 0)"
by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
-lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]
+lemma setsum_restrict_set':
+ "finite A \<Longrightarrow> setsum f {x \<in> A. x \<in> B} = (\<Sum>x\<in>A. if x \<in> B then f x else 0)"
+ by (simp add: setsum_restrict_set [symmetric] Int_def)
+
+lemma setsum_restrict_set'':
+ "finite A \<Longrightarrow> setsum f {x \<in> A. P x} = (\<Sum>x\<in>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 \<Longrightarrow> finite T \<Longrightarrow> setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y\<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T"
- by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)
- (rule setsum_commute)
+ "finite S \<Longrightarrow> finite T \<Longrightarrow>
+ setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y \<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> 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 (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
--- 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. *}
--- 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 =
--- 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 =
--- 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
--- 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)
--- 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 \<subseteq> inv_image (lprod R) (\<lambda> (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 \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
--- 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]: "\<lbrakk> M = N; !! x. zin x N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> zimage f M = zimage g N"
+lemma zimage_cong[fundef_cong]: "\<lbrakk> M = N; !! x. zin x N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> zimage f M = zimage g N"
by (auto simp add: zet_ext_eq zimage_iff)
end
--- 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) \<le> 12"
value [code] "(10::int) \<le> 12"
-value [SML] "(10::int) \<le> 12"
value [nbe] "(10::int) \<le> 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
--- 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
--- 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
--- 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
--- 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")