src/CCL/Wfd.ML
changeset 757 2ca12511676d
parent 642 0db578095e6a
child 1459 d12da312eff4
     1.1 --- a/src/CCL/Wfd.ML	Wed Nov 30 13:18:42 1994 +0100
     1.2 +++ b/src/CCL/Wfd.ML	Wed Nov 30 13:53:46 1994 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  \    P(a)";
     1.5  by (rtac (major RS spec RS mp RS spec RS CollectD) 1);
     1.6  by (fast_tac (set_cs addSIs [prem RS CollectI]) 1);
     1.7 -val wfd_induct = result();
     1.8 +qed "wfd_induct";
     1.9  
    1.10  val [p1,p2,p3] = goal Wfd.thy
    1.11      "[| !!x y.<x,y> : R ==> Q(x); \
    1.12 @@ -28,7 +28,7 @@
    1.13  \       !!x.Q(x) ==> x:P |] ==> a:P";
    1.14  by (rtac (p2 RS  spec  RS mp) 1);
    1.15  by (fast_tac (set_cs addSIs [p1 RS p3]) 1);
    1.16 -val wfd_strengthen_lemma = result();
    1.17 +qed "wfd_strengthen_lemma";
    1.18  
    1.19  fun wfd_strengthen_tac s i = res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN
    1.20                               assume_tac (i+1);
    1.21 @@ -38,12 +38,12 @@
    1.22  by (fast_tac (FOL_cs addIs prems) 1);
    1.23  by (rtac (wfd RS  wfd_induct) 1);
    1.24  by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
    1.25 -val wf_anti_sym = result();
    1.26 +qed "wf_anti_sym";
    1.27  
    1.28  val prems = goal Wfd.thy "[| Wfd(r);  <a,a>: r |] ==> P";
    1.29  by (rtac wf_anti_sym 1);
    1.30  by (REPEAT (resolve_tac prems 1));
    1.31 -val wf_anti_refl = result();
    1.32 +qed "wf_anti_refl";
    1.33  
    1.34  (*** Irreflexive transitive closure ***)
    1.35  
    1.36 @@ -59,24 +59,24 @@
    1.37  by (fast_tac ccl_cs 1);
    1.38  by (etac (spec RS mp RS spec RS mp) 1);
    1.39  by (REPEAT (atac 1));
    1.40 -val trancl_wf = result();
    1.41 +qed "trancl_wf";
    1.42  
    1.43  (*** Lexicographic Ordering ***)
    1.44  
    1.45  goalw Wfd.thy [lex_def] 
    1.46   "p : ra**rb <-> (EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
    1.47  by (fast_tac ccl_cs 1);
    1.48 -val lexXH = result();
    1.49 +qed "lexXH";
    1.50  
    1.51  val prems = goal Wfd.thy
    1.52   "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb";
    1.53  by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
    1.54 -val lexI1 = result();
    1.55 +qed "lexI1";
    1.56  
    1.57  val prems = goal Wfd.thy
    1.58   "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb";
    1.59  by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
    1.60 -val lexI2 = result();
    1.61 +qed "lexI2";
    1.62  
    1.63  val major::prems = goal Wfd.thy
    1.64   "[| p : ra**rb;  \
    1.65 @@ -86,13 +86,13 @@
    1.66  by (rtac (major RS (lexXH RS iffD1) RS exE) 1);
    1.67  by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
    1.68  by (ALLGOALS (fast_tac ccl_cs));
    1.69 -val lexE = result();
    1.70 +qed "lexE";
    1.71  
    1.72  val [major,minor] = goal Wfd.thy
    1.73   "[| p : r**s;  !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P";
    1.74  by (rtac (major RS lexE) 1);
    1.75  by (ALLGOALS (fast_tac (set_cs addSEs [minor])));
    1.76 -val lex_pair = result();
    1.77 +qed "lex_pair";
    1.78  
    1.79  val [wfa,wfb] = goal Wfd.thy
    1.80   "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)";
    1.81 @@ -105,26 +105,26 @@
    1.82  by (rtac (wfa RS wfd_induct RS allI) 1);
    1.83  by (rtac (wfb RS wfd_induct RS allI) 1);back();
    1.84  by (fast_tac (type_cs addSEs [lexE]) 1);
    1.85 -val lex_wf = result();
    1.86 +qed "lex_wf";
    1.87  
    1.88  (*** Mapping ***)
    1.89  
    1.90  goalw Wfd.thy [wmap_def] 
    1.91   "p : wmap(f,r) <-> (EX x y. p=<x,y>  &  <f(x),f(y)> : r)";
    1.92  by (fast_tac ccl_cs 1);
    1.93 -val wmapXH = result();
    1.94 +qed "wmapXH";
    1.95  
    1.96  val prems = goal Wfd.thy
    1.97   "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)";
    1.98  by (fast_tac (ccl_cs addSIs (prems @ [wmapXH RS iffD2])) 1);
    1.99 -val wmapI = result();
   1.100 +qed "wmapI";
   1.101  
   1.102  val major::prems = goal Wfd.thy
   1.103   "[| p : wmap(f,r);  !!a b.[| <f(a),f(b)> : r;  p=<a,b> |] ==> R |] ==> R";
   1.104  by (rtac (major RS (wmapXH RS iffD1) RS exE) 1);
   1.105  by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
   1.106  by (ALLGOALS (fast_tac ccl_cs));
   1.107 -val wmapE = result();
   1.108 +qed "wmapE";
   1.109  
   1.110  val [wf] = goal Wfd.thy
   1.111   "Wfd(r) ==> Wfd(wmap(f,r))";
   1.112 @@ -139,49 +139,49 @@
   1.113  by (etac (spec RS mp RS spec RS mp) 1);
   1.114  by (assume_tac 1);
   1.115  by (rtac refl 1);
   1.116 -val wmap_wf = result();
   1.117 +qed "wmap_wf";
   1.118  
   1.119  (* Projections *)
   1.120  
   1.121  val prems = goal Wfd.thy "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
   1.122  by (rtac wmapI 1);
   1.123  by (simp_tac (term_ss addsimps prems) 1);
   1.124 -val wfstI = result();
   1.125 +qed "wfstI";
   1.126  
   1.127  val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
   1.128  by (rtac wmapI 1);
   1.129  by (simp_tac (term_ss addsimps prems) 1);
   1.130 -val wsndI = result();
   1.131 +qed "wsndI";
   1.132  
   1.133  val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)";
   1.134  by (rtac wmapI 1);
   1.135  by (simp_tac (term_ss addsimps prems) 1);
   1.136 -val wthdI = result();
   1.137 +qed "wthdI";
   1.138  
   1.139  (*** Ground well-founded relations ***)
   1.140  
   1.141  val prems = goalw Wfd.thy [wf_def] 
   1.142      "[| Wfd(r);  a : r |] ==> a : wf(r)";
   1.143  by (fast_tac (set_cs addSIs prems) 1);
   1.144 -val wfI = result();
   1.145 +qed "wfI";
   1.146  
   1.147  val prems = goalw Wfd.thy [Wfd_def] "Wfd({})";
   1.148  by (fast_tac (set_cs addEs [EmptyXH RS iffD1 RS FalseE]) 1);
   1.149 -val Empty_wf = result();
   1.150 +qed "Empty_wf";
   1.151  
   1.152  val prems = goalw Wfd.thy [wf_def] "Wfd(wf(R))";
   1.153  by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1);
   1.154  by (ALLGOALS (asm_simp_tac CCL_ss));
   1.155  by (rtac Empty_wf 1);
   1.156 -val wf_wf = result();
   1.157 +qed "wf_wf";
   1.158  
   1.159  goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
   1.160  by (fast_tac set_cs 1);
   1.161 -val NatPRXH = result();
   1.162 +qed "NatPRXH";
   1.163  
   1.164  goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
   1.165  by (fast_tac set_cs 1);
   1.166 -val ListPRXH = result();
   1.167 +qed "ListPRXH";
   1.168  
   1.169  val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2));
   1.170  val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2)));
   1.171 @@ -192,7 +192,7 @@
   1.172  by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
   1.173  by (etac Nat_ind 1);
   1.174  by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
   1.175 -val NatPR_wf = result();
   1.176 +qed "NatPR_wf";
   1.177  
   1.178  goalw Wfd.thy [Wfd_def]  "Wfd(ListPR(A))";
   1.179  by (safe_tac set_cs);
   1.180 @@ -200,5 +200,5 @@
   1.181  by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
   1.182  by (etac List_ind 1);
   1.183  by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH])));
   1.184 -val ListPR_wf = result();
   1.185 +qed "ListPR_wf";
   1.186