src/ZF/Sum.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 1611 35e0fd1b1775
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1107
diff changeset
     1
(*  Title:      ZF/Sum
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1107
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Disjoint sums in Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open Sum;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    11
(*** Rules for the Part primitive ***)
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    12
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    13
goalw Sum.thy [Part_def]
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    14
    "a : Part(A,h) <-> a:A & (EX y. a=h(y))";
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    15
by (rtac separation 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    16
qed "Part_iff";
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    17
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    18
goalw Sum.thy [Part_def]
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    19
    "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part(A,h)";
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    20
by (REPEAT (ares_tac [exI,CollectI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    21
qed "Part_eqI";
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    22
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    23
val PartI = refl RSN (2,Part_eqI);
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    24
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    25
val major::prems = goalw Sum.thy [Part_def]
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    26
    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    27
\    |] ==> P";
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    28
by (rtac (major RS CollectE) 1);
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    29
by (etac exE 1);
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    30
by (REPEAT (ares_tac prems 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    31
qed "PartE";
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    32
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    33
goalw Sum.thy [Part_def] "Part(A,h) <= A";
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    34
by (rtac Collect_subset 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    35
qed "Part_subset";
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    36
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    37
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    38
(*** Rules for Disjoint Sums ***)
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    39
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
521
dfca17a698b0 ZF/Sum/Sigma_bool: new
lcp
parents: 435
diff changeset
    42
goalw Sum.thy (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)";
dfca17a698b0 ZF/Sum/Sigma_bool: new
lcp
parents: 435
diff changeset
    43
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    44
qed "Sigma_bool";
521
dfca17a698b0 ZF/Sum/Sigma_bool: new
lcp
parents: 435
diff changeset
    45
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
(** Introduction rules for the injections **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
goalw Sum.thy sum_defs "!!a A B. a : A ==> Inl(a) : A+B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
by (REPEAT (ares_tac [UnI1,SigmaI,singletonI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    50
qed "InlI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
goalw Sum.thy sum_defs "!!b A B. b : B ==> Inr(b) : A+B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
by (REPEAT (ares_tac [UnI2,SigmaI,singletonI] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    54
qed "InrI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
(** Elimination rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
val major::prems = goalw Sum.thy sum_defs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
    "[| u: A+B;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
\       !!x. [| x:A;  u=Inl(x) |] ==> P; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
\       !!y. [| y:B;  u=Inr(y) |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (rtac (major RS UnE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (REPEAT (rtac refl 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
     ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    66
qed "sumE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
(** Injection and freeness equivalences, for rewriting **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    70
goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
    71
by (simp_tac ZF_ss 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    72
qed "Inl_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    74
goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
    75
by (simp_tac ZF_ss 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    76
qed "Inr_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    78
goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
    79
by (simp_tac (ZF_ss addsimps [one_not_0 RS not_sym]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    80
qed "Inl_Inr_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    82
goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
    83
by (simp_tac (ZF_ss addsimps [one_not_0]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    84
qed "Inr_Inl_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    86
(*Injection and freeness rules*)
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    87
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 773
diff changeset
    88
bind_thm ("Inl_inject", (Inl_iff RS iffD1));
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 773
diff changeset
    89
bind_thm ("Inr_inject", (Inr_iff RS iffD1));
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 773
diff changeset
    90
bind_thm ("Inl_neq_Inr", (Inl_Inr_iff RS iffD1 RS FalseE));
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 773
diff changeset
    91
bind_thm ("Inr_neq_Inl", (Inr_Inl_iff RS iffD1 RS FalseE));
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    92
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    93
val sum_cs = ZF_cs addSIs [PartI, InlI, InrI] 
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    94
                   addSEs [PartE, sumE, Inl_neq_Inr, Inr_neq_Inl]
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
    95
                   addSDs [Inl_inject, Inr_inject];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    97
goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    98
by (fast_tac sum_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    99
qed "InlD";
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   100
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   101
goal Sum.thy "!!A B. Inr(b): A+B ==> b: B";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   102
by (fast_tac sum_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   103
qed "InrD";
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   104
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
by (fast_tac sum_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   107
qed "sum_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
goal Sum.thy "A+B <= C+D <-> A<=C & B<=D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
by (fast_tac sum_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   111
qed "sum_subset_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
goal Sum.thy "A+B = C+D <-> A=C & B=D";
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   114
by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   116
qed "sum_equal_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
521
dfca17a698b0 ZF/Sum/Sigma_bool: new
lcp
parents: 435
diff changeset
   118
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
(*** Eliminator -- case ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)";
1107
f0ac02ffa21d Modified proofs for new form of 'split'.
lcp
parents: 858
diff changeset
   122
by (simp_tac (ZF_ss addsimps [cond_0]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   123
qed "case_Inl";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)";
1107
f0ac02ffa21d Modified proofs for new form of 'split'.
lcp
parents: 858
diff changeset
   126
by (simp_tac (ZF_ss addsimps [cond_1]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   127
qed "case_Inr";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
val major::prems = goal Sum.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
    "[| u: A+B; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
\       !!x. x: A ==> c(x): C(Inl(x));   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
\       !!y. y: B ==> d(y): C(Inr(y)) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
\    |] ==> case(c,d,u) : C(u)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
by (rtac (major RS sumE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
by (ALLGOALS (etac ssubst));
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   136
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1107
diff changeset
   137
                            (prems@[case_Inl,case_Inr]))));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   138
qed "case_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
   140
goal Sum.thy
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
   141
  "!!u. u: A+B ==>   \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
   142
\       R(case(c,d,u)) <-> \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
   143
\       ((ALL x:A. u = Inl(x) --> R(c(x))) & \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
   144
\       (ALL y:B. u = Inr(y) --> R(d(y))))";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
   145
by (etac sumE 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
   146
by (asm_simp_tac (ZF_ss addsimps [case_Inl]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
   147
by (fast_tac sum_cs 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
   148
by (asm_simp_tac (ZF_ss addsimps [case_Inr]) 1);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
   149
by (fast_tac sum_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   150
qed "expand_case";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 55
diff changeset
   151
858
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   152
val major::prems = goal Sum.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1107
diff changeset
   153
  "[| z: A+B;   \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1107
diff changeset
   154
\     !!x. x:A ==> c(x)=c'(x);  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1107
diff changeset
   155
\     !!y. y:B ==> d(y)=d'(y)   \
858
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   156
\  |] ==> case(c,d,z) = case(c',d',z)";
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   157
by (resolve_tac [major RS sumE] 1);
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   158
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps ([case_Inl, case_Inr] @ prems))));
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   159
qed "case_cong";
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   160
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   161
val [major] = goal Sum.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1107
diff changeset
   162
  "z: A+B ==>   \
858
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   163
\  case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   164
\  case(%x. c(c'(x)), %y. d(d'(y)), z)";
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   165
by (resolve_tac [major RS sumE] 1);
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   166
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [case_Inl, case_Inr])));
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   167
qed "case_case";
b87867b3fd91 Proved case_cong and case_case.
lcp
parents: 803
diff changeset
   168
773
9f8bcf1a4cff sum_ss: moved down and added the rewrite rules for "case"
lcp
parents: 760
diff changeset
   169
val sum_ss = ZF_ss addsimps [InlI, InrI, Inl_iff, Inr_iff, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1107
diff changeset
   170
                             Inl_Inr_iff, Inr_Inl_iff,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1107
diff changeset
   171
                             case_Inl, case_Inr];
773
9f8bcf1a4cff sum_ss: moved down and added the rewrite rules for "case"
lcp
parents: 760
diff changeset
   172
9f8bcf1a4cff sum_ss: moved down and added the rewrite rules for "case"
lcp
parents: 760
diff changeset
   173
(*** More rules for Part(A,h) ***)
9f8bcf1a4cff sum_ss: moved down and added the rewrite rules for "case"
lcp
parents: 760
diff changeset
   174
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
   176
by (fast_tac sum_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   177
qed "Part_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
   179
goal Sum.thy "Part(Collect(A,P), h) = Collect(Part(A,h), P)";
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
   180
by (fast_tac (sum_cs addSIs [equalityI]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   181
qed "Part_Collect";
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
   182
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 782
diff changeset
   183
bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE);
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
   184
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
   186
by (fast_tac (sum_cs addIs [equalityI]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   187
qed "Part_Inl";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
   190
by (fast_tac (sum_cs addIs [equalityI]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   191
qed "Part_Inr";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
by (etac CollectD1 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   195
qed "PartD1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
goal Sum.thy "Part(A,%x.x) = A";
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
   198
by (fast_tac (sum_cs addIs [equalityI]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   199
qed "Part_id";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
   202
by (fast_tac (sum_cs addIs [equalityI]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   203
qed "Part_Inr2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 521
diff changeset
   206
by (fast_tac (sum_cs addIs [equalityI]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   207
qed "Part_sum_equality";