src/ZF/Epsilon.ML
changeset 9211 6236c5285bd8
parent 8201 a81d18b0a9b1
child 9907 473a6604da94
     1.1 --- a/src/ZF/Epsilon.ML	Fri Jun 30 12:49:11 2000 +0200
     1.2 +++ b/src/ZF/Epsilon.ML	Fri Jun 30 12:51:30 2000 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  bind_thm ("eclose_induct", Transset_eclose RSN (2, Transset_induct));
     1.5  
     1.6  (*Epsilon induction*)
     1.7 -val prems = goal Epsilon.thy
     1.8 +val prems = Goal
     1.9      "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)";
    1.10  by (rtac (arg_in_eclose_sing RS eclose_induct) 1);
    1.11  by (eresolve_tac prems 1);
    1.12 @@ -74,7 +74,7 @@
    1.13  qed "eclose_least";
    1.14  
    1.15  (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
    1.16 -val [major,base,step] = goal Epsilon.thy
    1.17 +val [major,base,step] = Goal
    1.18      "[| a: eclose(b);                                           \
    1.19  \       !!y.   [| y: b |] ==> P(y);                             \
    1.20  \       !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)        \
    1.21 @@ -126,10 +126,10 @@
    1.22                                    jmemi RSN (2,mem_eclose_sing_trans)]) 1);
    1.23  qed "wfrec_eclose_eq";
    1.24  
    1.25 -val [prem] = goal Epsilon.thy
    1.26 +Goal
    1.27      "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)";
    1.28  by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1);
    1.29 -by (rtac (prem RS arg_into_eclose_sing) 1);
    1.30 +by (etac arg_into_eclose_sing 1);
    1.31  qed "wfrec_eclose_eq2";
    1.32  
    1.33  Goalw [transrec_def]
    1.34 @@ -140,13 +140,13 @@
    1.35  qed "transrec";
    1.36  
    1.37  (*Avoids explosions in proofs; resolve it with a meta-level definition.*)
    1.38 -val rew::prems = goal Epsilon.thy
    1.39 +val rew::prems = Goal
    1.40      "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))";
    1.41  by (rewtac rew);
    1.42  by (REPEAT (resolve_tac (prems@[transrec]) 1));
    1.43  qed "def_transrec";
    1.44  
    1.45 -val prems = goal Epsilon.thy
    1.46 +val prems = Goal
    1.47      "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
    1.48  \    |]  ==> transrec(a,H) : B(a)";
    1.49  by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
    1.50 @@ -159,7 +159,7 @@
    1.51  by (rtac (succI1 RS singleton_subsetI) 1);
    1.52  qed "eclose_sing_Ord";
    1.53  
    1.54 -val prems = goal Epsilon.thy
    1.55 +val prems = Goal
    1.56      "[| j: i;  Ord(i);  \
    1.57  \       !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
    1.58  \    |]  ==> transrec(j,H) : B(j)";
    1.59 @@ -186,8 +186,8 @@
    1.60  qed "Ord_rank";
    1.61  Addsimps [Ord_rank];
    1.62  
    1.63 -val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
    1.64 -by (rtac (major RS trans_induct) 1);
    1.65 +Goal "Ord(i) ==> rank(i) = i";
    1.66 +by (etac trans_induct 1);
    1.67  by (stac rank 1);
    1.68  by (asm_simp_tac (simpset() addsimps [Ord_equality]) 1);
    1.69  qed "rank_of_Ord";
    1.70 @@ -199,8 +199,8 @@
    1.71  by Auto_tac;
    1.72  qed "rank_lt";
    1.73  
    1.74 -val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)";
    1.75 -by (rtac (major RS eclose_induct_down) 1);
    1.76 +Goal "a: eclose(b) ==> rank(a) < rank(b)";
    1.77 +by (etac eclose_induct_down 1);
    1.78  by (etac rank_lt 1);
    1.79  by (etac (rank_lt RS lt_trans) 1);
    1.80  by (assume_tac 1);