141 by (REPEAT (resolve_tac [ballI, Ord_linear] 1));; |
141 by (REPEAT (resolve_tac [ballI, Ord_linear] 1));; |
142 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));; |
142 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));; |
143 qed "well_ord_Memrel"; |
143 qed "well_ord_Memrel"; |
144 |
144 |
145 goal OrderType.thy "!!i. [| Ord(i); j:i |] ==> ordermap(i,Memrel(i)) ` j = j"; |
145 goal OrderType.thy "!!i. [| Ord(i); j:i |] ==> ordermap(i,Memrel(i)) ` j = j"; |
146 by (eresolve_tac [Ord_induct] 1); |
146 by (etac Ord_induct 1); |
147 ba 1; |
147 by (assume_tac 1); |
148 by (asm_simp_tac (ZF_ss addsimps |
148 by (asm_simp_tac (ZF_ss addsimps |
149 [well_ord_Memrel RS well_ord_is_wf RS ordermap_pred_unfold]) 1); |
149 [well_ord_Memrel RS well_ord_is_wf RS ordermap_pred_unfold]) 1); |
150 by (asm_simp_tac (ZF_ss addsimps [pred_def, Memrel_iff]) 1); |
150 by (asm_simp_tac (ZF_ss addsimps [pred_def, Memrel_iff]) 1); |
151 by (dresolve_tac [OrdmemD] 1); |
151 by (dtac OrdmemD 1); |
152 by (assume_tac 1); |
152 by (assume_tac 1); |
153 by (fast_tac eq_cs 1); |
153 by (fast_tac eq_cs 1); |
154 qed "ordermap_Memrel"; |
154 qed "ordermap_Memrel"; |
155 |
155 |
156 goal OrderType.thy "!!i. Ord(i) ==> ordertype(i,Memrel(i)) = i"; |
156 goal OrderType.thy "!!i. Ord(i) ==> ordertype(i,Memrel(i)) = i"; |
195 by (asm_simp_tac |
195 by (asm_simp_tac |
196 (ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1); |
196 (ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1); |
197 (*combining these two simplifications LOOPS! *) |
197 (*combining these two simplifications LOOPS! *) |
198 by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1); |
198 by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1); |
199 by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1); |
199 by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1); |
200 br (refl RSN (2,RepFun_cong)) 1; |
200 by (rtac (refl RSN (2,RepFun_cong)) 1); |
201 bd well_ord_is_trans_on 1; |
201 by (dtac well_ord_is_trans_on 1); |
202 by (fast_tac (eq_cs addSEs [trans_onD]) 1); |
202 by (fast_tac (eq_cs addSEs [trans_onD]) 1); |
203 qed "ordermap_pred_eq_ordermap"; |
203 qed "ordermap_pred_eq_ordermap"; |
204 |
204 |
205 |
205 |
206 goal OrderType.thy |
206 goal OrderType.thy |
227 |
227 |
228 goal OrderType.thy |
228 goal OrderType.thy |
229 "!!i. [| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) \ |
229 "!!i. [| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) \ |
230 \ |] ==> R"; |
230 \ |] ==> R"; |
231 by (forward_tac [lt_eq_pred] 1); |
231 by (forward_tac [lt_eq_pred] 1); |
232 be ltE 1; |
232 by (etac ltE 1); |
233 by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN |
233 by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN |
234 assume_tac 3 THEN assume_tac 1); |
234 assume_tac 3 THEN assume_tac 1); |
235 be subst 1; |
235 by (etac subst 1); |
236 by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1); |
236 by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1); |
237 (*Combining the two simplifications causes looping*) |
237 (*Combining the two simplifications causes looping*) |
238 by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); |
238 by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); |
239 by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type] |
239 by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type] |
240 addEs [Ord_trans]) 1); |
240 addEs [Ord_trans]) 1); |