# HG changeset patch # User paulson # Date 1250774605 -7200 # Node ID f3fed9cc423f1d15ae76c2e3dae005c371c9f7b3 # Parent a97e9caebd60ae95fb749ffda721a562856fa9ba A few Isar scripts diff -r a97e9caebd60 -r f3fed9cc423f src/ZF/ex/Limit.thy --- a/src/ZF/ex/Limit.thy Sat Aug 15 15:29:54 2009 +0200 +++ b/src/ZF/ex/Limit.thy Thu Aug 20 15:23:25 2009 +0200 @@ -488,18 +488,24 @@ and Mfun: "M \ nat->nat->set(D)" and cpoD: "cpo(D)" shows "matrix(D,M)" -apply (simp add: matrix_def, safe) -apply (rule Mfun) -apply (cut_tac y1 = m and n = n in yprem [THEN chain_rel], simp+) -apply (simp add: chain_rel xprem) -apply (rule cpo_trans [OF cpoD]) -apply (cut_tac y1 = m and n = n in yprem [THEN chain_rel], simp+) -apply (simp_all add: chain_fun [THEN apply_type] xprem) -done - -lemma lemma_rel_rel: - "[|m \ nat; rel(D, (\n \ nat. M`n`n)`m, y)|] ==> rel(D,M`m`m, y)" -by simp +proof - + { + fix n m assume "n : nat" "m : nat" + with chain_rel [OF yprem] + have "rel(D, M ` n ` m, M ` succ(n) ` m)" by simp + } note rel_succ = this + show "matrix(D,M)" + proof (simp add: matrix_def Mfun rel_succ, intro conjI ballI) + fix n m assume n: "n : nat" and m: "m : nat" + thus "rel(D, M ` n ` m, M ` n ` succ(m))" + by (simp add: chain_rel xprem) + next + fix n m assume n: "n : nat" and m: "m : nat" + thus "rel(D, M ` n ` m, M ` succ(n) ` succ(m))" + by (rule cpo_trans [OF cpoD rel_succ], + simp_all add: chain_fun [THEN apply_type] xprem) + qed +qed lemma lemma2: "[|x \ nat; m \ nat; rel(D,(\n \ nat. M`n`m1)`x,(\n \ nat. M`n`m1)`m)|] @@ -509,65 +515,72 @@ lemma isub_lemma: "[|isub(D, \n \ nat. M`n`n, y); matrix(D,M); cpo(D)|] ==> isub(D, \n \ nat. lub(D,\m \ nat. M`n`m), y)" -apply (unfold isub_def, safe) -apply (simp (no_asm_simp)) -apply (frule matrix_fun [THEN apply_type], assumption) -apply (simp (no_asm_simp)) -apply (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], assumption+) -apply (unfold isub_def, safe) -(*???VERY indirect proof: beta-redexes could be simplified now!*) -apply (rename_tac k n) -apply (case_tac "k le n") -apply (rule cpo_trans, assumption) -apply (rule lemma2) -apply (rule_tac [4] lemma_rel_rel) -prefer 5 apply blast -apply (assumption | rule chain_rel_gen matrix_chain_right matrix_in isubD1)+ -txt{*opposite case*} -apply (rule cpo_trans, assumption) -apply (rule not_le_iff_lt [THEN iffD1, THEN leI, THEN chain_rel_gen]) -prefer 3 apply assumption -apply (assumption | rule nat_into_Ord matrix_chain_left)+ -apply (rule lemma_rel_rel) -apply (simp_all add: matrix_in) -done +proof (simp add: isub_def, safe) + fix n + assume DM: "matrix(D, M)" and D: "cpo(D)" and n: "n \ nat" and y: "y \ set(D)" + and rel: "\n\nat. rel(D, M ` n ` n, y)" + have "rel(D, lub(D, M ` n), y)" + proof (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], simp_all add: n D DM) + show "isub(D, M ` n, y)" + proof (unfold isub_def, intro conjI ballI y) + fix k assume k: "k \ nat" + show "rel(D, M ` n ` k, y)" + proof (cases "n le k") + case True + hence yy: "rel(D, M`n`k, M`k`k)" + by (blast intro: lemma2 n k y DM D chain_rel_gen matrix_chain_right) + show "?thesis" + by (rule cpo_trans [OF D yy], + simp_all add: k rel n y DM matrix_in) + next + case False + hence le: "k le n" + by (blast intro: not_le_iff_lt [THEN iffD1, THEN leI] nat_into_Ord n k) + show "?thesis" + by (rule cpo_trans [OF D chain_rel_gen [OF le]], + simp_all add: n y k rel DM D matrix_chain_left) + qed + qed + qed + moreover + have "M ` n \ nat \ set(D)" by (blast intro: DM n matrix_fun [THEN apply_type]) + ultimately show "rel(D, lub(D, Lambda(nat, op `(M ` n))), y)" by simp +qed lemma matrix_chain_lub: "[|matrix(D,M); cpo(D)|] ==> chain(D,\n \ nat. lub(D,\m \ nat. M`n`m))" -apply (simp add: chain_def, safe) -apply (rule lam_type) -apply (rule islub_in) -apply (rule cpo_lub) -prefer 2 apply assumption -apply (rule chainI) -apply (rule lam_type) -apply (simp_all add: matrix_in) -apply (rule matrix_rel_0_1, assumption+) -apply (simp add: matrix_chain_left [THEN chain_fun, THEN eta]) -apply (rule dominate_islub) -apply (rule_tac [3] cpo_lub) -apply (rule_tac [2] cpo_lub) -apply (simp add: dominate_def) -apply (blast intro: matrix_rel_1_0) -apply (simp_all add: matrix_chain_left nat_succI chain_fun) -done +proof (simp add: chain_def, intro conjI ballI) + assume "matrix(D, M)" "cpo(D)" + thus "(\x\nat. lub(D, Lambda(nat, op `(M ` x)))) \ nat \ set(D)" + by (force intro: islub_in cpo_lub chainI lam_type matrix_in matrix_rel_0_1) +next + fix n + assume DD: "matrix(D, M)" "cpo(D)" "n \ nat" + hence "dominate(D, M ` n, M ` succ(n))" + by (force simp add: dominate_def intro: matrix_rel_1_0) + with DD show "rel(D, lub(D, Lambda(nat, op `(M ` n))), + lub(D, Lambda(nat, op `(M ` succ(n)))))" + by (simp add: matrix_chain_left [THEN chain_fun, THEN eta] + dominate_islub cpo_lub matrix_chain_left chain_fun) +qed lemma isub_eq: - "[|matrix(D,M); cpo(D)|] - ==> isub(D,(\n \ nat. lub(D,\m \ nat. M`n`m)),y) <-> - isub(D,(\n \ nat. M`n`n),y)" -apply (rule iffI) -apply (rule dominate_isub) -prefer 2 apply assumption -apply (simp add: dominate_def) -apply (rule ballI) -apply (rule bexI, auto) -apply (simp add: matrix_chain_left [THEN chain_fun, THEN eta]) -apply (rule islub_ub) -apply (rule cpo_lub) -apply (simp_all add: matrix_chain_left matrix_chain_diag chain_fun - matrix_chain_lub isub_lemma) -done + assumes DM: "matrix(D, M)" and D: "cpo(D)" + shows "isub(D,(\n \ nat. lub(D,\m \ nat. M`n`m)),y) <-> isub(D,(\n \ nat. M`n`n),y)" +proof + assume isub: "isub(D, \n\nat. lub(D, Lambda(nat, op `(M ` n))), y)" + hence dom: "dominate(D, \n\nat. M ` n ` n, \n\nat. lub(D, Lambda(nat, op `(M ` n))))" + using DM D + by (simp add: dominate_def, intro ballI bexI, + simp_all add: matrix_chain_left [THEN chain_fun, THEN eta] islub_ub cpo_lub matrix_chain_left) + thus "isub(D, \n\nat. M ` n ` n, y)" using DM D + by - (rule dominate_isub [OF dom isub], + simp_all add: matrix_chain_diag chain_fun matrix_chain_lub) +next + assume isub: "isub(D, \n\nat. M ` n ` n, y)" + thus "isub(D, \n\nat. lub(D, Lambda(nat, op `(M ` n))), y)" using DM D + by (simp add: isub_lemma) +qed lemma lub_matrix_diag_aux1: "lub(D,(\n \ nat. lub(D,\m \ nat. M`n`m))) = @@ -695,34 +708,43 @@ "[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |] ==> matrix(E,\x \ nat. \xa \ nat. X`x`(Xa`xa))" apply (rule matrix_chainI, auto) -apply (rule chainI) -apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in, simp) -apply (blast intro: cont_mono nat_succI chain_rel cf_cont chain_in) -apply (rule chainI) -apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in, simp) -apply (rule rel_cf) -apply (simp_all add: chain_in chain_rel) +apply (force intro: chainI lam_type apply_funtype cont_fun cf_cont cont_mono) +apply (force intro: chainI lam_type apply_funtype cont_fun cf_cont rel_cf) apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in) done lemma chain_cf_lub_cont: - "[|chain(cf(D,E),X); cpo(D); cpo(E) |] - ==> (\x \ set(D). lub(E, \n \ nat. X ` n ` x)) \ cont(D, E)" -apply (rule contI) -apply (rule lam_type) -apply (assumption | rule chain_cf [THEN cpo_lub, THEN islub_in])+ -apply simp -apply (rule dominate_islub) -apply (erule_tac [2] chain_cf [THEN cpo_lub], simp_all)+ -apply (rule dominateI, assumption, simp) -apply (assumption | rule chain_in [THEN cf_cont, THEN cont_mono])+ -apply (assumption | rule chain_cf [THEN chain_fun])+ -apply (simp add: cpo_lub [THEN islub_in] - chain_in [THEN cf_cont, THEN cont_lub]) -apply (frule matrix_lemma [THEN lub_matrix_diag], assumption+) -apply (simp add: chain_in [THEN beta]) -apply (drule matrix_lemma [THEN lub_matrix_diag_sym], auto) -done + assumes ch: "chain(cf(D,E),X)" and D: "cpo(D)" and E: "cpo(E)" + shows "(\x \ set(D). lub(E, \n \ nat. X ` n ` x)) \ cont(D, E)" +proof (rule contI) + show "(\x\set(D). lub(E, \n\nat. X ` n ` x)) \ set(D) \ set(E)" + by (blast intro: lam_type chain_cf [THEN cpo_lub, THEN islub_in] ch E) +next + fix x y + assume xy: "rel(D, x, y)" "x \ set(D)" "y \ set(D)" + hence dom: "dominate(E, \n\nat. X ` n ` x, \n\nat. X ` n ` y)" + by (force intro: dominateI chain_in [OF ch, THEN cf_cont, THEN cont_mono]) + note chE = chain_cf [OF ch] + from xy show "rel(E, (\x\set(D). lub(E, \n\nat. X ` n ` x)) ` x, + (\x\set(D). lub(E, \n\nat. X ` n ` x)) ` y)" + by (simp add: dominate_islub [OF dom] cpo_lub [OF chE] E chain_fun [OF chE]) +next + fix Y + assume chDY: "chain(D,Y)" + have "lub(E, \x\nat. lub(E, \y\nat. X ` x ` (Y ` y))) = + lub(E, \x\nat. X ` x ` (Y ` x))" + using matrix_lemma [THEN lub_matrix_diag, OF ch chDY] + by (simp add: D E) + also have "... = lub(E, \x\nat. lub(E, \n\nat. X ` n ` (Y ` x)))" + using matrix_lemma [THEN lub_matrix_diag_sym, OF ch chDY] + by (simp add: D E) + finally have "lub(E, \x\nat. lub(E, \n\nat. X ` x ` (Y ` n))) = + lub(E, \x\nat. lub(E, \n\nat. X ` n ` (Y ` x)))" . + thus "(\x\set(D). lub(E, \n\nat. X ` n ` x)) ` lub(D, Y) = + lub(E, \n\nat. (\x\set(D). lub(E, \n\nat. X ` n ` x)) ` (Y ` n))" + by (simp add: cpo_lub [THEN islub_in] D chDY + chain_in [THEN cf_cont, THEN cont_lub, OF ch]) + qed lemma islub_cf: "[| chain(cf(D,E),X); cpo(D); cpo(E)|]