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