90 |
90 |
91 (* ------------------------------------------------------------------------ *) |
91 (* ------------------------------------------------------------------------ *) |
92 (* The range of a chain is a totaly ordered << *) |
92 (* The range of a chain is a totaly ordered << *) |
93 (* ------------------------------------------------------------------------ *) |
93 (* ------------------------------------------------------------------------ *) |
94 |
94 |
95 qed_goalw "chain_is_tord" Porder.thy [is_tord] |
95 qed_goalw "chain_is_tord" Porder.thy [is_tord,range_def] |
96 "is_chain(F) ==> is_tord(range(F))" |
96 "is_chain(F) ==> is_tord(range(F))" |
97 ( fn prems => |
97 (fn prems => |
98 [ |
98 [ |
99 (cut_facts_tac prems 1), |
99 (cut_facts_tac prems 1), |
100 (rewrite_goals_tac [range_def]), |
100 (REPEAT (rtac allI 1 )), |
101 (rtac allI 1 ), |
|
102 (rtac allI 1 ), |
|
103 (rtac (mem_Collect_eq RS ssubst) 1), |
101 (rtac (mem_Collect_eq RS ssubst) 1), |
104 (rtac (mem_Collect_eq RS ssubst) 1), |
102 (rtac (mem_Collect_eq RS ssubst) 1), |
105 (strip_tac 1), |
103 (strip_tac 1), |
106 (etac conjE 1), |
104 (etac conjE 1), |
107 (etac exE 1), |
105 (REPEAT (etac exE 1)), |
108 (etac exE 1), |
106 (REPEAT (hyp_subst_tac 1)), |
109 (hyp_subst_tac 1), |
107 (rtac nat_less_cases 1), |
110 (hyp_subst_tac 1), |
|
111 (res_inst_tac [("m","xa"),("n","xb")] (nat_less_cases) 1), |
|
112 (rtac disjI1 1), |
108 (rtac disjI1 1), |
113 (rtac (chain_mono RS mp) 1), |
109 (etac (chain_mono RS mp) 1), |
114 (atac 1), |
|
115 (atac 1), |
110 (atac 1), |
116 (rtac disjI1 1), |
111 (rtac disjI1 1), |
117 (hyp_subst_tac 1), |
112 (hyp_subst_tac 1), |
118 (rtac refl_less 1), |
113 (rtac refl_less 1), |
119 (rtac disjI2 1), |
114 (rtac disjI2 1), |
120 (rtac (chain_mono RS mp) 1), |
115 (etac (chain_mono RS mp) 1), |
121 (atac 1), |
116 (atac 1) |
122 (atac 1) |
117 ]); |
123 ]); |
|
124 |
|
125 |
118 |
126 (* ------------------------------------------------------------------------ *) |
119 (* ------------------------------------------------------------------------ *) |
127 (* technical lemmas about lub and is_lub *) |
120 (* technical lemmas about lub and is_lub *) |
128 (* ------------------------------------------------------------------------ *) |
121 (* ------------------------------------------------------------------------ *) |
129 |
122 |
378 (* ------------------------------------------------------------------------ *) |
371 (* ------------------------------------------------------------------------ *) |
379 (* the maximal element in a chain is its lub *) |
372 (* the maximal element in a chain is its lub *) |
380 (* ------------------------------------------------------------------------ *) |
373 (* ------------------------------------------------------------------------ *) |
381 |
374 |
382 qed_goal "lub_chain_maxelem" Porder.thy |
375 qed_goal "lub_chain_maxelem" Porder.thy |
383 "[|is_chain(Y);? i.Y(i)=c;!i.Y(i)<<c|] ==> lub(range(Y)) = c" |
376 "[|? i.Y(i)=c;!i.Y(i)<<c|] ==> lub(range(Y)) = c" |
384 (fn prems => |
377 (fn prems => |
385 [ |
378 [ |
386 (cut_facts_tac prems 1), |
379 (cut_facts_tac prems 1), |
387 (rtac thelubI 1), |
380 (rtac thelubI 1), |
388 (rtac is_lubI 1), |
381 (rtac is_lubI 1), |
389 (rtac conjI 1), |
382 (rtac conjI 1), |
390 (etac ub_rangeI 1), |
383 (etac ub_rangeI 1), |
391 (strip_tac 1), |
384 (strip_tac 1), |
392 (res_inst_tac [("P","%i.Y(i)=c")] exE 1), |
385 (etac exE 1), |
393 (atac 1), |
|
394 (hyp_subst_tac 1), |
386 (hyp_subst_tac 1), |
395 (etac (ub_rangeE RS spec) 1) |
387 (etac (ub_rangeE RS spec) 1) |
396 ]); |
388 ]); |
397 |
389 |
398 (* ------------------------------------------------------------------------ *) |
390 (* ------------------------------------------------------------------------ *) |