--- a/src/HOL/Complete_Lattices.thy Mon Aug 01 13:51:17 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy Mon Aug 01 22:11:29 2016 +0200
@@ -1,9 +1,14 @@
-(* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
+(* Title: HOL/Complete_Lattices.thy
+ Author: Tobias Nipkow
+ Author: Lawrence C Paulson
+ Author: Markus Wenzel
+ Author: Florian Haftmann
+*)
section \<open>Complete lattices\<close>
theory Complete_Lattices
-imports Fun
+ imports Fun
begin
notation
@@ -14,27 +19,22 @@
subsection \<open>Syntactic infimum and supremum operations\<close>
class Inf =
- fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
+ fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
begin
abbreviation INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
- "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
+ where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
-lemma INF_image [simp]:
- "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
+lemma INF_image [simp]: "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
by (simp add: image_comp)
-lemma INF_identity_eq [simp]:
- "INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
+lemma INF_identity_eq [simp]: "INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
by simp
-lemma INF_id_eq [simp]:
- "INFIMUM A id = \<Sqinter>A"
+lemma INF_id_eq [simp]: "INFIMUM A id = \<Sqinter>A"
by simp
-lemma INF_cong:
- "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
+lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
by (simp add: image_def)
lemma strong_INF_cong [cong]:
@@ -44,27 +44,22 @@
end
class Sup =
- fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
+ fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
begin
abbreviation SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
- "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
+ where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
-lemma SUP_image [simp]:
- "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
+lemma SUP_image [simp]: "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
by (simp add: image_comp)
-lemma SUP_identity_eq [simp]:
- "SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
+lemma SUP_identity_eq [simp]: "SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
by simp
-lemma SUP_id_eq [simp]:
- "SUPREMUM A id = \<Squnion>A"
+lemma SUP_id_eq [simp]: "SUPREMUM A id = \<Squnion>A"
by (simp add: id_def)
-lemma SUP_cong:
- "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
+lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
by (simp add: image_def)
lemma strong_SUP_cong [cong]:
@@ -122,25 +117,25 @@
class complete_lattice = lattice + Inf + Sup + bot + top +
assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
- and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
- assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
- and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
- assumes Inf_empty [simp]: "\<Sqinter>{} = \<top>"
- assumes Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
+ and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
+ and Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
+ and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
+ and Inf_empty [simp]: "\<Sqinter>{} = \<top>"
+ and Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
begin
subclass bounded_lattice
proof
fix a
- show "\<bottom> \<le> a" by (auto intro: Sup_least simp only: Sup_empty [symmetric])
- show "a \<le> \<top>" by (auto intro: Inf_greatest simp only: Inf_empty [symmetric])
+ show "\<bottom> \<le> a"
+ by (auto intro: Sup_least simp only: Sup_empty [symmetric])
+ show "a \<le> \<top>"
+ by (auto intro: Inf_greatest simp only: Inf_empty [symmetric])
qed
-lemma dual_complete_lattice:
- "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
+lemma dual_complete_lattice: "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
by (auto intro!: class.complete_lattice.intro dual_lattice)
- (unfold_locales, (fact Inf_empty Sup_empty
- Sup_upper Sup_least Inf_lower Inf_greatest)+)
+ (unfold_locales, (fact Inf_empty Sup_empty Sup_upper Sup_least Inf_lower Inf_greatest)+)
end
@@ -217,12 +212,10 @@
lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
by (simp cong del: strong_SUP_cong)
-lemma Inf_UNIV [simp]:
- "\<Sqinter>UNIV = \<bottom>"
+lemma Inf_UNIV [simp]: "\<Sqinter>UNIV = \<bottom>"
by (auto intro!: antisym Inf_lower)
-lemma Sup_UNIV [simp]:
- "\<Squnion>UNIV = \<top>"
+lemma Sup_UNIV [simp]: "\<Squnion>UNIV = \<top>"
by (auto intro!: antisym Sup_upper)
lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
@@ -247,8 +240,7 @@
with \<open>a \<sqsubseteq> b\<close> 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)"
+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)"
using Inf_mono [of "g ` B" "f ` A"] by auto
lemma Sup_mono:
@@ -261,17 +253,14 @@
with \<open>a \<sqsubseteq> b\<close> 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)"
+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)"
using Sup_mono [of "f ` A" "g ` B"] by auto
-lemma INF_superset_mono:
- "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
+lemma INF_superset_mono: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
\<comment> \<open>The last inclusion is POSITIVE!\<close>
by (blast intro: INF_mono dest: subsetD)
-lemma SUP_subset_mono:
- "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)"
+lemma SUP_subset_mono: "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:
@@ -296,13 +285,13 @@
lemma INF_eq:
assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
- assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
+ and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
shows "INFIMUM A f = INFIMUM B g"
by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
lemma SUP_eq:
assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
- assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
+ and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
shows "SUPREMUM A f = SUPREMUM B g"
by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
@@ -315,25 +304,25 @@
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)"
+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 INF_greatest INF_lower)
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)"
+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_least SUP_upper)
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 INF_greatest, auto intro: le_infI1 le_infI2 INF_lower 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)" (is "?L = ?R")
+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)"
+ (is "?L = ?R")
proof (rule antisym)
- show "?L \<le> ?R" by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
-next
- show "?R \<le> ?L" by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
+ show "?L \<le> ?R"
+ by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
+ show "?R \<le> ?L"
+ by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
qed
lemma Inf_top_conv [simp]:
@@ -364,14 +353,14 @@
using Inf_top_conv [of "B ` A"] by simp_all
lemma Sup_bot_conv [simp]:
- "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
- "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
+ "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)"
+ "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)"
using dual_complete_lattice
by (rule complete_lattice.Inf_top_conv)+
lemma SUP_bot_conv [simp]:
- "(\<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>)"
+ "(\<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>)"
using Sup_bot_conv [of "B ` A"] by simp_all
lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
@@ -408,25 +397,22 @@
then show ?thesis by simp
qed
-lemma INF_inf_const1:
- "I \<noteq> {} \<Longrightarrow> (INF i:I. inf x (f i)) = inf x (INF i:I. f i)"
+lemma INF_inf_const1: "I \<noteq> {} \<Longrightarrow> (INF i:I. inf x (f i)) = inf x (INF i:I. f i)"
by (intro antisym INF_greatest inf_mono order_refl INF_lower)
(auto intro: INF_lower2 le_infI2 intro!: INF_mono)
-lemma INF_inf_const2:
- "I \<noteq> {} \<Longrightarrow> (INF i:I. inf (f i) x) = inf (INF i:I. f i) x"
+lemma INF_inf_const2: "I \<noteq> {} \<Longrightarrow> (INF i:I. inf (f i) x) = inf (INF i:I. f i) x"
using INF_inf_const1[of I x f] by (simp add: inf_commute)
-lemma INF_constant:
- "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
+lemma INF_constant: "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
by simp
-lemma SUP_constant:
- "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
+lemma SUP_constant: "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
by simp
lemma less_INF_D:
- assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
+ assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A"
+ shows "y < f i"
proof -
note \<open>y < (\<Sqinter>i\<in>A. f i)\<close>
also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using \<open>i \<in> A\<close>
@@ -435,20 +421,19 @@
qed
lemma SUP_lessD:
- assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
+ assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A"
+ shows "f i < y"
proof -
- have "f i \<le> (\<Squnion>i\<in>A. f i)" using \<open>i \<in> A\<close>
- by (rule SUP_upper)
+ have "f i \<le> (\<Squnion>i\<in>A. f i)"
+ using \<open>i \<in> A\<close> by (rule SUP_upper)
also note \<open>(\<Squnion>i\<in>A. f i) < y\<close>
finally show "f i < y" .
qed
-lemma INF_UNIV_bool_expand:
- "(\<Sqinter>b. A b) = A True \<sqinter> A False"
+lemma INF_UNIV_bool_expand: "(\<Sqinter>b. A b) = A True \<sqinter> A False"
by (simp add: UNIV_bool inf_commute)
-lemma SUP_UNIV_bool_expand:
- "(\<Squnion>b. A b) = A True \<squnion> A False"
+lemma SUP_UNIV_bool_expand: "(\<Squnion>b. A b) = A True \<squnion> A False"
by (simp add: UNIV_bool sup_commute)
lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
@@ -457,21 +442,17 @@
lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f"
using Inf_le_Sup [of "f ` A"] by simp
-lemma INF_eq_const:
- "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
+lemma INF_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
by (auto intro: INF_eqI)
-lemma SUP_eq_const:
- "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
+lemma SUP_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
by (auto intro: SUP_eqI)
-lemma INF_eq_iff:
- "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> (INFIMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
+lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> INFIMUM I f = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
using INF_eq_const [of I f c] INF_lower [of _ I f]
by (auto intro: antisym cong del: strong_INF_cong)
-lemma SUP_eq_iff:
- "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPREMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
+lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> SUPREMUM I f = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
using SUP_eq_const [of I f c] SUP_upper [of _ I f]
by (auto intro: antisym cong del: strong_SUP_cong)
@@ -479,61 +460,52 @@
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)"
+ and 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)"
+lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
by (simp add: sup_Inf)
-lemma inf_SUP:
- "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
+lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
by (simp add: inf_Sup)
lemma dual_complete_distrib_lattice:
"class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
apply (rule class.complete_distrib_lattice.intro)
- apply (fact dual_complete_lattice)
+ apply (fact dual_complete_lattice)
apply (rule class.complete_distrib_lattice_axioms.intro)
- apply (simp_all add: inf_Sup sup_Inf)
+ apply (simp_all add: inf_Sup sup_Inf)
done
-subclass distrib_lattice proof
+subclass distrib_lattice
+proof
fix a b c
- from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
+ have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" by (rule sup_Inf)
then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp
qed
-lemma Inf_sup:
- "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
+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)"
+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)"
+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)"
+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>)"
+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>)"
+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)"
+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)"
+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)
context
@@ -541,20 +513,16 @@
assumes "mono f"
begin
-lemma mono_Inf:
- shows "f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)"
+lemma mono_Inf: "f (\<Sqinter>A) \<le> (\<Sqinter>x\<in>A. f x)"
using \<open>mono f\<close> by (auto intro: complete_lattice_class.INF_greatest Inf_lower dest: monoD)
-lemma mono_Sup:
- shows "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
+lemma mono_Sup: "(\<Squnion>x\<in>A. f x) \<le> f (\<Squnion>A)"
using \<open>mono f\<close> by (auto intro: complete_lattice_class.SUP_least Sup_upper dest: monoD)
-lemma mono_INF:
- "f (INF i : I. A i) \<le> (INF x : I. f (A x))"
+lemma mono_INF: "f (INF i : I. A i) \<le> (INF x : I. f (A x))"
by (intro complete_lattice_class.INF_greatest monoD[OF \<open>mono f\<close>] INF_lower)
-lemma mono_SUP:
- "(SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
+lemma mono_SUP: "(SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
by (intro complete_lattice_class.SUP_least monoD[OF \<open>mono f\<close>] SUP_upper)
end
@@ -566,10 +534,11 @@
lemma dual_complete_boolean_algebra:
"class.complete_boolean_algebra Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
- by (rule class.complete_boolean_algebra.intro, rule dual_complete_distrib_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)"
+lemma uminus_Inf: "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
proof (rule antisym)
show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)"
by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp
@@ -580,13 +549,13 @@
lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
by (simp add: uminus_Inf image_image)
-lemma uminus_Sup:
- "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
+lemma uminus_Sup: "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
proof -
- have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_INF)
+ have "\<Squnion>A = - \<Sqinter>(uminus ` A)"
+ by (simp add: image_image uminus_INF)
then show ?thesis by simp
qed
-
+
lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
by (simp add: uminus_Sup image_image)
@@ -605,29 +574,27 @@
lemma complete_linorder_sup_max: "sup = max"
by (auto intro: antisym simp add: max_def fun_eq_iff)
-lemma Inf_less_iff:
- "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
+lemma Inf_less_iff: "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
by (simp add: not_le [symmetric] le_Inf_iff)
-lemma INF_less_iff:
- "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
+lemma INF_less_iff: "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
by (simp add: Inf_less_iff [of "f ` A"])
-lemma less_Sup_iff:
- "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
+lemma less_Sup_iff: "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
by (simp add: not_le [symmetric] Sup_le_iff)
-lemma less_SUP_iff:
- "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
+lemma less_SUP_iff: "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
by (simp add: less_Sup_iff [of _ "f ` A"])
-lemma Sup_eq_top_iff [simp]:
- "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
+lemma Sup_eq_top_iff [simp]: "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
proof
assume *: "\<Squnion>A = \<top>"
- show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
+ show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
+ unfolding * [symmetric]
proof (intro allI impI)
- fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
+ fix x
+ assume "x < \<Squnion>A"
+ then show "\<exists>i\<in>A. x < i"
by (simp add: less_Sup_iff)
qed
next
@@ -635,42 +602,40 @@
show "\<Squnion>A = \<top>"
proof (rule ccontr)
assume "\<Squnion>A \<noteq> \<top>"
- with top_greatest [of "\<Squnion>A"]
- have "\<Squnion>A < \<top>" unfolding le_less by auto
- then have "\<Squnion>A < \<Squnion>A"
- using * unfolding less_Sup_iff by auto
+ with top_greatest [of "\<Squnion>A"] have "\<Squnion>A < \<top>"
+ unfolding le_less by auto
+ with * have "\<Squnion>A < \<Squnion>A"
+ unfolding less_Sup_iff by auto
then show False by auto
qed
qed
-lemma SUP_eq_top_iff [simp]:
- "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
+lemma SUP_eq_top_iff [simp]: "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
using Sup_eq_top_iff [of "f ` A"] by simp
-lemma Inf_eq_bot_iff [simp]:
- "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
+lemma Inf_eq_bot_iff [simp]: "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
using dual_complete_linorder
by (rule complete_linorder.Sup_eq_top_iff)
-lemma INF_eq_bot_iff [simp]:
- "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
+lemma INF_eq_bot_iff [simp]: "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
using Inf_eq_bot_iff [of "f ` A"] by simp
lemma Inf_le_iff: "\<Sqinter>A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
proof safe
- fix y assume "x \<ge> \<Sqinter>A" "y > x"
+ fix y
+ assume "x \<ge> \<Sqinter>A" "y > x"
then have "y > \<Sqinter>A" by auto
then show "\<exists>a\<in>A. y > a"
unfolding Inf_less_iff .
qed (auto elim!: allE[of _ "\<Sqinter>A"] simp add: not_le[symmetric] Inf_lower)
-lemma INF_le_iff:
- "INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
+lemma INF_le_iff: "INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
using Inf_le_iff [of "f ` A"] by simp
lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
proof safe
- fix y assume "x \<le> \<Squnion>A" "y < x"
+ fix y
+ assume "x \<le> \<Squnion>A" "y < x"
then have "y < \<Squnion>A" by auto
then show "\<exists>a\<in>A. y < a"
unfolding less_Sup_iff .
@@ -696,35 +661,29 @@
instantiation bool :: complete_lattice
begin
-definition
- [simp, code]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
+definition [simp, code]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
-definition
- [simp, code]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
+definition [simp, code]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
-instance proof
-qed (auto intro: bool_induct)
+instance
+ by standard (auto intro: bool_induct)
end
-lemma not_False_in_image_Ball [simp]:
- "False \<notin> P ` A \<longleftrightarrow> Ball A P"
+lemma not_False_in_image_Ball [simp]: "False \<notin> P ` A \<longleftrightarrow> Ball A P"
by auto
-lemma True_in_image_Bex [simp]:
- "True \<in> P ` A \<longleftrightarrow> Bex A P"
+lemma True_in_image_Bex [simp]: "True \<in> P ` A \<longleftrightarrow> Bex A P"
by auto
-lemma INF_bool_eq [simp]:
- "INFIMUM = Ball"
+lemma INF_bool_eq [simp]: "INFIMUM = Ball"
by (simp add: fun_eq_iff)
-lemma SUP_bool_eq [simp]:
- "SUPREMUM = Bex"
+lemma SUP_bool_eq [simp]: "SUPREMUM = Bex"
by (simp add: fun_eq_iff)
-instance bool :: complete_boolean_algebra proof
-qed (auto intro: bool_induct)
+instance bool :: complete_boolean_algebra
+ by standard (auto intro: bool_induct)
subsection \<open>Complete lattice on @{typ "_ \<Rightarrow> _"}\<close>
@@ -732,11 +691,9 @@
instantiation "fun" :: (type, Inf) Inf
begin
-definition
- "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
+definition "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
-lemma Inf_apply [simp, code]:
- "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
+lemma Inf_apply [simp, code]: "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
by (simp add: Inf_fun_def)
instance ..
@@ -746,11 +703,9 @@
instantiation "fun" :: (type, Sup) Sup
begin
-definition
- "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
+definition "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
-lemma Sup_apply [simp, code]:
- "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
+lemma Sup_apply [simp, code]: "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
by (simp add: Sup_fun_def)
instance ..
@@ -760,57 +715,47 @@
instantiation "fun" :: (type, complete_lattice) complete_lattice
begin
-instance proof
-qed (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)
+instance
+ by standard (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)
end
-lemma INF_apply [simp]:
- "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
+lemma INF_apply [simp]: "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
using Inf_apply [of "f ` A"] by (simp add: comp_def)
-lemma SUP_apply [simp]:
- "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
+lemma SUP_apply [simp]: "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
using Sup_apply [of "f ` A"] by (simp add: comp_def)
-instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
-qed (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image)
+instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
+ by standard (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image)
instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
subsection \<open>Complete lattice on unary and binary predicates\<close>
-lemma Inf1_I:
- "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a"
+lemma Inf1_I: "(\<And>P. P \<in> A \<Longrightarrow> P a) \<Longrightarrow> (\<Sqinter>A) a"
by auto
-lemma INF1_I:
- "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
+lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
by simp
-lemma INF2_I:
- "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
+lemma INF2_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
by simp
-lemma Inf2_I:
- "(\<And>r. r \<in> A \<Longrightarrow> r a b) \<Longrightarrow> (\<Sqinter>A) a b"
+lemma Inf2_I: "(\<And>r. r \<in> A \<Longrightarrow> r a b) \<Longrightarrow> (\<Sqinter>A) a b"
by auto
-lemma Inf1_D:
- "(\<Sqinter>A) a \<Longrightarrow> P \<in> A \<Longrightarrow> P a"
+lemma Inf1_D: "(\<Sqinter>A) a \<Longrightarrow> P \<in> A \<Longrightarrow> P a"
by auto
-lemma INF1_D:
- "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
+lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
by simp
-lemma Inf2_D:
- "(\<Sqinter>A) a b \<Longrightarrow> r \<in> A \<Longrightarrow> r a b"
+lemma Inf2_D: "(\<Sqinter>A) a b \<Longrightarrow> r \<in> A \<Longrightarrow> r a b"
by auto
-lemma INF2_D:
- "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
+lemma INF2_D: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
by simp
lemma Inf1_E:
@@ -833,20 +778,16 @@
obtains "B a b c" | "a \<notin> A"
using assms by auto
-lemma Sup1_I:
- "P \<in> A \<Longrightarrow> P a \<Longrightarrow> (\<Squnion>A) a"
+lemma Sup1_I: "P \<in> A \<Longrightarrow> P a \<Longrightarrow> (\<Squnion>A) a"
by auto
-lemma SUP1_I:
- "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
+lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
by auto
-lemma Sup2_I:
- "r \<in> A \<Longrightarrow> r a b \<Longrightarrow> (\<Squnion>A) a b"
+lemma Sup2_I: "r \<in> A \<Longrightarrow> r a b \<Longrightarrow> (\<Squnion>A) a b"
by auto
-lemma SUP2_I:
- "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
+lemma SUP2_I: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
by auto
lemma Sup1_E:
@@ -875,29 +816,25 @@
instantiation "set" :: (type) complete_lattice
begin
-definition
- "\<Sqinter>A = {x. \<Sqinter>((\<lambda>B. x \<in> B) ` A)}"
+definition "\<Sqinter>A = {x. \<Sqinter>((\<lambda>B. x \<in> B) ` A)}"
-definition
- "\<Squnion>A = {x. \<Squnion>((\<lambda>B. x \<in> B) ` A)}"
+definition "\<Squnion>A = {x. \<Squnion>((\<lambda>B. x \<in> B) ` A)}"
-instance proof
-qed (auto simp add: less_eq_set_def Inf_set_def Sup_set_def le_fun_def)
+instance
+ by standard (auto simp add: less_eq_set_def Inf_set_def Sup_set_def le_fun_def)
end
instance "set" :: (type) complete_boolean_algebra
-proof
-qed (auto simp add: Inf_set_def Sup_set_def image_def)
-
+ by standard (auto simp add: Inf_set_def Sup_set_def image_def)
+
subsubsection \<open>Inter\<close>
abbreviation Inter :: "'a set set \<Rightarrow> 'a set" ("\<Inter>_" [900] 900)
where "\<Inter>S \<equiv> \<Sqinter>S"
-
-lemma Inter_eq:
- "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
+
+lemma Inter_eq: "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
proof (rule set_eqI)
fix x
have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
@@ -913,7 +850,7 @@
by (simp add: Inter_eq)
text \<open>
- \medskip A ``destruct'' rule -- every @{term X} in @{term C}
+ \<^medskip> A ``destruct'' rule -- every @{term X} in @{term C}
contains @{term A} as an element, but @{prop "A \<in> X"} can hold when
@{prop "X \<in> C"} does not! This rule is analogous to \<open>spec\<close>.
\<close>
@@ -924,13 +861,12 @@
lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R"
\<comment> \<open>``Classical'' elimination rule -- does not require proving
@{prop "X \<in> C"}.\<close>
- by (unfold Inter_eq) blast
+ unfolding Inter_eq by blast
lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B"
by (fact Inf_lower)
-lemma Inter_subset:
- "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
+lemma Inter_subset: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
by (fact Inf_less_eq)
lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> \<Inter>A"
@@ -992,8 +928,7 @@
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
-lemma INTER_eq:
- "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
+lemma INTER_eq: "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
by (auto intro!: INF_eqI)
lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
@@ -1036,23 +971,21 @@
lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
by (fact INF_union)
-lemma INT_insert_distrib:
- "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
+lemma INT_insert_distrib: "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
by blast
lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
by (fact INF_constant)
lemma INTER_UNIV_conv:
- "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
- "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
+ "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
+ "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
by (fact INF_top_conv)+ (* already simp *)
lemma INT_bool_eq: "(\<Inter>b. A b) = A True \<inter> A False"
by (fact INF_UNIV_bool_expand)
-lemma INT_anti_mono:
- "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
+lemma INT_anti_mono: "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
\<comment> \<open>The last inclusion is POSITIVE!\<close>
by (fact INF_superset_mono)
@@ -1068,8 +1001,7 @@
abbreviation Union :: "'a set set \<Rightarrow> 'a set" ("\<Union>_" [900] 900)
where "\<Union>S \<equiv> \<Squnion>S"
-lemma Union_eq:
- "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
+lemma Union_eq: "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
proof (rule set_eqI)
fix x
have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
@@ -1078,18 +1010,15 @@
by (simp add: Sup_set_def image_def)
qed
-lemma Union_iff [simp]:
- "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
+lemma Union_iff [simp]: "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
by (unfold Union_eq) blast
-lemma UnionI [intro]:
- "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
+lemma UnionI [intro]: "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
\<comment> \<open>The order of the premises presupposes that @{term C} is rigid;
@{term A} may be flexible.\<close>
by auto
-lemma UnionE [elim!]:
- "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A \<in> X \<Longrightarrow> X \<in> C \<Longrightarrow> R) \<Longrightarrow> R"
+lemma UnionE [elim!]: "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A \<in> X \<Longrightarrow> X \<in> C \<Longrightarrow> R) \<Longrightarrow> R"
by auto
lemma Union_upper: "B \<in> A \<Longrightarrow> B \<subseteq> \<Union>A"
@@ -1131,6 +1060,7 @@
lemma Union_subsetI: "(\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> B \<and> x \<subseteq> y) \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
by blast
+
subsubsection \<open>Unions of families\<close>
abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
@@ -1169,16 +1099,13 @@
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
-lemma UNION_eq:
- "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
+lemma UNION_eq: "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
by (auto intro!: SUP_eqI)
-lemma bind_UNION [code]:
- "Set.bind A f = UNION A f"
+lemma bind_UNION [code]: "Set.bind A f = UNION A f"
by (simp add: bind_def UNION_eq)
-lemma member_bind [simp]:
- "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
+lemma member_bind [simp]: "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
by (simp add: bind_UNION)
lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
@@ -1281,6 +1208,7 @@
lemma inj_on_image: "inj_on f (\<Union>A) \<Longrightarrow> inj_on (op ` f) A"
unfolding inj_on_def by blast
+
subsubsection \<open>Distributive laws\<close>
lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
@@ -1298,10 +1226,10 @@
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)" \<comment> \<open>FIXME drop\<close>
+lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)" (* FIXME drop *)
by (simp add: INT_Int_distrib)
-lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)" \<comment> \<open>FIXME drop\<close>
+lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)" (* FIXME drop *)
\<comment> \<open>Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:\<close>
\<comment> \<open>Union of a family of unions\<close>
by (simp add: UN_Un_distrib)
@@ -1323,86 +1251,82 @@
by (fact Sup_inf_eq_bot_iff)
lemma SUP_UNION: "(SUP x:(UN y:A. g y). f x) = (SUP y:A. SUP x:g y. f x :: _ :: complete_lattice)"
-by(rule order_antisym)(blast intro: SUP_least SUP_upper2)+
+ by (rule order_antisym) (blast intro: SUP_least SUP_upper2)+
+
subsection \<open>Injections and bijections\<close>
-lemma inj_on_Inter:
- "S \<noteq> {} \<Longrightarrow> (\<And>A. A \<in> S \<Longrightarrow> inj_on f A) \<Longrightarrow> inj_on f (\<Inter>S)"
+lemma inj_on_Inter: "S \<noteq> {} \<Longrightarrow> (\<And>A. A \<in> S \<Longrightarrow> inj_on f A) \<Longrightarrow> inj_on f (\<Inter>S)"
unfolding inj_on_def by blast
-lemma inj_on_INTER:
- "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)) \<Longrightarrow> inj_on f (\<Inter>i \<in> I. A i)"
+lemma inj_on_INTER: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)) \<Longrightarrow> inj_on f (\<Inter>i \<in> I. A i)"
unfolding inj_on_def by safe simp
lemma inj_on_UNION_chain:
- assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
- INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
+ assumes chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i"
+ and inj: "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)"
shows "inj_on f (\<Union>i \<in> I. A i)"
proof -
- {
- fix i j x y
- assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
- and ***: "f x = f y"
- have "x = y"
- proof -
- {
- assume "A i \<le> A j"
- with ** have "x \<in> A j" by auto
- with INJ * ** *** have ?thesis
- by(auto simp add: inj_on_def)
- }
- moreover
- {
- assume "A j \<le> A i"
- with ** have "y \<in> A i" by auto
- with INJ * ** *** have ?thesis
- by(auto simp add: inj_on_def)
- }
- ultimately show ?thesis using CH * by blast
- qed
- }
- then show ?thesis by (unfold inj_on_def UNION_eq) auto
+ have "x = y"
+ if *: "i \<in> I" "j \<in> I"
+ and **: "x \<in> A i" "y \<in> A j"
+ and ***: "f x = f y"
+ for i j x y
+ using chain [OF *]
+ proof
+ assume "A i \<le> A j"
+ with ** have "x \<in> A j" by auto
+ with inj * ** *** show ?thesis
+ by (auto simp add: inj_on_def)
+ next
+ assume "A j \<le> A i"
+ with ** have "y \<in> A i" by auto
+ with inj * ** *** show ?thesis
+ by (auto simp add: inj_on_def)
+ qed
+ then show ?thesis
+ by (unfold inj_on_def UNION_eq) auto
qed
lemma bij_betw_UNION_chain:
- assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
- BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
+ assumes chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i"
+ and bij: "\<And>i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
-proof (unfold bij_betw_def, auto)
- have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
- using BIJ bij_betw_def[of f] by auto
- thus "inj_on f (\<Union>i \<in> I. A i)"
- using CH inj_on_UNION_chain[of I A f] by auto
+ unfolding bij_betw_def
+proof auto (* slow *)
+ have "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)"
+ using bij bij_betw_def[of f] by auto
+ then show "inj_on f (\<Union>i \<in> I. A i)"
+ using chain inj_on_UNION_chain[of I A f] by auto
next
fix i x
assume *: "i \<in> I" "x \<in> A i"
- hence "f x \<in> A' i" using BIJ bij_betw_def[of f] by auto
- thus "\<exists>j \<in> I. f x \<in> A' j" using * by blast
+ then have "f x \<in> A' i"
+ using bij bij_betw_def[of f] by auto
+ with * show "\<exists>j \<in> I. f x \<in> A' j" by blast
next
fix i x'
assume *: "i \<in> I" "x' \<in> A' i"
- hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
- then have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
- using * by blast
- then show "x' \<in> f ` (\<Union>x\<in>I. A x)" by blast
+ then have "\<exists>x \<in> A i. x' = f x"
+ using bij bij_betw_def[of f] by blast
+ with * have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
+ by blast
+ then show "x' \<in> f ` (\<Union>x\<in>I. A x)"
+ by blast
qed
(*injectivity's required. Left-to-right inclusion holds even if A is empty*)
-lemma image_INT:
- "[| inj_on f C; ALL x:A. B x <= C; j:A |]
- ==> f ` (INTER A B) = (INT x:A. f ` B x)"
- by (simp add: inj_on_def, auto) blast
+lemma image_INT: "inj_on f C \<Longrightarrow> \<forall>x\<in>A. B x \<subseteq> C \<Longrightarrow> j \<in> A \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)"
+ by (auto simp add: inj_on_def) blast
-lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"
- apply (simp add: bij_def)
- apply (simp add: inj_on_def surj_def)
+lemma bij_image_INT: "bij f \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)"
+ apply (simp only: bij_def)
+ apply (simp only: inj_on_def surj_def)
apply auto
apply blast
done
-lemma UNION_fun_upd:
- "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
+lemma UNION_fun_upd: "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
by (auto simp add: set_eq_iff)
lemma bij_betw_Pow:
@@ -1436,8 +1360,7 @@
subsubsection \<open>Miniscoping and maxiscoping\<close>
-text \<open>\medskip Miniscoping: pushing in quantifiers and big Unions
- and Intersections.\<close>
+text \<open>\<^medskip> Miniscoping: pushing in quantifiers and big Unions and Intersections.\<close>
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))"
@@ -1473,7 +1396,7 @@
by auto
-text \<open>\medskip Maxiscoping: pulling out big Unions and Intersections.\<close>
+text \<open>\<^medskip> Maxiscoping: pulling out big Unions and Intersections.\<close>
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)))"
@@ -1513,4 +1436,3 @@
\<comment> \<open>Each of these has ALREADY been added \<open>[simp]\<close> above.\<close>
end
-
--- a/src/HOL/Fun.thy Mon Aug 01 13:51:17 2016 +0200
+++ b/src/HOL/Fun.thy Mon Aug 01 22:11:29 2016 +0200
@@ -7,8 +7,8 @@
section \<open>Notions about functions\<close>
theory Fun
-imports Set
-keywords "functor" :: thy_goal
+ imports Set
+ keywords "functor" :: thy_goal
begin
lemma apply_inverse: "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
@@ -63,12 +63,10 @@
lemma comp_id [simp]: "f \<circ> id = f"
by (simp add: fun_eq_iff)
-lemma comp_eq_dest:
- "a \<circ> b = c \<circ> d \<Longrightarrow> a (b v) = c (d v)"
+lemma comp_eq_dest: "a \<circ> b = c \<circ> d \<Longrightarrow> a (b v) = c (d v)"
by (simp add: fun_eq_iff)
-lemma comp_eq_elim:
- "a \<circ> b = c \<circ> d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
+lemma comp_eq_elim: "a \<circ> b = c \<circ> d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
by (simp add: fun_eq_iff)
lemma comp_eq_dest_lhs: "a \<circ> b = c \<Longrightarrow> a (b v) = c v"
@@ -104,7 +102,7 @@
subsection \<open>The Forward Composition Operator \<open>fcomp\<close>\<close>
-definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
+definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
where "f \<circ>> g = (\<lambda>x. g (f x))"
lemma fcomp_apply [simp]: "(f \<circ>> g) x = g (f x)"
@@ -145,8 +143,10 @@
definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" \<comment> \<open>bijective\<close>
where "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
-text \<open>A common special case: functions injective, surjective or bijective over
- the entire domain type.\<close>
+text \<open>
+ A common special case: functions injective, surjective or bijective over
+ the entire domain type.
+\<close>
abbreviation "inj f \<equiv> inj_on f UNIV"
@@ -212,7 +212,7 @@
lemma inj_on_subset:
assumes "inj_on f A"
- assumes "B \<subseteq> A"
+ and "B \<subseteq> A"
shows "inj_on f B"
proof (rule inj_onI)
fix a b
@@ -296,7 +296,7 @@
by (simp add: surj_def)
lemma surjE: "surj f \<Longrightarrow> (\<And>x. y = f x \<Longrightarrow> C) \<Longrightarrow> C"
- by (simp add: surj_def, blast)
+ by (simp add: surj_def) blast
lemma comp_surj: "surj f \<Longrightarrow> surj g \<Longrightarrow> surj (g \<circ> f)"
by (simp add: image_comp [symmetric])
@@ -354,18 +354,19 @@
using img
proof (auto simp add: bij_betw_def)
assume "inj_on (f' \<circ> f) A"
- then show "inj_on f A" using inj_on_imageI2 by blast
+ then show "inj_on f A"
+ using inj_on_imageI2 by blast
next
fix a'
assume **: "a' \<in> A'"
- then have "f' a' \<in> A''" using bij unfolding bij_betw_def by auto
- then obtain a where 1: "a \<in> A \<and> f'(f a) = f' a'"
- using * unfolding bij_betw_def by force
- then have "f a \<in> A'" using img by auto
- then have "f a = a'"
- using bij ** 1 unfolding bij_betw_def inj_on_def by auto
- then show "a' \<in> f ` A"
- using 1 by auto
+ with bij have "f' a' \<in> A''"
+ unfolding bij_betw_def by auto
+ with * obtain a where 1: "a \<in> A \<and> f' (f a) = f' a'"
+ unfolding bij_betw_def by force
+ with img have "f a \<in> A'" by auto
+ with bij ** 1 have "f a = a'"
+ unfolding bij_betw_def inj_on_def by auto
+ with 1 show "a' \<in> f ` A" by auto
qed
qed
@@ -379,9 +380,10 @@
let ?g = "\<lambda>b. The (?P b)"
have g: "?g b = a" if P: "?P b a" for a b
proof -
- from that have ex1: "\<exists>a. ?P b a" using s by blast
+ from that s have ex1: "\<exists>a. ?P b a" by blast
then have uex1: "\<exists>!a. ?P b a" by (blast dest:inj_onD[OF i])
- then show ?thesis using the1_equality[OF uex1, OF P] P by simp
+ then show ?thesis
+ using the1_equality[OF uex1, OF P] P by simp
qed
have "inj_on ?g B"
proof (rule inj_onI)
@@ -396,15 +398,16 @@
fix b
assume "b \<in> B"
with s obtain a where P: "?P b a" by blast
- then show "?g b \<in> A" using g[OF P] by auto
+ with g[OF P] show "?g b \<in> A" by auto
next
fix a
assume "a \<in> A"
- then obtain b where P: "?P b a" using s by blast
- then have "b \<in> B" using s by blast
+ with s obtain b where P: "?P b a" by blast
+ with s have "b \<in> B" by blast
with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
qed
- ultimately show ?thesis by (auto simp: bij_betw_def)
+ ultimately show ?thesis
+ by (auto simp: bij_betw_def)
qed
lemma bij_betw_cong: "(\<And> a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
@@ -500,9 +503,7 @@
lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
\<comment> \<open>The inverse image of a singleton under an injective function is included in a singleton.\<close>
- apply (auto simp add: inj_on_def)
- apply (blast intro: the_equality [symmetric])
- done
+ by (simp add: inj_on_def) (blast intro: the_equality [symmetric])
lemma inj_on_vimage_singleton: "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}"
by (auto simp add: inj_on_def intro: the_equality [symmetric])
@@ -516,21 +517,21 @@
lemma bij_betw_byWitness:
assumes left: "\<forall>a \<in> A. f' (f a) = a"
and right: "\<forall>a' \<in> A'. f (f' a') = a'"
- and "f ` A \<le> A'"
- and img2: "f' ` A' \<le> A"
+ and "f ` A \<subseteq> A'"
+ and img2: "f' ` A' \<subseteq> A"
shows "bij_betw f A A'"
using assms
unfolding bij_betw_def inj_on_def
proof safe
fix a b
- assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
- have "a = f' (f a) \<and> b = f'(f b)" using * left by simp
- with ** show "a = b" by simp
+ assume "a \<in> A" "b \<in> A"
+ with left have "a = f' (f a) \<and> b = f' (f b)" by simp
+ moreover assume "f a = f b"
+ ultimately show "a = b" by simp
next
fix a' assume *: "a' \<in> A'"
- then have "f' a' \<in> A" using img2 by blast
- moreover
- have "a' = f (f' a')" using * right by simp
+ with img2 have "f' a' \<in> A" by blast
+ moreover from * right have "a' = f (f' a')" by simp
ultimately show "a' \<in> f ` A" by blast
qed
@@ -565,7 +566,8 @@
moreover
have False if "f a = f b"
proof -
- have "a = b" using * ** that unfolding bij_betw_def inj_on_def by blast
+ have "a = b"
+ using * ** that unfolding bij_betw_def inj_on_def by blast
with \<open>b \<notin> A\<close> ** show ?thesis by blast
qed
ultimately show "f a \<in> A'" by blast
@@ -611,9 +613,9 @@
lemma fun_upd_idem_iff: "f(x:=y) = f \<longleftrightarrow> f x = y"
unfolding fun_upd_def
apply safe
- apply (erule subst)
- apply (rule_tac [2] ext)
- apply auto
+ apply (erule subst)
+ apply (rule_tac [2] ext)
+ apply auto
done
lemma fun_upd_idem: "f x = y \<Longrightarrow> f(x := y) = f"
@@ -667,10 +669,10 @@
by (simp add:override_on_def)
lemma override_on_insert: "override_on f g (insert x X) = (override_on f g X)(x:=g x)"
-unfolding override_on_def by (simp add: fun_eq_iff)
+ unfolding override_on_def by (simp add: fun_eq_iff)
lemma override_on_insert': "override_on f g (insert x X) = (override_on (f(x:=g x)) g X)"
-unfolding override_on_def by (simp add: fun_eq_iff)
+ unfolding override_on_def by (simp add: fun_eq_iff)
subsection \<open>\<open>swap\<close>\<close>
@@ -691,7 +693,7 @@
by (simp add: fun_upd_def swap_def fun_eq_iff)
lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
- by (rule ext, simp add: fun_upd_def swap_def)
+ by (rule ext) (simp add: fun_upd_def swap_def)
lemma swap_comp_involutory [simp]: "swap a b \<circ> swap a b = id"
by (rule ext) simp
@@ -757,14 +759,14 @@
lemma f_the_inv_into_f: "inj_on f A \<Longrightarrow> y \<in> f ` A \<Longrightarrow> f (the_inv_into A f y) = y"
apply (simp add: the_inv_into_def)
apply (rule the1I2)
- apply(blast dest: inj_onD)
+ apply (blast dest: inj_onD)
apply blast
done
lemma the_inv_into_into: "inj_on f A \<Longrightarrow> x \<in> f ` A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> the_inv_into A f x \<in> B"
apply (simp add: the_inv_into_def)
apply (rule the1I2)
- apply(blast dest: inj_onD)
+ apply (blast dest: inj_onD)
apply blast
done
--- a/src/HOL/HOL.thy Mon Aug 01 13:51:17 2016 +0200
+++ b/src/HOL/HOL.thy Mon Aug 01 22:11:29 2016 +0200
@@ -218,20 +218,20 @@
by (rule trans [OF _ sym])
lemma meta_eq_to_obj_eq:
- assumes meq: "A \<equiv> B"
+ assumes "A \<equiv> B"
shows "A = B"
- by (unfold meq) (rule refl)
+ unfolding assms by (rule refl)
text \<open>Useful with \<open>erule\<close> for proving equalities from known equalities.\<close>
(* a = b
| |
c = d *)
lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d"
-apply (rule trans)
-apply (rule trans)
-apply (rule sym)
-apply assumption+
-done
+ apply (rule trans)
+ apply (rule trans)
+ apply (rule sym)
+ apply assumption+
+ done
text \<open>For calculational reasoning:\<close>
@@ -246,25 +246,25 @@
text \<open>Similar to \<open>AP_THM\<close> in Gordon's HOL.\<close>
lemma fun_cong: "(f :: 'a \<Rightarrow> 'b) = g \<Longrightarrow> f x = g x"
-apply (erule subst)
-apply (rule refl)
-done
+ apply (erule subst)
+ apply (rule refl)
+ done
text \<open>Similar to \<open>AP_TERM\<close> in Gordon's HOL and FOL's \<open>subst_context\<close>.\<close>
lemma arg_cong: "x = y \<Longrightarrow> f x = f y"
-apply (erule subst)
-apply (rule refl)
-done
+ apply (erule subst)
+ apply (rule refl)
+ done
lemma arg_cong2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> f a c = f b d"
-apply (erule ssubst)+
-apply (rule refl)
-done
+ apply (erule ssubst)+
+ apply (rule refl)
+ done
lemma cong: "\<lbrakk>f = g; (x::'a) = y\<rbrakk> \<Longrightarrow> f x = g y"
-apply (erule subst)+
-apply (rule refl)
-done
+ apply (erule subst)+
+ apply (rule refl)
+ done
ML \<open>fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong}\<close>
@@ -295,7 +295,7 @@
subsubsection \<open>True\<close>
-lemma TrueI: "True"
+lemma TrueI: True
unfolding True_def by (rule refl)
lemma eqTrueI: "P \<Longrightarrow> P = True"
@@ -307,14 +307,16 @@
subsubsection \<open>Universal quantifier\<close>
-lemma allI: assumes "\<And>x::'a. P x" shows "\<forall>x. P x"
+lemma allI:
+ assumes "\<And>x::'a. P x"
+ shows "\<forall>x. P x"
unfolding All_def by (iprover intro: ext eqTrueI assms)
lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x"
-apply (unfold All_def)
-apply (rule eqTrueE)
-apply (erule fun_cong)
-done
+ apply (unfold All_def)
+ apply (rule eqTrueE)
+ apply (erule fun_cong)
+ done
lemma allE:
assumes major: "\<forall>x. P x"
@@ -380,24 +382,24 @@
lemma impE:
assumes "P \<longrightarrow> Q" P "Q \<Longrightarrow> R"
shows R
-by (iprover intro: assms mp)
+ by (iprover intro: assms mp)
-(* Reduces Q to P \<longrightarrow> Q, allowing substitution in P. *)
+text \<open>Reduces \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, allowing substitution in \<open>P\<close>.\<close>
lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-by (iprover intro: mp)
+ by (iprover intro: mp)
lemma contrapos_nn:
assumes major: "\<not> Q"
- and minor: "P \<Longrightarrow> Q"
+ and minor: "P \<Longrightarrow> Q"
shows "\<not> P"
-by (iprover intro: notI minor major [THEN notE])
+ by (iprover intro: notI minor major [THEN notE])
-(*not used at all, but we already have the other 3 combinations *)
+text \<open>Not used at all, but we already have the other 3 combinations.\<close>
lemma contrapos_pn:
assumes major: "Q"
- and minor: "P \<Longrightarrow> \<not> Q"
+ and minor: "P \<Longrightarrow> \<not> Q"
shows "\<not> P"
-by (iprover intro: notI minor major notE)
+ by (iprover intro: notI minor major notE)
lemma not_sym: "t \<noteq> s \<Longrightarrow> s \<noteq> t"
by (erule contrapos_nn) (erule sym)
@@ -409,69 +411,56 @@
subsubsection \<open>Existential quantifier\<close>
lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x"
-apply (unfold Ex_def)
-apply (iprover intro: allI allE impI mp)
-done
+ unfolding Ex_def by (iprover intro: allI allE impI mp)
lemma exE:
assumes major: "\<exists>x::'a. P x"
- and minor: "\<And>x. P x \<Longrightarrow> Q"
+ and minor: "\<And>x. P x \<Longrightarrow> Q"
shows "Q"
-apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
-apply (iprover intro: impI [THEN allI] minor)
-done
+ by (rule major [unfolded Ex_def, THEN spec, THEN mp]) (iprover intro: impI [THEN allI] minor)
subsubsection \<open>Conjunction\<close>
lemma conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"
-apply (unfold and_def)
-apply (iprover intro: impI [THEN allI] mp)
-done
+ unfolding and_def by (iprover intro: impI [THEN allI] mp)
lemma conjunct1: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> P"
-apply (unfold and_def)
-apply (iprover intro: impI dest: spec mp)
-done
+ unfolding and_def by (iprover intro: impI dest: spec mp)
lemma conjunct2: "\<lbrakk>P \<and> Q\<rbrakk> \<Longrightarrow> Q"
-apply (unfold and_def)
-apply (iprover intro: impI dest: spec mp)
-done
+ unfolding and_def by (iprover intro: impI dest: spec mp)
lemma conjE:
assumes major: "P \<and> Q"
- and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
+ and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
shows R
-apply (rule minor)
-apply (rule major [THEN conjunct1])
-apply (rule major [THEN conjunct2])
-done
+ apply (rule minor)
+ apply (rule major [THEN conjunct1])
+ apply (rule major [THEN conjunct2])
+ done
lemma context_conjI:
- assumes P "P \<Longrightarrow> Q" shows "P \<and> Q"
-by (iprover intro: conjI assms)
+ assumes P "P \<Longrightarrow> Q"
+ shows "P \<and> Q"
+ by (iprover intro: conjI assms)
subsubsection \<open>Disjunction\<close>
lemma disjI1: "P \<Longrightarrow> P \<or> Q"
-apply (unfold or_def)
-apply (iprover intro: allI impI mp)
-done
+ unfolding or_def by (iprover intro: allI impI mp)
lemma disjI2: "Q \<Longrightarrow> P \<or> Q"
-apply (unfold or_def)
-apply (iprover intro: allI impI mp)
-done
+ unfolding or_def by (iprover intro: allI impI mp)
lemma disjE:
assumes major: "P \<or> Q"
- and minorP: "P \<Longrightarrow> R"
- and minorQ: "Q \<Longrightarrow> R"
+ and minorP: "P \<Longrightarrow> R"
+ and minorQ: "Q \<Longrightarrow> R"
shows R
-by (iprover intro: minorP minorQ impI
- major [unfolded or_def, THEN spec, THEN mp, THEN mp])
+ by (iprover intro: minorP minorQ impI
+ major [unfolded or_def, THEN spec, THEN mp, THEN mp])
subsubsection \<open>Classical logic\<close>
@@ -479,37 +468,37 @@
lemma classical:
assumes prem: "\<not> P \<Longrightarrow> P"
shows P
-apply (rule True_or_False [THEN disjE, THEN eqTrueE])
-apply assumption
-apply (rule notI [THEN prem, THEN eqTrueI])
-apply (erule subst)
-apply assumption
-done
+ apply (rule True_or_False [THEN disjE, THEN eqTrueE])
+ apply assumption
+ apply (rule notI [THEN prem, THEN eqTrueI])
+ apply (erule subst)
+ apply assumption
+ done
lemmas ccontr = FalseE [THEN classical]
-(*notE with premises exchanged; it discharges \<not> R so that it can be used to
- make elimination rules*)
+text \<open>\<open>notE\<close> with premises exchanged; it discharges \<open>\<not> R\<close> so that it can be used to
+ make elimination rules.\<close>
lemma rev_notE:
assumes premp: P
- and premnot: "\<not> R \<Longrightarrow> \<not> P"
+ and premnot: "\<not> R \<Longrightarrow> \<not> P"
shows R
-apply (rule ccontr)
-apply (erule notE [OF premnot premp])
-done
+ apply (rule ccontr)
+ apply (erule notE [OF premnot premp])
+ done
-(*Double negation law*)
+text \<open>Double negation law.\<close>
lemma notnotD: "\<not>\<not> P \<Longrightarrow> P"
-apply (rule classical)
-apply (erule notE)
-apply assumption
-done
+ apply (rule classical)
+ apply (erule notE)
+ apply assumption
+ done
lemma contrapos_pp:
assumes p1: Q
- and p2: "\<not> P \<Longrightarrow> \<not> Q"
+ and p2: "\<not> P \<Longrightarrow> \<not> Q"
shows P
-by (iprover intro: classical p1 p2 notE)
+ by (iprover intro: classical p1 p2 notE)
subsubsection \<open>Unique existence\<close>
@@ -517,90 +506,87 @@
lemma ex1I:
assumes "P a" "\<And>x. P x \<Longrightarrow> x = a"
shows "\<exists>!x. P x"
-by (unfold Ex1_def, iprover intro: assms exI conjI allI impI)
+ unfolding Ex1_def by (iprover intro: assms exI conjI allI impI)
-text\<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close>
+text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close>
lemma ex_ex1I:
assumes ex_prem: "\<exists>x. P x"
- and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y"
+ and eq: "\<And>x y. \<lbrakk>P x; P y\<rbrakk> \<Longrightarrow> x = y"
shows "\<exists>!x. P x"
-by (iprover intro: ex_prem [THEN exE] ex1I eq)
+ by (iprover intro: ex_prem [THEN exE] ex1I eq)
lemma ex1E:
assumes major: "\<exists>!x. P x"
- and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R"
+ and minor: "\<And>x. \<lbrakk>P x; \<forall>y. P y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R"
shows R
-apply (rule major [unfolded Ex1_def, THEN exE])
-apply (erule conjE)
-apply (iprover intro: minor)
-done
+ apply (rule major [unfolded Ex1_def, THEN exE])
+ apply (erule conjE)
+ apply (iprover intro: minor)
+ done
lemma ex1_implies_ex: "\<exists>!x. P x \<Longrightarrow> \<exists>x. P x"
-apply (erule ex1E)
-apply (rule exI)
-apply assumption
-done
+ apply (erule ex1E)
+ apply (rule exI)
+ apply assumption
+ done
subsubsection \<open>Classical intro rules for disjunction and existential quantifiers\<close>
lemma disjCI:
- assumes "\<not> Q \<Longrightarrow> P" shows "P \<or> Q"
-apply (rule classical)
-apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
-done
+ assumes "\<not> Q \<Longrightarrow> P"
+ shows "P \<or> Q"
+ by (rule classical) (iprover intro: assms disjI1 disjI2 notI elim: notE)
lemma excluded_middle: "\<not> P \<or> P"
-by (iprover intro: disjCI)
+ by (iprover intro: disjCI)
text \<open>
case distinction as a natural deduction rule.
- Note that @{term "\<not> P"} is the second case, not the first
+ Note that \<open>\<not> P\<close> is the second case, not the first.
\<close>
lemma case_split [case_names True False]:
assumes prem1: "P \<Longrightarrow> Q"
- and prem2: "\<not> P \<Longrightarrow> Q"
+ and prem2: "\<not> P \<Longrightarrow> Q"
shows Q
-apply (rule excluded_middle [THEN disjE])
-apply (erule prem2)
-apply (erule prem1)
-done
+ apply (rule excluded_middle [THEN disjE])
+ apply (erule prem2)
+ apply (erule prem1)
+ done
-(*Classical implies (\<longrightarrow>) elimination. *)
+text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
lemma impCE:
assumes major: "P \<longrightarrow> Q"
- and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R"
+ and minor: "\<not> P \<Longrightarrow> R" "Q \<Longrightarrow> R"
shows R
-apply (rule excluded_middle [of P, THEN disjE])
-apply (iprover intro: minor major [THEN mp])+
-done
+ apply (rule excluded_middle [of P, THEN disjE])
+ apply (iprover intro: minor major [THEN mp])+
+ done
-(*This version of \<longrightarrow> elimination works on Q before P. It works best for
- those cases in which P holds "almost everywhere". Can't install as
- default: would break old proofs.*)
+text \<open>
+ This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>. It works best for
+ those cases in which \<open>P\<close> holds "almost everywhere". Can't install as
+ default: would break old proofs.
+\<close>
lemma impCE':
assumes major: "P \<longrightarrow> Q"
- and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R"
+ and minor: "Q \<Longrightarrow> R" "\<not> P \<Longrightarrow> R"
shows R
-apply (rule excluded_middle [of P, THEN disjE])
-apply (iprover intro: minor major [THEN mp])+
-done
+ apply (rule excluded_middle [of P, THEN disjE])
+ apply (iprover intro: minor major [THEN mp])+
+ done
-(*Classical <-> elimination. *)
+text \<open>Classical \<open>\<longleftrightarrow>\<close> elimination.\<close>
lemma iffCE:
assumes major: "P = Q"
- and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
+ and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
shows R
-apply (rule major [THEN iffE])
-apply (iprover intro: minor elim: impCE notE)
-done
+ by (rule major [THEN iffE]) (iprover intro: minor elim: impCE notE)
lemma exCI:
assumes "\<forall>x. \<not> P x \<Longrightarrow> P a"
shows "\<exists>x. P x"
-apply (rule ccontr)
-apply (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
-done
+ by (rule ccontr) (iprover intro: assms exI allI notI notE [of "\<exists>x. P x"])
subsubsection \<open>Intuitionistic Reasoning\<close>
@@ -650,7 +636,7 @@
subsubsection \<open>Atomizing meta-level connectives\<close>
axiomatization where
- eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" (*admissible axiom*)
+ eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" \<comment> \<open>admissible axiom\<close>
lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
proof
@@ -731,9 +717,9 @@
subsubsection \<open>Sledgehammer setup\<close>
text \<open>
-Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
-that are prolific (match too many equality or membership literals) and relate to
-seldom-used facts. Some duplicate other rules.
+ Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
+ that are prolific (match too many equality or membership literals) and relate to
+ seldom-used facts. Some duplicate other rules.
\<close>
named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
@@ -830,18 +816,18 @@
lemmas [intro?] = ext
and [elim?] = ex1_implies_ex
-(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
+text \<open>Better than \<open>ex1E\<close> for classical reasoner: needs no quantifier duplication!\<close>
lemma alt_ex1E [elim!]:
assumes major: "\<exists>!x. P x"
- and prem: "\<And>x. \<lbrakk> P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y' \<rbrakk> \<Longrightarrow> R"
+ and prem: "\<And>x. \<lbrakk>P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
shows R
-apply (rule ex1E [OF major])
-apply (rule prem)
-apply assumption
-apply (rule allI)+
-apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>)
-apply iprover
-done
+ apply (rule ex1E [OF major])
+ apply (rule prem)
+ apply assumption
+ apply (rule allI)+
+ apply (tactic \<open>eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1\<close>)
+ apply iprover
+ done
ML \<open>
structure Blast = Blast
@@ -862,27 +848,29 @@
lemma the_equality [intro]:
assumes "P a"
- and "\<And>x. P x \<Longrightarrow> x = a"
+ and "\<And>x. P x \<Longrightarrow> x = a"
shows "(THE x. P x) = a"
by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial])
lemma theI:
- assumes "P a" and "\<And>x. P x \<Longrightarrow> x = a"
+ assumes "P a"
+ and "\<And>x. P x \<Longrightarrow> x = a"
shows "P (THE x. P x)"
-by (iprover intro: assms the_equality [THEN ssubst])
+ by (iprover intro: assms the_equality [THEN ssubst])
lemma theI': "\<exists>!x. P x \<Longrightarrow> P (THE x. P x)"
by (blast intro: theI)
-(*Easier to apply than theI: only one occurrence of P*)
+text \<open>Easier to apply than \<open>theI\<close>: only one occurrence of \<open>P\<close>.\<close>
lemma theI2:
assumes "P a" "\<And>x. P x \<Longrightarrow> x = a" "\<And>x. P x \<Longrightarrow> Q x"
shows "Q (THE x. P x)"
-by (iprover intro: assms theI)
+ by (iprover intro: assms theI)
-lemma the1I2: assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
-by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
- elim:allE impE)
+lemma the1I2:
+ assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
+ shows "Q (THE x. P x)"
+ by (iprover intro: assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] elim: allE impE)
lemma the1_equality [elim?]: "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> (THE x. P x) = a"
by blast
@@ -929,136 +917,136 @@
"\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t"
by (blast, blast, blast, blast, blast, iprover+)
-lemma disj_absorb: "(A \<or> A) = A"
+lemma disj_absorb: "A \<or> A \<longleftrightarrow> A"
by blast
-lemma disj_left_absorb: "(A \<or> (A \<or> B)) = (A \<or> B)"
+lemma disj_left_absorb: "A \<or> (A \<or> B) \<longleftrightarrow> A \<or> B"
by blast
-lemma conj_absorb: "(A \<and> A) = A"
+lemma conj_absorb: "A \<and> A \<longleftrightarrow> A"
by blast
-lemma conj_left_absorb: "(A \<and> (A \<and> B)) = (A \<and> B)"
+lemma conj_left_absorb: "A \<and> (A \<and> B) \<longleftrightarrow> A \<and> B"
by blast
lemma eq_ac:
shows eq_commute: "a = b \<longleftrightarrow> b = a"
and iff_left_commute: "(P \<longleftrightarrow> (Q \<longleftrightarrow> R)) \<longleftrightarrow> (Q \<longleftrightarrow> (P \<longleftrightarrow> R))"
- and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))" by (iprover, blast+)
+ and iff_assoc: "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
+ by (iprover, blast+)
+
lemma neq_commute: "a \<noteq> b \<longleftrightarrow> b \<noteq> a" by iprover
lemma conj_comms:
- shows conj_commute: "(P \<and> Q) = (Q \<and> P)"
- and conj_left_commute: "(P \<and> (Q \<and> R)) = (Q \<and> (P \<and> R))" by iprover+
-lemma conj_assoc: "((P \<and> Q) \<and> R) = (P \<and> (Q \<and> R))" by iprover
+ shows conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P"
+ and conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover+
+lemma conj_assoc: "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)" by iprover
lemmas conj_ac = conj_commute conj_left_commute conj_assoc
lemma disj_comms:
- shows disj_commute: "(P \<or> Q) = (Q \<or> P)"
- and disj_left_commute: "(P \<or> (Q \<or> R)) = (Q \<or> (P \<or> R))" by iprover+
-lemma disj_assoc: "((P \<or> Q) \<or> R) = (P \<or> (Q \<or> R))" by iprover
+ shows disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P"
+ and disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover+
+lemma disj_assoc: "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)" by iprover
lemmas disj_ac = disj_commute disj_left_commute disj_assoc
-lemma conj_disj_distribL: "(P \<and> (Q \<or> R)) = (P \<and> Q \<or> P \<and> R)" by iprover
-lemma conj_disj_distribR: "((P \<or> Q) \<and> R) = (P \<and> R \<or> Q \<and> R)" by iprover
+lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R" by iprover
+lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> P \<and> R \<or> Q \<and> R" by iprover
-lemma disj_conj_distribL: "(P \<or> (Q \<and> R)) = ((P \<or> Q) \<and> (P \<or> R))" by iprover
-lemma disj_conj_distribR: "((P \<and> Q) \<or> R) = ((P \<or> R) \<and> (Q \<or> R))" by iprover
+lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover
+lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover
lemma imp_conjR: "(P \<longrightarrow> (Q \<and> R)) = ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))" by iprover
lemma imp_conjL: "((P \<and> Q) \<longrightarrow> R) = (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover
lemma imp_disjL: "((P \<or> Q) \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" by iprover
text \<open>These two are specialized, but \<open>imp_disj_not1\<close> is useful in \<open>Auth/Yahalom\<close>.\<close>
-lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) = (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
-lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) = (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
+lemma imp_disj_not1: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> Q \<longrightarrow> P \<longrightarrow> R)" by blast
+lemma imp_disj_not2: "(P \<longrightarrow> Q \<or> R) \<longleftrightarrow> (\<not> R \<longrightarrow> P \<longrightarrow> Q)" by blast
-lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) = (P \<longrightarrow> Q \<or> R)" by blast
-lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) = (P \<longrightarrow> Q \<or> R)" by blast
+lemma imp_disj1: "((P \<longrightarrow> Q) \<or> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
+lemma imp_disj2: "(Q \<or> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
-lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) = (P' \<longrightarrow> Q'))"
+lemma imp_cong: "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q'))"
by iprover
-lemma de_Morgan_disj: "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)" by iprover
-lemma de_Morgan_conj: "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)" by blast
-lemma not_imp: "(\<not> (P \<longrightarrow> Q)) = (P \<and> \<not> Q)" by blast
-lemma not_iff: "(P \<noteq> Q) = (P = (\<not> Q))" by blast
-lemma disj_not1: "(\<not> P \<or> Q) = (P \<longrightarrow> Q)" by blast
-lemma disj_not2: "(P \<or> \<not> Q) = (Q \<longrightarrow> P)" \<comment> \<open>changes orientation :-(\<close>
- by blast
-lemma imp_conv_disj: "(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" by blast
+lemma de_Morgan_disj: "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q" by iprover
+lemma de_Morgan_conj: "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q" by blast
+lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> P \<and> \<not> Q" by blast
+lemma not_iff: "P \<noteq> Q \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
+lemma disj_not1: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)" by blast
+lemma disj_not2: "P \<or> \<not> Q \<longleftrightarrow> (Q \<longrightarrow> P)" by blast \<comment> \<open>changes orientation :-(\<close>
+lemma imp_conv_disj: "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P) \<or> Q" by blast
lemma disj_imp: "P \<or> Q \<longleftrightarrow> \<not> P \<longrightarrow> Q" by blast
-lemma iff_conv_conj_imp: "(P = Q) = ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))" by iprover
+lemma iff_conv_conj_imp: "(P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)" by iprover
-lemma cases_simp: "((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q)) = Q"
+lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
\<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close>
\<comment> \<open>cases boil down to the same thing.\<close>
by blast
-lemma not_all: "(\<not> (\<forall>x. P x)) = (\<exists>x. \<not> P x)" by blast
-lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) = (\<exists>x. P x \<longrightarrow> Q)" by blast
-lemma not_ex: "(\<not> (\<exists>x. P x)) = (\<forall>x. \<not> P x)" by iprover
-lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) = (\<forall>x. P x \<longrightarrow> Q)" by iprover
-lemma all_not_ex: "(\<forall>x. P x) = (\<not> (\<exists>x. \<not> P x ))" by blast
+lemma not_all: "\<not> (\<forall>x. P x) \<longleftrightarrow> (\<exists>x. \<not> P x)" by blast
+lemma imp_all: "((\<forall>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P x \<longrightarrow> Q)" by blast
+lemma not_ex: "\<not> (\<exists>x. P x) \<longleftrightarrow> (\<forall>x. \<not> P x)" by iprover
+lemma imp_ex: "((\<exists>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q)" by iprover
+lemma all_not_ex: "(\<forall>x. P x) \<longleftrightarrow> \<not> (\<exists>x. \<not> P x)" by blast
declare All_def [no_atp]
-lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) = ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by iprover
-lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) = ((\<forall>x. P x) \<and> (\<forall>x. Q x))" by iprover
+lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" by iprover
+lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" by iprover
text \<open>
- \medskip The \<open>\<and>\<close> congruence rule: not included by default!
+ \<^medskip> The \<open>\<and>\<close> congruence rule: not included by default!
May slow rewrite proofs down by as much as 50\%\<close>
-lemma conj_cong:
- "(P = P') \<Longrightarrow> (P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))"
+lemma conj_cong: "P = P' \<Longrightarrow> (P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
by iprover
-lemma rev_conj_cong:
- "(Q = Q') \<Longrightarrow> (Q' \<Longrightarrow> (P = P')) \<Longrightarrow> ((P \<and> Q) = (P' \<and> Q'))"
+lemma rev_conj_cong: "Q = Q' \<Longrightarrow> (Q' \<Longrightarrow> P = P') \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')"
by iprover
text \<open>The \<open>|\<close> congruence rule: not included by default!\<close>
-lemma disj_cong:
- "(P = P') \<Longrightarrow> (\<not> P' \<Longrightarrow> (Q = Q')) \<Longrightarrow> ((P \<or> Q) = (P' \<or> Q'))"
+lemma disj_cong: "P = P' \<Longrightarrow> (\<not> P' \<Longrightarrow> Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
by blast
-text \<open>\medskip if-then-else rules\<close>
+text \<open>\<^medskip> if-then-else rules\<close>
lemma if_True [code]: "(if True then x else y) = x"
- by (unfold If_def) blast
+ unfolding If_def by blast
lemma if_False [code]: "(if False then x else y) = y"
- by (unfold If_def) blast
+ unfolding If_def by blast
lemma if_P: "P \<Longrightarrow> (if P then x else y) = x"
- by (unfold If_def) blast
+ unfolding If_def by blast
lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y"
- by (unfold If_def) blast
+ unfolding If_def by blast
lemma if_split: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))"
apply (rule case_split [of Q])
apply (simplesubst if_P)
- prefer 3 apply (simplesubst if_not_P, blast+)
+ prefer 3
+ apply (simplesubst if_not_P)
+ apply blast+
done
lemma if_split_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))"
-by (simplesubst if_split, blast)
+ by (simplesubst if_split) blast
lemmas if_splits [no_atp] = if_split if_split_asm
lemma if_cancel: "(if c then x else x) = x"
-by (simplesubst if_split, blast)
+ by (simplesubst if_split) blast
lemma if_eq_cancel: "(if x = y then y else x) = x"
-by (simplesubst if_split, blast)
+ by (simplesubst if_split) blast
lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))"
\<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close>
@@ -1068,10 +1056,10 @@
\<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close>
by (simplesubst if_split) blast
-lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" by (unfold atomize_eq) iprover
-lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" by (unfold atomize_eq) iprover
+lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" unfolding atomize_eq by iprover
+lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" unfolding atomize_eq by iprover
-text \<open>\medskip let rules for simproc\<close>
+text \<open>\<^medskip> let rules for simproc\<close>
lemma Let_folded: "f x \<equiv> g x \<Longrightarrow> Let x f \<equiv> Let x g"
by (unfold Let_def)
@@ -1085,8 +1073,8 @@
its premise.
\<close>
-definition simp_implies :: "[prop, prop] \<Rightarrow> prop" (infixr "=simp=>" 1) where
- "simp_implies \<equiv> op \<Longrightarrow>"
+definition simp_implies :: "prop \<Rightarrow> prop \<Rightarrow> prop" (infixr "=simp=>" 1)
+ where "simp_implies \<equiv> op \<Longrightarrow>"
lemma simp_impliesI:
assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
@@ -1098,8 +1086,8 @@
lemma simp_impliesE:
assumes PQ: "PROP P =simp=> PROP Q"
- and P: "PROP P"
- and QR: "PROP Q \<Longrightarrow> PROP R"
+ and P: "PROP P"
+ and QR: "PROP Q \<Longrightarrow> PROP R"
shows "PROP R"
apply (rule QR)
apply (rule PQ [unfolded simp_implies_def])
@@ -1108,18 +1096,19 @@
lemma simp_implies_cong:
assumes PP' :"PROP P \<equiv> PROP P'"
- and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')"
+ and P'QQ': "PROP P' \<Longrightarrow> (PROP Q \<equiv> PROP Q')"
shows "(PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')"
-proof (unfold simp_implies_def, rule equal_intr_rule)
+ unfolding simp_implies_def
+proof (rule equal_intr_rule)
assume PQ: "PROP P \<Longrightarrow> PROP Q"
- and P': "PROP P'"
+ and P': "PROP P'"
from PP' [symmetric] and P' have "PROP P"
by (rule equal_elim_rule1)
then have "PROP Q" by (rule PQ)
with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1)
next
assume P'Q': "PROP P' \<Longrightarrow> PROP Q'"
- and P: "PROP P"
+ and P: "PROP P"
from PP' and P have P': "PROP P'" by (rule equal_elim_rule1)
then have "PROP Q'" by (rule P'Q')
with P'QQ' [OF P', symmetric] show "PROP Q"
@@ -1141,12 +1130,10 @@
shows "(\<exists>x. P x) = (\<exists>x. Q x)"
using assms by blast
-lemma all_comm:
- "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
+lemma all_comm: "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
by blast
-lemma ex_comm:
- "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
+lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
by blast
ML_file "Tools/simpdata.ML"
@@ -1163,79 +1150,80 @@
text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
simproc_setup neq ("x = y") = \<open>fn _ =>
-let
- val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
- fun is_neq eq lhs rhs thm =
- (case Thm.prop_of thm of
- _ $ (Not $ (eq' $ l' $ r')) =>
- Not = HOLogic.Not andalso eq' = eq andalso
- r' aconv lhs andalso l' aconv rhs
- | _ => false);
- fun proc ss ct =
- (case Thm.term_of ct of
- eq $ lhs $ rhs =>
- (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
- SOME thm => SOME (thm RS neq_to_EQ_False)
- | NONE => NONE)
- | _ => NONE);
-in proc end;
+ let
+ val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
+ fun is_neq eq lhs rhs thm =
+ (case Thm.prop_of thm of
+ _ $ (Not $ (eq' $ l' $ r')) =>
+ Not = HOLogic.Not andalso eq' = eq andalso
+ r' aconv lhs andalso l' aconv rhs
+ | _ => false);
+ fun proc ss ct =
+ (case Thm.term_of ct of
+ eq $ lhs $ rhs =>
+ (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of
+ SOME thm => SOME (thm RS neq_to_EQ_False)
+ | NONE => NONE)
+ | _ => NONE);
+ in proc end;
\<close>
simproc_setup let_simp ("Let x f") = \<open>
-let
- fun count_loose (Bound i) k = if i >= k then 1 else 0
- | count_loose (s $ t) k = count_loose s k + count_loose t k
- | count_loose (Abs (_, _, t)) k = count_loose t (k + 1)
- | count_loose _ _ = 0;
- fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
- (case t of
- Abs (_, _, t') => count_loose t' 0 <= 1
- | _ => true);
-in
- fn _ => fn ctxt => fn ct =>
- if is_trivial_let (Thm.term_of ct)
- then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
- else
- let (*Norbert Schirmer's case*)
- val t = Thm.term_of ct;
- val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
- in
- Option.map (hd o Variable.export ctxt' ctxt o single)
- (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
- if is_Free x orelse is_Bound x orelse is_Const x
- then SOME @{thm Let_def}
- else
- let
- val n = case f of (Abs (x, _, _)) => x | _ => "x";
- val cx = Thm.cterm_of ctxt x;
- val xT = Thm.typ_of_cterm cx;
- val cf = Thm.cterm_of ctxt f;
- val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
- val (_ $ _ $ g) = Thm.prop_of fx_g;
- val g' = abstract_over (x, g);
- val abs_g'= Abs (n, xT, g');
- in
- if g aconv g' then
- let
- val rl =
- infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
- in SOME (rl OF [fx_g]) end
- else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
- then NONE (*avoid identity conversion*)
- else
- let
- val g'x = abs_g' $ x;
- val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
- val rl =
- @{thm Let_folded} |> infer_instantiate ctxt
- [(("f", 0), Thm.cterm_of ctxt f),
- (("x", 0), cx),
- (("g", 0), Thm.cterm_of ctxt abs_g')];
- in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
- end
- | _ => NONE)
- end
-end\<close>
+ let
+ fun count_loose (Bound i) k = if i >= k then 1 else 0
+ | count_loose (s $ t) k = count_loose s k + count_loose t k
+ | count_loose (Abs (_, _, t)) k = count_loose t (k + 1)
+ | count_loose _ _ = 0;
+ fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
+ (case t of
+ Abs (_, _, t') => count_loose t' 0 <= 1
+ | _ => true);
+ in
+ fn _ => fn ctxt => fn ct =>
+ if is_trivial_let (Thm.term_of ct)
+ then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
+ else
+ let (*Norbert Schirmer's case*)
+ val t = Thm.term_of ct;
+ val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
+ in
+ Option.map (hd o Variable.export ctxt' ctxt o single)
+ (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
+ if is_Free x orelse is_Bound x orelse is_Const x
+ then SOME @{thm Let_def}
+ else
+ let
+ val n = case f of (Abs (x, _, _)) => x | _ => "x";
+ val cx = Thm.cterm_of ctxt x;
+ val xT = Thm.typ_of_cterm cx;
+ val cf = Thm.cterm_of ctxt f;
+ val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
+ val (_ $ _ $ g) = Thm.prop_of fx_g;
+ val g' = abstract_over (x, g);
+ val abs_g'= Abs (n, xT, g');
+ in
+ if g aconv g' then
+ let
+ val rl =
+ infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
+ in SOME (rl OF [fx_g]) end
+ else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
+ then NONE (*avoid identity conversion*)
+ else
+ let
+ val g'x = abs_g' $ x;
+ val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
+ val rl =
+ @{thm Let_folded} |> infer_instantiate ctxt
+ [(("f", 0), Thm.cterm_of ctxt f),
+ (("x", 0), cx),
+ (("g", 0), Thm.cterm_of ctxt abs_g')];
+ in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
+ end
+ | _ => NONE)
+ end
+ end
+\<close>
lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
proof
@@ -1254,9 +1242,10 @@
(* This is not made a simp rule because it does not improve any proofs
but slows some AFP entries down by 5% (cpu time). May 2015 *)
-lemma implies_False_swap: "NO_MATCH (Trueprop False) P \<Longrightarrow>
- (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
-by(rule swap_prems_eq)
+lemma implies_False_swap:
+ "NO_MATCH (Trueprop False) P \<Longrightarrow>
+ (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
+ by (rule swap_prems_eq)
lemma ex_simps:
"\<And>P Q. (\<exists>x. P x \<and> Q) = ((\<exists>x. P x) \<and> Q)"
@@ -1279,19 +1268,19 @@
by (iprover | blast)+
lemmas [simp] =
- triv_forall_equality (*prunes params*)
- True_implies_equals implies_True_equals (*prune True in asms*)
- False_implies_equals (*prune False in asms*)
+ triv_forall_equality \<comment> \<open>prunes params\<close>
+ True_implies_equals implies_True_equals \<comment> \<open>prune \<open>True\<close> in asms\<close>
+ False_implies_equals \<comment> \<open>prune \<open>False\<close> in asms\<close>
if_True
if_False
if_cancel
if_eq_cancel
- imp_disjL
- (*In general it seems wrong to add distributive laws by default: they
- might cause exponential blow-up. But imp_disjL has been in for a while
+ imp_disjL \<comment>
+ \<open>In general it seems wrong to add distributive laws by default: they
+ might cause exponential blow-up. But \<open>imp_disjL\<close> has been in for a while
and cannot be removed without affecting existing proofs. Moreover,
- rewriting by "(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))" might be justified on the
- grounds that it allows simplification of R in the two cases.*)
+ rewriting by \<open>(P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))\<close> might be justified on the
+ grounds that it allows simplification of \<open>R\<close> in the two cases.\<close>
conj_assoc
disj_assoc
de_Morgan_conj
@@ -1314,15 +1303,15 @@
ML \<open>val HOL_ss = simpset_of @{context}\<close>
-text \<open>Simplifies @{term x} assuming @{prop c} and @{term y} assuming @{prop "\<not> c"}\<close>
+text \<open>Simplifies \<open>x\<close> assuming \<open>c\<close> and \<open>y\<close> assuming \<open>\<not> c\<close>.\<close>
lemma if_cong:
assumes "b = c"
- and "c \<Longrightarrow> x = u"
- and "\<not> c \<Longrightarrow> y = v"
+ and "c \<Longrightarrow> x = u"
+ and "\<not> c \<Longrightarrow> y = v"
shows "(if b then x else y) = (if c then u else v)"
using assms by simp
-text \<open>Prevents simplification of x and y:
+text \<open>Prevents simplification of \<open>x\<close> and \<open>y\<close>:
faster and allows the execution of functional programs.\<close>
lemma if_weak_cong [cong]:
assumes "b = c"
@@ -1341,11 +1330,10 @@
shows "(t \<equiv> u) \<equiv> (t \<equiv> u')"
using assms by simp
-lemma if_distrib:
- "f (if c then x else y) = (if c then f x else f y)"
+lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)"
by simp
-text\<open>As a simplification rule, it replaces all function equalities by
+text \<open>As a simplification rule, it replaces all function equalities by
first-order equalities.\<close>
lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
by auto
@@ -1578,27 +1566,32 @@
lemma choice_eq: "(\<forall>x. \<exists>!y. P x y) = (\<exists>!f. \<forall>x. P x (f x))"
apply (rule iffI)
- apply (rule_tac a = "\<lambda>x. THE y. P x y" in ex1I)
- apply (fast dest!: theI')
- apply (fast intro: the1_equality [symmetric])
+ apply (rule_tac a = "\<lambda>x. THE y. P x y" in ex1I)
+ apply (fast dest!: theI')
+ apply (fast intro: the1_equality [symmetric])
apply (erule ex1E)
apply (rule allI)
apply (rule ex1I)
- apply (erule spec)
+ apply (erule spec)
apply (erule_tac x = "\<lambda>z. if z = x then y else f z" in allE)
apply (erule impE)
- apply (rule allI)
- apply (case_tac "xa = x")
- apply (drule_tac [3] x = x in fun_cong, simp_all)
+ apply (rule allI)
+ apply (case_tac "xa = x")
+ apply (drule_tac [3] x = x in fun_cong)
+ apply simp_all
done
lemmas eq_sym_conv = eq_commute
lemma nnf_simps:
- "(\<not>(P \<and> Q)) = (\<not> P \<or> \<not> Q)" "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
- "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
- "(\<not> \<not>(P)) = P"
-by blast+
+ "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)"
+ "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)"
+ "(P \<longrightarrow> Q) = (\<not> P \<or> Q)"
+ "(P = Q) = ((P \<and> Q) \<or> (\<not> P \<and> \<not> Q))"
+ "(\<not> (P = Q)) = ((P \<and> \<not> Q) \<or> (\<not> P \<and> Q))"
+ "(\<not> \<not> P) = P"
+ by blast+
+
subsection \<open>Basic ML bindings\<close>
@@ -1659,12 +1652,15 @@
section \<open>\<open>NO_MATCH\<close> simproc\<close>
text \<open>
- The simplification procedure can be used to avoid simplification of terms of a certain form
+ The simplification procedure can be used to avoid simplification of terms
+ of a certain form.
\<close>
-definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH pat val \<equiv> True"
+definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
+ where "NO_MATCH pat val \<equiv> True"
-lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val" by (rule refl)
+lemma NO_MATCH_cong[cong]: "NO_MATCH pat val = NO_MATCH pat val"
+ by (rule refl)
declare [[coercion_args NO_MATCH - -]]
@@ -1678,24 +1674,26 @@
text \<open>
This setup ensures that a rewrite rule of the form @{term "NO_MATCH pat val \<Longrightarrow> t"}
- is only applied, if the pattern @{term pat} does not match the value @{term val}.
+ is only applied, if the pattern \<open>pat\<close> does not match the value \<open>val\<close>.
\<close>
-text\<open>Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
-not to simplify the argument and to solve it by an assumption.\<close>
+text\<open>
+ Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
+ not to simplify the argument and to solve it by an assumption.
+\<close>
-definition ASSUMPTION :: "bool \<Rightarrow> bool" where
-"ASSUMPTION A \<equiv> A"
+definition ASSUMPTION :: "bool \<Rightarrow> bool"
+ where "ASSUMPTION A \<equiv> A"
lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
-by (rule refl)
+ by (rule refl)
lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
-by(simp add: ASSUMPTION_def)
+ by (simp add: ASSUMPTION_def)
lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
-by(simp add: ASSUMPTION_def)
+ by (simp add: ASSUMPTION_def)
setup \<open>
let
@@ -1712,12 +1710,10 @@
subsubsection \<open>Generic code generator preprocessor setup\<close>
-lemma conj_left_cong:
- "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
+lemma conj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<and> R \<longleftrightarrow> Q \<and> R"
by (fact arg_cong)
-lemma disj_left_cong:
- "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
+lemma disj_left_cong: "P \<longleftrightarrow> Q \<Longrightarrow> P \<or> R \<longleftrightarrow> Q \<or> R"
by (fact arg_cong)
setup \<open>
@@ -1772,29 +1768,32 @@
shows "False \<and> P \<longleftrightarrow> False"
and "True \<and> P \<longleftrightarrow> P"
and "P \<and> False \<longleftrightarrow> False"
- and "P \<and> True \<longleftrightarrow> P" by simp_all
+ and "P \<and> True \<longleftrightarrow> P"
+ by simp_all
lemma [code]:
shows "False \<or> P \<longleftrightarrow> P"
and "True \<or> P \<longleftrightarrow> True"
and "P \<or> False \<longleftrightarrow> P"
- and "P \<or> True \<longleftrightarrow> True" by simp_all
+ and "P \<or> True \<longleftrightarrow> True"
+ by simp_all
lemma [code]:
shows "(False \<longrightarrow> P) \<longleftrightarrow> True"
and "(True \<longrightarrow> P) \<longleftrightarrow> P"
and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
- and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
+ and "(P \<longrightarrow> True) \<longleftrightarrow> True"
+ by simp_all
text \<open>More about @{typ prop}\<close>
lemma [code nbe]:
shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
- and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
+ and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)"
+ by (auto intro!: equal_intr_rule)
-lemma Trueprop_code [code]:
- "Trueprop True \<equiv> Code_Generator.holds"
+lemma Trueprop_code [code]: "Trueprop True \<equiv> Code_Generator.holds"
by (auto intro!: equal_intr_rule holds)
declare Trueprop_code [symmetric, code_post]
@@ -1806,21 +1805,21 @@
instantiation itself :: (type) equal
begin
-definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
- "equal_itself x y \<longleftrightarrow> x = y"
+definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool"
+ where "equal_itself x y \<longleftrightarrow> x = y"
-instance proof
-qed (fact equal_itself_def)
+instance
+ by standard (fact equal_itself_def)
end
-lemma equal_itself_code [code]:
- "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
+lemma equal_itself_code [code]: "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
by (simp add: equal)
setup \<open>Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a::type \<Rightarrow> 'a \<Rightarrow> bool"})\<close>
-lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
+lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)"
+ (is "?ofclass \<equiv> ?equal")
proof
assume "PROP ?ofclass"
show "PROP ?equal"
@@ -1900,15 +1899,13 @@
code_module Pure \<rightharpoonup>
(SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
-text \<open>using built-in Haskell equality\<close>
-
+text \<open>Using built-in Haskell equality.\<close>
code_printing
type_class equal \<rightharpoonup> (Haskell) "Eq"
| constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
| constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
-text \<open>undefined\<close>
-
+text \<open>\<open>undefined\<close>\<close>
code_printing
constant undefined \<rightharpoonup>
(SML) "!(raise/ Fail/ \"undefined\")"
@@ -1956,7 +1953,7 @@
and nitpick_choice_spec "choice specification of constants as needed by Nitpick"
declare if_bool_eq_conj [nitpick_unfold, no_atp]
- if_bool_eq_disj [no_atp]
+ and if_bool_eq_disj [no_atp]
subsection \<open>Preprocessing for the predicate compiler\<close>
--- a/src/HOL/Product_Type.thy Mon Aug 01 13:51:17 2016 +0200
+++ b/src/HOL/Product_Type.thy Mon Aug 01 22:11:29 2016 +0200
@@ -6,8 +6,8 @@
section \<open>Cartesian products\<close>
theory Product_Type
-imports Typedef Inductive Fun
-keywords "inductive_set" "coinductive_set" :: thy_decl
+ imports Typedef Inductive Fun
+ keywords "inductive_set" "coinductive_set" :: thy_decl
begin
subsection \<open>@{typ bool} is a datatype\<close>
@@ -38,7 +38,7 @@
\<comment> "prefer plain propositional version"
lemma [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
- and [code]: "HOL.equal True P \<longleftrightarrow> P"
+ and [code]: "HOL.equal True P \<longleftrightarrow> P"
and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
and [code]: "HOL.equal P True \<longleftrightarrow> P"
and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
@@ -317,7 +317,7 @@
(case (head_of t) of
Const (@{const_syntax case_prod}, _) => raise Match
| _ =>
- let
+ let
val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
@@ -618,7 +618,7 @@
declare case_prodI2' [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
declare case_prodI2 [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
declare case_prodI [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close>
-
+
lemma mem_case_prodE [elim!]:
assumes "z \<in> case_prod c p"
obtains x y where "p = (x, y)" and "z \<in> c x y"
@@ -631,10 +631,10 @@
| exists_p_split (Abs (_, _, t)) = exists_p_split t
| exists_p_split _ = false;
in
-fun split_conv_tac ctxt = SUBGOAL (fn (t, i) =>
- if exists_p_split t
- then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms case_prod_conv}) i
- else no_tac);
+ fun split_conv_tac ctxt = SUBGOAL (fn (t, i) =>
+ if exists_p_split t
+ then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms case_prod_conv}) i
+ else no_tac);
end;
\<close>
@@ -656,7 +656,7 @@
a) only helps in special situations
b) can lead to nontermination in the presence of split_def
*)
-lemma split_comp_eq:
+lemma split_comp_eq:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
and g :: "'d \<Rightarrow> 'a"
shows "(\<lambda>u. f (g (fst u)) (snd u)) = case_prod (\<lambda>x. f (g x))"
@@ -836,7 +836,7 @@
apply (rule major [THEN imageE])
apply (case_tac x)
apply (rule cases)
- apply simp_all
+ apply simp_all
done
definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
@@ -845,10 +845,10 @@
definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
where "apsnd f = map_prod id f"
-lemma apfst_conv [simp, code]: "apfst f (x, y) = (f x, y)"
+lemma apfst_conv [simp, code]: "apfst f (x, y) = (f x, y)"
by (simp add: apfst_def)
-lemma apsnd_conv [simp, code]: "apsnd f (x, y) = (x, f y)"
+lemma apsnd_conv [simp, code]: "apsnd f (x, y) = (x, f y)"
by (simp add: apsnd_def)
lemma fst_apfst [simp]: "fst (apfst f x) = f (fst x)"
@@ -1029,11 +1029,11 @@
lemma Collect_case_prod_mono: "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
by auto (auto elim!: le_funE)
-lemma Collect_split_mono_strong:
+lemma Collect_split_mono_strong:
"X = fst ` A \<Longrightarrow> Y = snd ` A \<Longrightarrow> \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b
\<Longrightarrow> A \<subseteq> Collect (case_prod P) \<Longrightarrow> A \<subseteq> Collect (case_prod Q)"
by fastforce
-
+
lemma UN_Times_distrib: "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
\<comment> \<open>Suggested by Pierre Chartier\<close>
by blast
@@ -1151,18 +1151,19 @@
context
begin
-qualified definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
- [code_abbrev]: "product A B = A \<times> B"
+qualified definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"
+ where [code_abbrev]: "product A B = A \<times> B"
lemma member_product: "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B"
by (simp add: product_def)
end
-
+
text \<open>The following @{const map_prod} lemmas are due to Joachim Breitner:\<close>
lemma map_prod_inj_on:
- assumes "inj_on f A" and "inj_on g B"
+ assumes "inj_on f A"
+ and "inj_on g B"
shows "inj_on (map_prod f g) (A \<times> B)"
proof (rule inj_onI)
fix x :: "'a \<times> 'c"
--- a/src/HOL/Sum_Type.thy Mon Aug 01 13:51:17 2016 +0200
+++ b/src/HOL/Sum_Type.thy Mon Aug 01 22:11:29 2016 +0200
@@ -3,10 +3,10 @@
Copyright 1992 University of Cambridge
*)
-section\<open>The Disjoint Sum of Two Types\<close>
+section \<open>The Disjoint Sum of Two Types\<close>
theory Sum_Type
-imports Typedef Inductive Fun
+ imports Typedef Inductive Fun
begin
subsection \<open>Construction of the sum type and its basic abstract operations\<close>
@@ -85,7 +85,8 @@
proof (rule Abs_sum_cases [of s])
fix f
assume "s = Abs_sum f" and "f \<in> sum"
- with assms show P by (auto simp add: sum_def Inl_def Inr_def)
+ with assms show P
+ by (auto simp add: sum_def Inl_def Inr_def)
qed
free_constructors case_sum for
@@ -123,9 +124,9 @@
setup \<open>Sign.parent_path\<close>
primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
-where
- "map_sum f1 f2 (Inl a) = Inl (f1 a)"
-| "map_sum f1 f2 (Inr a) = Inr (f2 a)"
+ where
+ "map_sum f1 f2 (Inl a) = Inl (f1 a)"
+ | "map_sum f1 f2 (Inr a) = Inr (f2 a)"
functor map_sum: map_sum
proof -