# HG changeset patch
# User paulson
# Date 979209339 -3600
# Node ID f0b0a125ae4bfe22cec9f82a5a37dd8a98a809fa
# Parent  fef84fefd33fb96cce84ec7af2731c7bf715d6fb
revisions corresponding to the new version of sets.tex

diff -r fef84fefd33f -r f0b0a125ae4b doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Wed Jan 10 20:41:14 2001 +0100
+++ b/doc-src/TutorialI/Sets/Examples.thy	Thu Jan 11 11:35:39 2001 +0100
@@ -9,8 +9,7 @@
 text{*complement, union and universal set*}
 
 lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] IntI[no_vars]}
@@ -24,8 +23,7 @@
 *}
 
 lemma "(x \<in> -A) = (x \<notin> A)"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] Compl_iff[no_vars]}
@@ -33,8 +31,7 @@
 *}
 
 lemma "- (A \<union> B) = -A \<inter> -B"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] Compl_Un[no_vars]}
@@ -42,8 +39,7 @@
 *}
 
 lemma "A-A = {}"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] Diff_disjoint[no_vars]}
@@ -53,8 +49,7 @@
   
 
 lemma "A \<union> -A = UNIV"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] Compl_partition[no_vars]}
@@ -73,8 +68,7 @@
 *}
 
 lemma "((A \<union> B) \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] Un_subset_iff[no_vars]}
@@ -82,8 +76,7 @@
 *}
 
 lemma "(A \<subseteq> -B) = (B \<subseteq> -A)"
-  apply (blast)
-  done
+by blast
 
 lemma "(A <= -B) = (B <= -A)"
   oops
@@ -92,8 +85,7 @@
  it doesn't have to be sets*}
 
 lemma "((A:: 'a set) <= -B) = (B <= -A)"
-  apply (blast)
-  done
+by blast
 
 text{*A type constraint lets it work*}
 
@@ -119,8 +111,7 @@
 text{*finite set notation*}
 
 lemma "insert x A = {x} \<union> A"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] insert_is_Un[no_vars]}
@@ -128,26 +119,23 @@
 *}
 
 lemma "{a,b} \<union> {c,d} = {a,b,c,d}"
-  apply (blast)
-  done
+by blast
 
 lemma "{a,b} \<inter> {b,c} = {b}"
-  apply (auto)
-  oops
+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
+apply simp
+by blast
 
 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
+by blast
 
 text{*
 @{thm[display] mem_Collect_eq[no_vars]}
@@ -155,8 +143,7 @@
 *}
 
 lemma "{x. x \<in> A} = A"
-  apply (blast)
-  done
+by blast
   
 text{*
 @{thm[display] Collect_mem_eq[no_vars]}
@@ -164,12 +151,10 @@
 *}
 
 lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A"
-  apply (blast)
-  done
+by blast
 
 lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"
-  apply (blast)
-  done
+by blast
 
 constdefs
   prime   :: "nat set"
@@ -177,16 +162,14 @@
 
 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
+by (rule refl)
 
 text{*binders*}
 
 text{*bounded quantifiers*}
 
 lemma "(\<exists>x\<in>A. P x) = (\<exists>x. x\<in>A \<and> P x)"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] bexI[no_vars]}
@@ -199,8 +182,7 @@
 *}
 
 lemma "(\<forall>x\<in>A. P x) = (\<forall>x. x\<in>A \<longrightarrow> P x)"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] ballI[no_vars]}
@@ -215,8 +197,7 @@
 text{*indexed unions and variations*}
 
 lemma "(\<Union>x. B x) = (\<Union>x\<in>UNIV. B x)"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] UN_iff[no_vars]}
@@ -229,12 +210,10 @@
 *}
 
 lemma "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
-  apply (blast)
-  done
+by blast
 
 lemma "\<Union>S = (\<Union>x\<in>S. x)"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] UN_I[no_vars]}
@@ -249,8 +228,7 @@
 text{*indexed intersections*}
 
 lemma "(\<Inter>x. B x) = {y. \<forall>x. y \<in> B x}"
-  apply (blast)
-  done
+by blast
 
 text{*
 @{thm[display] INT_iff[no_vars]}
diff -r fef84fefd33f -r f0b0a125ae4b doc-src/TutorialI/Sets/Relations.thy
--- a/doc-src/TutorialI/Sets/Relations.thy	Wed Jan 10 20:41:14 2001 +0100
+++ b/doc-src/TutorialI/Sets/Relations.thy	Thu Jan 11 11:35:39 2001 +0100
@@ -7,159 +7,154 @@
 (*refl, antisym,trans,univalent,\<dots> ho hum*)
 
 text{*
-@{thm[display]"Id_def"}
+@{thm[display] Id_def[no_vars]}
 \rulename{Id_def}
 *}
 
 text{*
-@{thm[display]"comp_def"}
+@{thm[display] comp_def[no_vars]}
 \rulename{comp_def}
 *}
 
 text{*
-@{thm[display]"R_O_Id"}
+@{thm[display] R_O_Id[no_vars]}
 \rulename{R_O_Id}
 *}
 
 text{*
-@{thm[display]"comp_mono"}
+@{thm[display] comp_mono[no_vars]}
 \rulename{comp_mono}
 *}
 
 text{*
-@{thm[display]"converse_iff"}
+@{thm[display] converse_iff[no_vars]}
 \rulename{converse_iff}
 *}
 
 text{*
-@{thm[display]"converse_comp"}
+@{thm[display] converse_comp[no_vars]}
 \rulename{converse_comp}
 *}
 
 text{*
-@{thm[display]"Image_iff"}
+@{thm[display] Image_iff[no_vars]}
 \rulename{Image_iff}
 *}
 
 text{*
-@{thm[display]"Image_UN"}
+@{thm[display] Image_UN[no_vars]}
 \rulename{Image_UN}
 *}
 
 text{*
-@{thm[display]"Domain_iff"}
+@{thm[display] Domain_iff[no_vars]}
 \rulename{Domain_iff}
 *}
 
 text{*
-@{thm[display]"Range_iff"}
+@{thm[display] Range_iff[no_vars]}
 \rulename{Range_iff}
 *}
 
 text{*
-@{thm[display]"relpow.simps"}
+@{thm[display] relpow.simps[no_vars]}
 \rulename{relpow.simps}
 
-@{thm[display]"rtrancl_unfold"}
+@{thm[display] rtrancl_unfold[no_vars]}
 \rulename{rtrancl_unfold}
 
-@{thm[display]"rtrancl_refl"}
+@{thm[display] rtrancl_refl[no_vars]}
 \rulename{rtrancl_refl}
 
-@{thm[display]"r_into_rtrancl"}
+@{thm[display] r_into_rtrancl[no_vars]}
 \rulename{r_into_rtrancl}
 
-@{thm[display]"rtrancl_trans"}
+@{thm[display] rtrancl_trans[no_vars]}
 \rulename{rtrancl_trans}
 
-@{thm[display]"rtrancl_induct"}
+@{thm[display] rtrancl_induct[no_vars]}
 \rulename{rtrancl_induct}
 
-@{thm[display]"rtrancl_idemp"}
+@{thm[display] rtrancl_idemp[no_vars]}
 \rulename{rtrancl_idemp}
 
-@{thm[display]"r_into_trancl"}
+@{thm[display] r_into_trancl[no_vars]}
 \rulename{r_into_trancl}
 
-@{thm[display]"trancl_trans"}
+@{thm[display] trancl_trans[no_vars]}
 \rulename{trancl_trans}
 
-@{thm[display]"trancl_into_rtrancl"}
+@{thm[display] trancl_into_rtrancl[no_vars]}
 \rulename{trancl_into_rtrancl}
 
-@{thm[display]"trancl_converse"}
+@{thm[display] trancl_converse[no_vars]}
 \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
+apply (erule rtrancl_induct)
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
+ 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
+apply (erule rtrancl_induct)
+ apply (rule rtrancl_refl)
+apply (blast intro: r_into_rtrancl rtrancl_trans)
+done
+
+lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
+by (auto intro: rtrancl_converseI dest: rtrancl_converseD)
 
 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
-  apply (auto intro: rtrancl_converseI dest: rtrancl_converseD)
-  done
+apply (intro equalityI subsetI)
+txt{*
+after intro rules
+
+@{subgoals[display,indent=0,margin=65]}
+*};
+apply clarify
+txt{*
+after splitting
+@{subgoals[display,indent=0,margin=65]}
+*};
+oops
 
 
-lemma "A \<subseteq> Id"
-  apply (rule subsetI)
-  apply (auto)
-  oops
+lemma "(\<forall>u v. (u,v) \<in> A \<longrightarrow> u=v) \<Longrightarrow> A \<subseteq> Id"
+apply (rule subsetI)
+txt{*
+@{subgoals[display,indent=0,margin=65]}
 
-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
+after subsetI
+*};
+apply clarify
+txt{*
+@{subgoals[display,indent=0,margin=65]}
 
-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
-*}
+subgoals after clarify
+*};
+by blast
 
-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
+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}
-*}
-*)
+apply (simp add: psubset_def)
+done
 
 end