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