--- a/Admin/build Wed Mar 14 20:34:20 2012 +0100
+++ b/Admin/build Wed Mar 14 22:34:18 2012 +0100
@@ -23,9 +23,10 @@
Produce Isabelle distribution modules from current repository sources.
The MODULES list may contain any of the following:
- all all modules below
+ all all modules below *except* doc-src
browser graph browser (requires jdk)
doc documentation (requires latex and rail)
+ doc-src documentation sources from Isabelle theories
jars Isabelle/Scala layer (requires Scala in \$SCALA_HOME)
jars_fresh fresh build of jars
@@ -82,6 +83,25 @@
}
+function build_doc-src ()
+{
+ echo "###"
+ echo "### Building documentation sources..."
+ echo "###"
+
+ cd "$ISABELLE_HOME/doc-src"
+ for DOC in $(cat Dirs)
+ do
+ pushd "$DOC" >/dev/null
+ if [[ -f "IsaMakefile" ]]
+ then
+ "$ISABELLE_TOOL" make || exit $?
+ fi
+ popd >/dev/null
+ done
+}
+
+
function build_jars ()
{
pushd "$ISABELLE_HOME/src/Pure" >/dev/null
@@ -98,6 +118,7 @@
all) build_all;;
browser) build_browser;;
doc) build_doc;;
+ doc-src) build_doc-src;;
jars) build_jars;;
jars_fresh) build_jars -f;;
*) fail "Bad module $MODULE"
--- a/Admin/makedist Wed Mar 14 20:34:20 2012 +0100
+++ b/Admin/makedist Wed Mar 14 22:34:18 2012 +0100
@@ -5,9 +5,8 @@
## global settings
REPOS_NAME="isabelle"
-REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}"
-
-DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
+REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}"
+DISTPREFIX="${DISTPREFIX:-~/tmp/isadist}"
umask 022
@@ -95,8 +94,14 @@
echo "### Retrieving Mercurial repository $VERSION"
echo "###"
-{ wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
- fail "Failed to retrieve $VERSION"
+if expr match "$REPOS" "https\?://" > /dev/null
+then
+ { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
+ fail "Failed to retrieve $VERSION"
+else
+ { hg --repository "$REPOS" archive --type tgz - | tar -xzf -; } || \
+ fail "Failed to retrieve $VERSION"
+fi
IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
@@ -225,5 +230,4 @@
rm -rf "${DISTNAME}-old"
-
echo "DONE"
--- a/Admin/mira.py Wed Mar 14 20:34:20 2012 +0100
+++ b/Admin/mira.py Wed Mar 14 22:34:18 2012 +0100
@@ -17,6 +17,7 @@
from mira.tools import tool
from mira import schedule, misc
from mira.environment import scheduler
+from mira import repositories
# build and evaluation tools
@@ -256,6 +257,21 @@
"""HOL image"""
return build_isabelle_image('HOL', 'Pure', 'HOL', *args)
+@configuration(repos = [Isabelle], deps = [(HOL, [0])])
+def HOL_Library(*args):
+ """HOL-Library image"""
+ return build_isabelle_image('HOL', 'HOL', 'HOL-Library', *args)
+
+@configuration(repos = [Isabelle], deps = [(Pure, [0])])
+def ZF(*args):
+ """ZF image"""
+ return build_isabelle_image('ZF', 'Pure', 'ZF', *args)
+
+@configuration(repos = [Isabelle], deps = [(HOL, [0])])
+def HOL_HOLCF(*args):
+ """HOLCF image"""
+ return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args)
+
@configuration(repos = [Isabelle], deps = [(Pure_64, [0])])
def HOL_64(*args):
"""HOL image (64 bit)"""
@@ -292,6 +308,40 @@
return isabelle_makeall(*args)
+# distribution and documentation Build
+
+@configuration(repos = [Isabelle], deps = [])
+def Distribution(env, case, paths, dep_paths, playground):
+ """Build of distribution"""
+ ## FIXME This is rudimentary; study Admin/CHECKLIST to complete this configuration accordingly
+ isabelle_home = paths[0]
+ (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'makedist'),
+ REPOS = repositories.get(Isabelle).local_path, DISTPREFIX = os.getcwd())
+ return (return_code == 0, '', ## FIXME might add summary here
+ {}, {'log': log}, None) ## FIXME might add proper result here
+
+@configuration(repos = [Isabelle], deps = [
+ (HOL, [0]),
+ (HOL_HOLCF, [0]),
+ (ZF, [0]),
+ (HOL_Library, [0])
+ ])
+def Documentation_images(*args):
+ """Isabelle images needed to build the documentation"""
+ return isabelle_dependency_only(*args)
+
+@configuration(repos = [Isabelle], deps = [(Documentation_images, [0])])
+def Documentation(env, case, paths, dep_paths, playground):
+ """Build of documentation"""
+ isabelle_home = paths[0]
+ dep_path = dep_paths[0]
+ prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
+ usedir_options = default_usedir_options)
+ (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'build', 'doc-src'))
+ return (return_code == 0, extract_isabelle_run_summary(log),
+ extract_report_data(isabelle_home, log), {'log': log}, None)
+
+
# Mutabelle configurations
def invoke_mutabelle(theory, env, case, paths, dep_paths, playground):
--- a/doc-src/TutorialI/CTL/CTL.thy Wed Mar 14 20:34:20 2012 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy Wed Mar 14 22:34:18 2012 +0100
@@ -370,11 +370,11 @@
lemma "lfp(eufix A B) \<subseteq> eusem A B"
apply(rule lfp_lowerbound)
-apply(auto simp add: eusem_def eufix_def);
- apply(rule_tac x = "[]" in exI);
+apply(auto simp add: eusem_def eufix_def)
+ apply(rule_tac x = "[]" in exI)
apply simp
-apply(rule_tac x = "y#xc" in exI);
-apply simp;
+apply(rule_tac x = "xa#xb" in exI)
+apply simp
done
lemma mono_eufix: "mono(eufix A B)";
--- a/src/ZF/Cardinal.thy Wed Mar 14 20:34:20 2012 +0100
+++ b/src/ZF/Cardinal.thy Wed Mar 14 22:34:18 2012 +0100
@@ -540,15 +540,21 @@
done
-lemma nat_lepoll_imp_le [rule_format]:
- "m \<in> nat ==> \<forall>n\<in>nat. m \<lesssim> n \<longrightarrow> m \<le> n"
-apply (induct_tac m)
-apply (blast intro!: nat_0_le)
-apply (rule ballI)
-apply (erule_tac n = n in natE)
-apply (simp (no_asm_simp) add: lepoll_def inj_def)
-apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
-done
+lemma nat_lepoll_imp_le:
+ "m \<in> nat ==> n \<in> nat \<Longrightarrow> m \<lesssim> n \<Longrightarrow> m \<le> n"
+proof (induct m arbitrary: n rule: nat_induct)
+ case 0 thus ?case by (blast intro!: nat_0_le)
+next
+ case (succ m)
+ show ?case using `n \<in> nat`
+ proof (cases rule: natE)
+ case 0 thus ?thesis using succ
+ by (simp add: lepoll_def inj_def)
+ next
+ case (succ n') thus ?thesis using succ.hyps ` succ(m) \<lesssim> n`
+ by (blast intro!: succ_leI dest!: succ_lepoll_succD)
+ qed
+qed
lemma nat_eqpoll_iff: "[| m \<in> nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
apply (rule iffI)
--- a/src/ZF/CardinalArith.thy Wed Mar 14 20:34:20 2012 +0100
+++ b/src/ZF/CardinalArith.thy Wed Mar 14 22:34:18 2012 +0100
@@ -628,28 +628,25 @@
assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K"
proof -
have OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card)
- have "InfCard(K) \<longrightarrow> K \<otimes> K = K"
- proof (rule trans_induct [OF OK], rule impI)
- fix i
- assume i: "Ord(i)" "InfCard(i)"
- and ih: " \<forall>y\<in>i. InfCard(y) \<longrightarrow> y \<otimes> y = y"
- show "i \<otimes> i = i"
- proof (rule le_anti_sym)
- have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|"
- by (rule cardinal_cong,
- simp add: i well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
- hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" using i
- by (simp add: cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
- moreover
- have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using ih i
- by (simp add: ordertype_csquare_le)
- ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
- next
- show "i \<le> i \<otimes> i" using i
- by (blast intro: cmult_square_le InfCard_is_Card)
- qed
+ show "InfCard(K) ==> K \<otimes> K = K" using OK
+ proof (induct rule: trans_induct)
+ case (step i)
+ show "i \<otimes> i = i"
+ proof (rule le_anti_sym)
+ have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|"
+ by (rule cardinal_cong,
+ simp add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
+ hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))"
+ by (simp add: step.hyps cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
+ moreover
+ have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using step
+ by (simp add: ordertype_csquare_le)
+ ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
+ next
+ show "i \<le> i \<otimes> i" using step
+ by (blast intro: cmult_square_le InfCard_is_Card)
qed
- thus ?thesis using IK ..
+ qed
qed
(*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)
@@ -910,10 +907,15 @@
finally show ?thesis .
qed
-lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<longrightarrow> i \<in> nat | i=nat"
-apply (erule trans_induct3, auto)
-apply (blast dest!: nat_le_Limit [THEN le_imp_subset])
-done
+lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<Longrightarrow> i \<in> nat | i=nat"
+proof (induct i rule: trans_induct3)
+ case 0 thus ?case by auto
+next
+ case (succ i) thus ?case by auto
+next
+ case (limit l) thus ?case
+ by (blast dest: nat_le_Limit le_imp_subset)
+qed
lemma Ord_nat_subset_into_Card: "[| Ord(i); i \<subseteq> nat |] ==> Card(i)"
by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)
--- a/src/ZF/Constructible/AC_in_L.thy Wed Mar 14 20:34:20 2012 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy Wed Mar 14 22:34:18 2012 +0100
@@ -424,14 +424,14 @@
lemma (in Nat_Times_Nat) L_r_type:
"Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)"
-apply (induct i rule: trans_induct3_rule)
+apply (induct i rule: trans_induct3)
apply (simp_all add: Lset_succ DPow_r_type well_ord_DPow_r rlimit_def
Transset_subset_DPow [OF Transset_Lset], blast)
done
lemma (in Nat_Times_Nat) well_ord_L_r:
"Ord(i) ==> well_ord(Lset(i), L_r(fn,i))"
-apply (induct i rule: trans_induct3_rule)
+apply (induct i rule: trans_induct3)
apply (simp_all add: well_ord0 Lset_succ L_r_type well_ord_DPow_r
well_ord_rlimit ltD)
done
--- a/src/ZF/Constructible/Normal.thy Wed Mar 14 20:34:20 2012 +0100
+++ b/src/ZF/Constructible/Normal.thy Wed Mar 14 22:34:18 2012 +0100
@@ -243,7 +243,7 @@
by (simp add: Normal_def mono_Ord_def)
lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"
-apply (induct i rule: trans_induct3_rule)
+apply (induct i rule: trans_induct3)
apply (simp add: subset_imp_le)
apply (subgoal_tac "F(x) < F(succ(x))")
apply (force intro: lt_trans1)
@@ -383,7 +383,7 @@
lemma Ord_normalize [simp, intro]:
"[| Ord(a); !!x. Ord(x) ==> Ord(F(x)) |] ==> Ord(normalize(F, a))"
-apply (induct a rule: trans_induct3_rule)
+apply (induct a rule: trans_induct3)
apply (simp_all add: ltD def_transrec2 [OF normalize_def])
done
--- a/src/ZF/Nat_ZF.thy Wed Mar 14 20:34:20 2012 +0100
+++ b/src/ZF/Nat_ZF.thy Wed Mar 14 22:34:18 2012 +0100
@@ -87,14 +87,16 @@
(*Mathematical induction*)
lemma nat_induct [case_names 0 succ, induct set: nat]:
- "[| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)"
+ "[| n \<in> nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)"
by (erule def_induct [OF nat_def nat_bnd_mono], blast)
lemma natE:
- "[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
-by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto)
+ assumes "n \<in> nat"
+ obtains (0) "n=0" | (succ) x where "x \<in> nat" "n=succ(x)"
+using assms
+by (rule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE]) auto
-lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
+lemma nat_into_Ord [simp]: "n \<in> nat ==> Ord(n)"
by (erule nat_induct, auto)
(* @{term"i: nat ==> 0 \<le> i"}; same thing as @{term"0<succ(i)"} *)
@@ -123,7 +125,7 @@
lemma succ_natD: "succ(i): nat ==> i: nat"
by (rule Ord_trans [OF succI1], auto)
-lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n: nat"
+lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n \<in> nat"
by (blast dest!: succ_natD)
lemma nat_le_Limit: "Limit(i) ==> nat \<le> i"
@@ -138,7 +140,7 @@
(* [| succ(i): k; k: nat |] ==> i: k *)
lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord]
-lemma lt_nat_in_nat: "[| m<n; n: nat |] ==> m: nat"
+lemma lt_nat_in_nat: "[| m<n; n \<in> nat |] ==> m: nat"
apply (erule ltE)
apply (erule Ord_trans, assumption, simp)
done
@@ -158,7 +160,7 @@
lemma nat_induct_from_lemma [rule_format]:
- "[| n: nat; m: nat;
+ "[| n \<in> nat; m: nat;
!!x. [| x: nat; m \<le> x; P(x) |] ==> P(succ(x)) |]
==> m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)"
apply (erule nat_induct)
@@ -167,7 +169,7 @@
(*Induction starting from m rather than 0*)
lemma nat_induct_from:
- "[| m \<le> n; m: nat; n: nat;
+ "[| m \<le> n; m: nat; n \<in> nat;
P(m);
!!x. [| x: nat; m \<le> x; P(x) |] ==> P(succ(x)) |]
==> P(n)"
@@ -176,7 +178,7 @@
(*Induction suitable for subtraction and less-than*)
lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
- "[| m: nat; n: nat;
+ "[| m: nat; n \<in> nat;
!!x. x: nat ==> P(x,0);
!!y. y: nat ==> P(0,succ(y));
!!x y. [| x: nat; y: nat; P(x,y) |] ==> P(succ(x),succ(y)) |]
@@ -201,7 +203,7 @@
done
lemma succ_lt_induct:
- "[| m<n; n: nat;
+ "[| m<n; n \<in> nat;
P(m,succ(m));
!!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) |]
==> P(m,n)"
@@ -241,7 +243,7 @@
by (simp add: nat_case_def)
lemma nat_case_type [TC]:
- "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |]
+ "[| n \<in> nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |]
==> nat_case(a,b,n) \<in> C(n)";
by (erule nat_induct, auto)
--- a/src/ZF/OrderType.thy Wed Mar 14 20:34:20 2012 +0100
+++ b/src/ZF/OrderType.thy Wed Mar 14 22:34:18 2012 +0100
@@ -631,16 +631,19 @@
text{*Order/monotonicity properties of ordinal addition *}
lemma oadd_le_self2: "Ord(i) ==> i \<le> j++i"
-apply (erule_tac i = i in trans_induct3)
-apply (simp (no_asm_simp) add: Ord_0_le)
-apply (simp (no_asm_simp) add: oadd_succ succ_leI)
-apply (simp (no_asm_simp) add: oadd_Limit)
-apply (rule le_trans)
-apply (rule_tac [2] le_implies_UN_le_UN)
-apply (erule_tac [2] bspec)
- prefer 2 apply assumption
-apply (simp add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord)
-done
+proof (induct i rule: trans_induct3)
+ case 0 thus ?case by (simp add: Ord_0_le)
+next
+ case (succ i) thus ?case by (simp add: oadd_succ succ_leI)
+next
+ case (limit l)
+ hence "l = (\<Union>x\<in>l. x)"
+ by (simp add: Union_eq_UN [symmetric] Limit_Union_eq)
+ also have "... \<le> (\<Union>x\<in>l. j++x)"
+ by (rule le_implies_UN_le_UN) (rule limit.hyps)
+ finally have "l \<le> (\<Union>x\<in>l. j++x)" .
+ thus ?case using limit.hyps by (simp add: oadd_Limit)
+qed
lemma oadd_le_mono1: "k \<le> j ==> k++i \<le> j++i"
apply (frule lt_Ord)
@@ -925,15 +928,23 @@
lemma omult_le_self: "[| Ord(i); 0<j |] ==> i \<le> i**j"
by (blast intro: all_lt_imp_le Ord_omult lt_omult1 lt_Ord2)
-lemma omult_le_mono1: "[| k \<le> j; Ord(i) |] ==> k**i \<le> j**i"
-apply (frule lt_Ord)
-apply (frule le_Ord2)
-apply (erule trans_induct3)
-apply (simp (no_asm_simp) add: le_refl Ord_0)
-apply (simp (no_asm_simp) add: omult_succ oadd_le_mono)
-apply (simp (no_asm_simp) add: omult_Limit)
-apply (rule le_implies_UN_le_UN, blast)
-done
+lemma omult_le_mono1:
+ assumes kj: "k \<le> j" and i: "Ord(i)" shows "k**i \<le> j**i"
+proof -
+ have o: "Ord(k)" "Ord(j)" by (rule lt_Ord [OF kj] le_Ord2 [OF kj])+
+ show ?thesis using i
+ proof (induct i rule: trans_induct3)
+ case 0 thus ?case
+ by simp
+ next
+ case (succ i) thus ?case
+ by (simp add: o kj omult_succ oadd_le_mono)
+ next
+ case (limit l)
+ thus ?case
+ by (auto simp add: o kj omult_Limit le_implies_UN_le_UN)
+ qed
+qed
lemma omult_lt_mono2: "[| k<j; 0<i |] ==> i**k < i**j"
apply (rule ltI)
@@ -955,20 +966,30 @@
lemma omult_lt_mono: "[| i' \<le> i; j'<j; 0<i |] ==> i'**j' < i**j"
by (blast intro: lt_trans1 omult_le_mono1 omult_lt_mono2 Ord_succD elim: ltE)
-lemma omult_le_self2: "[| Ord(i); 0<j |] ==> i \<le> j**i"
-apply (frule lt_Ord2)
-apply (erule_tac i = i in trans_induct3)
-apply (simp (no_asm_simp))
-apply (simp (no_asm_simp) add: omult_succ)
-apply (erule lt_trans1)
-apply (rule_tac b = "j**x" in oadd_0 [THEN subst], rule_tac [2] oadd_lt_mono2)
-apply (blast intro: Ord_omult, assumption)
-apply (simp (no_asm_simp) add: omult_Limit)
-apply (rule le_trans)
-apply (rule_tac [2] le_implies_UN_le_UN)
-prefer 2 apply blast
-apply (simp (no_asm_simp) add: Union_eq_UN [symmetric] Limit_Union_eq Limit_is_Ord)
-done
+lemma omult_le_self2:
+ assumes i: "Ord(i)" and j: "0<j" shows "i \<le> j**i"
+proof -
+ have oj: "Ord(j)" by (rule lt_Ord2 [OF j])
+ show ?thesis using i
+ proof (induct i rule: trans_induct3)
+ case 0 thus ?case
+ by simp
+ next
+ case (succ i)
+ have "j \<times>\<times> i ++ 0 < j \<times>\<times> i ++ j"
+ by (rule oadd_lt_mono2 [OF j])
+ with succ.hyps show ?case
+ by (simp add: oj j omult_succ ) (rule lt_trans1)
+ next
+ case (limit l)
+ hence "l = (\<Union>x\<in>l. x)"
+ by (simp add: Union_eq_UN [symmetric] Limit_Union_eq)
+ also have "... \<le> (\<Union>x\<in>l. j**x)"
+ by (rule le_implies_UN_le_UN) (rule limit.hyps)
+ finally have "l \<le> (\<Union>x\<in>l. j**x)" .
+ thus ?case using limit.hyps by (simp add: oj omult_Limit)
+ qed
+qed
text{*Further properties of ordinal multiplication *}
--- a/src/ZF/Ordinal.thy Wed Mar 14 20:34:20 2012 +0100
+++ b/src/ZF/Ordinal.thy Wed Mar 14 22:34:18 2012 +0100
@@ -236,7 +236,7 @@
done
-(** Recall that @{term"i \<le> j"} abbreviates @{term"i<succ(j)"} !! **)
+text{* Recall that @{term"i \<le> j"} abbreviates @{term"i<succ(j)"} !! *}
lemma le_iff: "i \<le> j <-> i<j | (i=j & Ord(j))"
by (unfold lt_def, blast)
@@ -335,12 +335,11 @@
done
(*Induction over an ordinal*)
-lemmas Ord_induct [consumes 2] = Transset_induct [OF _ Ord_is_Transset]
-lemmas Ord_induct_rule = Ord_induct [rule_format, consumes 2]
+lemmas Ord_induct [consumes 2] = Transset_induct [rule_format, OF _ Ord_is_Transset]
(*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
-lemma trans_induct [consumes 1]:
+lemma trans_induct [rule_format, consumes 1, case_names step]:
"[| Ord(i);
!!x.[| Ord(x); \<forall>y\<in>x. P(y) |] ==> P(x) |]
==> P(i)"
@@ -348,10 +347,8 @@
apply (blast intro: Ord_succ [THEN Ord_in_Ord])
done
-lemmas trans_induct_rule = trans_induct [rule_format, consumes 1]
-
-(*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
+section{*Fundamental properties of the epsilon ordering (< on ordinals)*}
subsubsection{*Proving That < is a Linear Ordering on the Ordinals*}
@@ -364,23 +361,27 @@
apply (blast dest: Ord_trans)
done
-(*The trichotomy law for ordinals!*)
+text{*The trichotomy law for ordinals*}
lemma Ord_linear_lt:
- "[| Ord(i); Ord(j); i<j ==> P; i=j ==> P; j<i ==> P |] ==> P"
+ assumes o: "Ord(i)" "Ord(j)"
+ obtains (lt) "i<j" | (eq) "i=j" | (gt) "j<i"
apply (simp add: lt_def)
-apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE], blast+)
+apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE])
+apply (blast intro: o)+
done
lemma Ord_linear2:
- "[| Ord(i); Ord(j); i<j ==> P; j \<le> i ==> P |] ==> P"
+ assumes o: "Ord(i)" "Ord(j)"
+ obtains (lt) "i<j" | (ge) "j \<le> i"
apply (rule_tac i = i and j = j in Ord_linear_lt)
-apply (blast intro: leI le_eqI sym ) +
+apply (blast intro: leI le_eqI sym o) +
done
lemma Ord_linear_le:
- "[| Ord(i); Ord(j); i \<le> j ==> P; j \<le> i ==> P |] ==> P"
+ assumes o: "Ord(i)" "Ord(j)"
+ obtains (le) "i \<le> j" | (ge) "j \<le> i"
apply (rule_tac i = i and j = j in Ord_linear_lt)
-apply (blast intro: leI le_eqI ) +
+apply (blast intro: leI le_eqI o) +
done
lemma le_imp_not_lt: "j \<le> i ==> ~ i<j"
@@ -701,14 +702,11 @@
by (blast intro!: non_succ_LimitI Ord_0_lt)
lemma Ord_cases:
- "[| Ord(i);
- i=0 ==> P;
- !!j. [| Ord(j); i=succ(j) |] ==> P;
- Limit(i) ==> P
- |] ==> P"
-by (drule Ord_cases_disj, blast)
+ assumes i: "Ord(i)"
+ obtains (0) "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)"
+by (insert Ord_cases_disj [OF i], auto)
-lemma trans_induct3 [case_names 0 succ limit, consumes 1]:
+lemma trans_induct3_raw:
"[| Ord(i);
P(0);
!!x. [| Ord(x); P(x) |] ==> P(succ(x));
@@ -718,7 +716,7 @@
apply (erule Ord_cases, blast+)
done
-lemmas trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1]
+lemmas trans_induct3 = trans_induct3_raw [rule_format, case_names 0 succ limit, consumes 1]
text{*A set of ordinals is either empty, contains its own union, or its
union is a limit ordinal.*}
--- a/src/ZF/ex/LList.thy Wed Mar 14 20:34:20 2012 +0100
+++ b/src/ZF/ex/LList.thy Wed Mar 14 22:34:18 2012 +0100
@@ -106,15 +106,22 @@
declare qunivD [dest!]
declare Ord_in_Ord [elim!]
-lemma llist_quniv_lemma [rule_format]:
- "Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l \<inter> Vset(i) \<subseteq> univ(eclose(A))"
-apply (erule trans_induct)
-apply (rule ballI)
-apply (erule llist.cases)
-apply (simp_all add: QInl_def QInr_def llist.con_defs)
-(*LCons case: I simply can't get rid of the deepen_tac*)
-apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
-done
+lemma llist_quniv_lemma:
+ "Ord(i) ==> l \<in> llist(quniv(A)) \<Longrightarrow> l \<inter> Vset(i) \<subseteq> univ(eclose(A))"
+proof (induct i arbitrary: l rule: trans_induct)
+ case (step i l)
+ show ?case using `l \<in> llist(quniv(A))`
+ proof (cases l rule: llist.cases)
+ case LNil thus ?thesis
+ by (simp add: QInl_def QInr_def llist.con_defs)
+ next
+ case (LCons a l) thus ?thesis using step.hyps
+ proof (simp add: QInl_def QInr_def llist.con_defs)
+ show "<1; <a; l>> \<inter> Vset(i) \<subseteq> univ(eclose(A))" using LCons `Ord(i)`
+ by (fast intro: step Ord_trans Int_lower1 [THEN subset_trans])
+ qed
+ qed
+qed
lemma llist_quniv: "llist(quniv(A)) \<subseteq> quniv(A)"
apply (rule qunivI [THEN subsetI])
@@ -134,14 +141,19 @@
declare Ord_in_Ord [elim!]
(*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*)
-lemma lleq_Int_Vset_subset [rule_format]:
- "Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) \<longrightarrow> l \<inter> Vset(i) \<subseteq> l'"
-apply (erule trans_induct)
-apply (intro allI impI)
-apply (erule lleq.cases)
-apply (unfold QInr_def llist.con_defs, safe)
-apply (fast elim!: Ord_trans bspec [elim_format])
-done
+lemma lleq_Int_Vset_subset:
+ "Ord(i) ==> <l,l'> \<in> lleq(A) \<Longrightarrow> l \<inter> Vset(i) \<subseteq> l'"
+proof (induct i arbitrary: l l' rule: trans_induct)
+ case (step i l l')
+ show ?case using `\<langle>l, l'\<rangle> \<in> lleq(A)`
+ proof (cases rule: lleq.cases)
+ case LNil thus ?thesis
+ by (auto simp add: QInr_def llist.con_defs)
+ next
+ case (LCons a l l') thus ?thesis using step.hyps
+ by (auto simp add: QInr_def llist.con_defs intro: Ord_trans)
+ qed
+qed
(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
lemma lleq_symmetric: "<l,l'> \<in> lleq(A) ==> <l',l> \<in> lleq(A)"
@@ -208,15 +220,22 @@
(*Reasoning borrowed from lleq.ML; a similar proof works for all
"productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
-lemma flip_llist_quniv_lemma [rule_format]:
- "Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) \<inter> Vset(i) \<subseteq> univ(eclose(bool))"
-apply (erule trans_induct)
-apply (rule ballI)
-apply (erule llist.cases, simp_all)
-apply (simp_all add: QInl_def QInr_def llist.con_defs)
-(*LCons case: I simply can't get rid of the deepen_tac*)
-apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
-done
+lemma flip_llist_quniv_lemma:
+ "Ord(i) ==> l \<in> llist(bool) \<Longrightarrow> flip(l) \<inter> Vset(i) \<subseteq> univ(eclose(bool))"
+proof (induct i arbitrary: l rule: trans_induct)
+ case (step i l)
+ show ?case using `l \<in> llist(bool)`
+ proof (cases l rule: llist.cases)
+ case LNil thus ?thesis
+ by (simp, simp add: QInl_def QInr_def llist.con_defs)
+ next
+ case (LCons a l) thus ?thesis using step.hyps
+ proof (simp, simp add: QInl_def QInr_def llist.con_defs)
+ show "<1; <not(a); flip(l)>> \<inter> Vset(i) \<subseteq> univ(eclose(bool))" using LCons step.hyps
+ by (auto intro: Ord_trans)
+ qed
+ qed
+qed
lemma flip_in_quniv: "l \<in> llist(bool) ==> flip(l) \<in> quniv(bool)"
by (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI], assumption+)