src/ZF/Order.ML

 Goalw [part_ord_def, irrefl_def, trans_on_def, asym_def]
     "part_ord(A,r) ==> asym(r Int A*A)";
 by (Blast_tac 1);
 qed "part_ord_Imp_asym";
 
-val major::premx::premy::prems = goalw Order.thy [linear_def]
+val major::premx::premy::prems = Goalw [linear_def]
     "[| linear(A,r);  x:A;  y:A;  \
 \       <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |] ==> P";
 by (cut_facts_tac [major,premx,premy] 1);
 by (REPEAT_FIRST (eresolve_tac [ballE,disjE]));
 by (EVERY1 (map etac prems));

 by (Blast_tac 1);
 qed "pred_iff";
 
 bind_thm ("predI", conjI RS (pred_iff RS iffD2));
 
-val [major,minor] = goalw Order.thy [pred_def]
+val [major,minor] = Goalw [pred_def]
     "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P";
 by (rtac (major RS CollectE) 1);
 by (REPEAT (ares_tac [minor] 1));
 qed "predE";
 

 qed "mono_map_is_inj";
 
 
 (** Order-isomorphisms -- or similarities, as Suppes calls them **)
 
-val prems = goalw Order.thy [ord_iso_def]
+val prems = Goalw [ord_iso_def]
     "[| f: bij(A, B);   \
 \       !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s \
 \    |] ==> f: ord_iso(A,r,B,s)";
 by (blast_tac (claset() addSIs prems) 1);
 qed "ord_isoI";

 by (subgoal_tac "<g`(f`x), g`(f`y)> : r" 1);
 by (blast_tac (claset() addIs [apply_funtype]) 2);
 by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff RS iffD1]) 1);
 qed "mono_ord_isoI";
 
-Goal
-    "[| well_ord(A,r);  well_ord(B,s);                             \
+Goal "[| well_ord(A,r);  well_ord(B,s);                             \
 \            f: mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r)      \
 \         |] ==> f: ord_iso(A,r,B,s)";
 by (REPEAT (ares_tac [mono_ord_isoI] 1));
 by (forward_tac [mono_map_is_fun RS fun_is_rel] 1);
 by (etac (converse_converse RS subst) 1 THEN rtac left_comp_inverse 1);

 by (Blast_tac 1);
 qed "well_ord_iso_subset_lemma";
 
 (*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
                      of a well-ordering*)
-Goal
-    "[| well_ord(A,r);  f : ord_iso(A, r, pred(A,x,r), r);  x:A |] ==> P";
+Goal "[| well_ord(A,r);  f : ord_iso(A, r, pred(A,x,r), r);  x:A |] ==> P";
 by (metacut_tac well_ord_iso_subset_lemma 1);
 by (REPEAT_FIRST (ares_tac [pred_subset]));
 (*Now we know  f`x < x *)
 by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type),
              assume_tac]);
 (*Now we also know f`x : pred(A,x,r);  contradiction! *)
 by (asm_full_simp_tac (simpset() addsimps [well_ord_def, pred_def]) 1);
 qed "well_ord_iso_predE";
 
 (*Simple consequence of Lemma 6.1*)
-Goal
- "[| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);  \
+Goal "[| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);  \
 \         a:A;  c:A |] ==> a=c";
 by (forward_tac [well_ord_is_trans_on] 1);
 by (forward_tac [well_ord_is_linear] 1);
 by (linear_case_tac 1);
 by (dtac ord_iso_sym 1);

 by (asm_simp_tac bij_inverse_ss 1);
 qed "ord_iso_image_pred";
 
 (*But in use, A and B may themselves be initial segments.  Then use
   trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
-Goal
- "[| f : ord_iso(A,r,B,s);   a:A |] ==>    \
+Goal "[| f : ord_iso(A,r,B,s);   a:A |] ==>    \
 \      restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)";
 by (asm_simp_tac (simpset() addsimps [ord_iso_image_pred RS sym]) 1);
 by (rewtac ord_iso_def);
 by (etac CollectE 1);
 by (rtac CollectI 1);
 by (asm_full_simp_tac (simpset() addsimps [pred_def]) 2);
 by (eresolve_tac [[bij_is_inj, pred_subset] MRS restrict_bij] 1);
 qed "ord_iso_restrict_pred";
 
 (*Tricky; a lot of forward proof!*)
-Goal
- "[| well_ord(A,r);  well_ord(B,s);  <a,c>: r;     \
+Goal "[| well_ord(A,r);  well_ord(B,s);  <a,c>: r;     \
 \         f : ord_iso(pred(A,a,r), r, pred(B,b,s), s);  \
 \         g : ord_iso(pred(A,c,r), r, pred(B,d,s), s);  \
 \         a:A;  c:A;  b:B;  d:B |] ==> <b,d>: s";
 by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1  THEN
     REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1));

 
 val  bij_apply_cs = claset() addSIs [bij_converse_bij]
                             addIs  [ord_iso_is_bij, bij_is_fun, apply_funtype];
 
 (*See Halmos, page 72*)
-Goal
-    "[| well_ord(A,r);  \
+Goal "[| well_ord(A,r);  \
 \            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |] \
 \         ==> ~ <g`y, f`y> : s";
 by (forward_tac [well_ord_iso_subset_lemma] 1);
 by (res_inst_tac [("f","converse(f)"), ("g","g")] ord_iso_trans 1);
 by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym]));

 by (EVERY (map (blast_tac bij_apply_cs) [1,1,1]));
 by (asm_full_simp_tac bij_inverse_ss 1);
 qed "well_ord_iso_unique_lemma";
 
 (*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
-Goal
-    "[| well_ord(A,r);  \
+Goal "[| well_ord(A,r);  \
 \            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g";
 by (rtac fun_extension 1);
 by (REPEAT (etac (ord_iso_is_bij RS bij_is_fun) 1));
 by (subgoals_tac ["f`x : B", "g`x : B", "linear(B,s)"] 1);
 by (REPEAT (blast_tac bij_apply_cs 3));

     "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))";
 by (blast_tac (claset() addIs [well_ord_iso_pred_eq, 
 			      ord_iso_sym, ord_iso_trans]) 1);
 qed "function_ord_iso_map";
 
-Goal
-    "well_ord(B,s) ==> ord_iso_map(A,r,B,s)        \
+Goal "well_ord(B,s) ==> ord_iso_map(A,r,B,s)        \
 \          : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))";
 by (asm_simp_tac 
     (simpset() addsimps [Pi_iff, function_ord_iso_map,
                      ord_iso_map_subset RS domain_times_range]) 1);
 qed "ord_iso_map_fun";

     (simpset() addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1);
 by (Blast_tac 1);
 qed "domain_ord_iso_map_subset";
 
 (*For the 4-way case analysis in the main result*)
-Goal
-  "[| well_ord(A,r);  well_ord(B,s) |] ==> \
+Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
 \       domain(ord_iso_map(A,r,B,s)) = A |      \
 \       (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))";
 by (forward_tac [well_ord_is_wf] 1);
 by (rewrite_goals_tac [wf_on_def, wf_def]);
 by (dres_inst_tac [("x", "A-domain(ord_iso_map(A,r,B,s))")] spec 1);

 by (blast_tac (claset() addSEs [predE]) 2);
 by (REPEAT (ares_tac [domain_ord_iso_map_subset] 1));
 qed "domain_ord_iso_map_cases";
 
 (*As above, by duality*)
-Goal
-  "[| well_ord(A,r);  well_ord(B,s) |] ==> \
+Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
 \       range(ord_iso_map(A,r,B,s)) = B |       \
 \       (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))";
 by (resolve_tac [converse_ord_iso_map RS subst] 1);
 by (asm_simp_tac
     (simpset() addsimps [range_converse, domain_ord_iso_map_cases]) 1);
 qed "range_ord_iso_map_cases";
 
 (*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
-Goal
-  "[| well_ord(A,r);  well_ord(B,s) |] ==>         \
+Goal "[| well_ord(A,r);  well_ord(B,s) |] ==>         \
 \       ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) |    \
 \       (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | \
 \       (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))";
 by (forw_inst_tac [("B","B")] domain_ord_iso_map_cases 1);
 by (forw_inst_tac [("B","B")] range_ord_iso_map_cases 2);