# HG changeset patch
# User wenzelm
# Date 1332449006 -3600
# Node ID eba1cea4eef6c39bf104afa8adfac5f05ee98300
# Parent  08c22e8ffe70d0a6a9f040dcc62ecb23d2f67b18# Parent  737d7bc8e50fe9b17d9cd2ef77049489ecaba306
merged;

diff -r 737d7bc8e50f -r eba1cea4eef6 NEWS
--- a/NEWS	Thu Mar 22 16:44:19 2012 +0100
+++ b/NEWS	Thu Mar 22 21:43:26 2012 +0100
@@ -120,6 +120,9 @@
 
 Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.
 
+See theory "Relation" for examples for making use of pred/set conversions
+by means of attributes "to_set" and "to_pred".
+
 INCOMPATIBILITY.
 
 * Consolidated various theorem names relating to Finite_Set.fold
diff -r 737d7bc8e50f -r eba1cea4eef6 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Mar 22 16:44:19 2012 +0100
+++ b/src/HOL/Relation.thy	Thu Mar 22 21:43:26 2012 +0100
@@ -543,7 +543,7 @@
   "{} O R = {}"
   by blast
 
-lemma prod_comp_bot1 [simp]:
+lemma pred_comp_bot1 [simp]:
   "\<bottom> OO R = \<bottom>"
   by (fact rel_comp_empty1 [to_pred])
 
diff -r 737d7bc8e50f -r eba1cea4eef6 src/HOL/SPARK/Tools/fdl_lexer.ML
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Thu Mar 22 16:44:19 2012 +0100
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Thu Mar 22 21:43:26 2012 +0100
@@ -96,7 +96,6 @@
 
 val lexicon = Scan.make_lexicon (map raw_explode
   ["rule_family",
-   "title",
    "For",
    ":",
    "[",
diff -r 737d7bc8e50f -r eba1cea4eef6 src/HOL/SPARK/Tools/fdl_parser.ML
--- a/src/HOL/SPARK/Tools/fdl_parser.ML	Thu Mar 22 16:44:19 2012 +0100
+++ b/src/HOL/SPARK/Tools/fdl_parser.ML	Thu Mar 22 21:43:26 2012 +0100
@@ -323,7 +323,7 @@
    $$$ ":" -- identifier)) >> add_fun_decl) x;
 
 fun declarations x =
- ($$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" --
+ (the_identifier "title" |-- subprogram_kind -- identifier --| $$$ ";" --
   (Scan.repeat ((type_decl || const_decl || var_decl || fun_decl) --|
      !!! ($$$ ";")) >> (fn ds => fold I ds empty_decls)) --|
   $$$ "end" --| $$$ ";") x;
diff -r 737d7bc8e50f -r eba1cea4eef6 src/ZF/Constructible/AC_in_L.thy
--- a/src/ZF/Constructible/AC_in_L.thy	Thu Mar 22 16:44:19 2012 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy	Thu Mar 22 21:43:26 2012 +0100
@@ -4,7 +4,7 @@
 
 header {* The Axiom of Choice Holds in L! *}
 
-theory AC_in_L imports Formula begin
+theory AC_in_L imports Formula Separation begin
 
 subsection{*Extending a Wellordering over a List -- Lexicographic Power*}
 
@@ -44,22 +44,32 @@
 by (simp add: shorterI)
 
 lemma linear_rlist:
-    "linear(A,r) ==> linear(list(A),rlist(A,r))"
-apply (simp (no_asm_simp) add: linear_def)
-apply (rule ballI)
-apply (induct_tac x)
- apply (rule ballI)
- apply (induct_tac y)
-  apply (simp_all add: shorterI)
-apply (rule ballI)
-apply (erule_tac a=y in list.cases)
- apply (rename_tac [2] a2 l2)
- apply (rule_tac [2] i = "length(l)" and j = "length(l2)" in Ord_linear_lt)
-     apply (simp_all add: shorterI)
-apply (erule_tac x=a and y=a2 in linearE)
-    apply (simp_all add: diffI)
-apply (blast intro: sameI)
-done
+  assumes r: "linear(A,r)" shows "linear(list(A),rlist(A,r))"
+proof -
+  { fix xs ys
+    have "xs \<in> list(A) \<Longrightarrow> ys \<in> list(A) \<Longrightarrow> \<langle>xs,ys\<rangle> \<in> rlist(A,r) \<or> xs = ys \<or> \<langle>ys,xs\<rangle> \<in> rlist(A, r) "
+    proof (induct xs arbitrary: ys rule: list.induct)
+      case Nil 
+      thus ?case by (induct ys rule: list.induct) (auto simp add: shorterI)
+    next
+      case (Cons x xs)
+      { fix y ys
+        assume "y \<in> A" and "ys \<in> list(A)"
+        with Cons
+        have "\<langle>Cons(x,xs),Cons(y,ys)\<rangle> \<in> rlist(A,r) \<or> x=y & xs = ys \<or> \<langle>Cons(y,ys), Cons(x,xs)\<rangle> \<in> rlist(A,r)" 
+          apply (rule_tac i = "length(xs)" and j = "length(ys)" in Ord_linear_lt)
+          apply (simp_all add: shorterI)
+          apply (rule linearE [OF r, of x y]) 
+          apply (auto simp add: diffI intro: sameI) 
+          done
+      }
+      note yConsCase = this
+      show ?case using `ys \<in> list(A)`
+        by (cases rule: list.cases) (simp_all add: Cons rlist_Nil_Cons yConsCase) 
+    qed
+  }
+  thus ?thesis by (simp add: linear_def) 
+qed
 
 
 subsubsection{*Well-foundedness*}
@@ -452,8 +462,20 @@
 apply (blast dest!: well_ord_L_r intro: well_ord_subset)
 done
 
-text{*In order to prove @{term" \<exists>r[L]. wellordered(L, A, r)"}, it's necessary to know 
-that @{term r} is actually constructible. Of course, it follows from the assumption ``@{term V} equals @{term L''}, 
+interpretation L?: M_basic L by (rule M_basic_L)
+
+theorem "\<forall>x[L]. \<exists>r. wellordered(L,x,r)"
+proof 
+  fix x
+  assume "L(x)"
+  then obtain r where "well_ord(x,r)" 
+    by (blast dest: L_implies_AC) 
+  thus "\<exists>r. wellordered(L,x,r)" 
+    by (blast intro: well_ord_imp_relativized)
+qed
+
+text{*In order to prove @{term" \<exists>r[L]. wellordered(L,x,r)"}, it's necessary to know 
+that @{term r} is actually constructible. It follows from the assumption ``@{term V} equals @{term L''}, 
 but this reasoning doesn't appear to work in Isabelle.*}
 
 end