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