tuned;
authorwenzelm
Tue Oct 16 17:51:50 2001 +0200 (2001-10-16)
changeset 1180330f2104953a1
parent 11802 1d5f5d2427d2
child 11804 d69e7acd9380
tuned;
src/HOL/PreList.thy
     1.1 --- a/src/HOL/PreList.thy	Tue Oct 16 17:51:12 2001 +0200
     1.2 +++ b/src/HOL/PreList.thy	Tue Oct 16 17:51:50 2001 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
     1.5    Relation_Power + Calculation + SVC_Oracle:
     1.6  
     1.7 -(*belongs to theory HOL*)
     1.8 +(*belongs to theory Datatype*)
     1.9  declare case_split [cases type: bool]
    1.10  
    1.11  (*belongs to theory Wellfounded_Recursion*)
    1.12 @@ -21,70 +21,67 @@
    1.13  hide const Node Atom Leaf Numb Lim Funs Split Case
    1.14  hide type node item
    1.15  
    1.16 -(*belongs to theory Product_Type; canonical case/induct rules for 3-7 tuples*)
    1.17 -lemma prod_cases3 [cases type: *]: "(!!a b c. y = (a, b, c) ==> P) ==> P"
    1.18 -apply (cases y)
    1.19 -apply (case_tac b)
    1.20 -apply blast
    1.21 -done
    1.22 +(*belongs to theory Datatype; canonical case/induct rules for 3-7 tuples*)
    1.23 +lemma prod_cases3 [cases type]: "(!!a b c. y = (a, b, c) ==> P) ==> P"
    1.24 +  apply (cases y)
    1.25 +  apply (case_tac b)
    1.26 +  apply blast
    1.27 +  done
    1.28  
    1.29 -lemma prod_induct3 [induct type: *]: "(!!a b c. P (a, b, c)) ==> P x"
    1.30 -apply (cases x)
    1.31 -apply blast
    1.32 -done
    1.33 +lemma prod_induct3 [induct type]: "(!!a b c. P (a, b, c)) ==> P x"
    1.34 +  apply (cases x)
    1.35 +  apply blast
    1.36 +  done
    1.37  
    1.38 -lemma prod_cases4 [cases type: *]: "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
    1.39 -apply (cases y)
    1.40 -apply (case_tac c)
    1.41 -apply blast
    1.42 -done
    1.43 +lemma prod_cases4 [cases type]: "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
    1.44 +  apply (cases y)
    1.45 +  apply (case_tac c)
    1.46 +  apply blast
    1.47 +  done
    1.48  
    1.49 -lemma prod_induct4 [induct type: *]: "(!!a b c d. P (a, b, c, d)) ==> P x"
    1.50 -apply (cases x)
    1.51 -apply blast
    1.52 -done
    1.53 +lemma prod_induct4 [induct type]: "(!!a b c d. P (a, b, c, d)) ==> P x"
    1.54 +  apply (cases x)
    1.55 +  apply blast
    1.56 +  done
    1.57  
    1.58 -lemma prod_cases5 [cases type: *]: "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
    1.59 -apply (cases y)
    1.60 -apply (case_tac d)
    1.61 -apply blast
    1.62 -done
    1.63 +lemma prod_cases5 [cases type]: "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
    1.64 +  apply (cases y)
    1.65 +  apply (case_tac d)
    1.66 +  apply blast
    1.67 +  done
    1.68  
    1.69 -lemma prod_induct5 [induct type: *]: "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
    1.70 -apply (cases x)
    1.71 -apply blast
    1.72 -done
    1.73 +lemma prod_induct5 [induct type]: "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
    1.74 +  apply (cases x)
    1.75 +  apply blast
    1.76 +  done
    1.77  
    1.78 -lemma prod_cases6 [cases type: *]: "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
    1.79 -apply (cases y)
    1.80 -apply (case_tac e)
    1.81 -apply blast
    1.82 -done
    1.83 +lemma prod_cases6 [cases type]: "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
    1.84 +  apply (cases y)
    1.85 +  apply (case_tac e)
    1.86 +  apply blast
    1.87 +  done
    1.88  
    1.89 -lemma prod_induct6 [induct type: *]: "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
    1.90 -apply (cases x)
    1.91 -apply blast
    1.92 -done
    1.93 +lemma prod_induct6 [induct type]: "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
    1.94 +  apply (cases x)
    1.95 +  apply blast
    1.96 +  done
    1.97  
    1.98 -lemma prod_cases7 [cases type: *]: "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
    1.99 -apply (cases y)
   1.100 -apply (case_tac f)
   1.101 -apply blast
   1.102 -done
   1.103 +lemma prod_cases7 [cases type]: "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
   1.104 +  apply (cases y)
   1.105 +  apply (case_tac f)
   1.106 +  apply blast
   1.107 +  done
   1.108  
   1.109 -lemma prod_induct7 [induct type: *]: "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   1.110 -apply (cases x)
   1.111 -apply blast
   1.112 -done
   1.113 +lemma prod_induct7 [induct type]: "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   1.114 +  apply (cases x)
   1.115 +  apply blast
   1.116 +  done
   1.117  
   1.118  
   1.119  (* generic summation indexed over nat *)
   1.120  
   1.121 -(*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*)
   1.122 -(*FIXME port theorems from Algebra/abstract/NatSum*)
   1.123 -
   1.124  consts
   1.125 -  Summation :: "(nat => 'a::{zero,plus}) => nat => 'a"
   1.126 +  Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
   1.127  primrec
   1.128    "Summation f 0 = 0"
   1.129    "Summation f (Suc n) = Summation f n + f n"