moved product cases/induct to theory Datatype;
authorwenzelm
Sat Oct 27 00:00:38 2001 +0200 (2001-10-27)
changeset 119555818c5abb415
parent 11954 3d1780208bf3
child 11956 b814360b0267
moved product cases/induct to theory Datatype;
src/HOL/PreList.thy
     1.1 --- a/src/HOL/PreList.thy	Sat Oct 27 00:00:05 2001 +0200
     1.2 +++ b/src/HOL/PreList.thy	Sat Oct 27 00:00:38 2001 +0200
     1.3 @@ -11,72 +11,9 @@
     1.4    Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
     1.5    Relation_Power + Calculation + SVC_Oracle:
     1.6  
     1.7 -(*belongs to theory Datatype*)
     1.8 -declare case_split [cases type: bool]
     1.9 -
    1.10  (*belongs to theory Wellfounded_Recursion*)
    1.11  declare wf_induct [induct set: wf]
    1.12  
    1.13 -(*belongs to theory Datatype_Universe; hides popular names *)
    1.14 -hide const Node Atom Leaf Numb Lim Funs Split Case
    1.15 -hide type node item
    1.16 -
    1.17 -(*belongs to theory Datatype; canonical case/induct rules for 3-7 tuples*)
    1.18 -lemma prod_cases3 [cases type]: "(!!a b c. y = (a, b, c) ==> P) ==> P"
    1.19 -  apply (cases y)
    1.20 -  apply (case_tac b)
    1.21 -  apply blast
    1.22 -  done
    1.23 -
    1.24 -lemma prod_induct3 [induct type]: "(!!a b c. P (a, b, c)) ==> P x"
    1.25 -  apply (cases x)
    1.26 -  apply blast
    1.27 -  done
    1.28 -
    1.29 -lemma prod_cases4 [cases type]: "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
    1.30 -  apply (cases y)
    1.31 -  apply (case_tac c)
    1.32 -  apply blast
    1.33 -  done
    1.34 -
    1.35 -lemma prod_induct4 [induct type]: "(!!a b c d. P (a, b, c, d)) ==> P x"
    1.36 -  apply (cases x)
    1.37 -  apply blast
    1.38 -  done
    1.39 -
    1.40 -lemma prod_cases5 [cases type]: "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
    1.41 -  apply (cases y)
    1.42 -  apply (case_tac d)
    1.43 -  apply blast
    1.44 -  done
    1.45 -
    1.46 -lemma prod_induct5 [induct type]: "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
    1.47 -  apply (cases x)
    1.48 -  apply blast
    1.49 -  done
    1.50 -
    1.51 -lemma prod_cases6 [cases type]: "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
    1.52 -  apply (cases y)
    1.53 -  apply (case_tac e)
    1.54 -  apply blast
    1.55 -  done
    1.56 -
    1.57 -lemma prod_induct6 [induct type]: "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
    1.58 -  apply (cases x)
    1.59 -  apply blast
    1.60 -  done
    1.61 -
    1.62 -lemma prod_cases7 [cases type]: "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
    1.63 -  apply (cases y)
    1.64 -  apply (case_tac f)
    1.65 -  apply blast
    1.66 -  done
    1.67 -
    1.68 -lemma prod_induct7 [induct type]: "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
    1.69 -  apply (cases x)
    1.70 -  apply blast
    1.71 -  done
    1.72 -
    1.73  
    1.74  (* generic summation indexed over nat *)
    1.75