# HG changeset patch # User wenzelm # Date 1003247510 -7200 # Node ID 30f2104953a154e8280461fcb87e0d84eb5e2688 # Parent 1d5f5d2427d26a8c3c4458b74a81ed87c9e1e488 tuned; diff -r 1d5f5d2427d2 -r 30f2104953a1 src/HOL/PreList.thy --- a/src/HOL/PreList.thy Tue Oct 16 17:51:12 2001 +0200 +++ b/src/HOL/PreList.thy Tue Oct 16 17:51:50 2001 +0200 @@ -11,7 +11,7 @@ Option + Wellfounded_Relations + NatSimprocs + Recdef + Record + Relation_Power + Calculation + SVC_Oracle: -(*belongs to theory HOL*) +(*belongs to theory Datatype*) declare case_split [cases type: bool] (*belongs to theory Wellfounded_Recursion*) @@ -21,70 +21,67 @@ hide const Node Atom Leaf Numb Lim Funs Split Case hide type node item -(*belongs to theory Product_Type; canonical case/induct rules for 3-7 tuples*) -lemma prod_cases3 [cases type: *]: "(!!a b c. y = (a, b, c) ==> P) ==> P" -apply (cases y) -apply (case_tac b) -apply blast -done +(*belongs to theory Datatype; canonical case/induct rules for 3-7 tuples*) +lemma prod_cases3 [cases type]: "(!!a b c. y = (a, b, c) ==> P) ==> P" + apply (cases y) + apply (case_tac b) + apply blast + done -lemma prod_induct3 [induct type: *]: "(!!a b c. P (a, b, c)) ==> P x" -apply (cases x) -apply blast -done +lemma prod_induct3 [induct type]: "(!!a b c. P (a, b, c)) ==> P x" + apply (cases x) + apply blast + done -lemma prod_cases4 [cases type: *]: "(!!a b c d. y = (a, b, c, d) ==> P) ==> P" -apply (cases y) -apply (case_tac c) -apply blast -done +lemma prod_cases4 [cases type]: "(!!a b c d. y = (a, b, c, d) ==> P) ==> P" + apply (cases y) + apply (case_tac c) + apply blast + done -lemma prod_induct4 [induct type: *]: "(!!a b c d. P (a, b, c, d)) ==> P x" -apply (cases x) -apply blast -done +lemma prod_induct4 [induct type]: "(!!a b c d. P (a, b, c, d)) ==> P x" + apply (cases x) + apply blast + done -lemma prod_cases5 [cases type: *]: "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P" -apply (cases y) -apply (case_tac d) -apply blast -done +lemma prod_cases5 [cases type]: "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P" + apply (cases y) + apply (case_tac d) + apply blast + done -lemma prod_induct5 [induct type: *]: "(!!a b c d e. P (a, b, c, d, e)) ==> P x" -apply (cases x) -apply blast -done +lemma prod_induct5 [induct type]: "(!!a b c d e. P (a, b, c, d, e)) ==> P x" + apply (cases x) + apply blast + done -lemma prod_cases6 [cases type: *]: "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P" -apply (cases y) -apply (case_tac e) -apply blast -done +lemma prod_cases6 [cases type]: "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P" + apply (cases y) + apply (case_tac e) + apply blast + done -lemma prod_induct6 [induct type: *]: "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" -apply (cases x) -apply blast -done +lemma prod_induct6 [induct type]: "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" + apply (cases x) + apply blast + done -lemma prod_cases7 [cases type: *]: "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P" -apply (cases y) -apply (case_tac f) -apply blast -done +lemma prod_cases7 [cases type]: "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P" + apply (cases y) + apply (case_tac f) + apply blast + done -lemma prod_induct7 [induct type: *]: "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" -apply (cases x) -apply blast -done +lemma prod_induct7 [induct type]: "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" + apply (cases x) + apply blast + done (* generic summation indexed over nat *) -(*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*) -(*FIXME port theorems from Algebra/abstract/NatSum*) - consts - Summation :: "(nat => 'a::{zero,plus}) => nat => 'a" + Summation :: "(nat => 'a::{zero, plus}) => nat => 'a" primrec "Summation f 0 = 0" "Summation f (Suc n) = Summation f n + f n"