src/CCL/Wfd.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 8 c3d2c6dcf3f0
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	CCL/wf
     2     ID:         $Id$
     3 
     4 For wf.thy.
     5 
     6 Based on
     7     Titles: 	ZF/wf.ML and HOL/ex/lex-prod
     8     Authors: 	Lawrence C Paulson and Tobias Nipkow
     9     Copyright   1992  University of Cambridge
    10 
    11 *)
    12 
    13 open Wfd;
    14 
    15 (***********)
    16 
    17 val wfd_congs = mk_congs Wfd.thy ["Wfd","wf","op **","wmap","ListPR"];
    18 
    19 (***********)
    20 
    21 val [major,prem] = goalw Wfd.thy [Wfd_def]
    22     "[| Wfd(R);       \
    23 \       !!x.[| ALL y. <y,x>: R --> P(y) |] ==> P(x) |]  ==>  \
    24 \    P(a)";
    25 by (rtac (major RS spec RS mp RS spec RS CollectD) 1);
    26 by (fast_tac (set_cs addSIs [prem RS CollectI]) 1);
    27 val wfd_induct = result();
    28 
    29 val [p1,p2,p3] = goal Wfd.thy
    30     "[| !!x y.<x,y> : R ==> Q(x); \
    31 \       ALL x. (ALL y. <y,x> : R --> y : P) --> x : P; \
    32 \       !!x.Q(x) ==> x:P |] ==> a:P";
    33 br (p2 RS  spec  RS mp) 1;
    34 by (fast_tac (set_cs addSIs [p1 RS p3]) 1);
    35 val wfd_strengthen_lemma = result();
    36 
    37 fun wfd_strengthen_tac s i = res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN
    38                              assume_tac (i+1);
    39 
    40 val wfd::prems = goal Wfd.thy "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P";
    41 by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
    42 by (fast_tac (FOL_cs addIs prems) 1);
    43 br (wfd RS  wfd_induct) 1;
    44 by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
    45 val wf_anti_sym = result();
    46 
    47 val prems = goal Wfd.thy "[| Wfd(r);  <a,a>: r |] ==> P";
    48 by (rtac wf_anti_sym 1);
    49 by (REPEAT (resolve_tac prems 1));
    50 val wf_anti_refl = result();
    51 
    52 (*** Irreflexive transitive closure ***)
    53 
    54 val [prem] = goal Wfd.thy "Wfd(R) ==> Wfd(R^+)";
    55 by (rewtac Wfd_def);
    56 by (REPEAT (ares_tac [allI,ballI,impI] 1));
    57 (*must retain the universal formula for later use!*)
    58 by (rtac allE 1 THEN assume_tac 1);
    59 by (etac mp 1);
    60 br (prem RS wfd_induct) 1;
    61 by (rtac (impI RS allI) 1);
    62 by (etac tranclE 1);
    63 by (fast_tac ccl_cs 1);
    64 be (spec RS mp RS spec RS mp) 1;
    65 by (REPEAT (atac 1));
    66 val trancl_wf = result();
    67 
    68 (*** Lexicographic Ordering ***)
    69 
    70 goalw Wfd.thy [lex_def] 
    71  "p : ra**rb <-> (EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
    72 by (fast_tac ccl_cs 1);
    73 val lexXH = result();
    74 
    75 val prems = goal Wfd.thy
    76  "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb";
    77 by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
    78 val lexI1 = result();
    79 
    80 val prems = goal Wfd.thy
    81  "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb";
    82 by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
    83 val lexI2 = result();
    84 
    85 val major::prems = goal Wfd.thy
    86  "[| p : ra**rb;  \
    87 \    !!a a' b b'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R;  \
    88 \    !!a b b'.[| <b,b'> : rb;  p = <<a,b>,<a,b'>> |] ==> R  |] ==> \
    89 \ R";
    90 br (major RS (lexXH RS iffD1) RS exE) 1;
    91 by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
    92 by (ALLGOALS (fast_tac ccl_cs));
    93 val lexE = result();
    94 
    95 val [major,minor] = goal Wfd.thy
    96  "[| p : r**s;  !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P";
    97 br (major RS lexE) 1;
    98 by (ALLGOALS (fast_tac (set_cs addSEs [minor])));
    99 val lex_pair = result();
   100 
   101 val [wfa,wfb] = goal Wfd.thy
   102  "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)";
   103 bw Wfd_def;
   104 by (safe_tac ccl_cs);
   105 by (wfd_strengthen_tac "%x.EX a b.x=<a,b>" 1);
   106 by (fast_tac (term_cs addSEs [lex_pair]) 1);
   107 by (subgoal_tac "ALL a b.<a,b>:P" 1);
   108 by (fast_tac ccl_cs 1);
   109 br (wfa RS wfd_induct RS allI) 1;
   110 br (wfb RS wfd_induct RS allI) 1;back();
   111 by (fast_tac (type_cs addSEs [lexE]) 1);
   112 val lex_wf = result();
   113 
   114 (*** Mapping ***)
   115 
   116 goalw Wfd.thy [wmap_def] 
   117  "p : wmap(f,r) <-> (EX x y. p=<x,y>  &  <f(x),f(y)> : r)";
   118 by (fast_tac ccl_cs 1);
   119 val wmapXH = result();
   120 
   121 val prems = goal Wfd.thy
   122  "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)";
   123 by (fast_tac (ccl_cs addSIs (prems @ [wmapXH RS iffD2])) 1);
   124 val wmapI = result();
   125 
   126 val major::prems = goal Wfd.thy
   127  "[| p : wmap(f,r);  !!a b.[| <f(a),f(b)> : r;  p=<a,b> |] ==> R |] ==> R";
   128 br (major RS (wmapXH RS iffD1) RS exE) 1;
   129 by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
   130 by (ALLGOALS (fast_tac ccl_cs));
   131 val wmapE = result();
   132 
   133 val [wf] = goal Wfd.thy
   134  "Wfd(r) ==> Wfd(wmap(f,r))";
   135 bw Wfd_def;
   136 by (safe_tac ccl_cs);
   137 by (subgoal_tac "ALL b.ALL a.f(a)=b-->a:P" 1);
   138 by (fast_tac ccl_cs 1);
   139 br (wf RS wfd_induct RS allI) 1;
   140 by (safe_tac ccl_cs);
   141 be (spec RS mp) 1;
   142 by (safe_tac (ccl_cs addSEs [wmapE]));
   143 be (spec RS mp RS spec RS mp) 1;
   144 ba 1;
   145 br refl 1;
   146 val wmap_wf = result();
   147 
   148 (* Projections *)
   149 
   150 val prems = goal Wfd.thy "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
   151 br wmapI 1;
   152 by (SIMP_TAC (term_ss addrews prems) 1);
   153 val wfstI = result();
   154 
   155 val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
   156 br wmapI 1;
   157 by (SIMP_TAC (term_ss addrews prems) 1);
   158 val wsndI = result();
   159 
   160 val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)";
   161 br wmapI 1;
   162 by (SIMP_TAC (term_ss addrews prems) 1);
   163 val wthdI = result();
   164 
   165 (*** Ground well-founded relations ***)
   166 
   167 val prems = goalw Wfd.thy [wf_def] 
   168     "[| Wfd(r);  a : r |] ==> a : wf(r)";
   169 by (fast_tac (set_cs addSIs prems) 1);
   170 val wfI = result();
   171 
   172 val prems = goalw Wfd.thy [Wfd_def] "Wfd({})";
   173 by (fast_tac (set_cs addEs [EmptyXH RS iffD1 RS FalseE]) 1);
   174 val Empty_wf = result();
   175 
   176 val prems = goalw Wfd.thy [wf_def] "Wfd(wf(R))";
   177 by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1);
   178 by (ALLGOALS (ASM_SIMP_TAC (CCL_ss addcongs wfd_congs)));
   179 br Empty_wf 1;
   180 val wf_wf = result();
   181 
   182 goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
   183 by (fast_tac set_cs 1);
   184 val NatPRXH = result();
   185 
   186 goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)";
   187 by (fast_tac set_cs 1);
   188 val ListPRXH = result();
   189 
   190 val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2));
   191 val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2)));
   192 
   193 goalw Wfd.thy [Wfd_def]  "Wfd(NatPR)";
   194 by (safe_tac set_cs);
   195 by (wfd_strengthen_tac "%x.x:Nat" 1);
   196 by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
   197 be Nat_ind 1;
   198 by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
   199 val NatPR_wf = result();
   200 
   201 goalw Wfd.thy [Wfd_def]  "Wfd(ListPR(A))";
   202 by (safe_tac set_cs);
   203 by (wfd_strengthen_tac "%x.x:List(A)" 1);
   204 by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
   205 be List_ind 1;
   206 by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH])));
   207 val ListPR_wf = result();
   208