src/ZF/WF.thy
author wenzelm
Wed, 14 May 2008 14:43:37 +0200
changeset 26889 ccea41fb5c39
parent 24893 b8ef7afe3a6b
child 35762 af3ff2ba4c54
permissions -rw-r--r--
names_of: exclude intermediate ids -- less verbosity;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
     1
(*  Title:      ZF/WF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     3
    Author:     Tobias Nipkow and Lawrence C Paulson
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 124
diff changeset
     4
    Copyright   1994  University of Cambridge
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
     6
Derived first for transitive relations, and finally for arbitrary WF relations
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
     7
via wf_trancl and trans_trancl.
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
     8
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
     9
It is difficult to derive this general case directly, using r^+ instead of
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    10
r.  In is_recfun, the two occurrences of the relation must have the same
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    11
form.  Inserting r^+ in the_recfun or wftrec yields a recursion rule with
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    12
r^+ -`` {a} instead of r-``{a}.  This recursion rule is stronger in
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    13
principle, but harder to use, especially to prove wfrec_eclose_eq in
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    14
epsilon.ML.  Expanding out the definition of wftrec in wfrec would yield
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    15
a mess.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    18
header{*Well-Founded Recursion*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    19
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13784
diff changeset
    20
theory WF imports Trancl begin
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    21
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    22
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    23
  wf           :: "i=>o"  where
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    24
    (*r is a well-founded relation*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    25
    "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    26
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    27
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    28
  wf_on        :: "[i,i]=>o"                      ("wf[_]'(_')")  where
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    29
    (*r is well-founded on A*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    30
    "wf_on(A,r) == wf(r Int A*A)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    31
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    32
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    33
  is_recfun    :: "[i, i, [i,i]=>i, i] =>o"  where
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    34
    "is_recfun(r,a,H,f) == (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    35
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    36
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    37
  the_recfun   :: "[i, i, [i,i]=>i] =>i"  where
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    38
    "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    39
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    40
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    41
  wftrec :: "[i, i, [i,i]=>i] =>i"  where
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    42
    "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    43
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    44
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    45
  wfrec :: "[i, i, [i,i]=>i] =>i"  where
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    46
    (*public version.  Does not require r to be transitive*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    47
    "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    48
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    49
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 22710
diff changeset
    50
  wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"       ("wfrec[_]'(_,_,_')")  where
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    51
    "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    52
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    53
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    54
subsection{*Well-Founded Relations*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    55
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
    56
subsubsection{*Equivalences between @{term wf} and @{term wf_on}*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    57
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    58
lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)"
13780
af7b79271364 more new-style theories
paulson
parents: 13634
diff changeset
    59
by (unfold wf_def wf_on_def, force) 
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    60
13248
ae66c22ed52e new theorems
paulson
parents: 13219
diff changeset
    61
lemma wf_on_imp_wf: "[|wf[A](r); r <= A*A|] ==> wf(r)";
ae66c22ed52e new theorems
paulson
parents: 13219
diff changeset
    62
by (simp add: wf_on_def subset_Int_iff)
ae66c22ed52e new theorems
paulson
parents: 13219
diff changeset
    63
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    64
lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    65
by (unfold wf_def wf_on_def, fast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    66
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    67
lemma wf_iff_wf_on_field: "wf(r) <-> wf[field(r)](r)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    68
by (blast intro: wf_imp_wf_on wf_on_field_imp_wf)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    69
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    70
lemma wf_on_subset_A: "[| wf[A](r);  B<=A |] ==> wf[B](r)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    71
by (unfold wf_on_def wf_def, fast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    72
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    73
lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    74
by (unfold wf_on_def wf_def, fast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    75
13217
bc5dc2392578 new theorems
paulson
parents: 13203
diff changeset
    76
lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)"
bc5dc2392578 new theorems
paulson
parents: 13203
diff changeset
    77
by (simp add: wf_def, fast)
bc5dc2392578 new theorems
paulson
parents: 13203
diff changeset
    78
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
    79
subsubsection{*Introduction Rules for @{term wf_on}*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    80
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
    81
text{*If every non-empty subset of @{term A} has an @{term r}-minimal element
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
    82
   then we have @{term "wf[A](r)"}.*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    83
lemma wf_onI:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    84
 assumes prem: "!!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    85
 shows         "wf[A](r)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    86
apply (unfold wf_on_def wf_def)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    87
apply (rule equals0I [THEN disjCI, THEN allI])
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13780
diff changeset
    88
apply (rule_tac Z = Z in prem, blast+)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    89
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    90
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
    91
text{*If @{term r} allows well-founded induction over @{term A}
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
    92
   then we have @{term "wf[A](r)"}.   Premise is equivalent to
22710
f44439cdce77 read prop as prop, not term;
wenzelm
parents: 16417
diff changeset
    93
  @{prop "!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B"} *}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    94
lemma wf_onI2:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    95
 assumes prem: "!!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A |]
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    96
                       ==> y:B"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    97
 shows         "wf[A](r)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    98
apply (rule wf_onI)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
    99
apply (rule_tac c=u in prem [THEN DiffE])
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   100
  prefer 3 apply blast 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   101
 apply fast+
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   102
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   103
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   104
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   105
subsubsection{*Well-founded Induction*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   106
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   107
text{*Consider the least @{term z} in @{term "domain(r)"} such that
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   108
  @{term "P(z)"} does not hold...*}
13534
ca6debb89d77 avoid duplicate fact bindings;
wenzelm
parents: 13357
diff changeset
   109
lemma wf_induct [induct set: wf]:
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   110
    "[| wf(r);
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   111
        !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) |]  
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   112
     ==> P(a)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   113
apply (unfold wf_def) 
13252
8c79a0dce4c0 tweaked
paulson
parents: 13248
diff changeset
   114
apply (erule_tac x = "{z : domain(r). ~ P(z)}" in allE)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   115
apply blast 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   116
done
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 124
diff changeset
   117
13534
ca6debb89d77 avoid duplicate fact bindings;
wenzelm
parents: 13357
diff changeset
   118
lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf]
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13175
diff changeset
   119
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   120
text{*The form of this rule is designed to match @{text wfI}*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   121
lemma wf_induct2:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   122
    "[| wf(r);  a:A;  field(r)<=A;
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   123
        !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) |]
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   124
     ==>  P(a)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   125
apply (erule_tac P="a:A" in rev_mp)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   126
apply (erule_tac a=a in wf_induct, blast) 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   127
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   128
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   129
lemma field_Int_square: "field(r Int A*A) <= A"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   130
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   131
13534
ca6debb89d77 avoid duplicate fact bindings;
wenzelm
parents: 13357
diff changeset
   132
lemma wf_on_induct [consumes 2, induct set: wf_on]:
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   133
    "[| wf[A](r);  a:A;
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   134
        !!x.[| x: A;  ALL y:A. <y,x>: r --> P(y) |] ==> P(x)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   135
     |]  ==>  P(a)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   136
apply (unfold wf_on_def) 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   137
apply (erule wf_induct2, assumption)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   138
apply (rule field_Int_square, blast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   139
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   140
13534
ca6debb89d77 avoid duplicate fact bindings;
wenzelm
parents: 13357
diff changeset
   141
lemmas wf_on_induct_rule =
ca6debb89d77 avoid duplicate fact bindings;
wenzelm
parents: 13357
diff changeset
   142
  wf_on_induct [rule_format, consumes 2, induct set: wf_on]
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13175
diff changeset
   143
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13175
diff changeset
   144
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   145
text{*If @{term r} allows well-founded induction 
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   146
   then we have @{term "wf(r)"}.*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   147
lemma wfI:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   148
    "[| field(r)<=A;
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   149
        !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;  y:A|]
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   150
               ==> y:B |]
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   151
     ==>  wf(r)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   152
apply (rule wf_on_subset_A [THEN wf_on_field_imp_wf])
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   153
apply (rule wf_onI2)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   154
 prefer 2 apply blast  
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   155
apply blast 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   156
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   157
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   158
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   159
subsection{*Basic Properties of Well-Founded Relations*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   160
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   161
lemma wf_not_refl: "wf(r) ==> <a,a> ~: r"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   162
by (erule_tac a=a in wf_induct, blast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   163
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   164
lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. <a,x>:r --> <x,a> ~: r"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   165
by (erule_tac a=a in wf_induct, blast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   166
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   167
(* [| wf(r);  <a,x> : r;  ~P ==> <x,a> : r |] ==> P *)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   168
lemmas wf_asym = wf_not_sym [THEN swap, standard]
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   169
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   170
lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> <a,a> ~: r"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13252
diff changeset
   171
by (erule_tac a=a in wf_on_induct, assumption, blast)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   173
lemma wf_on_not_sym [rule_format]:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   174
     "[| wf[A](r);  a:A |] ==> ALL b:A. <a,b>:r --> <b,a>~:r"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13252
diff changeset
   175
apply (erule_tac a=a in wf_on_induct, assumption, blast)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   176
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   177
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   178
lemma wf_on_asym:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   179
     "[| wf[A](r);  ~Z ==> <a,b> : r;
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   180
         <b,a> ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13252
diff changeset
   181
by (blast dest: wf_on_not_sym) 
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   182
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   183
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   184
(*Needed to prove well_ordI.  Could also reason that wf[A](r) means
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   185
  wf(r Int A*A);  thus wf( (r Int A*A)^+ ) and use wf_not_refl *)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   186
lemma wf_on_chain3:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   187
     "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   188
apply (subgoal_tac "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P",
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   189
       blast) 
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13252
diff changeset
   190
apply (erule_tac a=a in wf_on_induct, assumption, blast)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   191
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   192
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   193
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   194
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   195
text{*transitive closure of a WF relation is WF provided 
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   196
  @{term A} is downward closed*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   197
lemma wf_on_trancl:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   198
    "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   199
apply (rule wf_onI2)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   200
apply (frule bspec [THEN mp], assumption+)
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13780
diff changeset
   201
apply (erule_tac a = y in wf_on_induct, assumption)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   202
apply (blast elim: tranclE, blast) 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   203
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   204
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   205
lemma wf_trancl: "wf(r) ==> wf(r^+)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   206
apply (simp add: wf_iff_wf_on_field)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   207
apply (rule wf_on_subset_A) 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   208
 apply (erule wf_on_trancl)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   209
 apply blast 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   210
apply (rule trancl_type [THEN field_rel_subset])
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   211
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   212
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   213
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   214
text{*@{term "r-``{a}"} is the set of everything under @{term a} in @{term r}*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   215
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   216
lemmas underI = vimage_singleton_iff [THEN iffD2, standard]
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   217
lemmas underD = vimage_singleton_iff [THEN iffD1, standard]
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   218
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   219
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   220
subsection{*The Predicate @{term is_recfun}*}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   222
lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   223
apply (unfold is_recfun_def)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   224
apply (erule ssubst)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   225
apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   226
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   227
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13252
diff changeset
   228
lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function]
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13252
diff changeset
   229
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   230
lemma apply_recfun:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   231
    "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   232
apply (unfold is_recfun_def) 
13175
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13165
diff changeset
   233
  txt{*replace f only on the left-hand side*}
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13165
diff changeset
   234
apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13252
diff changeset
   235
apply (simp add: underI) 
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   236
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   237
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   238
lemma is_recfun_equal [rule_format]:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   239
     "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |]
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   240
      ==> <x,a>:r --> <x,b>:r --> f`x=g`x"
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13780
diff changeset
   241
apply (frule_tac f = f in is_recfun_type)
b9f6154427a4 tidying (by script)
paulson
parents: 13780
diff changeset
   242
apply (frule_tac f = g in is_recfun_type)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   243
apply (simp add: is_recfun_def)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   244
apply (erule_tac a=x in wf_induct)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   245
apply (intro impI)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   246
apply (elim ssubst)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   247
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   248
apply (rule_tac t = "%z. H (?x,z) " in subst_context)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   249
apply (subgoal_tac "ALL y : r-``{x}. ALL z. <y,z>:f <-> <y,z>:g")
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   250
 apply (blast dest: transD)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   251
apply (simp add: apply_iff)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   252
apply (blast dest: transD intro: sym)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   253
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   254
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   255
lemma is_recfun_cut:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   256
     "[| wf(r);  trans(r);
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   257
         is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |]
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   258
      ==> restrict(f, r-``{b}) = g"
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13780
diff changeset
   259
apply (frule_tac f = f in is_recfun_type)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   260
apply (rule fun_extension)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   261
  apply (blast dest: transD intro: restrict_type2)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   262
 apply (erule is_recfun_type, simp)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   263
apply (blast dest: transD intro: is_recfun_equal)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   264
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   265
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   266
subsection{*Recursion: Main Existence Lemma*}
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 124
diff changeset
   267
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   268
lemma is_recfun_functional:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   269
     "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   270
by (blast intro: fun_extension is_recfun_type is_recfun_equal)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   271
13248
ae66c22ed52e new theorems
paulson
parents: 13219
diff changeset
   272
lemma the_recfun_eq:
ae66c22ed52e new theorems
paulson
parents: 13219
diff changeset
   273
    "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |] ==> the_recfun(r,a,H) = f"
ae66c22ed52e new theorems
paulson
parents: 13219
diff changeset
   274
apply (unfold the_recfun_def)
ae66c22ed52e new theorems
paulson
parents: 13219
diff changeset
   275
apply (blast intro: is_recfun_functional)
ae66c22ed52e new theorems
paulson
parents: 13219
diff changeset
   276
done
ae66c22ed52e new theorems
paulson
parents: 13219
diff changeset
   277
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   278
(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   279
lemma is_the_recfun:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   280
    "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   281
     ==> is_recfun(r, a, H, the_recfun(r,a,H))"
13248
ae66c22ed52e new theorems
paulson
parents: 13219
diff changeset
   282
by (simp add: the_recfun_eq)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   283
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   284
lemma unfold_the_recfun:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   285
     "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   286
apply (rule_tac a=a in wf_induct, assumption)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   287
apply (rename_tac a1) 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   288
apply (rule_tac f = "lam y: r-``{a1}. wftrec (r,y,H)" in is_the_recfun)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   289
  apply typecheck
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   290
apply (unfold is_recfun_def wftrec_def)
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   291
  --{*Applying the substitution: must keep the quantified assumption!*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   292
apply (rule lam_cong [OF refl]) 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   293
apply (drule underD) 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   294
apply (fold is_recfun_def)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   295
apply (rule_tac t = "%z. H(?x,z)" in subst_context)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   296
apply (rule fun_extension)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   297
  apply (blast intro: is_recfun_type)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   298
 apply (rule lam_type [THEN restrict_type2])
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   299
  apply blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   300
 apply (blast dest: transD)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   301
apply (frule spec [THEN mp], assumption)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   302
apply (subgoal_tac "<xa,a1> : r")
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13780
diff changeset
   303
 apply (drule_tac x1 = xa in spec [THEN mp], assumption)
13175
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13165
diff changeset
   304
apply (simp add: vimage_singleton_iff 
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   305
                 apply_recfun is_recfun_cut)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   306
apply (blast dest: transD)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   307
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   308
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   309
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   310
subsection{*Unfolding @{term "wftrec(r,a,H)"}*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   311
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   312
lemma the_recfun_cut:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   313
     "[| wf(r);  trans(r);  <b,a>:r |]
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   314
      ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13252
diff changeset
   315
by (blast intro: is_recfun_cut unfold_the_recfun)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   317
(*NOT SUITABLE FOR REWRITING: it is recursive!*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   318
lemma wftrec:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   319
    "[| wf(r);  trans(r) |] ==>
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   320
          wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   321
apply (unfold wftrec_def)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   322
apply (subst unfold_the_recfun [unfolded is_recfun_def])
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   323
apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   324
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   325
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   326
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   327
subsubsection{*Removal of the Premise @{term "trans(r)"}*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   328
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   329
(*NOT SUITABLE FOR REWRITING: it is recursive!*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   330
lemma wfrec:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   331
    "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   332
apply (unfold wfrec_def) 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   333
apply (erule wf_trancl [THEN wftrec, THEN ssubst])
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   334
 apply (rule trans_trancl)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   335
apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context])
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   336
 apply (erule r_into_trancl)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   337
apply (rule subset_refl)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   338
done
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   340
(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   341
lemma def_wfrec:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   342
    "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==>
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   343
     h(a) = H(a, lam x: r-``{a}. h(x))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   344
apply simp
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   345
apply (elim wfrec) 
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   346
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   347
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   348
lemma wfrec_type:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   349
    "[| wf(r);  a:A;  field(r)<=A;
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   350
        !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   351
     |] ==> wfrec(r,a,H) : B(a)"
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13780
diff changeset
   352
apply (rule_tac a = a in wf_induct2, assumption+)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   353
apply (subst wfrec, assumption)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   354
apply (simp add: lam_type underD)  
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   355
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   356
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   357
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   358
lemma wfrec_on:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   359
 "[| wf[A](r);  a: A |] ==>
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   360
         wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   361
apply (unfold wf_on_def wfrec_on_def)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   362
apply (erule wfrec [THEN trans])
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   363
apply (simp add: vimage_Int_square cons_subset_iff)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   364
done
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   366
text{*Minimal-element characterization of well-foundedness*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   367
lemma wf_eq_minimal:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 3840
diff changeset
   368
     "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q))"
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   369
by (unfold wf_def, blast)
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13534
diff changeset
   370
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
end