src/CCL/Wfd.ML
changeset 642 0db578095e6a
parent 289 78541329ff35
child 757 2ca12511676d
     1.1 --- a/src/CCL/Wfd.ML	Wed Oct 12 16:38:58 1994 +0100
     1.2 +++ b/src/CCL/Wfd.ML	Wed Oct 19 09:23:56 1994 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4      "[| !!x y.<x,y> : R ==> Q(x); \
     1.5  \       ALL x. (ALL y. <y,x> : R --> y : P) --> x : P; \
     1.6  \       !!x.Q(x) ==> x:P |] ==> a:P";
     1.7 -br (p2 RS  spec  RS mp) 1;
     1.8 +by (rtac (p2 RS  spec  RS mp) 1);
     1.9  by (fast_tac (set_cs addSIs [p1 RS p3]) 1);
    1.10  val wfd_strengthen_lemma = result();
    1.11  
    1.12 @@ -36,7 +36,7 @@
    1.13  val wfd::prems = goal Wfd.thy "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P";
    1.14  by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
    1.15  by (fast_tac (FOL_cs addIs prems) 1);
    1.16 -br (wfd RS  wfd_induct) 1;
    1.17 +by (rtac (wfd RS  wfd_induct) 1);
    1.18  by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
    1.19  val wf_anti_sym = result();
    1.20  
    1.21 @@ -53,11 +53,11 @@
    1.22  (*must retain the universal formula for later use!*)
    1.23  by (rtac allE 1 THEN assume_tac 1);
    1.24  by (etac mp 1);
    1.25 -br (prem RS wfd_induct) 1;
    1.26 +by (rtac (prem RS wfd_induct) 1);
    1.27  by (rtac (impI RS allI) 1);
    1.28  by (etac tranclE 1);
    1.29  by (fast_tac ccl_cs 1);
    1.30 -be (spec RS mp RS spec RS mp) 1;
    1.31 +by (etac (spec RS mp RS spec RS mp) 1);
    1.32  by (REPEAT (atac 1));
    1.33  val trancl_wf = result();
    1.34  
    1.35 @@ -83,27 +83,27 @@
    1.36  \    !!a a' b b'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R;  \
    1.37  \    !!a b b'.[| <b,b'> : rb;  p = <<a,b>,<a,b'>> |] ==> R  |] ==> \
    1.38  \ R";
    1.39 -br (major RS (lexXH RS iffD1) RS exE) 1;
    1.40 +by (rtac (major RS (lexXH RS iffD1) RS exE) 1);
    1.41  by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
    1.42  by (ALLGOALS (fast_tac ccl_cs));
    1.43  val lexE = result();
    1.44  
    1.45  val [major,minor] = goal Wfd.thy
    1.46   "[| p : r**s;  !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P";
    1.47 -br (major RS lexE) 1;
    1.48 +by (rtac (major RS lexE) 1);
    1.49  by (ALLGOALS (fast_tac (set_cs addSEs [minor])));
    1.50  val lex_pair = result();
    1.51  
    1.52  val [wfa,wfb] = goal Wfd.thy
    1.53   "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)";
    1.54 -bw Wfd_def;
    1.55 +by (rewtac Wfd_def);
    1.56  by (safe_tac ccl_cs);
    1.57  by (wfd_strengthen_tac "%x.EX a b.x=<a,b>" 1);
    1.58  by (fast_tac (term_cs addSEs [lex_pair]) 1);
    1.59  by (subgoal_tac "ALL a b.<a,b>:P" 1);
    1.60  by (fast_tac ccl_cs 1);
    1.61 -br (wfa RS wfd_induct RS allI) 1;
    1.62 -br (wfb RS wfd_induct RS allI) 1;back();
    1.63 +by (rtac (wfa RS wfd_induct RS allI) 1);
    1.64 +by (rtac (wfb RS wfd_induct RS allI) 1);back();
    1.65  by (fast_tac (type_cs addSEs [lexE]) 1);
    1.66  val lex_wf = result();
    1.67  
    1.68 @@ -121,40 +121,40 @@
    1.69  
    1.70  val major::prems = goal Wfd.thy
    1.71   "[| p : wmap(f,r);  !!a b.[| <f(a),f(b)> : r;  p=<a,b> |] ==> R |] ==> R";
    1.72 -br (major RS (wmapXH RS iffD1) RS exE) 1;
    1.73 +by (rtac (major RS (wmapXH RS iffD1) RS exE) 1);
    1.74  by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
    1.75  by (ALLGOALS (fast_tac ccl_cs));
    1.76  val wmapE = result();
    1.77  
    1.78  val [wf] = goal Wfd.thy
    1.79   "Wfd(r) ==> Wfd(wmap(f,r))";
    1.80 -bw Wfd_def;
    1.81 +by (rewtac Wfd_def);
    1.82  by (safe_tac ccl_cs);
    1.83  by (subgoal_tac "ALL b.ALL a.f(a)=b-->a:P" 1);
    1.84  by (fast_tac ccl_cs 1);
    1.85 -br (wf RS wfd_induct RS allI) 1;
    1.86 +by (rtac (wf RS wfd_induct RS allI) 1);
    1.87  by (safe_tac ccl_cs);
    1.88 -be (spec RS mp) 1;
    1.89 +by (etac (spec RS mp) 1);
    1.90  by (safe_tac (ccl_cs addSEs [wmapE]));
    1.91 -be (spec RS mp RS spec RS mp) 1;
    1.92 -ba 1;
    1.93 -br refl 1;
    1.94 +by (etac (spec RS mp RS spec RS mp) 1);
    1.95 +by (assume_tac 1);
    1.96 +by (rtac refl 1);
    1.97  val wmap_wf = result();
    1.98  
    1.99  (* Projections *)
   1.100  
   1.101  val prems = goal Wfd.thy "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
   1.102 -br wmapI 1;
   1.103 +by (rtac wmapI 1);
   1.104  by (simp_tac (term_ss addsimps prems) 1);
   1.105  val wfstI = result();
   1.106  
   1.107  val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
   1.108 -br wmapI 1;
   1.109 +by (rtac wmapI 1);
   1.110  by (simp_tac (term_ss addsimps prems) 1);
   1.111  val wsndI = result();
   1.112  
   1.113  val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)";
   1.114 -br wmapI 1;
   1.115 +by (rtac wmapI 1);
   1.116  by (simp_tac (term_ss addsimps prems) 1);
   1.117  val wthdI = result();
   1.118  
   1.119 @@ -172,7 +172,7 @@
   1.120  val prems = goalw Wfd.thy [wf_def] "Wfd(wf(R))";
   1.121  by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1);
   1.122  by (ALLGOALS (asm_simp_tac CCL_ss));
   1.123 -br Empty_wf 1;
   1.124 +by (rtac Empty_wf 1);
   1.125  val wf_wf = result();
   1.126  
   1.127  goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
   1.128 @@ -190,7 +190,7 @@
   1.129  by (safe_tac set_cs);
   1.130  by (wfd_strengthen_tac "%x.x:Nat" 1);
   1.131  by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
   1.132 -be Nat_ind 1;
   1.133 +by (etac Nat_ind 1);
   1.134  by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
   1.135  val NatPR_wf = result();
   1.136  
   1.137 @@ -198,7 +198,7 @@
   1.138  by (safe_tac set_cs);
   1.139  by (wfd_strengthen_tac "%x.x:List(A)" 1);
   1.140  by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
   1.141 -be List_ind 1;
   1.142 +by (etac List_ind 1);
   1.143  by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH])));
   1.144  val ListPR_wf = result();
   1.145