author | wenzelm |
Tue, 03 Mar 2009 14:07:43 +0100 | |
changeset 30211 | 556d1810cdad |
parent 29183 | f1648e009dc1 |
child 31080 | 21ffc770ebc0 |
permissions | -rw-r--r-- |
10213 | 1 |
(* Title: HOL/Sum_Type.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1992 University of Cambridge |
|
5 |
*) |
|
6 |
||
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
7 |
header{*The Disjoint Sum of Two Types*} |
10213 | 8 |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
9 |
theory Sum_Type |
22424 | 10 |
imports Typedef Fun |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
11 |
begin |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
12 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
13 |
text{*The representations of the two injections*} |
10213 | 14 |
|
15 |
constdefs |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
16 |
Inl_Rep :: "['a, 'a, 'b, bool] => bool" |
10213 | 17 |
"Inl_Rep == (%a. %x y p. x=a & p)" |
18 |
||
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
19 |
Inr_Rep :: "['b, 'a, 'b, bool] => bool" |
10213 | 20 |
"Inr_Rep == (%b. %x y p. y=b & ~p)" |
21 |
||
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
22 |
|
10213 | 23 |
global |
24 |
||
25 |
typedef (Sum) |
|
22838 | 26 |
('a, 'b) "+" (infixr "+" 10) |
10213 | 27 |
= "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}" |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
28 |
by auto |
10213 | 29 |
|
30 |
local |
|
31 |
||
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
32 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
33 |
text{*abstract constants and syntax*} |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
34 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
35 |
constdefs |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
36 |
Inl :: "'a => 'a + 'b" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
37 |
"Inl == (%a. Abs_Sum(Inl_Rep(a)))" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
38 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
39 |
Inr :: "'b => 'a + 'b" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
40 |
"Inr == (%b. Abs_Sum(Inr_Rep(b)))" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
41 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
42 |
Plus :: "['a set, 'b set] => ('a + 'b) set" (infixr "<+>" 65) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
43 |
"A <+> B == (Inl`A) Un (Inr`B)" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
44 |
--{*disjoint sum for sets; the operator + is overloaded with wrong type!*} |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
45 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
46 |
Part :: "['a set, 'b => 'a] => 'a set" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
47 |
"Part A h == A Int {x. ? z. x = h(z)}" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
48 |
--{*for selecting out the components of a mutually recursive definition*} |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
49 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
50 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
51 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
52 |
(** Inl_Rep and Inr_Rep: Representations of the constructors **) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
53 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
54 |
(*This counts as a non-emptiness result for admitting 'a+'b as a type*) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
55 |
lemma Inl_RepI: "Inl_Rep(a) : Sum" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
56 |
by (auto simp add: Sum_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
57 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
58 |
lemma Inr_RepI: "Inr_Rep(b) : Sum" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
59 |
by (auto simp add: Sum_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
60 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
61 |
lemma inj_on_Abs_Sum: "inj_on Abs_Sum Sum" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
62 |
apply (rule inj_on_inverseI) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
63 |
apply (erule Abs_Sum_inverse) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
64 |
done |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
65 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
66 |
subsection{*Freeness Properties for @{term Inl} and @{term Inr}*} |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
67 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
68 |
text{*Distinctness*} |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
69 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
70 |
lemma Inl_Rep_not_Inr_Rep: "Inl_Rep(a) ~= Inr_Rep(b)" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
71 |
by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
72 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
73 |
lemma Inl_not_Inr [iff]: "Inl(a) ~= Inr(b)" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
74 |
apply (simp add: Inl_def Inr_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
75 |
apply (rule inj_on_Abs_Sum [THEN inj_on_contraD]) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
76 |
apply (rule Inl_Rep_not_Inr_Rep) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
77 |
apply (rule Inl_RepI) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
78 |
apply (rule Inr_RepI) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
79 |
done |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
80 |
|
17084
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17026
diff
changeset
|
81 |
lemmas Inr_not_Inl = Inl_not_Inr [THEN not_sym, standard] |
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17026
diff
changeset
|
82 |
declare Inr_not_Inl [iff] |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
83 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
84 |
lemmas Inl_neq_Inr = Inl_not_Inr [THEN notE, standard] |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
85 |
lemmas Inr_neq_Inl = sym [THEN Inl_neq_Inr, standard] |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
86 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
87 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
88 |
text{*Injectiveness*} |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
89 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
90 |
lemma Inl_Rep_inject: "Inl_Rep(a) = Inl_Rep(c) ==> a=c" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
91 |
by (auto simp add: Inl_Rep_def expand_fun_eq) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
92 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
93 |
lemma Inr_Rep_inject: "Inr_Rep(b) = Inr_Rep(d) ==> b=d" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
94 |
by (auto simp add: Inr_Rep_def expand_fun_eq) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
95 |
|
29025
8c8859c0d734
move lemmas from Numeral_Type.thy to other theories
huffman
parents:
28524
diff
changeset
|
96 |
lemma inj_Inl [simp]: "inj_on Inl A" |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
97 |
apply (simp add: Inl_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
98 |
apply (rule inj_onI) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
99 |
apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inl_Rep_inject]) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
100 |
apply (rule Inl_RepI) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
101 |
apply (rule Inl_RepI) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
102 |
done |
29025
8c8859c0d734
move lemmas from Numeral_Type.thy to other theories
huffman
parents:
28524
diff
changeset
|
103 |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
104 |
lemmas Inl_inject = inj_Inl [THEN injD, standard] |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
105 |
|
29025
8c8859c0d734
move lemmas from Numeral_Type.thy to other theories
huffman
parents:
28524
diff
changeset
|
106 |
lemma inj_Inr [simp]: "inj_on Inr A" |
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
107 |
apply (simp add: Inr_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
108 |
apply (rule inj_onI) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
109 |
apply (erule inj_on_Abs_Sum [THEN inj_onD, THEN Inr_Rep_inject]) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
110 |
apply (rule Inr_RepI) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
111 |
apply (rule Inr_RepI) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
112 |
done |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
113 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
114 |
lemmas Inr_inject = inj_Inr [THEN injD, standard] |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
115 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
116 |
lemma Inl_eq [iff]: "(Inl(x)=Inl(y)) = (x=y)" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
117 |
by (blast dest!: Inl_inject) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
118 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
119 |
lemma Inr_eq [iff]: "(Inr(x)=Inr(y)) = (x=y)" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
120 |
by (blast dest!: Inr_inject) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
121 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
122 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
123 |
subsection{*The Disjoint Sum of Sets*} |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
124 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
125 |
(** Introduction rules for the injections **) |
10213 | 126 |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
127 |
lemma InlI [intro!]: "a : A ==> Inl(a) : A <+> B" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
128 |
by (simp add: Plus_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
129 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
130 |
lemma InrI [intro!]: "b : B ==> Inr(b) : A <+> B" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
131 |
by (simp add: Plus_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
132 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
133 |
(** Elimination rules **) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
134 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
135 |
lemma PlusE [elim!]: |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
136 |
"[| u: A <+> B; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
137 |
!!x. [| x:A; u=Inl(x) |] ==> P; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
138 |
!!y. [| y:B; u=Inr(y) |] ==> P |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
139 |
|] ==> P" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
140 |
by (auto simp add: Plus_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
141 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
142 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
143 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
144 |
text{*Exhaustion rule for sums, a degenerate form of induction*} |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
145 |
lemma sumE: |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
146 |
"[| !!x::'a. s = Inl(x) ==> P; !!y::'b. s = Inr(y) ==> P |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
147 |
|] ==> P" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
148 |
apply (rule Abs_Sum_cases [of s]) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
149 |
apply (auto simp add: Sum_def Inl_def Inr_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
150 |
done |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
151 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
152 |
|
17026 | 153 |
lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV" |
154 |
apply (rule set_ext) |
|
155 |
apply(rename_tac s) |
|
156 |
apply(rule_tac s=s in sumE) |
|
157 |
apply auto |
|
158 |
done |
|
159 |
||
160 |
||
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
161 |
subsection{*The @{term Part} Primitive*} |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
162 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
163 |
lemma Part_eqI [intro]: "[| a : A; a=h(b) |] ==> a : Part A h" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
164 |
by (auto simp add: Part_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
165 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
166 |
lemmas PartI = Part_eqI [OF _ refl, standard] |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
167 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
168 |
lemma PartE [elim!]: "[| a : Part A h; !!z. [| a : A; a=h(z) |] ==> P |] ==> P" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
169 |
by (auto simp add: Part_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
170 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
171 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
172 |
lemma Part_subset: "Part A h <= A" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
173 |
by (auto simp add: Part_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
174 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
175 |
lemma Part_mono: "A<=B ==> Part A h <= Part B h" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
176 |
by blast |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
177 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
178 |
lemmas basic_monos = basic_monos Part_mono |
10213 | 179 |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
180 |
lemma PartD1: "a : Part A h ==> a : A" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
181 |
by (simp add: Part_def) |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
182 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
183 |
lemma Part_id: "Part A (%x. x) = A" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
184 |
by blast |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
185 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
186 |
lemma Part_Int: "Part (A Int B) h = (Part A h) Int (Part B h)" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
187 |
by blast |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
188 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
189 |
lemma Part_Collect: "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}" |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
190 |
by blast |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
191 |
|
20588 | 192 |
|
15391
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
193 |
ML |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
194 |
{* |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
195 |
val Inl_RepI = thm "Inl_RepI"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
196 |
val Inr_RepI = thm "Inr_RepI"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
197 |
val inj_on_Abs_Sum = thm "inj_on_Abs_Sum"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
198 |
val Inl_Rep_not_Inr_Rep = thm "Inl_Rep_not_Inr_Rep"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
199 |
val Inl_not_Inr = thm "Inl_not_Inr"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
200 |
val Inr_not_Inl = thm "Inr_not_Inl"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
201 |
val Inl_neq_Inr = thm "Inl_neq_Inr"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
202 |
val Inr_neq_Inl = thm "Inr_neq_Inl"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
203 |
val Inl_Rep_inject = thm "Inl_Rep_inject"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
204 |
val Inr_Rep_inject = thm "Inr_Rep_inject"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
205 |
val inj_Inl = thm "inj_Inl"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
206 |
val Inl_inject = thm "Inl_inject"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
207 |
val inj_Inr = thm "inj_Inr"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
208 |
val Inr_inject = thm "Inr_inject"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
209 |
val Inl_eq = thm "Inl_eq"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
210 |
val Inr_eq = thm "Inr_eq"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
211 |
val InlI = thm "InlI"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
212 |
val InrI = thm "InrI"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
213 |
val PlusE = thm "PlusE"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
214 |
val sumE = thm "sumE"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
215 |
val Part_eqI = thm "Part_eqI"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
216 |
val PartI = thm "PartI"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
217 |
val PartE = thm "PartE"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
218 |
val Part_subset = thm "Part_subset"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
219 |
val Part_mono = thm "Part_mono"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
220 |
val PartD1 = thm "PartD1"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
221 |
val Part_id = thm "Part_id"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
222 |
val Part_Int = thm "Part_Int"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
223 |
val Part_Collect = thm "Part_Collect"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
224 |
|
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
225 |
val basic_monos = thms "basic_monos"; |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
226 |
*} |
797ed46d724b
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents:
11609
diff
changeset
|
227 |
|
10213 | 228 |
end |