--- 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
--- 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])
--- 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",
":",
"[",
--- 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;
--- 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