src/CCL/Wfd.ML
changeset 0 a5a9c433f639
child 8 c3d2c6dcf3f0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/Wfd.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,208 @@
     1.4 +(*  Title: 	CCL/wf
     1.5 +    ID:         $Id$
     1.6 +
     1.7 +For wf.thy.
     1.8 +
     1.9 +Based on
    1.10 +    Titles: 	ZF/wf.ML and HOL/ex/lex-prod
    1.11 +    Authors: 	Lawrence C Paulson and Tobias Nipkow
    1.12 +    Copyright   1992  University of Cambridge
    1.13 +
    1.14 +*)
    1.15 +
    1.16 +open Wfd;
    1.17 +
    1.18 +(***********)
    1.19 +
    1.20 +val wfd_congs = mk_congs Wfd.thy ["Wfd","wf","op **","wmap","ListPR"];
    1.21 +
    1.22 +(***********)
    1.23 +
    1.24 +val [major,prem] = goalw Wfd.thy [Wfd_def]
    1.25 +    "[| Wfd(R);       \
    1.26 +\       !!x.[| ALL y. <y,x>: R --> P(y) |] ==> P(x) |]  ==>  \
    1.27 +\    P(a)";
    1.28 +by (rtac (major RS spec RS mp RS spec RS CollectD) 1);
    1.29 +by (fast_tac (set_cs addSIs [prem RS CollectI]) 1);
    1.30 +val wfd_induct = result();
    1.31 +
    1.32 +val [p1,p2,p3] = goal Wfd.thy
    1.33 +    "[| !!x y.<x,y> : R ==> Q(x); \
    1.34 +\       ALL x. (ALL y. <y,x> : R --> y : P) --> x : P; \
    1.35 +\       !!x.Q(x) ==> x:P |] ==> a:P";
    1.36 +br (p2 RS  spec  RS mp) 1;
    1.37 +by (fast_tac (set_cs addSIs [p1 RS p3]) 1);
    1.38 +val wfd_strengthen_lemma = result();
    1.39 +
    1.40 +fun wfd_strengthen_tac s i = res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN
    1.41 +                             assume_tac (i+1);
    1.42 +
    1.43 +val wfd::prems = goal Wfd.thy "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P";
    1.44 +by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
    1.45 +by (fast_tac (FOL_cs addIs prems) 1);
    1.46 +br (wfd RS  wfd_induct) 1;
    1.47 +by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
    1.48 +val wf_anti_sym = result();
    1.49 +
    1.50 +val prems = goal Wfd.thy "[| Wfd(r);  <a,a>: r |] ==> P";
    1.51 +by (rtac wf_anti_sym 1);
    1.52 +by (REPEAT (resolve_tac prems 1));
    1.53 +val wf_anti_refl = result();
    1.54 +
    1.55 +(*** Irreflexive transitive closure ***)
    1.56 +
    1.57 +val [prem] = goal Wfd.thy "Wfd(R) ==> Wfd(R^+)";
    1.58 +by (rewtac Wfd_def);
    1.59 +by (REPEAT (ares_tac [allI,ballI,impI] 1));
    1.60 +(*must retain the universal formula for later use!*)
    1.61 +by (rtac allE 1 THEN assume_tac 1);
    1.62 +by (etac mp 1);
    1.63 +br (prem RS wfd_induct) 1;
    1.64 +by (rtac (impI RS allI) 1);
    1.65 +by (etac tranclE 1);
    1.66 +by (fast_tac ccl_cs 1);
    1.67 +be (spec RS mp RS spec RS mp) 1;
    1.68 +by (REPEAT (atac 1));
    1.69 +val trancl_wf = result();
    1.70 +
    1.71 +(*** Lexicographic Ordering ***)
    1.72 +
    1.73 +goalw Wfd.thy [lex_def] 
    1.74 + "p : ra**rb <-> (EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
    1.75 +by (fast_tac ccl_cs 1);
    1.76 +val lexXH = result();
    1.77 +
    1.78 +val prems = goal Wfd.thy
    1.79 + "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb";
    1.80 +by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
    1.81 +val lexI1 = result();
    1.82 +
    1.83 +val prems = goal Wfd.thy
    1.84 + "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb";
    1.85 +by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
    1.86 +val lexI2 = result();
    1.87 +
    1.88 +val major::prems = goal Wfd.thy
    1.89 + "[| p : ra**rb;  \
    1.90 +\    !!a a' b b'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R;  \
    1.91 +\    !!a b b'.[| <b,b'> : rb;  p = <<a,b>,<a,b'>> |] ==> R  |] ==> \
    1.92 +\ R";
    1.93 +br (major RS (lexXH RS iffD1) RS exE) 1;
    1.94 +by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
    1.95 +by (ALLGOALS (fast_tac ccl_cs));
    1.96 +val lexE = result();
    1.97 +
    1.98 +val [major,minor] = goal Wfd.thy
    1.99 + "[| p : r**s;  !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P";
   1.100 +br (major RS lexE) 1;
   1.101 +by (ALLGOALS (fast_tac (set_cs addSEs [minor])));
   1.102 +val lex_pair = result();
   1.103 +
   1.104 +val [wfa,wfb] = goal Wfd.thy
   1.105 + "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)";
   1.106 +bw Wfd_def;
   1.107 +by (safe_tac ccl_cs);
   1.108 +by (wfd_strengthen_tac "%x.EX a b.x=<a,b>" 1);
   1.109 +by (fast_tac (term_cs addSEs [lex_pair]) 1);
   1.110 +by (subgoal_tac "ALL a b.<a,b>:P" 1);
   1.111 +by (fast_tac ccl_cs 1);
   1.112 +br (wfa RS wfd_induct RS allI) 1;
   1.113 +br (wfb RS wfd_induct RS allI) 1;back();
   1.114 +by (fast_tac (type_cs addSEs [lexE]) 1);
   1.115 +val lex_wf = result();
   1.116 +
   1.117 +(*** Mapping ***)
   1.118 +
   1.119 +goalw Wfd.thy [wmap_def] 
   1.120 + "p : wmap(f,r) <-> (EX x y. p=<x,y>  &  <f(x),f(y)> : r)";
   1.121 +by (fast_tac ccl_cs 1);
   1.122 +val wmapXH = result();
   1.123 +
   1.124 +val prems = goal Wfd.thy
   1.125 + "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)";
   1.126 +by (fast_tac (ccl_cs addSIs (prems @ [wmapXH RS iffD2])) 1);
   1.127 +val wmapI = result();
   1.128 +
   1.129 +val major::prems = goal Wfd.thy
   1.130 + "[| p : wmap(f,r);  !!a b.[| <f(a),f(b)> : r;  p=<a,b> |] ==> R |] ==> R";
   1.131 +br (major RS (wmapXH RS iffD1) RS exE) 1;
   1.132 +by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
   1.133 +by (ALLGOALS (fast_tac ccl_cs));
   1.134 +val wmapE = result();
   1.135 +
   1.136 +val [wf] = goal Wfd.thy
   1.137 + "Wfd(r) ==> Wfd(wmap(f,r))";
   1.138 +bw Wfd_def;
   1.139 +by (safe_tac ccl_cs);
   1.140 +by (subgoal_tac "ALL b.ALL a.f(a)=b-->a:P" 1);
   1.141 +by (fast_tac ccl_cs 1);
   1.142 +br (wf RS wfd_induct RS allI) 1;
   1.143 +by (safe_tac ccl_cs);
   1.144 +be (spec RS mp) 1;
   1.145 +by (safe_tac (ccl_cs addSEs [wmapE]));
   1.146 +be (spec RS mp RS spec RS mp) 1;
   1.147 +ba 1;
   1.148 +br refl 1;
   1.149 +val wmap_wf = result();
   1.150 +
   1.151 +(* Projections *)
   1.152 +
   1.153 +val prems = goal Wfd.thy "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
   1.154 +br wmapI 1;
   1.155 +by (SIMP_TAC (term_ss addrews prems) 1);
   1.156 +val wfstI = result();
   1.157 +
   1.158 +val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
   1.159 +br wmapI 1;
   1.160 +by (SIMP_TAC (term_ss addrews prems) 1);
   1.161 +val wsndI = result();
   1.162 +
   1.163 +val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)";
   1.164 +br wmapI 1;
   1.165 +by (SIMP_TAC (term_ss addrews prems) 1);
   1.166 +val wthdI = result();
   1.167 +
   1.168 +(*** Ground well-founded relations ***)
   1.169 +
   1.170 +val prems = goalw Wfd.thy [wf_def] 
   1.171 +    "[| Wfd(r);  a : r |] ==> a : wf(r)";
   1.172 +by (fast_tac (set_cs addSIs prems) 1);
   1.173 +val wfI = result();
   1.174 +
   1.175 +val prems = goalw Wfd.thy [Wfd_def] "Wfd({})";
   1.176 +by (fast_tac (set_cs addEs [EmptyXH RS iffD1 RS FalseE]) 1);
   1.177 +val Empty_wf = result();
   1.178 +
   1.179 +val prems = goalw Wfd.thy [wf_def] "Wfd(wf(R))";
   1.180 +by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1);
   1.181 +by (ALLGOALS (ASM_SIMP_TAC (CCL_ss addcongs wfd_congs)));
   1.182 +br Empty_wf 1;
   1.183 +val wf_wf = result();
   1.184 +
   1.185 +goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
   1.186 +by (fast_tac set_cs 1);
   1.187 +val NatPRXH = result();
   1.188 +
   1.189 +goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)";
   1.190 +by (fast_tac set_cs 1);
   1.191 +val ListPRXH = result();
   1.192 +
   1.193 +val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2));
   1.194 +val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2)));
   1.195 +
   1.196 +goalw Wfd.thy [Wfd_def]  "Wfd(NatPR)";
   1.197 +by (safe_tac set_cs);
   1.198 +by (wfd_strengthen_tac "%x.x:Nat" 1);
   1.199 +by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
   1.200 +be Nat_ind 1;
   1.201 +by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
   1.202 +val NatPR_wf = result();
   1.203 +
   1.204 +goalw Wfd.thy [Wfd_def]  "Wfd(ListPR(A))";
   1.205 +by (safe_tac set_cs);
   1.206 +by (wfd_strengthen_tac "%x.x:List(A)" 1);
   1.207 +by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
   1.208 +be List_ind 1;
   1.209 +by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH])));
   1.210 +val ListPR_wf = result();
   1.211 +