src/ZF/Main_ZF.thy
author wenzelm
Wed, 19 Mar 2008 22:47:35 +0100
changeset 26339 7825c83c9eff
parent 26056 6a0801279f4c
child 29580 117b88da143c
permissions -rw-r--r--
eliminated change_claset/simpset;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     1
(*$Id$*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     2
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     3
header{*Theory Main: Everything Except AC*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     4
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     5
theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     6
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     7
(*The theory of "iterates" logically belongs to Nat, but can't go there because
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     8
  primrec isn't available into after Datatype.*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     9
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    10
subsection{* Iteration of the function @{term F} *}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    11
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    12
consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    13
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    14
primrec
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    15
    "F^0 (x) = x"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    16
    "F^(succ(n)) (x) = F(F^n (x))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    17
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    18
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    19
  iterates_omega :: "[i=>i,i] => i"  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    20
    "iterates_omega(F,x) == \<Union>n\<in>nat. F^n (x)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    21
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    22
notation (xsymbols)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    23
  iterates_omega  ("(_^\<omega> '(_'))" [60,1000] 60)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    24
notation (HTML output)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    25
  iterates_omega  ("(_^\<omega> '(_'))" [60,1000] 60)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    26
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    27
lemma iterates_triv:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    28
     "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"  
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    29
by (induct n rule: nat_induct, simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    30
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    31
lemma iterates_type [TC]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    32
     "[| n:nat;  a: A; !!x. x:A ==> F(x) : A |] 
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    33
      ==> F^n (a) : A"  
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    34
by (induct n rule: nat_induct, simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    35
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    36
lemma iterates_omega_triv:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    37
    "F(x) = x ==> F^\<omega> (x) = x" 
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    38
by (simp add: iterates_omega_def iterates_triv) 
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    39
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    40
lemma Ord_iterates [simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    41
     "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |] 
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    42
      ==> Ord(F^n (x))"  
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    43
by (induct n rule: nat_induct, simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    44
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    45
lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    46
by (induct_tac n, simp_all)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    47
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    48
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    49
subsection{* Transfinite Recursion *}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    50
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    51
text{*Transfinite recursion for definitions based on the 
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    52
    three cases of ordinals*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    53
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    54
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    55
  transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    56
    "transrec3(k, a, b, c) ==                     
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    57
       transrec(k, \<lambda>x r.
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    58
         if x=0 then a
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    59
         else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    60
         else b(Arith.pred(x), r ` Arith.pred(x)))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    61
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    62
lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    63
by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    64
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    65
lemma transrec3_succ [simp]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    66
     "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    67
by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    68
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    69
lemma transrec3_Limit:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    70
     "Limit(i) ==> 
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    71
      transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    72
by (rule transrec3_def [THEN def_transrec, THEN trans], force)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    73
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    74
26339
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 26056
diff changeset
    75
declaration {* fn _ =>
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 26056
diff changeset
    76
  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    77
*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    78
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    79
end