# HG changeset patch
# User paulson
# Date 972311092 -7200
# Node ID 2ec9c808a8a73bcb100e625236d1074642849bf7
# Parent  354e885b3e0a107e2fc97210cf7300ef08437689
the Sets chapter and theories

diff -r 354e885b3e0a -r 2ec9c808a8a7 doc-src/TutorialI/Sets/Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Sets/Examples.thy	Mon Oct 23 16:24:52 2000 +0200
@@ -0,0 +1,278 @@
+theory Examples = Main:
+
+ML "reset eta_contract"
+ML "Pretty.setmargin 64"
+
+text{*membership, intersection *}
+text{*difference and empty set*}
+text{*complement, union and universal set*}
+
+lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] IntI[no_vars]}
+\rulename{IntI}
+
+@{thm[display] IntD1[no_vars]}
+\rulename{IntD1}
+
+@{thm[display] IntD2[no_vars]}
+\rulename{IntD2}
+*}
+
+lemma "(x \<in> -A) = (x \<notin> A)"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] Compl_iff[no_vars]}
+\rulename{Compl_iff}
+*}
+
+lemma "- (A \<union> B) = -A \<inter> -B"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] Compl_Un[no_vars]}
+\rulename{Compl_Un}
+*}
+
+lemma "A-A = {}"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] Diff_disjoint[no_vars]}
+\rulename{Diff_disjoint}
+*}
+
+  
+
+lemma "A \<union> -A = UNIV"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] Compl_partition[no_vars]}
+\rulename{Compl_partition}
+*}
+
+text{*subset relation*}
+
+
+text{*
+@{thm[display] subsetI[no_vars]}
+\rulename{subsetI}
+
+@{thm[display] subsetD[no_vars]}
+\rulename{subsetD}
+*}
+
+lemma "((A \<union> B) \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] Un_subset_iff[no_vars]}
+\rulename{Un_subset_iff}
+*}
+
+lemma "(A \<subseteq> -B) = (B \<subseteq> -A)"
+  apply (blast)
+  done
+
+lemma "(A <= -B) = (B <= -A)"
+  oops
+
+text{*ASCII version: blast fails because of overloading because
+ it doesn't have to be sets*}
+
+lemma "((A:: 'a set) <= -B) = (B <= -A)"
+  apply (blast)
+  done
+
+text{*A type constraint lets it work*}
+
+text{*An issue here: how do we discuss the distinction between ASCII and
+X-symbol notation?  Here the latter disambiguates.*}
+
+
+text{*
+set extensionality
+
+@{thm[display] set_ext[no_vars]}
+\rulename{set_ext}
+
+@{thm[display] equalityI[no_vars]}
+\rulename{equalityI}
+
+@{thm[display] equalityE[no_vars]}
+\rulename{equalityE}
+*}
+
+
+text{*finite sets: insertion and membership relation*}
+text{*finite set notation*}
+
+lemma "insert x A = {x} \<union> A"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] insert_is_Un[no_vars]}
+\rulename{insert_is_Un}
+*}
+
+lemma "{a,b} \<union> {c,d} = {a,b,c,d}"
+  apply (blast)
+  done
+
+lemma "{a,b} \<inter> {b,c} = {b}"
+  apply (auto)
+  oops
+text{*fails because it isn't valid*}
+
+lemma "{a,b} \<inter> {b,c} = (if a=c then {a,b} else {b})"
+  apply (simp)
+  apply (blast)
+  done
+
+text{*or just force or auto.  blast alone can't handle the if-then-else*}
+
+text{*next: some comprehension examples*}
+
+lemma "(a \<in> {z. P z}) = P a"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] mem_Collect_eq[no_vars]}
+\rulename{mem_Collect_eq}
+*}
+
+lemma "{x. x \<in> A} = A"
+  apply (blast)
+  done
+  
+text{*
+@{thm[display] Collect_mem_eq[no_vars]}
+\rulename{Collect_mem_eq}
+*}
+
+lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A"
+  apply (blast)
+  done
+
+lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"
+  apply (blast)
+  done
+
+constdefs
+  prime   :: "nat set"
+    "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
+
+lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} = 
+       {z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}"
+  apply (blast)
+  done
+
+text{*binders*}
+
+text{*bounded quantifiers*}
+
+lemma "(\<exists>x\<in>A. P x) = (\<exists>x. x\<in>A \<and> P x)"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] bexI[no_vars]}
+\rulename{bexI}
+*}
+
+text{*
+@{thm[display] bexE[no_vars]}
+\rulename{bexE}
+*}
+
+lemma "(\<forall>x\<in>A. P x) = (\<forall>x. x\<in>A \<longrightarrow> P x)"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] ballI[no_vars]}
+\rulename{ballI}
+*}
+
+text{*
+@{thm[display] bspec[no_vars]}
+\rulename{bspec}
+*}
+
+text{*indexed unions and variations*}
+
+lemma "(\<Union>x. B x) = (\<Union>x\<in>UNIV. B x)"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] UN_iff[no_vars]}
+\rulename{UN_iff}
+*}
+
+text{*
+@{thm[display] Union_iff[no_vars]}
+\rulename{Union_iff}
+*}
+
+lemma "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
+  apply (blast)
+  done
+
+lemma "\<Union>S = (\<Union>x\<in>S. x)"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] UN_I[no_vars]}
+\rulename{UN_I}
+*}
+
+text{*
+@{thm[display] UN_E[no_vars]}
+\rulename{UN_E}
+*}
+
+text{*indexed intersections*}
+
+lemma "(\<Inter>x. B x) = {y. \<forall>x. y \<in> B x}"
+  apply (blast)
+  done
+
+text{*
+@{thm[display] INT_iff[no_vars]}
+\rulename{INT_iff}
+*}
+
+text{*
+@{thm[display] Inter_iff[no_vars]}
+\rulename{Inter_iff}
+*}
+
+text{*mention also card, Pow, etc.*}
+
+
+text{*
+@{thm[display] card_Un_Int[no_vars]}
+\rulename{card_Un_Int}
+
+@{thm[display] card_Pow[no_vars]}
+\rulename{card_Pow}
+
+@{thm[display] n_subsets[no_vars]}
+\rulename{n_subsets}
+*}
+
+end
diff -r 354e885b3e0a -r 2ec9c808a8a7 doc-src/TutorialI/Sets/Functions.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Sets/Functions.thy	Mon Oct 23 16:24:52 2000 +0200
@@ -0,0 +1,149 @@
+theory Functions = Main:
+
+ML "Pretty.setmargin 64"
+
+
+text{*
+@{thm[display] id_def[no_vars]}
+\rulename{id_def}
+
+@{thm[display] o_def[no_vars]}
+\rulename{o_def}
+
+@{thm[display] o_assoc[no_vars]}
+\rulename{o_assoc}
+*}
+
+text{*
+@{thm[display] fun_upd_apply[no_vars]}
+\rulename{fun_upd_apply}
+
+@{thm[display] fun_upd_upd[no_vars]}
+\rulename{fun_upd_upd}
+*}
+
+
+text{*
+definitions of injective, surjective, bijective
+
+@{thm[display] inj_on_def[no_vars]}
+\rulename{inj_on_def}
+
+@{thm[display] surj_def[no_vars]}
+\rulename{surj_def}
+
+@{thm[display] bij_def[no_vars]}
+\rulename{bij_def}
+*}
+
+
+
+text{*
+possibly interesting theorems about inv
+*}
+
+text{*
+@{thm[display] inv_f_f[no_vars]}
+\rulename{inv_f_f}
+
+@{thm[display] inj_imp_surj_inv[no_vars]}
+\rulename{inj_imp_surj_inv}
+
+@{thm[display] surj_imp_inj_inv[no_vars]}
+\rulename{surj_imp_inj_inv}
+
+@{thm[display] surj_f_inv_f[no_vars]}
+\rulename{surj_f_inv_f}
+
+@{thm[display] bij_imp_bij_inv[no_vars]}
+\rulename{bij_imp_bij_inv}
+
+@{thm[display] inv_inv_eq[no_vars]}
+\rulename{inv_inv_eq}
+
+@{thm[display] o_inv_distrib[no_vars]}
+\rulename{o_inv_distrib}
+*}
+
+
+
+text{*
+small sample proof
+
+@{thm[display] ext[no_vars]}
+\rulename{ext}
+
+@{thm[display] expand_fun_eq[no_vars]}
+\rulename{expand_fun_eq}
+*}
+
+lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
+  apply (simp add: expand_fun_eq inj_on_def o_def)
+  apply (auto)
+  done
+
+text{*
+\begin{isabelle}
+inj\ f\ \isasymLongrightarrow \ (f\ \isasymcirc \ g\ =\ f\ \isasymcirc \ h)\ =\ (g\ =\ h)\isanewline
+\ 1.\ \isasymforall x\ y.\ f\ x\ =\ f\ y\ \isasymlongrightarrow \ x\ =\ y\ \isasymLongrightarrow \isanewline
+\ \ \ \ (\isasymforall x.\ f\ (g\ x)\ =\ f\ (h\ x))\ =\ (\isasymforall x.\ g\ x\ =\ h\ x)
+\end{isabelle}
+*}
+ 
+
+text{*image, inverse image*}
+
+text{*
+@{thm[display] image_def[no_vars]}
+\rulename{image_def}
+*}
+
+text{*
+@{thm[display] image_Un[no_vars]}
+\rulename{image_Un}
+*}
+
+text{*
+@{thm[display] image_compose[no_vars]}
+\rulename{image_compose}
+
+@{thm[display] image_Int[no_vars]}
+\rulename{image_Int}
+
+@{thm[display] bij_image_Compl_eq[no_vars]}
+\rulename{bij_image_Compl_eq}
+*}
+
+
+text{*
+illustrates Union as well as image
+*}
+lemma "f``A \<union> g``A = (\<Union>x\<in>A. {f x, g x})"
+  apply (blast)
+  done
+
+lemma "f `` {(x,y). P x y} = {f(x,y) | x y. P x y}"
+  apply (blast)
+  done
+
+text{*actually a macro!*}
+
+lemma "range f = f``UNIV"
+  apply (blast)
+  done
+
+
+text{*
+inverse image
+*}
+
+text{*
+@{thm[display] vimage_def[no_vars]}
+\rulename{vimage_def}
+
+@{thm[display] vimage_Compl[no_vars]}
+\rulename{vimage_Compl}
+*}
+
+
+end
diff -r 354e885b3e0a -r 2ec9c808a8a7 doc-src/TutorialI/Sets/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Sets/ROOT.ML	Mon Oct 23 16:24:52 2000 +0200
@@ -0,0 +1,4 @@
+use_thy "Examples";
+use_thy "Functions";
+use_thy "Relations";
+use_thy "Recur";
diff -r 354e885b3e0a -r 2ec9c808a8a7 doc-src/TutorialI/Sets/Recur.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Sets/Recur.thy	Mon Oct 23 16:24:52 2000 +0200
@@ -0,0 +1,82 @@
+theory Recur = Main:
+
+ML "Pretty.setmargin 64"
+
+
+text{*
+@{thm[display] mono_def[no_vars]}
+\rulename{mono_def}
+
+@{thm[display] monoI[no_vars]}
+\rulename{monoI}
+
+@{thm[display] monoD[no_vars]}
+\rulename{monoD}
+
+@{thm[display] lfp_unfold[no_vars]}
+\rulename{lfp_unfold}
+
+@{thm[display] lfp_induct[no_vars]}
+\rulename{lfp_induct}
+
+@{thm[display] gfp_unfold[no_vars]}
+\rulename{gfp_unfold}
+
+@{thm[display] coinduct[no_vars]}
+\rulename{coinduct}
+*}
+
+text{*\noindent
+A relation $<$ is
+\bfindex{wellfounded} if it has no infinite descending chain $\cdots <
+a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
+of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
+of an equation and $r$ the argument of some recursive call on the
+corresponding right-hand side, induces a wellfounded relation. 
+
+The HOL library formalizes
+some of the theory of wellfounded relations. For example
+@{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is
+wellfounded.
+Finally we should mention that HOL already provides the mother of all
+inductions, \textbf{wellfounded
+induction}\indexbold{induction!wellfounded}\index{wellfounded
+induction|see{induction, wellfounded}} (@{thm[source]wf_induct}):
+@{thm[display]wf_induct[no_vars]}
+where @{term"wf r"} means that the relation @{term r} is wellfounded
+
+*}
+
+text{*
+
+@{thm[display] wf_induct[no_vars]}
+\rulename{wf_induct}
+
+@{thm[display] less_than_iff[no_vars]}
+\rulename{less_than_iff}
+
+@{thm[display] inv_image_def[no_vars]}
+\rulename{inv_image_def}
+
+@{thm[display] measure_def[no_vars]}
+\rulename{measure_def}
+
+@{thm[display] wf_less_than[no_vars]}
+\rulename{wf_less_than}
+
+@{thm[display] wf_inv_image[no_vars]}
+\rulename{wf_inv_image}
+
+@{thm[display] wf_measure[no_vars]}
+\rulename{wf_measure}
+
+@{thm[display] lex_prod_def[no_vars]}
+\rulename{lex_prod_def}
+
+@{thm[display] wf_lex_prod[no_vars]}
+\rulename{wf_lex_prod}
+
+*}
+
+end
+
diff -r 354e885b3e0a -r 2ec9c808a8a7 doc-src/TutorialI/Sets/Relations.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Sets/Relations.thy	Mon Oct 23 16:24:52 2000 +0200
@@ -0,0 +1,164 @@
+theory Relations = Main:
+
+ML "Pretty.setmargin 64"
+
+(*Id is only used in UNITY*)
+(*refl, antisym,trans,univalent,\<dots> ho hum*)
+
+text{*
+@{thm[display]"Id_def"}
+\rulename{Id_def}
+*}
+
+text{*
+@{thm[display]"comp_def"}
+\rulename{comp_def}
+*}
+
+text{*
+@{thm[display]"R_O_Id"}
+\rulename{R_O_Id}
+*}
+
+text{*
+@{thm[display]"comp_mono"}
+\rulename{comp_mono}
+*}
+
+text{*
+@{thm[display]"converse_iff"}
+\rulename{converse_iff}
+*}
+
+text{*
+@{thm[display]"converse_comp"}
+\rulename{converse_comp}
+*}
+
+text{*
+@{thm[display]"Image_iff"}
+\rulename{Image_iff}
+*}
+
+text{*
+@{thm[display]"Image_UN"}
+\rulename{Image_UN}
+*}
+
+text{*
+@{thm[display]"Domain_iff"}
+\rulename{Domain_iff}
+*}
+
+text{*
+@{thm[display]"Range_iff"}
+\rulename{Range_iff}
+*}
+
+text{*
+@{thm[display]"relpow.simps"}
+\rulename{relpow.simps}
+
+@{thm[display]"rtrancl_unfold"}
+\rulename{rtrancl_unfold}
+
+@{thm[display]"rtrancl_refl"}
+\rulename{rtrancl_refl}
+
+@{thm[display]"r_into_rtrancl"}
+\rulename{r_into_rtrancl}
+
+@{thm[display]"rtrancl_trans"}
+\rulename{rtrancl_trans}
+
+@{thm[display]"rtrancl_induct"}
+\rulename{rtrancl_induct}
+
+@{thm[display]"rtrancl_idemp"}
+\rulename{rtrancl_idemp}
+
+@{thm[display]"r_into_trancl"}
+\rulename{r_into_trancl}
+
+@{thm[display]"trancl_trans"}
+\rulename{trancl_trans}
+
+@{thm[display]"trancl_into_rtrancl"}
+\rulename{trancl_into_rtrancl}
+
+@{thm[display]"trancl_converse"}
+\rulename{trancl_converse}
+*}
+
+text{*Relations.  transitive closure*}
+
+lemma rtrancl_converseD: "(x,y) \<in> (r^-1)^* \<Longrightarrow> (y,x) \<in> r^*"
+  apply (erule rtrancl_induct)
+   apply (rule rtrancl_refl)
+  apply (blast intro: r_into_rtrancl rtrancl_trans)
+  done
+
+text{*
+proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline
+\isanewline
+goal\ {\isacharparenleft}lemma\ rtrancl{\isacharunderscore}converseD{\isacharparenright}{\isacharcolon}\isanewline
+{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharparenleft}r{\isacharcircum}{\isacharminus}\isadigit{1}{\isacharparenright}{\isacharcircum}{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}\isanewline
+\ \isadigit{1}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}\isanewline
+\ \isadigit{2}{\isachardot}\ {\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharparenleft}r{\isacharcircum}{\isacharminus}\isadigit{1}{\isacharparenright}{\isacharcircum}{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharminus}\isadigit{1}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}z{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}
+*}
+
+lemma rtrancl_converseI: "(y,x) \<in> r^* \<Longrightarrow> (x,y) \<in> (r^-1)^*"
+  apply (erule rtrancl_induct)
+   apply (rule rtrancl_refl)
+  apply (blast intro: r_into_rtrancl rtrancl_trans)
+  done
+
+lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
+  apply (auto intro: rtrancl_converseI dest: rtrancl_converseD)
+  done
+
+
+lemma "A \<subseteq> Id"
+  apply (rule subsetI)
+  apply (auto)
+  oops
+
+text{*
+proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline
+\isanewline
+goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
+A\ {\isasymsubseteq}\ Id\isanewline
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ x\ {\isasymin}\ Id
+
+proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{2}\isanewline
+\isanewline
+goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
+A\ {\isasymsubseteq}\ Id\isanewline
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ A\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ b
+*}
+
+text{*questions: do we cover force?  (Why not?)
+Do we include tables of operators in ASCII and X-symbol notation like in the Logics manuals?*}
+
+
+text{*rejects*}
+
+lemma "(a \<in> {z. P z} \<union> {y. Q y}) = P a \<or> Q a"
+  apply (blast)
+  done
+
+text{*Pow, Inter too little used*}
+
+lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)"
+  apply (simp add: psubset_def)
+  done
+
+(*
+text{*
+@{thm[display]"DD"}
+\rulename{DD}
+*}
+*)
+
+end