src/CCL/wfd.ML
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 289 78541329ff35
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.
lcp@226
     1
(*  Title: 	CCL/wfd.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
lcp@226
     4
For wfd.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@289
   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