# HG changeset patch # User wenzelm # Date 1331760858 -3600 # Node ID efb98d27dc1a41dd3e566e68095b2920918d0e89 # Parent 571ce2bc0b64994555273eee440e939e5479a253# Parent 98ffc3fe31cc38c968b27d85d75a7f9636294e0d merged diff -r 98ffc3fe31cc -r efb98d27dc1a Admin/build --- 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" diff -r 98ffc3fe31cc -r efb98d27dc1a Admin/makedist --- 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" diff -r 98ffc3fe31cc -r efb98d27dc1a Admin/mira.py --- 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): diff -r 98ffc3fe31cc -r efb98d27dc1a doc-src/TutorialI/CTL/CTL.thy --- 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) \ 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)"; diff -r 98ffc3fe31cc -r efb98d27dc1a src/ZF/Cardinal.thy --- 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 \ nat ==> \n\nat. m \ n \ m \ 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 \ nat ==> n \ nat \ m \ n \ m \ 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 \ 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) \ n` + by (blast intro!: succ_leI dest!: succ_lepoll_succD) + qed +qed lemma nat_eqpoll_iff: "[| m \ nat; n: nat |] ==> m \ n \ m = n" apply (rule iffI) diff -r 98ffc3fe31cc -r efb98d27dc1a src/ZF/CardinalArith.thy --- 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 \ K = K" proof - have OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card) - have "InfCard(K) \ K \ K = K" - proof (rule trans_induct [OF OK], rule impI) - fix i - assume i: "Ord(i)" "InfCard(i)" - and ih: " \y\i. InfCard(y) \ y \ y = y" - show "i \ i = i" - proof (rule le_anti_sym) - have "|i \ i| = |ordertype(i \ i, csquare_rel(i))|" - by (rule cardinal_cong, - simp add: i well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll]) - hence "i \ i \ ordertype(i \ i, csquare_rel(i))" using i - by (simp add: cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype]) - moreover - have "ordertype(i \ i, csquare_rel(i)) \ i" using ih i - by (simp add: ordertype_csquare_le) - ultimately show "i \ i \ i" by (rule le_trans) - next - show "i \ i \ i" using i - by (blast intro: cmult_square_le InfCard_is_Card) - qed + show "InfCard(K) ==> K \ K = K" using OK + proof (induct rule: trans_induct) + case (step i) + show "i \ i = i" + proof (rule le_anti_sym) + have "|i \ i| = |ordertype(i \ i, csquare_rel(i))|" + by (rule cardinal_cong, + simp add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll]) + hence "i \ i \ ordertype(i \ i, csquare_rel(i))" + by (simp add: step.hyps cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype]) + moreover + have "ordertype(i \ i, csquare_rel(i)) \ i" using step + by (simp add: ordertype_csquare_le) + ultimately show "i \ i \ i" by (rule le_trans) + next + show "i \ i \ 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 \ nat \ i \ 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 \ nat \ i \ 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 \ nat |] ==> Card(i)" by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card) diff -r 98ffc3fe31cc -r efb98d27dc1a src/ZF/Constructible/AC_in_L.thy --- 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) \ 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 diff -r 98ffc3fe31cc -r efb98d27dc1a src/ZF/Constructible/Normal.thy --- 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\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 diff -r 98ffc3fe31cc -r efb98d27dc1a src/ZF/Nat_ZF.thy --- 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 \ 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 \ nat" + obtains (0) "n=0" | (succ) x where "x \ 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 \ nat ==> Ord(n)" by (erule nat_induct, auto) (* @{term"i: nat ==> 0 \ i"}; same thing as @{term"0 i: nat" by (rule Ord_trans [OF succI1], auto) -lemma nat_succ_iff [iff]: "succ(n): nat \ n: nat" +lemma nat_succ_iff [iff]: "succ(n): nat \ n \ nat" by (blast dest!: succ_natD) lemma nat_le_Limit: "Limit(i) ==> nat \ 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 m: nat" +lemma lt_nat_in_nat: "[| m 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 \ nat; m: nat; !!x. [| x: nat; m \ x; P(x) |] ==> P(succ(x)) |] ==> m \ n \ P(m) \ P(n)" apply (erule nat_induct) @@ -167,7 +169,7 @@ (*Induction starting from m rather than 0*) lemma nat_induct_from: - "[| m \ n; m: nat; n: nat; + "[| m \ n; m: nat; n \ nat; P(m); !!x. [| x: nat; m \ 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 \ 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 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 \ nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |] ==> nat_case(a,b,n) \ C(n)"; by (erule nat_induct, auto) diff -r 98ffc3fe31cc -r efb98d27dc1a src/ZF/OrderType.thy --- 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 \ 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 = (\x\l. x)" + by (simp add: Union_eq_UN [symmetric] Limit_Union_eq) + also have "... \ (\x\l. j++x)" + by (rule le_implies_UN_le_UN) (rule limit.hyps) + finally have "l \ (\x\l. j++x)" . + thus ?case using limit.hyps by (simp add: oadd_Limit) +qed lemma oadd_le_mono1: "k \ j ==> k++i \ j++i" apply (frule lt_Ord) @@ -925,15 +928,23 @@ lemma omult_le_self: "[| Ord(i); 0 i \ i**j" by (blast intro: all_lt_imp_le Ord_omult lt_omult1 lt_Ord2) -lemma omult_le_mono1: "[| k \ j; Ord(i) |] ==> k**i \ 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 \ j" and i: "Ord(i)" shows "k**i \ 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 i**k < i**j" apply (rule ltI) @@ -955,20 +966,30 @@ lemma omult_lt_mono: "[| i' \ i; j' 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 i \ 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**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 \\ i ++ 0 < j \\ 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 = (\x\l. x)" + by (simp add: Union_eq_UN [symmetric] Limit_Union_eq) + also have "... \ (\x\l. j**x)" + by (rule le_implies_UN_le_UN) (rule limit.hyps) + finally have "l \ (\x\l. j**x)" . + thus ?case using limit.hyps by (simp add: oj omult_Limit) + qed +qed text{*Further properties of ordinal multiplication *} diff -r 98ffc3fe31cc -r efb98d27dc1a src/ZF/Ordinal.thy --- 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 \ j"} abbreviates @{term"i j"} abbreviates @{term"i j <-> iy\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 P; i=j ==> P; j P |] ==> P" + assumes o: "Ord(i)" "Ord(j)" + obtains (lt) "i P; j \ i ==> P |] ==> P" + assumes o: "Ord(i)" "Ord(j)" + obtains (lt) "i 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 \ j ==> P; j \ i ==> P |] ==> P" + assumes o: "Ord(i)" "Ord(j)" + obtains (le) "i \ j" | (ge) "j \ 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 \ i ==> ~ i 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.*} diff -r 98ffc3fe31cc -r efb98d27dc1a src/ZF/ex/LList.thy --- 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) ==> \l \ llist(quniv(A)). l \ Vset(i) \ 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 \ llist(quniv(A)) \ l \ Vset(i) \ univ(eclose(A))" +proof (induct i arbitrary: l rule: trans_induct) + case (step i l) + show ?case using `l \ 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; > \ Vset(i) \ 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)) \ 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) ==> \l l'. \ lleq(A) \ l \ Vset(i) \ 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) ==> \ lleq(A) \ l \ Vset(i) \ l'" +proof (induct i arbitrary: l l' rule: trans_induct) + case (step i l l') + show ?case using `\l, l'\ \ 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: " \ lleq(A) ==> \ 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) ==> \l \ llist(bool). flip(l) \ Vset(i) \ 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 \ llist(bool) \ flip(l) \ Vset(i) \ univ(eclose(bool))" +proof (induct i arbitrary: l rule: trans_induct) + case (step i l) + show ?case using `l \ 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; > \ Vset(i) \ univ(eclose(bool))" using LCons step.hyps + by (auto intro: Ord_trans) + qed + qed +qed lemma flip_in_quniv: "l \ llist(bool) ==> flip(l) \ quniv(bool)" by (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI], assumption+)