src/HOL/Sum.ML
changeset 5069 3ea049f7979d
parent 4988 8f4dc836a2ea
child 5143 b94cd208f073
     1.1 --- a/src/HOL/Sum.ML	Mon Jun 22 17:13:09 1998 +0200
     1.2 +++ b/src/HOL/Sum.ML	Mon Jun 22 17:26:46 1998 +0200
     1.3 @@ -11,29 +11,29 @@
     1.4  (** Inl_Rep and Inr_Rep: Representations of the constructors **)
     1.5  
     1.6  (*This counts as a non-emptiness result for admitting 'a+'b as a type*)
     1.7 -goalw Sum.thy [Sum_def] "Inl_Rep(a) : Sum";
     1.8 +Goalw [Sum_def] "Inl_Rep(a) : Sum";
     1.9  by (EVERY1 [rtac CollectI, rtac disjI1, rtac exI, rtac refl]);
    1.10  qed "Inl_RepI";
    1.11  
    1.12 -goalw Sum.thy [Sum_def] "Inr_Rep(b) : Sum";
    1.13 +Goalw [Sum_def] "Inr_Rep(b) : Sum";
    1.14  by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]);
    1.15  qed "Inr_RepI";
    1.16  
    1.17 -goal Sum.thy "inj_on Abs_Sum Sum";
    1.18 +Goal "inj_on Abs_Sum Sum";
    1.19  by (rtac inj_on_inverseI 1);
    1.20  by (etac Abs_Sum_inverse 1);
    1.21  qed "inj_on_Abs_Sum";
    1.22  
    1.23  (** Distinctness of Inl and Inr **)
    1.24  
    1.25 -goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)";
    1.26 +Goalw [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)";
    1.27  by (EVERY1 [rtac notI,
    1.28              etac (fun_cong RS fun_cong RS fun_cong RS iffE), 
    1.29              rtac (notE RS ccontr),  etac (mp RS conjunct2), 
    1.30              REPEAT o (ares_tac [refl,conjI]) ]);
    1.31  qed "Inl_Rep_not_Inr_Rep";
    1.32  
    1.33 -goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
    1.34 +Goalw [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
    1.35  by (rtac (inj_on_Abs_Sum RS inj_on_contraD) 1);
    1.36  by (rtac Inl_Rep_not_Inr_Rep 1);
    1.37  by (rtac Inl_RepI 1);
    1.38 @@ -61,7 +61,7 @@
    1.39  by (Blast_tac 1);
    1.40  qed "Inr_Rep_inject";
    1.41  
    1.42 -goalw Sum.thy [Inl_def] "inj(Inl)";
    1.43 +Goalw [Inl_def] "inj(Inl)";
    1.44  by (rtac injI 1);
    1.45  by (etac (inj_on_Abs_Sum RS inj_onD RS Inl_Rep_inject) 1);
    1.46  by (rtac Inl_RepI 1);
    1.47 @@ -69,7 +69,7 @@
    1.48  qed "inj_Inl";
    1.49  val Inl_inject = inj_Inl RS injD;
    1.50  
    1.51 -goalw Sum.thy [Inr_def] "inj(Inr)";
    1.52 +Goalw [Inr_def] "inj(Inr)";
    1.53  by (rtac injI 1);
    1.54  by (etac (inj_on_Abs_Sum RS inj_onD RS Inr_Rep_inject) 1);
    1.55  by (rtac Inr_RepI 1);
    1.56 @@ -77,11 +77,11 @@
    1.57  qed "inj_Inr";
    1.58  val Inr_inject = inj_Inr RS injD;
    1.59  
    1.60 -goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
    1.61 +Goal "(Inl(x)=Inl(y)) = (x=y)";
    1.62  by (blast_tac (claset() addSDs [Inl_inject]) 1);
    1.63  qed "Inl_eq";
    1.64  
    1.65 -goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
    1.66 +Goal "(Inr(x)=Inr(y)) = (x=y)";
    1.67  by (blast_tac (claset() addSDs [Inr_inject]) 1);
    1.68  qed "Inr_eq";
    1.69  
    1.70 @@ -91,11 +91,11 @@
    1.71  
    1.72  (** Introduction rules for the injections **)
    1.73  
    1.74 -goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A Plus B";
    1.75 +Goalw [sum_def] "!!a A B. a : A ==> Inl(a) : A Plus B";
    1.76  by (Blast_tac 1);
    1.77  qed "InlI";
    1.78  
    1.79 -goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A Plus B";
    1.80 +Goalw [sum_def] "!!b A B. b : B ==> Inr(b) : A Plus B";
    1.81  by (Blast_tac 1);
    1.82  qed "InrI";
    1.83  
    1.84 @@ -118,11 +118,11 @@
    1.85  
    1.86  (** sum_case -- the selection operator for sums **)
    1.87  
    1.88 -goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
    1.89 +Goalw [sum_case_def] "sum_case f g (Inl x) = f(x)";
    1.90  by (Blast_tac 1);
    1.91  qed "sum_case_Inl";
    1.92  
    1.93 -goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
    1.94 +Goalw [sum_case_def] "sum_case f g (Inr x) = g(x)";
    1.95  by (Blast_tac 1);
    1.96  qed "sum_case_Inr";
    1.97  
    1.98 @@ -140,13 +140,13 @@
    1.99                      rtac (Rep_Sum_inverse RS sym)]));
   1.100  qed "sumE";
   1.101  
   1.102 -goal Sum.thy "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
   1.103 +Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
   1.104  by (EVERY1 [res_inst_tac [("s","s")] sumE, 
   1.105              etac ssubst, rtac sum_case_Inl,
   1.106              etac ssubst, rtac sum_case_Inr]);
   1.107  qed "surjective_sum";
   1.108  
   1.109 -goal Sum.thy "R(sum_case f g s) = \
   1.110 +Goal "R(sum_case f g s) = \
   1.111  \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
   1.112  by (res_inst_tac [("s","s")] sumE 1);
   1.113  by Auto_tac;
   1.114 @@ -166,7 +166,7 @@
   1.115  
   1.116  (** Rules for the Part primitive **)
   1.117  
   1.118 -goalw Sum.thy [Part_def]
   1.119 +Goalw [Part_def]
   1.120      "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part A h";
   1.121  by (Blast_tac 1);
   1.122  qed "Part_eqI";
   1.123 @@ -185,29 +185,29 @@
   1.124  AddIs  [Part_eqI];
   1.125  AddSEs [PartE];
   1.126  
   1.127 -goalw Sum.thy [Part_def] "Part A h <= A";
   1.128 +Goalw [Part_def] "Part A h <= A";
   1.129  by (rtac Int_lower1 1);
   1.130  qed "Part_subset";
   1.131  
   1.132 -goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
   1.133 +Goal "!!A B. A<=B ==> Part A h <= Part B h";
   1.134  by (Blast_tac 1);
   1.135  qed "Part_mono";
   1.136  
   1.137  val basic_monos = basic_monos @ [Part_mono];
   1.138  
   1.139 -goalw Sum.thy [Part_def] "!!a. a : Part A h ==> a : A";
   1.140 +Goalw [Part_def] "!!a. a : Part A h ==> a : A";
   1.141  by (etac IntD1 1);
   1.142  qed "PartD1";
   1.143  
   1.144 -goal Sum.thy "Part A (%x. x) = A";
   1.145 +Goal "Part A (%x. x) = A";
   1.146  by (Blast_tac 1);
   1.147  qed "Part_id";
   1.148  
   1.149 -goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
   1.150 +Goal "Part (A Int B) h = (Part A h) Int (Part B h)";
   1.151  by (Blast_tac 1);
   1.152  qed "Part_Int";
   1.153  
   1.154  (*For inductive definitions*)
   1.155 -goal Sum.thy "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}";
   1.156 +Goal "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}";
   1.157  by (Blast_tac 1);
   1.158  qed "Part_Collect";