src/ZF/OrderType.ML
changeset 807 3abd026e68a4
parent 803 4c8333ab3eae
child 814 a32b420c33d4
equal deleted inserted replaced
806:6330ca0a3ac5 807:3abd026e68a4
   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);