doc-src/HOL/HOL-rules.txt
author wenzelm
Wed, 26 Jul 2006 00:44:44 +0200
changeset 20207 4c57e850e8d5
parent 6580 ff2c3ffd38ee
permissions -rw-r--r--
added Pure/subgoal.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6580
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
     1
ruleshell.ML lemmas.ML set.ML fun.ML subset.ML equalities.ML prod.ML sum.ML wf.ML mono.ML fixedpt.ML nat.ML list.ML
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
     2
----------------------------------------------------------------
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
     3
ruleshell.ML
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
     4
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
     5
\idx{refl}      t = t::'a
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
     6
\idx{subst}     [| s = t; P(s) |] ==> P(t::'a)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
     7
\idx{abs},!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x)))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
     8
\idx{disch}     (P ==> Q) ==> P-->Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
     9
\idx{mp}        [| P-->Q;  P |] ==> Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    10
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    11
\idx{True_def}  True = ((%x.x)=(%x.x))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    12
\idx{All_def}   All  = (%P. P = (%x.True))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    13
\idx{Ex_def}    Ex   = (%P. P(Eps(P)))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    14
\idx{False_def} False = (!P.P)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    15
\idx{not_def}   not  = (%P. P-->False)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    16
\idx{and_def}   op & = (%P Q. !R. (P-->Q-->R) --> R)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    17
\idx{or_def}    op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    18
\idx{Ex1_def}   Ex1 == (%P. ? x. P(x) & (! y. P(y) --> y=x))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    19
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    20
\idx{iff}       (P-->Q) --> (Q-->P) --> (P=Q)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    21
\idx{True_or_False}     (P=True) | (P=False)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    22
\idx{select}    P(x::'a) --> P(Eps(P))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    23
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    24
\idx{Inv_def}   Inv = (%(f::'a=>'b) y. @x. f(x)=y)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    25
\idx{o_def}     op o = (%(f::'b=>'c) g (x::'a). f(g(x)))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    26
\idx{Cond_def}  Cond = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    27
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    28
----------------------------------------------------------------
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    29
lemmas.ML
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    30
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    31
\idx{sym}    s=t ==> t=s
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    32
\idx{trans}    [| r=s; s=t |] ==> r=t
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    33
\idx{box_equals}    
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    34
    [| a=b;  a=c;  b=d |] ==> c=d  
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    35
\idx{ap_term}    s=t ==> f(s)=f(t)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    36
\idx{ap_thm}    s::'a=>'b = t ==> s(x)=t(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    37
\idx{cong}    
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    38
   [| f = g; x::'a = y |] ==> f(x) = g(y)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    39
\idx{iffI}    
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    40
   [| P ==> Q;  Q ==> P |] ==> P=Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    41
\idx{iffD1}    [| P=Q; Q |] ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    42
\idx{iffE}    
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    43
    [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    44
\idx{eqTrueI}    P ==> P=True 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    45
\idx{eqTrueE}    P=True ==> P 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    46
\idx{allI}    (!!x::'a. P(x)) ==> !x. P(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    47
\idx{spec}    !x::'a.P(x) ==> P(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    48
\idx{allE}    [| !x.P(x);  P(x) ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    49
\idx{all_dupE}    
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    50
    [| ! x.P(x);  [| P(x); ! x.P(x) |] ==> R 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    51
    |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    52
\idx{FalseE}    False ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    53
\idx{False_neq_True}    False=True ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    54
\idx{notI}    (P ==> False) ==> ~P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    55
\idx{notE}    [| ~P;  P |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    56
\idx{impE}    [| P-->Q;  P;  Q ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    57
\idx{rev_mp}    [| P;  P --> Q |] ==> Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    58
\idx{contrapos}    [| ~Q;  P==>Q |] ==> ~P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    59
\idx{exI}    P(x) ==> ? x::'a.P(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    60
\idx{exE}    [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    61
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    62
\idx{conjI}    [| P; Q |] ==> P&Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    63
\idx{conjunct1}    [| P & Q |] ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    64
\idx{conjunct2}    [| P & Q |] ==> Q 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    65
\idx{conjE}    [| P&Q;  [| P; Q |] ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    66
\idx{disjI1}    P ==> P|Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    67
\idx{disjI2}    Q ==> P|Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    68
\idx{disjE}    [| P | Q; P ==> R; Q ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    69
\idx{ccontr}    (~P ==> False) ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    70
\idx{classical}    (~P ==> P) ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    71
\idx{notnotD}    ~~P ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    72
\idx{ex1I}    
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    73
    [| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    74
\idx{ex1E}    
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    75
    [| ?! x.P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    76
\idx{select_equality}    
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    77
    [| P(a);  !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    78
\idx{disjCI}    (~Q ==> P) ==> P|Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    79
\idx{excluded_middle}    ~P | P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    80
\idx{impCE}    [| P-->Q; ~P ==> R; Q ==> R |] ==> R 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    81
\idx{iffCE}    
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    82
    [| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    83
\idx{exCI}    (! x. ~P(x) ==> P(a)) ==> ? x.P(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    84
\idx{swap}    ~P ==> (~Q ==> P) ==> Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    85
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    86
----------------------------------------------------------------
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    87
simpdata.ML
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    88
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    89
\idx{if_True}    Cond(True,x,y) = x
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    90
\idx{if_False}    Cond(False,x,y) = y
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    91
\idx{if_P}    P ==> Cond(P,x,y) = x
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    92
\idx{if_not_P}    ~P ==> Cond(P,x,y) = y
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    93
\idx{expand_if}    
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    94
    P(Cond(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    95
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    96
----------------------------------------------------------------
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    97
\idx{set.ML}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    98
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
    99
\idx{CollectI}          [| P(a) |] ==> a : \{x.P(x)\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   100
\idx{CollectD}          [| a : \{x.P(x)\} |] ==> P(a)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   101
\idx{set_ext}           [| !!x. (x:A) = (x:B) |] ==> A = B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   102
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   103
\idx{Ball_def}          Ball(A,P)  == ! x. x:A --> P(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   104
\idx{Bex_def}           Bex(A,P)   == ? x. x:A & P(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   105
\idx{subset_def}        A <= B     == ! x:A. x:B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   106
\idx{Un_def}            A Un B     == \{x.x:A | x:B\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   107
\idx{Int_def}           A Int B    == \{x.x:A & x:B\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   108
\idx{Compl_def}         Compl(A)   == \{x. ~x:A\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   109
\idx{Inter_def}         Inter(S)   == \{x. ! A:S. x:A\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   110
\idx{Union_def}         Union(S)   == \{x. ? A:S. x:A\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   111
\idx{INTER_def}         INTER(A,B) == \{y. ! x:A. y: B(x)\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   112
\idx{UNION_def}         UNION(A,B) == \{y. ? x:A. y: B(x)\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   113
\idx{mono_def}          mono(f)    == (!A B. A <= B --> f(A) <= f(B))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   114
\idx{image_def}         f``A       == \{y. ? x:A. y=f(x)\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   115
\idx{singleton_def}     \{a\}      == \{x.x=a\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   116
\idx{range_def}         range(f)   == \{y. ? x. y=f(x)\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   117
\idx{One_One_def}       One_One(f) == ! x y. f(x)=f(y) --> x=y
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   118
\idx{One_One_on_def}    One_One_on(f,A) == !x y. x:A --> y:A --> f(x)=f(y) --> x=y
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   119
\idx{Onto_def}          Onto(f) == ! y. ? x. y=f(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   120
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   121
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   122
\idx{Collect_cong}    [| !!x. P(x)=Q(x) |] ==> \{x. P(x)\} = \{x. Q(x)\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   123
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   124
\idx{ballI}    [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   125
\idx{bspec}    [| ! x:A. P(x);  x:A |] ==> P(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   126
\idx{ballE}    [| ! x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   127
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   128
\idx{bexI}     [| P(x);  x:A |] ==> ? x:A. P(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   129
\idx{bexCI}    [| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A.P(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   130
\idx{bexE}     [| ? x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   131
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   132
\idx{ball_cong}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   133
    [| A=A';  !!x. x:A' ==> P(x) = P'(x) |] ==> 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   134
    (! x:A. P(x)) = (! x:A'. P'(x))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   135
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   136
\idx{bex_cong}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   137
    [| A=A';  !!x. x:A' ==> P(x) = P'(x) |] ==> 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   138
    (? x:A. P(x)) = (? x:A'. P'(x))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   139
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   140
\idx{subsetI}         (!!x.x:A ==> x:B) ==> A <= B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   141
\idx{subsetD}         [| A <= B;  c:A |] ==> c:B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   142
\idx{subsetCE}        [| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   143
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   144
\idx{subset_refl}     A <= A
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   145
\idx{subset_antisym}  [| A <= B;  B <= A |] ==> A = B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   146
\idx{subset_trans}    [| A<=B;  B<=C |] ==> A<=C
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   147
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   148
\idx{equalityD1}      A = B ==> A<=B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   149
\idx{equalityD2}      A = B ==> B<=A
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   150
\idx{equalityE}       [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   151
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   152
\idx{singletonI}      a : \{a\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   153
\idx{singletonD}      b : \{a\} ==> b=a
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   154
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   155
\idx{imageI}    [| x:A |] ==> f(x) : f``A
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   156
\idx{imageE}    [| b : f``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   157
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   158
\idx{rangeI}    f(x) : range(f)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   159
\idx{rangeE}    [| b : range(f);  !!x.[| b=f(x) |] ==> P |] ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   160
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   161
\idx{UnionI}    [| X:C;  A:X |] ==> A : Union(C)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   162
\idx{UnionE}    [| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   163
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   164
\idx{InterI}    [| !!X. X:C ==> A:X |] ==> A : Inter(C)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   165
\idx{InterD}    [| A : Inter(C);  X:C |] ==> A:X
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   166
\idx{InterE}    [| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   167
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   168
\idx{UN_I}    [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   169
\idx{UN_E}    [| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   170
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   171
\idx{INT_I}    (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   172
\idx{INT_D}    [| b : (INT x:A. B(x));  a:A |] ==> b: B(a)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   173
\idx{INT_E}    [| b : (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   174
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   175
\idx{UnI1}    c:A ==> c : A Un B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   176
\idx{UnI2}    c:B ==> c : A Un B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   177
\idx{UnCI}    (~c:B ==> c:A) ==> c : A Un B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   178
\idx{UnE}    [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   179
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   180
\idx{IntI}    [| c:A;  c:B |] ==> c : A Int B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   181
\idx{IntD1}    c : A Int B ==> c:A
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   182
\idx{IntD2}    c : A Int B ==> c:B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   183
\idx{IntE}    [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   184
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   185
\idx{ComplI}    [| c:A ==> False |] ==> c : Compl(A)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   186
\idx{ComplD}    [| c : Compl(A) |] ==> ~c:A
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   187
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   188
\idx{monoI}    [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   189
\idx{monoD}    [| mono(f);  A <= B |] ==> f(A) <= f(B)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   190
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   191
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   192
----------------------------------------------------------------
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   193
\idx{fun.ML}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   194
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   195
\idx{One_OneI}            [| !! x y. f(x) = f(y) ==> x=y |] ==> One_One(f)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   196
\idx{One_One_inverseI}    (!!x. g(f(x)) = x) ==> One_One(f)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   197
\idx{One_OneD}            [| One_One(f); f(x) = f(y) |] ==> x=y
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   198
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   199
\idx{Inv_f_f}             One_One(f)   ==> Inv(f,f(x)) = x
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   200
\idx{f_Inv_f}             y : range(f) ==> f(Inv(f,y)) = y
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   201
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   202
\idx{Inv_injective}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   203
    [| Inv(f,x)=Inv(f,y); x: range(f);  y: range(f) |] ==> x=y
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   204
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   205
\idx{One_One_onI}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   206
    (!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> One_One_on(f,A)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   207
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   208
\idx{One_One_on_inverseI}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   209
    (!!x. x:A ==> g(f(x)) = x) ==> One_One_on(f,A)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   210
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   211
\idx{One_One_onD}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   212
    [| One_One_on(f,A);  f(x)=f(y);  x:A;  y:A |] ==> x=y
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   213
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   214
\idx{One_One_on_contraD}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   215
    [| One_One_on(f,A);  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   216
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   217
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   218
----------------------------------------------------------------
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   219
\idx{subset.ML}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   220
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   221
\idx{Union_upper}     B:A ==> B <= Union(A)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   222
\idx{Union_least}     [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   223
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   224
\idx{Inter_lower}     B:A ==> Inter(A) <= B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   225
\idx{Inter_greatest}  [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   226
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   227
\idx{Un_upper1}       A <= A Un B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   228
\idx{Un_upper2}       B <= A Un B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   229
\idx{Un_least}        [| A<=C;  B<=C |] ==> A Un B <= C
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   230
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   231
\idx{Int_lower1}      A Int B <= A
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   232
\idx{Int_lower2}      A Int B <= B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   233
\idx{Int_greatest}    [| C<=A;  C<=B |] ==> C <= A Int B
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   234
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   235
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   236
----------------------------------------------------------------
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   237
\idx{equalities.ML}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   238
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   239
\idx{Int_absorb}        A Int A = A
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   240
\idx{Int_commute}       A Int B  =  B Int A
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   241
\idx{Int_assoc}         (A Int B) Int C  =  A Int (B Int C)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   242
\idx{Int_Un_distrib}    (A Un B) Int C  =  (A Int C) Un (B Int C)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   243
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   244
\idx{Un_absorb}         A Un A = A
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   245
\idx{Un_commute}        A Un B  =  B Un A
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   246
\idx{Un_assoc}          (A Un B) Un C  =  A Un (B Un C)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   247
\idx{Un_Int_distrib}    (A Int B) Un C  =  (A Un C) Int (B Un C)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   248
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   249
\idx{Compl_disjoint}    A Int Compl(A) = \{x.False\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   250
\idx{Compl_partition    A Un Compl(A) = \{x.True\}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   251
\idx{double_complement} Compl(Compl(A)) = A
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   252
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   253
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   254
\idx{Compl_Un}          Compl(A Un B) = Compl(A) Int Compl(B)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   255
\idx{Compl_Int}         Compl(A Int B) = Compl(A) Un Compl(B)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   256
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   257
\idx{Union_Un_distrib}  Union(A Un B) = Union(A) Un Union(B)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   258
\idx{Int_Union_image}   A Int Union(B) = (UN C:B. A Int C)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   259
\idx{Un_Union_image}    (UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   260
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   261
\idx{Inter_Un_distrib}  Inter(A Un B) = Inter(A) Int Inter(B)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   262
\idx{Un_Inter_image}    A Un Inter(B) = (INT C:B. A Un C)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   263
\idx{Int_Inter_image}   (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   264
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   265
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   266
----------------------------------------------------------------
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   267
prod.ML
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   268
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   269
      mixfix = [ Delimfix((1<_,/_>), ['a,'b] => ('a,'b)prod, Pair),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   270
                 TInfixl(*, prod, 20) ],
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   271
thy = extend_theory Set.thy Prod
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   272
  [([prod],([[term],[term]],term))],
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   273
   ([fst],              'a * 'b => 'a),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   274
   ([snd],              'a * 'b => 'b),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   275
   ([split],            ['a * 'b, ['a,'b]=>'c] => 'c)],
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   276
\idx{fst_def}             fst(p) == @a. ? b. p = <a,b>),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   277
\idx{snd_def}             snd(p) == @b. ? a. p = <a,b>),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   278
\idx{split_def}           split(p,c) == c(fst(p),snd(p)))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   279
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   280
\idx{Pair_inject}  [| <a, b> = <a',b'>;  [| a=a';  b=b' |] ==> R |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   281
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   282
\idx{fst_conv}     fst(<a,b>) = a
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   283
\idx{snd_conv}     snd(<a,b>) = b
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   284
\idx{split_conv}   split(<a,b>, c) = c(a,b)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   285
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   286
\idx{surjective_pairing}    p = <fst(p),snd(p)>
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   287
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   288
----------------------------------------------------------------
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   289
sum.ML
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   290
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   291
      mixfix = [TInfixl(+, sum, 10)],
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   292
thy = extend_theory Prod.thy sum
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   293
  [([sum], ([[term],[term]],term))],
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   294
 [Inl],              'a => 'a+'b),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   295
 [Inr],              'b => 'a+'b),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   296
 [when],             ['a+'b, 'a=>'c, 'b=>'c] =>'c)],
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   297
\idx{when_def}    when == (%p f g. @z.  (!x. p=Inl(x) --> z=f(x))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   298
                                    & (!y. p=Inr(y) --> z=g(y))))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   299
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   300
\idx{Inl_not_Inr}    ~ (Inl(a) = Inr(b))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   301
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   302
\idx{One_One_Inl}    One_One(Inl)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   303
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   304
\idx{One_One_Inr}    One_One(Inr)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   305
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   306
\idx{when_Inl_conv}    when(Inl(x), f, g) = f(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   307
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   308
\idx{when_Inr_conv}    when(Inr(x), f, g) = g(x)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   309
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   310
\idx{sumE}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   311
    [| !!x::'a. P(Inl(x));  !!y::'b. P(Inr(y)) 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   312
    |] ==> P(s)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   313
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   314
\idx{surjective_sum}    when(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   315
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   316
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   317
????????????????????????????????????????????????????????????????
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   318
trancl?
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   319
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   320
----------------------------------------------------------------
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   321
nat.ML
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   322
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   323
  Sext\{mixfix=[Delimfix(0, nat, 0),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   324
               Infixl(<,[nat,nat] => bool,50)],
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   325
thy = extend_theory Trancl.thy Nat
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   326
[nat], ([],term))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   327
[nat_case],          [nat, 'a, nat=>'a] =>'a),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   328
[pred_nat],nat*nat) set),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   329
[nat_rec],           [nat, 'a, [nat, 'a]=>'a] => 'a)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   330
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   331
\idx{nat_case_def}        nat_case == (%n a f. @z.  (n=0 --> z=a)  
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   332
                                          & (!x. n=Suc(x) --> z=f(x)))),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   333
\idx{pred_nat_def}        pred_nat == \{p. ? n. p = <n, Suc(n)>\} ),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   334
\idx{less_def} m<n == <m,n>:trancl(pred_nat)),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   335
\idx{nat_rec_def} 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   336
   nat_rec(n,c,d) == wfrec(trancl(pred_nat), 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   337
                        %rec l. nat_case(l, c, %m. d(m,rec(m))), 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   338
                        n) )
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   339
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   340
\idx{nat_induct}    [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |]  ==> P(n)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   341
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   342
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   343
\idx{Suc_not_Zero}    ~ (Suc(m) = 0)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   344
\idx{One_One_Suc}    One_One(Suc)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   345
\idx{n_not_Suc_n}    ~(n=Suc(n))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   346
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   347
\idx{nat_case_0_conv}    nat_case(0, a, f) = a
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   348
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   349
\idx{nat_case_Suc_conv}    nat_case(Suc(k), a, f) = f(k)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   350
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   351
\idx{pred_natI}    <n, Suc(n)> : pred_nat
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   352
\idx{pred_natE}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   353
    [| p : pred_nat;  !!x n. [| p = <n, Suc(n)> |] ==> R 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   354
    |] ==> R
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   355
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   356
\idx{wf_pred_nat}    wf(pred_nat)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   357
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   358
\idx{nat_rec_0_conv}    nat_rec(0,c,h) = c
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   359
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   360
\idx{nat_rec_Suc_conv}    nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   361
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   362
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   363
(*** Basic properties of less than ***)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   364
\idx{less_trans}     [| i<j;  j<k |] ==> i<k
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   365
\idx{lessI}          n < Suc(n)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   366
\idx{zero_less_Suc}  0 < Suc(n)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   367
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   368
\idx{less_not_sym}   n<m --> ~m<n 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   369
\idx{less_not_refl}  ~ (n<n)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   370
\idx{not_less0}      ~ (n<0)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   371
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   372
\idx{Suc_less_eq}    (Suc(m) < Suc(n)) = (m<n)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   373
\idx{less_induct}    [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |]  ==>  P(n)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   374
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   375
\idx{less_linear}    m<n | m=n | n<m
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   376
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   377
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   378
----------------------------------------------------------------
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   379
list.ML
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   380
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   381
 [([list], ([[term]],term))],
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   382
  ([Nil],       'a list),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   383
  ([Cons],      ['a, 'a list] => 'a list),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   384
  ([list_rec],        ['a list, 'b, ['a ,'a list, 'b]=>'b] => 'b),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   385
  ([list_all],        ('a => bool) => ('a list => bool)),
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   386
  ([map],               ('a=>'b) => ('a list => 'b list))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   387
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   388
\idx{map_def}     map(f,xs) == list_rec(xs, Nil, %x l r. Cons(f(x), r)) )
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   389
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   390
\idx{list_induct}
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   391
    [| P(Nil);   
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   392
       !!x xs. [| P(xs) |] ==> P(Cons(x,xs)) |]  ==> P(l)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   393
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   394
\idx{Cons_not_Nil}   ~ Cons(x,xs) = Nil
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   395
\idx{Cons_Cons_eq}   (Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys)
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   396
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   397
\idx{list_rec_Nil_conv}    list_rec(Nil,c,h) = c
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   398
\idx{list_rec_Cons_conv}   list_rec(Cons(a,l), c, h) = 
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   399
                               h(a, l, list_rec(l,c,h))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   400
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   401
\idx{map_Nil_conv}   map(f,Nil) = Nil
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   402
\idx{map_Cons_conv}  map(f, Cons(x,xs)) = Cons(f(x), map(f,xs))
ff2c3ffd38ee used to be part of 'logics' manual;
wenzelm
parents:
diff changeset
   403