# HG changeset patch # User wenzelm # Date 981057073 -3600 # Node ID 23bf8d787b04f4f3f810190b1be3c9e323860fb8 # Parent 6e6c8d1ec89eacd35ef53c54f6ba6cce9bcfb78a converted to new-style theories; diff -r 6e6c8d1ec89e -r 23bf8d787b04 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Feb 01 20:48:58 2001 +0100 +++ b/src/HOL/IsaMakefile Thu Feb 01 20:51:13 2001 +0100 @@ -484,13 +484,13 @@ HOL-ex: HOL $(LOG)/HOL-ex.gz $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.ML ex/AVL.thy ex/Antiquote.thy \ - ex/BT.ML ex/BT.thy ex/BinEx.ML ex/BinEx.thy ex/Group.ML ex/Group.thy \ + ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy \ ex/InSort.ML ex/InSort.thy ex/IntRing.ML ex/IntRing.thy \ ex/Lagrange.ML ex/Lagrange.thy ex/LocaleGroup.ML ex/LocaleGroup.thy \ - ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.ML \ - ex/NatSum.thy ex/PER.thy ex/PiSets.ML ex/PiSets.thy ex/Primrec.ML \ + ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \ + ex/NatSum.thy ex/PER.thy ex/PiSets.ML ex/PiSets.thy \ ex/Primrec.thy ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \ - ex/ROOT.ML ex/Recdefs.ML ex/Recdefs.thy ex/Records.thy ex/Ring.ML \ + ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/Ring.ML \ ex/Ring.thy ex/StringEx.thy ex/Tarski.ML \ ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML ex/mesontest2.ML \ ex/mesontest2.thy ex/set.ML ex/set.thy ex/svc_test.ML ex/svc_test.thy diff -r 6e6c8d1ec89e -r 23bf8d787b04 src/HOL/ex/BT.ML --- a/src/HOL/ex/BT.ML Thu Feb 01 20:48:58 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,57 +0,0 @@ -(* Title: HOL/ex/BT.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1995 University of Cambridge - -Datatype definition of binary trees -*) - -(** BT simplification **) - -Goal "n_leaves(reflect(t)) = n_leaves(t)"; -by (induct_tac "t" 1); -by Auto_tac; -qed "n_leaves_reflect"; - -Goal "n_nodes(reflect(t)) = n_nodes(t)"; -by (induct_tac "t" 1); -by Auto_tac; -qed "n_nodes_reflect"; - -(*The famous relationship between the numbers of leaves and nodes*) -Goal "n_leaves(t) = Suc(n_nodes(t))"; -by (induct_tac "t" 1); -by Auto_tac; -qed "n_leaves_nodes"; - -Goal "reflect(reflect(t))=t"; -by (induct_tac "t" 1); -by Auto_tac; -qed "reflect_reflect_ident"; - -Goal "bt_map f (reflect t) = reflect (bt_map f t)"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "bt_map_reflect"; - -Goal "inorder (bt_map f t) = map f (inorder t)"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "inorder_bt_map"; - -Goal "preorder (reflect t) = rev (postorder t)"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "preorder_reflect"; - -Goal "inorder (reflect t) = rev (inorder t)"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "inorder_reflect"; - -Goal "postorder (reflect t) = rev (preorder t)"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "postorder_reflect"; - - diff -r 6e6c8d1ec89e -r 23bf8d787b04 src/HOL/ex/BT.thy --- a/src/HOL/ex/BT.thy Thu Feb 01 20:48:58 2001 +0100 +++ b/src/HOL/ex/BT.thy Thu Feb 01 20:51:13 2001 +0100 @@ -3,26 +3,29 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge -Binary trees (based on the ZF version) +Binary trees (based on the ZF version). *) -BT = Main + +header {* Binary trees *} + +theory BT = Main: -datatype 'a bt = Lf - | Br 'a ('a bt) ('a bt) - +datatype 'a bt = + Lf + | Br 'a "'a bt" "'a bt" + consts - n_nodes :: 'a bt => nat - n_leaves :: 'a bt => nat - reflect :: 'a bt => 'a bt - bt_map :: ('a=>'b) => ('a bt => 'b bt) - preorder :: 'a bt => 'a list - inorder :: 'a bt => 'a list - postorder :: 'a bt => 'a list + n_nodes :: "'a bt => nat" + n_leaves :: "'a bt => nat" + reflect :: "'a bt => 'a bt" + bt_map :: "('a => 'b) => ('a bt => 'b bt)" + preorder :: "'a bt => 'a list" + inorder :: "'a bt => 'a list" + postorder :: "'a bt => 'a list" primrec "n_nodes (Lf) = 0" - "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)" + "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" primrec "n_leaves (Lf) = Suc 0" @@ -48,5 +51,56 @@ "postorder (Lf) = []" "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" + +text {* \medskip BT simplification *} + +lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" + apply (induct t) + apply auto + done + +lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" + apply (induct t) + apply auto + done + +text {* + The famous relationship between the numbers of leaves and nodes. +*} + +lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" + apply (induct t) + apply auto + done + +lemma reflect_reflect_ident: "reflect (reflect t) = t" + apply (induct t) + apply auto + done + +lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" + apply (induct t) + apply simp_all + done + +lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" + apply (induct t) + apply simp_all + done + +lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" + apply (induct t) + apply simp_all + done + +lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" + apply (induct t) + apply simp_all + done + +lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" + apply (induct t) + apply simp_all + done + end - diff -r 6e6c8d1ec89e -r 23bf8d787b04 src/HOL/ex/BinEx.ML --- a/src/HOL/ex/BinEx.ML Thu Feb 01 20:48:58 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,372 +0,0 @@ -(* Title: HOL/ex/BinEx.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Examples of performing binary arithmetic by simplification - -Also a proof that binary arithmetic on normalized operands -yields normalized results. -*) - -(**** The Integers ****) - -(*** Addition ***) - -Goal "(#13::int) + #19 = #32"; -by (Simp_tac 1); -result(); - -Goal "(#1234::int) + #5678 = #6912"; -by (Simp_tac 1); -result(); - -Goal "(#1359::int) + #-2468 = #-1109"; -by (Simp_tac 1); -result(); - -Goal "(#93746::int) + #-46375 = #47371"; -by (Simp_tac 1); -result(); - -(*** Negation ***) - -Goal "- (#65745::int) = #-65745"; -by (Simp_tac 1); -result(); - -Goal "- (#-54321::int) = #54321"; -by (Simp_tac 1); -result(); - - -(*** Multiplication ***) - -Goal "(#13::int) * #19 = #247"; -by (Simp_tac 1); -result(); - -Goal "(#-84::int) * #51 = #-4284"; -by (Simp_tac 1); -result(); - -Goal "(#255::int) * #255 = #65025"; -by (Simp_tac 1); -result(); - -Goal "(#1359::int) * #-2468 = #-3354012"; -by (Simp_tac 1); -result(); - -Goal "(#89::int) * #10 ~= #889"; -by (Simp_tac 1); -result(); - -Goal "(#13::int) < #18 - #4"; -by (Simp_tac 1); -result(); - -Goal "(#-345::int) < #-242 + #-100"; -by (Simp_tac 1); -result(); - -Goal "(#13557456::int) < #18678654"; -by (Simp_tac 1); -result(); - -Goal "(#999999::int) <= (#1000001 + #1)-#2"; -by (Simp_tac 1); -result(); - -Goal "(#1234567::int) <= #1234567"; -by (Simp_tac 1); -result(); - - -(*** Quotient and Remainder ***) - -Goal "(#10::int) div #3 = #3"; -by (Simp_tac 1); -result(); - -Goal "(#10::int) mod #3 = #1"; -by (Simp_tac 1); -result(); - -(** A negative divisor **) - -Goal "(#10::int) div #-3 = #-4"; -by (Simp_tac 1); -result(); - -Goal "(#10::int) mod #-3 = #-2"; -by (Simp_tac 1); -result(); - -(** A negative dividend - [ The definition agrees with mathematical convention but not with - the hardware of most computers ] -**) - -Goal "(#-10::int) div #3 = #-4"; -by (Simp_tac 1); -result(); - -Goal "(#-10::int) mod #3 = #2"; -by (Simp_tac 1); -result(); - -(** A negative dividend AND divisor **) - -Goal "(#-10::int) div #-3 = #3"; -by (Simp_tac 1); -result(); - -Goal "(#-10::int) mod #-3 = #-1"; -by (Simp_tac 1); -result(); - -(** A few bigger examples **) - -Goal "(#8452::int) mod #3 = #1"; -by (Simp_tac 1); -result(); - -Goal "(#59485::int) div #434 = #137"; -by (Simp_tac 1); -result(); - -Goal "(#1000006::int) mod #10 = #6"; -by (Simp_tac 1); -result(); - - -(** division by shifting **) - -Goal "#10000000 div #2 = (#5000000::int)"; -by (Simp_tac 1); -result(); - -Goal "#10000001 mod #2 = (#1::int)"; -by (Simp_tac 1); -result(); - -Goal "#10000055 div #32 = (#312501::int)"; -by (Simp_tac 1); - -Goal "#10000055 mod #32 = (#23::int)"; -by (Simp_tac 1); - -Goal "#100094 div #144 = (#695::int)"; -by (Simp_tac 1); -result(); - -Goal "#100094 mod #144 = (#14::int)"; -by (Simp_tac 1); -result(); - - - -(**** The Natural Numbers ****) - -(** Successor **) - -Goal "Suc #99999 = #100000"; -by (asm_simp_tac (simpset() addsimps [Suc_nat_number_of]) 1); - (*not a default rewrite since sometimes we want to have Suc(#nnn)*) -result(); - - -(** Addition **) - -Goal "(#13::nat) + #19 = #32"; -by (Simp_tac 1); -result(); - -Goal "(#1234::nat) + #5678 = #6912"; -by (Simp_tac 1); -result(); - -Goal "(#973646::nat) + #6475 = #980121"; -by (Simp_tac 1); -result(); - - -(** Subtraction **) - -Goal "(#32::nat) - #14 = #18"; -by (Simp_tac 1); -result(); - -Goal "(#14::nat) - #15 = #0"; -by (Simp_tac 1); -result(); - -Goal "(#14::nat) - #1576644 = #0"; -by (Simp_tac 1); -result(); - -Goal "(#48273776::nat) - #3873737 = #44400039"; -by (Simp_tac 1); -result(); - - -(** Multiplication **) - -Goal "(#12::nat) * #11 = #132"; -by (Simp_tac 1); -result(); - -Goal "(#647::nat) * #3643 = #2357021"; -by (Simp_tac 1); -result(); - - -(** Quotient and Remainder **) - -Goal "(#10::nat) div #3 = #3"; -by (Simp_tac 1); -result(); - -Goal "(#10::nat) mod #3 = #1"; -by (Simp_tac 1); -result(); - -Goal "(#10000::nat) div #9 = #1111"; -by (Simp_tac 1); -result(); - -Goal "(#10000::nat) mod #9 = #1"; -by (Simp_tac 1); -result(); - -Goal "(#10000::nat) div #16 = #625"; -by (Simp_tac 1); -result(); - -Goal "(#10000::nat) mod #16 = #0"; -by (Simp_tac 1); -result(); - - -(*** Testing the cancellation of complementary terms ***) - -Goal "y + (x + -x) = (#0::int) + y"; -by (Simp_tac 1); -result(); - -Goal "y + (-x + (- y + x)) = (#0::int)"; -by (Simp_tac 1); -result(); - -Goal "-x + (y + (- y + x)) = (#0::int)"; -by (Simp_tac 1); -result(); - -Goal "x + (x + (- x + (- x + (- y + - z)))) = (#0::int) - y - z"; -by (Simp_tac 1); -result(); - -Goal "x + x - x - x - y - z = (#0::int) - y - z"; -by (Simp_tac 1); -result(); - -Goal "x + y + z - (x + z) = y - (#0::int)"; -by (Simp_tac 1); -result(); - -Goal "x+(y+(y+(y+ (-x + -x)))) = (#0::int) + y - x + y + y"; -by (Simp_tac 1); -result(); - -Goal "x+(y+(y+(y+ (-y + -x)))) = y + (#0::int) + y"; -by (Simp_tac 1); -result(); - -Goal "x + y - x + z - x - y - z + x < (#1::int)"; -by (Simp_tac 1); -result(); - - -Addsimps normal.intrs; - -Goal "(w BIT b): normal ==> (w BIT b BIT c): normal"; -by (case_tac "c" 1); -by Auto_tac; -qed "normal_BIT_I"; - -Addsimps [normal_BIT_I]; - -Goal "w BIT b: normal ==> w: normal"; -by (etac normal.elim 1); -by Auto_tac; -qed "normal_BIT_D"; - -Goal "w : normal --> NCons w b : normal"; -by (induct_tac "w" 1); -by (auto_tac (claset(), simpset() addsimps [NCons_Pls, NCons_Min])); -qed_spec_mp "NCons_normal"; - -Addsimps [NCons_normal]; - -Goal "NCons w True ~= Pls"; -by (induct_tac "w" 1); -by Auto_tac; -qed "NCons_True"; - -Goal "NCons w False ~= Min"; -by (induct_tac "w" 1); -by Auto_tac; -qed "NCons_False"; - -Goal "w: normal ==> bin_succ w : normal"; -by (etac normal.induct 1); -by (case_tac "w" 4); -by (auto_tac (claset(), simpset() addsimps [NCons_True, bin_succ_BIT])); -qed "bin_succ_normal"; - -Goal "w: normal ==> bin_pred w : normal"; -by (etac normal.induct 1); -by (case_tac "w" 3); -by (auto_tac (claset(), simpset() addsimps [NCons_False, bin_pred_BIT])); -qed "bin_pred_normal"; - -Addsimps [bin_succ_normal, bin_pred_normal]; - -Goal "w : normal --> (ALL z. z: normal --> bin_add w z : normal)"; -by (induct_tac "w" 1); -by (Simp_tac 1); -by (Simp_tac 1); -by (rtac impI 1); -by (rtac allI 1); -by (induct_tac "z" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_add_BIT]))); -by (safe_tac (claset() addSDs [normal_BIT_D])); -by (ALLGOALS Asm_simp_tac); -qed_spec_mp "bin_add_normal"; - -Goal "w: normal ==> (w = Pls) = (number_of w = (#0::int))"; -by (etac normal.induct 1); -by Auto_tac; -qed "normal_Pls_eq_0"; - -Goal "w : normal ==> bin_minus w : normal"; -by (etac normal.induct 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_BIT]))); -by (resolve_tac normal.intrs 1); -by (assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps [normal_Pls_eq_0]) 1); -by (asm_full_simp_tac - (simpset_of Int.thy - addsimps [number_of_minus, iszero_def, - read_instantiate [("y","int 0")] zminus_equation]) 1); -by (etac not_sym 1); -qed "bin_minus_normal"; - -Goal "w : normal ==> z: normal --> bin_mult w z : normal"; -by (etac normal.induct 1); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps [bin_minus_normal, bin_mult_BIT]))); -by (safe_tac (claset() addSDs [normal_BIT_D])); -by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1); -qed_spec_mp "bin_mult_normal"; diff -r 6e6c8d1ec89e -r 23bf8d787b04 src/HOL/ex/BinEx.thy --- a/src/HOL/ex/BinEx.thy Thu Feb 01 20:48:58 2001 +0100 +++ b/src/HOL/ex/BinEx.thy Thu Feb 01 20:51:13 2001 +0100 @@ -2,26 +2,328 @@ ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge - -Definition of normal form for proving that binary arithmetic on -normalized operands yields normalized results. - -Normal means no leading 0s on positive numbers and no leading 1s on negatives. *) -BinEx = Main + +header {* Binary arithmetic examples *} + +theory BinEx = Main: + +subsection {* The Integers *} + +text {* Addition *} + +lemma "(#13::int) + #19 = #32" + by simp + +lemma "(#1234::int) + #5678 = #6912" + by simp + +lemma "(#1359::int) + #-2468 = #-1109" + by simp + +lemma "(#93746::int) + #-46375 = #47371" + by simp + + +text {* \medskip Negation *} + +lemma "- (#65745::int) = #-65745" + by simp + +lemma "- (#-54321::int) = #54321" + by simp + + +text {* \medskip Multiplication *} + +lemma "(#13::int) * #19 = #247" + by simp + +lemma "(#-84::int) * #51 = #-4284" + by simp + +lemma "(#255::int) * #255 = #65025" + by simp + +lemma "(#1359::int) * #-2468 = #-3354012" + by simp + +lemma "(#89::int) * #10 \ #889" + by simp + +lemma "(#13::int) < #18 - #4" + by simp + +lemma "(#-345::int) < #-242 + #-100" + by simp + +lemma "(#13557456::int) < #18678654" + by simp + +lemma "(#999999::int) \ (#1000001 + #1) - #2" + by simp + +lemma "(#1234567::int) \ #1234567" + by simp + + +text {* \medskip Quotient and Remainder *} + +lemma "(#10::int) div #3 = #3" + by simp + +lemma "(#10::int) mod #3 = #1" + by simp + +text {* A negative divisor *} + +lemma "(#10::int) div #-3 = #-4" + by simp + +lemma "(#10::int) mod #-3 = #-2" + by simp -consts normal :: bin set - -inductive "normal" - intrs +text {* + A negative dividend\footnote{The definition agrees with mathematical + convention but not with the hardware of most computers} +*} + +lemma "(#-10::int) div #3 = #-4" + by simp + +lemma "(#-10::int) mod #3 = #2" + by simp + +text {* A negative dividend \emph{and} divisor *} + +lemma "(#-10::int) div #-3 = #3" + by simp + +lemma "(#-10::int) mod #-3 = #-1" + by simp + +text {* A few bigger examples *} + +lemma "(#8452::int) mod #3 = #1" + by simp + +lemma "(#59485::int) div #434 = #137" + by simp + +lemma "(#1000006::int) mod #10 = #6" + by simp + + +text {* \medskip Division by shifting *} + +lemma "#10000000 div #2 = (#5000000::int)" + by simp + +lemma "#10000001 mod #2 = (#1::int)" + by simp + +lemma "#10000055 div #32 = (#312501::int)" + by simp + +lemma "#10000055 mod #32 = (#23::int)" + by simp + +lemma "#100094 div #144 = (#695::int)" + by simp + +lemma "#100094 mod #144 = (#14::int)" + by simp + + +subsection {* The Natural Numbers *} + +text {* Successor *} + +lemma "Suc #99999 = #100000" + by (simp add: Suc_nat_number_of) + -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *} + + +text {* \medskip Addition *} + +lemma "(#13::nat) + #19 = #32" + by simp + +lemma "(#1234::nat) + #5678 = #6912" + by simp + +lemma "(#973646::nat) + #6475 = #980121" + by simp + + +text {* \medskip Subtraction *} + +lemma "(#32::nat) - #14 = #18" + by simp + +lemma "(#14::nat) - #15 = #0" + by simp - Pls "Pls: normal" +lemma "(#14::nat) - #1576644 = #0" + by simp + +lemma "(#48273776::nat) - #3873737 = #44400039" + by simp + + +text {* \medskip Multiplication *} + +lemma "(#12::nat) * #11 = #132" + by simp + +lemma "(#647::nat) * #3643 = #2357021" + by simp + + +text {* \medskip Quotient and Remainder *} + +lemma "(#10::nat) div #3 = #3" + by simp + +lemma "(#10::nat) mod #3 = #1" + by simp + +lemma "(#10000::nat) div #9 = #1111" + by simp + +lemma "(#10000::nat) mod #9 = #1" + by simp + +lemma "(#10000::nat) div #16 = #625" + by simp + +lemma "(#10000::nat) mod #16 = #0" + by simp + - Min "Min: normal" +text {* \medskip Testing the cancellation of complementary terms *} + +lemma "y + (x + -x) = (#0::int) + y" + by simp + +lemma "y + (-x + (- y + x)) = (#0::int)" + by simp + +lemma "-x + (y + (- y + x)) = (#0::int)" + by simp + +lemma "x + (x + (- x + (- x + (- y + - z)))) = (#0::int) - y - z" + by simp + +lemma "x + x - x - x - y - z = (#0::int) - y - z" + by simp + +lemma "x + y + z - (x + z) = y - (#0::int)" + by simp + +lemma "x + (y + (y + (y + (-x + -x)))) = (#0::int) + y - x + y + y" + by simp + +lemma "x + (y + (y + (y + (-y + -x)))) = y + (#0::int) + y" + by simp + +lemma "x + y - x + z - x - y - z + x < (#1::int)" + by simp + + +subsection {* Normal form of bit strings *} + +text {* + Definition of normal form for proving that binary arithmetic on + normalized operands yields normalized results. Normal means no + leading 0s on positive numbers and no leading 1s on negatives. +*} - BIT_F "[| w: normal; w ~= Pls |] ==> w BIT False : normal" +consts normal :: "bin set" +inductive "normal" + intros [simp] + Pls: "Pls: normal" + Min: "Min: normal" + BIT_F: "w: normal ==> w \ Pls ==> w BIT False : normal" + BIT_T: "w: normal ==> w \ Min ==> w BIT True : normal" + +text {* + \medskip Binary arithmetic on normalized operands yields normalized + results. +*} + +lemma normal_BIT_I [simp]: "w BIT b \ normal ==> w BIT b BIT c \ normal" + apply (case_tac c) + apply auto + done + +lemma normal_BIT_D: "w BIT b \ normal ==> w \ normal" + apply (erule normal.cases) + apply auto + done + +lemma NCons_normal [simp]: "w \ normal ==> NCons w b \ normal" + apply (induct w) + apply (auto simp add: NCons_Pls NCons_Min) + done + +lemma NCons_True: "NCons w True \ Pls" + apply (induct w) + apply auto + done + +lemma NCons_False: "NCons w False \ Min" + apply (induct w) + apply auto + done - BIT_T "[| w: normal; w ~= Min |] ==> w BIT True : normal" +lemma bin_succ_normal [simp]: "w \ normal ==> bin_succ w \ normal" + apply (erule normal.induct) + apply (case_tac [4] w) + apply (auto simp add: NCons_True bin_succ_BIT) + done + +lemma bin_pred_normal [simp]: "w \ normal ==> bin_pred w \ normal" + apply (erule normal.induct) + apply (case_tac [3] w) + apply (auto simp add: NCons_False bin_pred_BIT) + done + +lemma bin_add_normal [rule_format]: + "w \ normal --> (\z. z \ normal --> bin_add w z \ normal)" + apply (induct w) + apply simp + apply simp + apply (rule impI) + apply (rule allI) + apply (induct_tac z) + apply (simp_all add: bin_add_BIT) + apply (safe dest!: normal_BIT_D) + apply simp_all + done + +lemma normal_Pls_eq_0: "w \ normal ==> (w = Pls) = (number_of w = (#0::int))" + apply (erule normal.induct) + apply auto + done + +lemma bin_minus_normal: "w \ normal ==> bin_minus w \ normal" + apply (erule normal.induct) + apply (simp_all add: bin_minus_BIT) + apply (rule normal.intros) + apply assumption + apply (simp add: normal_Pls_eq_0) + apply (simp only: number_of_minus iszero_def zminus_equation [of _ "int 0"]) + apply (rule not_sym) + apply simp + done + +lemma bin_mult_normal [rule_format]: + "w \ normal ==> z \ normal --> bin_mult w z \ normal" + apply (erule normal.induct) + apply (simp_all add: bin_minus_normal bin_mult_BIT) + apply (safe dest!: normal_BIT_D) + apply (simp add: bin_add_normal) + done end diff -r 6e6c8d1ec89e -r 23bf8d787b04 src/HOL/ex/NatSum.ML --- a/src/HOL/ex/NatSum.ML Thu Feb 01 20:48:58 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,96 +0,0 @@ -(* Title: HOL/ex/NatSum.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1994 TU Muenchen - -Summing natural numbers, squares, cubes, etc. - -Originally demonstrated permutative rewriting, but add_ac is no longer needed - thanks to new simprocs. - -Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, - http://www.research.att.com/~njas/sequences/ -*) - -Addsimps [lessThan_Suc, atMost_Suc]; -Addsimps [add_mult_distrib, add_mult_distrib2]; -Addsimps [diff_mult_distrib, diff_mult_distrib2]; - -(*The sum of the first n odd numbers equals n squared.*) -Goal "setsum (%i. Suc(i+i)) (lessThan n) = n*n"; -by (induct_tac "n" 1); -by Auto_tac; -qed "sum_of_odds"; - -(*The sum of the first n odd squares*) -Goal "#3 * setsum (%i. Suc(i+i)*Suc(i+i)) (lessThan n) = n * (#4*n*n - #1)"; -by (induct_tac "n" 1); -(*This removes the -#1 from the inductive step*) -by (case_tac "n" 2); -by Auto_tac; -qed "sum_of_odd_squares"; - -(*The sum of the first n odd cubes*) -Goal "setsum (%i. Suc(i+i)*Suc(i+i)*Suc(i+i)) (lessThan n) = n * n * (#2*n*n - #1)"; -by (induct_tac "n" 1); -(*This removes the -#1 from the inductive step*) -by (case_tac "n" 2); -by Auto_tac; -qed "sum_of_odd_cubes"; - -(*The sum of the first n positive integers equals n(n+1)/2.*) -Goal "#2 * setsum id (atMost n) = n*Suc(n)"; -by (induct_tac "n" 1); -by Auto_tac; -qed "sum_of_naturals"; - -Goal "#6 * setsum (%i. i*i) (atMost n) = n * Suc(n) * Suc(#2*n)"; -by (induct_tac "n" 1); -by Auto_tac; -qed "sum_of_squares"; - -Goal "#4 * setsum (%i. i*i*i) (atMost n) = n * n * Suc(n) * Suc(n)"; -by (induct_tac "n" 1); -by Auto_tac; -qed "sum_of_cubes"; - -(** Sum of fourth powers: two versions **) - -Goal "#30 * setsum (%i. i*i*i*i) (atMost n) = \ -\ n * Suc(n) * Suc(#2*n) * (#3*n*n + #3*n - #1)"; -by (induct_tac "n" 1); -by Auto_tac; -(*Eliminates the subtraction*) -by (case_tac "n" 1); -by (ALLGOALS Asm_simp_tac); -qed "sum_of_fourth_powers"; - -(*Alternative proof, with a change of variables and much more subtraction, - performed using the integers.*) - -Addsimps [zmult_int RS sym, zadd_zmult_distrib, zadd_zmult_distrib2, - zdiff_zmult_distrib, zdiff_zmult_distrib2]; - -Goal "#30 * int (setsum (%i. i*i*i*i) (lessThan m)) = \ -\ int m * (int m - #1) * (int (#2*m) - #1) * \ -\ (int (#3*m*m) - int(#3*m) - #1)"; -by (induct_tac "m" 1); -by (ALLGOALS Asm_simp_tac); -qed "int_sum_of_fourth_powers"; - -(** Sums of geometric series: 2, 3 and the general case **) - -Goal "setsum (%i. #2^i) (lessThan n) = #2^n - 1"; -by (induct_tac "n" 1); -by Auto_tac; -qed "sum_of_2_powers"; - -Goal "#2 * setsum (%i. #3^i) (lessThan n) = #3^n - 1"; -by (induct_tac "n" 1); -by Auto_tac; -qed "sum_of_3_powers"; - -Goal "0 (k-1) * setsum (%i. k^i) (lessThan n) = k^n - 1"; -by (induct_tac "n" 1); -by Auto_tac; -qed "sum_of_powers"; diff -r 6e6c8d1ec89e -r 23bf8d787b04 src/HOL/ex/NatSum.thy --- a/src/HOL/ex/NatSum.thy Thu Feb 01 20:48:58 2001 +0100 +++ b/src/HOL/ex/NatSum.thy Thu Feb 01 20:51:13 2001 +0100 @@ -1,1 +1,132 @@ -NatSum = Main +(* Title: HOL/ex/NatSum.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Summing natural numbers, squares, cubes, etc. + +Originally demonstrated permutative rewriting, but add_ac is no longer +needed thanks to new simprocs. + +Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, +http://www.research.att.com/~njas/sequences/ +*) + +header {* Summing natural numbers *} + +theory NatSum = Main: + +declare lessThan_Suc [simp] atMost_Suc [simp] +declare add_mult_distrib [simp] add_mult_distrib2 [simp] +declare diff_mult_distrib [simp] diff_mult_distrib2 [simp] + +text {* + \medskip The sum of the first @{term n} odd numbers equals @{term n} + squared. +*} + +lemma sum_of_odds: "setsum (\i. Suc (i + i)) (lessThan n) = n * n" + apply (induct n) + apply auto + done + + +text {* + \medskip The sum of the first @{text n} odd squares. +*} + +lemma sum_of_odd_squares: + "#3 * setsum (\i. Suc (i + i) * Suc (i + i)) (lessThan n) = n * (#4 * n * n - #1)" + apply (induct n) + txt {* This removes the @{term "-#1"} from the inductive step *} + apply (case_tac [2] n) + apply auto + done + + +text {* + \medskip The sum of the first @{term n} odd cubes +*} + +lemma sum_of_odd_cubes: + "setsum (\i. Suc (i + i) * Suc (i + i) * Suc (i + i)) (lessThan n) = + n * n * (#2 * n * n - #1)" + apply (induct "n") + txt {* This removes the @{term "-#1"} from the inductive step *} + apply (case_tac [2] "n") + apply auto + done + +text {* + \medskip The sum of the first @{term n} positive integers equals + @{text "n (n + 1) / 2"}.*} + +lemma sum_of_naturals: "#2 * setsum id (atMost n) = n * Suc n" + apply (induct n) + apply auto + done + +lemma sum_of_squares: "#6 * setsum (\i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)" + apply (induct n) + apply auto + done + +lemma sum_of_cubes: "#4 * setsum (\i. i * i * i) (atMost n) = n * n * Suc n * Suc n" + apply (induct n) + apply auto + done + + +text {* + \medskip Sum of fourth powers: two versions. +*} + +lemma sum_of_fourth_powers: + "#30 * setsum (\i. i * i * i * i) (atMost n) = + n * Suc n * Suc (#2 * n) * (#3 * n * n + #3 * n - #1)" + apply (induct n) + apply auto + txt {* Eliminates the subtraction *} + apply (case_tac n) + apply simp_all + done + +text {* + Alternative proof, with a change of variables and much more + subtraction, performed using the integers. *} + +declare + zmult_int [symmetric, simp] + zadd_zmult_distrib [simp] + zadd_zmult_distrib2 [simp] + zdiff_zmult_distrib [simp] + zdiff_zmult_distrib2 [simp] + +lemma int_sum_of_fourth_powers: + "#30 * int (setsum (\i. i * i * i * i) (lessThan m)) = + int m * (int m - #1) * (int (#2 * m) - #1) * + (int (#3 * m * m) - int (#3 * m) - #1)" + apply (induct m) + apply simp_all + done + + +text {* + \medskip Sums of geometric series: 2, 3 and the general case *} + +lemma sum_of_2_powers: "setsum (\i. #2^i) (lessThan n) = #2^n - 1" + apply (induct n) + apply auto + done + +lemma sum_of_3_powers: "#2 * setsum (\i. #3^i) (lessThan n) = #3^n - 1" + apply (induct n) + apply auto + done + +lemma sum_of_powers: "0 < k ==> (k - 1) * setsum (\i. k^i) (lessThan n) = k^n - 1" + apply (induct n) + apply auto + done + +end diff -r 6e6c8d1ec89e -r 23bf8d787b04 src/HOL/ex/Primrec.ML --- a/src/HOL/ex/Primrec.ML Thu Feb 01 20:48:58 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,270 +0,0 @@ -(* Title: HOL/ex/Primrec - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -Primitive Recursive Functions - -Proof adopted from -Nora Szasz, -A Machine Checked Proof that Ackermann's Function is not Primitive Recursive, -In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338. - -See also E. Mendelson, Introduction to Mathematical Logic. -(Van Nostrand, 1964), page 250, exercise 11. -*) - - -(** Useful special cases of evaluation ***) - -Goalw [SC_def] "SC (x#l) = Suc x"; -by (Asm_simp_tac 1); -qed "SC"; - -Goalw [CONST_def] "CONST k l = k"; -by (Asm_simp_tac 1); -qed "CONST"; - -Goalw [PROJ_def] "PROJ(0) (x#l) = x"; -by (Asm_simp_tac 1); -qed "PROJ_0"; - -Goalw [COMP_def] "COMP g [f] l = g [f l]"; -by (Asm_simp_tac 1); -qed "COMP_1"; - -Goalw [PREC_def] "PREC f g (0#l) = f l"; -by (Asm_simp_tac 1); -qed "PREC_0"; - -Goalw [PREC_def] "PREC f g (Suc x # l) = g (PREC f g (x#l) # x # l)"; -by (Asm_simp_tac 1); -qed "PREC_Suc"; - -Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc]; - - -(*PROPERTY A 4*) -Goal "j < ack(i,j)"; -by (induct_thm_tac ack.induct "i j" 1); -by (ALLGOALS Asm_simp_tac); -qed "less_ack2"; - -AddIffs [less_ack2]; - -(*PROPERTY A 5-, the single-step lemma*) -Goal "ack(i,j) < ack(i, Suc(j))"; -by (induct_thm_tac ack.induct "i j" 1); -by (ALLGOALS Asm_simp_tac); -qed "ack_less_ack_Suc2"; - -AddIffs [ack_less_ack_Suc2]; - -(*PROPERTY A 5, monotonicity for < *) -Goal "j ack(i,j) < ack(i,k)"; -by (induct_thm_tac ack.induct "i k" 1); -by (ALLGOALS Asm_simp_tac); -by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1); -qed_spec_mp "ack_less_mono2"; - -(*PROPERTY A 5', monotonicity for<=*) -Goal "j<=k ==> ack(i,j)<=ack(i,k)"; -by (full_simp_tac (simpset() addsimps [order_le_less]) 1); -by (blast_tac (claset() addIs [ack_less_mono2]) 1); -qed "ack_le_mono2"; - -(*PROPERTY A 6*) -Goal "ack(i, Suc(j)) <= ack(Suc(i), j)"; -by (induct_tac "j" 1); -by (ALLGOALS Asm_simp_tac); -by (blast_tac (claset() addIs [ack_le_mono2, less_ack2 RS Suc_leI, - le_trans]) 1); -qed "ack2_le_ack1"; - -AddIffs [ack2_le_ack1]; - -(*PROPERTY A 7-, the single-step lemma*) -Goal "ack(i,j) < ack(Suc(i),j)"; -by (blast_tac (claset() addIs [ack_less_mono2, less_le_trans]) 1); -qed "ack_less_ack_Suc1"; - -AddIffs [ack_less_ack_Suc1]; - -(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*) -Goal "i < ack(i,j)"; -by (induct_tac "i" 1); -by (ALLGOALS Asm_simp_tac); -by (blast_tac (claset() addIs [Suc_leI, le_less_trans]) 1); -qed "less_ack1"; -AddIffs [less_ack1]; - -(*PROPERTY A 8*) -Goal "ack(1,j) = j + #2"; -by (induct_tac "j" 1); -by (ALLGOALS Asm_simp_tac); -qed "ack_1"; -Addsimps [ack_1]; - -(*PROPERTY A 9. The unary 1 and 2 in ack is essential for the rewriting.*) -Goal "ack(2,j) = #2*j + #3"; -by (induct_tac "j" 1); -by (ALLGOALS Asm_simp_tac); -qed "ack_2"; -Addsimps [ack_2]; - - -(*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*) -Goal "ack(i,k) < ack(Suc(i+i'),k)"; -by (induct_thm_tac ack.induct "i k" 1); -by (ALLGOALS Asm_full_simp_tac); -by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2); -by (induct_thm_tac ack.induct "i' n" 1); -by (ALLGOALS Asm_simp_tac); -by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1); -by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1); -val lemma = result(); - -Goal "i ack(i,k) < ack(j,k)"; -by (dtac less_imp_Suc_add 1); -by (blast_tac (claset() addSIs [lemma]) 1); -qed "ack_less_mono1"; - -(*PROPERTY A 7', monotonicity for<=*) -Goal "i<=j ==> ack(i,k)<=ack(j,k)"; -by (full_simp_tac (simpset() addsimps [order_le_less]) 1); -by (blast_tac (claset() addIs [ack_less_mono1]) 1); -qed "ack_le_mono1"; - -(*PROPERTY A 10*) -Goal "ack(i1, ack(i2,j)) < ack(#2 + (i1+i2), j)"; -by (simp_tac numeral_ss 1); -by (rtac (ack2_le_ack1 RSN (2,less_le_trans)) 1); -by (Asm_simp_tac 1); -by (rtac (le_add1 RS ack_le_mono1 RS le_less_trans) 1); -by (rtac (ack_less_mono1 RS ack_less_mono2) 1); -by (simp_tac (simpset() addsimps [le_imp_less_Suc, le_add2]) 1); -qed "ack_nest_bound"; - -(*PROPERTY A 11*) -Goal "ack(i1,j) + ack(i2,j) < ack(#4 + (i1 + i2), j)"; -by (res_inst_tac [("j", "ack(2, ack(i1 + i2, j))")] less_trans 1); -by (Asm_simp_tac 1); -by (rtac (ack_nest_bound RS less_le_trans) 2); -by (asm_simp_tac (simpset() addsimps [Suc3_eq_add_3]) 2); -by (cut_inst_tac [("i","i1"), ("m1","i2"), ("k","j")] - (le_add1 RS ack_le_mono1) 1); -by (cut_inst_tac [("i","i2"), ("m1","i1"), ("k","j")] - (le_add2 RS ack_le_mono1) 1); -by Auto_tac; -qed "ack_add_bound"; - -(*PROPERTY A 12. Article uses existential quantifier but the ALF proof - used k+4. Quantified version must be nested EX k'. ALL i,j... *) -Goal "i < ack(k,j) ==> i+j < ack(#4 + k, j)"; -by (res_inst_tac [("j", "ack(k,j) + ack(0,j)")] less_trans 1); -by (rtac (ack_add_bound RS less_le_trans) 2); -by (Asm_simp_tac 2); -by (REPEAT (ares_tac ([add_less_mono, less_ack2]) 1)); -qed "ack_add_bound2"; - - -(*** Inductive definition of the PR functions ***) - -(*** MAIN RESULT ***) - -Goalw [SC_def] "SC l < ack(1, list_add l)"; -by (induct_tac "l" 1); -by (ALLGOALS (simp_tac (simpset() addsimps [le_add1, le_imp_less_Suc]))); -qed "SC_case"; - -Goal "CONST k l < ack(k, list_add l)"; -by (Simp_tac 1); -qed "CONST_case"; - -Goalw [PROJ_def] "ALL i. PROJ i l < ack(0, list_add l)"; -by (Simp_tac 1); -by (induct_tac "l" 1); -by (ALLGOALS Asm_simp_tac); -by (rtac allI 1); -by (case_tac "i" 1); -by (asm_simp_tac (simpset() addsimps [le_add1, le_imp_less_Suc]) 1); -by (Asm_simp_tac 1); -by (blast_tac (claset() addIs [less_le_trans] - addSIs [le_add2]) 1); -qed_spec_mp "PROJ_case"; - -(** COMP case **) - -Goal "fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \ -\ ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)"; -by (etac lists.induct 1); -by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1); -by Safe_tac; -by (Asm_simp_tac 1); -by (rtac exI 1); -by (blast_tac (claset() addIs [add_less_mono, ack_add_bound, less_trans]) 1); -qed "COMP_map_lemma"; - -Goalw [COMP_def] - "[| ALL l. g l < ack(kg, list_add l); \ -\ fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \ -\ |] ==> EX k. ALL l. COMP g fs l < ack(k, list_add l)"; -by (forward_tac [impOfSubs (Int_lower1 RS lists_mono)] 1); -by (etac (COMP_map_lemma RS exE) 1); -by (rtac exI 1); -by (rtac allI 1); -by (REPEAT (dtac spec 1)); -by (etac less_trans 1); -by (blast_tac (claset() addIs [ack_less_mono2, ack_nest_bound, less_trans]) 1); -qed "COMP_case"; - -(** PREC case **) - -Goalw [PREC_def] - "[| ALL l. f l + list_add l < ack(kf, list_add l); \ -\ ALL l. g l + list_add l < ack(kg, list_add l) \ -\ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)"; -by (case_tac "l" 1); -by (ALLGOALS Asm_simp_tac); -by (blast_tac (claset() addIs [less_trans]) 1); -by (etac ssubst 1); (*get rid of the needless assumption*) -by (induct_tac "a" 1); -by (ALLGOALS Asm_simp_tac); -(*base case*) -by (blast_tac (claset() addIs [le_add1 RS le_imp_less_Suc RS ack_less_mono1, - less_trans]) 1); -(*induction step*) -by (rtac (Suc_leI RS le_less_trans) 1); -by (rtac (le_refl RS add_le_mono RS le_less_trans) 1); -by (etac spec 2); -by (asm_simp_tac (simpset() addsimps [le_add2]) 1); -(*final part of the simplification*) -by (Asm_simp_tac 1); -by (rtac (le_add2 RS ack_le_mono1 RS le_less_trans) 1); -by (etac ack_less_mono2 1); -qed "PREC_case_lemma"; - -Goal "[| ALL l. f l < ack(kf, list_add l); \ -\ ALL l. g l < ack(kg, list_add l) \ -\ |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)"; -by (rtac exI 1); -by (rtac allI 1); -by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1); -by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1)); -qed "PREC_case"; - -Goal "f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)"; -by (etac PRIMREC.induct 1); -by (ALLGOALS - (blast_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, - PREC_case]))); -qed "ack_bounds_PRIMREC"; - -Goal "(%l. case l of [] => 0 | x#l' => ack(x,x)) ~: PRIMREC"; -by (rtac notI 1); -by (etac (ack_bounds_PRIMREC RS exE) 1); -by (rtac less_irrefl 1); -by (dres_inst_tac [("x", "[x]")] spec 1); -by (Asm_full_simp_tac 1); -qed "ack_not_PRIMREC"; - diff -r 6e6c8d1ec89e -r 23bf8d787b04 src/HOL/ex/Primrec.thy --- a/src/HOL/ex/Primrec.thy Thu Feb 01 20:48:58 2001 +0100 +++ b/src/HOL/ex/Primrec.thy Thu Feb 01 20:51:13 2001 +0100 @@ -1,72 +1,348 @@ -(* Title: HOL/ex/Primrec +(* Title: HOL/ex/Primrec.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge -Primitive Recursive Functions - -Proof adopted from -Nora Szasz, -A Machine Checked Proof that Ackermann's Function is not Primitive Recursive, -In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338. - -See also E. Mendelson, Introduction to Mathematical Logic. -(Van Nostrand, 1964), page 250, exercise 11. - -Demonstrates recursive definitions, the TFL package +Primitive Recursive Functions. Demonstrates recursive definitions, +the TFL package. *) -Primrec = Main + +header {* Primitive Recursive Functions *} + +theory Primrec = Main: + +text {* + Proof adopted from + + Nora Szasz, A Machine Checked Proof that Ackermann's Function is not + Primitive Recursive, In: Huet \& Plotkin, eds., Logical Environments + (CUP, 1993), 317-338. + + See also E. Mendelson, Introduction to Mathematical Logic. (Van + Nostrand, 1964), page 250, exercise 11. + \medskip +*} + +consts ack :: "nat * nat => nat" +recdef ack "less_than <*lex*> less_than" + "ack (0, n) = Suc n" + "ack (Suc m, 0) = ack (m, 1)" + "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))" + +consts list_add :: "nat list => nat" +primrec + "list_add [] = 0" + "list_add (m # ms) = m + list_add ms" + +consts zeroHd :: "nat list => nat" +primrec + "zeroHd [] = 0" + "zeroHd (m # ms) = m" + + +text {* The set of primitive recursive functions of type @{typ "nat list => nat"}. *} + +constdefs + SC :: "nat list => nat" + "SC l == Suc (zeroHd l)" -consts ack :: "nat * nat => nat" -recdef ack "less_than <*lex*> less_than" - "ack (0,n) = Suc n" - "ack (Suc m,0) = (ack (m, 1))" - "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))" + CONST :: "nat => nat list => nat" + "CONST k l == k" + + PROJ :: "nat => nat list => nat" + "PROJ i l == zeroHd (drop i l)" + + COMP :: "(nat list => nat) => (nat list => nat) list => nat list => nat" + "COMP g fs l == g (map (\f. f l) fs)" + + PREC :: "(nat list => nat) => (nat list => nat) => nat list => nat" + "PREC f g l == + case l of + [] => 0 + | x # l' => nat_rec (f l') (\y r. g (r # y # l')) x" + -- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *} + +consts PRIMREC :: "(nat list => nat) set" +inductive PRIMREC + intros + SC: "SC \ PRIMREC" + CONST: "CONST k \ PRIMREC" + PROJ: "PROJ i \ PRIMREC" + COMP: "g \ PRIMREC ==> fs \ lists PRIMREC ==> COMP g fs \ PRIMREC" + PREC: "f \ PRIMREC ==> g \ PRIMREC ==> PREC f g \ PRIMREC" + + +text {* Useful special cases of evaluation *} + +lemma SC [simp]: "SC (x # l) = Suc x" + apply (simp add: SC_def) + done + +lemma CONST [simp]: "CONST k l = k" + apply (simp add: CONST_def) + done + +lemma PROJ_0 [simp]: "PROJ 0 (x # l) = x" + apply (simp add: PROJ_def) + done + +lemma COMP_1 [simp]: "COMP g [f] l = g [f l]" + apply (simp add: COMP_def) + done -consts list_add :: nat list => nat -primrec - "list_add [] = 0" - "list_add (m#ms) = m + list_add ms" +lemma PREC_0 [simp]: "PREC f g (0 # l) = f l" + apply (simp add: PREC_def) + done + +lemma PREC_Suc [simp]: "PREC f g (Suc x # l) = g (PREC f g (x # l) # x # l)" + apply (simp add: PREC_def) + done + + +text {* PROPERTY A 4 *} + +lemma less_ack2 [iff]: "j < ack (i, j)" + apply (induct i j rule: ack.induct) + apply simp_all + done + + +text {* PROPERTY A 5-, the single-step lemma *} + +lemma ack_less_ack_Suc2 [iff]: "ack(i, j) < ack (i, Suc j)" + apply (induct i j rule: ack.induct) + apply simp_all + done + + +text {* PROPERTY A 5, monotonicity for @{text "<"} *} + +lemma ack_less_mono2: "j < k ==> ack (i, j) < ack (i, k)" + apply (induct i k rule: ack.induct) + apply simp_all + apply (blast elim!: less_SucE intro: less_trans) + done + + +text {* PROPERTY A 5', monotonicity for @{text \} *} + +lemma ack_le_mono2: "j \ k ==> ack (i, j) \ ack (i, k)" + apply (simp add: order_le_less) + apply (blast intro: ack_less_mono2) + done -consts zeroHd :: nat list => nat -primrec - "zeroHd [] = 0" - "zeroHd (m#ms) = m" + +text {* PROPERTY A 6 *} + +lemma ack2_le_ack1 [iff]: "ack (i, Suc j) \ ack (Suc i, j)" + apply (induct j) + apply simp_all + apply (blast intro: ack_le_mono2 less_ack2 [THEN Suc_leI] le_trans) + done + + +text {* PROPERTY A 7-, the single-step lemma *} + +lemma ack_less_ack_Suc1 [iff]: "ack (i, j) < ack (Suc i, j)" + apply (blast intro: ack_less_mono2 less_le_trans) + done + + +text {* PROPERTY A 4'? Extra lemma needed for @{term CONST} case, constant functions *} + +lemma less_ack1 [iff]: "i < ack (i, j)" + apply (induct i) + apply simp_all + apply (blast intro: Suc_leI le_less_trans) + done + + +text {* PROPERTY A 8 *} + +lemma ack_1 [simp]: "ack (1, j) = j + #2" + apply (induct j) + apply simp_all + done + + +text {* PROPERTY A 9. The unary @{term 1} and @{term 2} in @{term + ack} is essential for the rewriting. *} + +lemma ack_2 [simp]: "ack (2, j) = #2 * j + #3" + apply (induct j) + apply simp_all + done -(** The set of primitive recursive functions of type nat list => nat **) -consts - PRIMREC :: (nat list => nat) set - SC :: nat list => nat - CONST :: [nat, nat list] => nat - PROJ :: [nat, nat list] => nat - COMP :: [nat list => nat, (nat list => nat)list, nat list] => nat - PREC :: [nat list => nat, nat list => nat, nat list] => nat +text {* PROPERTY A 7, monotonicity for @{text "<"} [not clear why + @{thm [source] ack_1} is now needed first!] *} + +lemma ack_less_mono1_aux: "ack (i, k) < ack (Suc (i +i'), k)" + apply (induct i k rule: ack.induct) + apply simp_all + prefer 2 + apply (blast intro: less_trans ack_less_mono2) + apply (induct_tac i' n rule: ack.induct) + apply simp_all + apply (blast intro: Suc_leI [THEN le_less_trans] ack_less_mono2) + done + +lemma ack_less_mono1: "i < j ==> ack (i, k) < ack (j, k)" + apply (drule less_imp_Suc_add) + apply (blast intro!: ack_less_mono1_aux) + done + + +text {* PROPERTY A 7', monotonicity for @{text "\"} *} + +lemma ack_le_mono1: "i \ j ==> ack (i, k) \ ack (j, k)" + apply (simp add: order_le_less) + apply (blast intro: ack_less_mono1) + done + + +text {* PROPERTY A 10 *} + +lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (#2 + (i1 + i2), j)" + apply (simp add: numerals) + apply (rule ack2_le_ack1 [THEN [2] less_le_trans]) + apply simp + apply (rule le_add1 [THEN ack_le_mono1, THEN le_less_trans]) + apply (rule ack_less_mono1 [THEN ack_less_mono2]) + apply (simp add: le_imp_less_Suc le_add2) + done + -defs +text {* PROPERTY A 11 *} - SC_def "SC l == Suc (zeroHd l)" +lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (#4 + (i1 + i2), j)" + apply (rule_tac j = "ack (2, ack (i1 + i2, j))" in less_trans) + prefer 2 + apply (rule ack_nest_bound [THEN less_le_trans]) + apply (simp add: Suc3_eq_add_3) + apply simp + apply (cut_tac i = i1 and m1 = i2 and k = j in le_add1 [THEN ack_le_mono1]) + apply (cut_tac i = "i2" and m1 = i1 and k = j in le_add2 [THEN ack_le_mono1]) + apply auto + done + + +text {* PROPERTY A 12. Article uses existential quantifier but the ALF proof + used @{text "k + 4"}. Quantified version must be nested @{text + "\k'. \i j. ..."} *} - CONST_def "CONST k l == k" +lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (#4 + k, j)" + apply (rule_tac j = "ack (k, j) + ack (0, j)" in less_trans) + prefer 2 + apply (rule ack_add_bound [THEN less_le_trans]) + apply simp + apply (rule add_less_mono less_ack2 | assumption)+ + done + + + +text {* Inductive definition of the @{term PR} functions *} - PROJ_def "PROJ i l == zeroHd (drop i l)" +text {* MAIN RESULT *} + +lemma SC_case: "SC l < ack (1, list_add l)" + apply (unfold SC_def) + apply (induct l) + apply (simp_all add: le_add1 le_imp_less_Suc) + done + +lemma CONST_case: "CONST k l < ack (k, list_add l)" + apply simp + done - COMP_def "COMP g fs l == g (map (%f. f l) fs)" +lemma PROJ_case [rule_format]: "\i. PROJ i l < ack (0, list_add l)" + apply (simp add: PROJ_def) + apply (induct l) + apply simp_all + apply (rule allI) + apply (case_tac i) + apply (simp (no_asm_simp) add: le_add1 le_imp_less_Suc) + apply (simp (no_asm_simp)) + apply (blast intro: less_le_trans intro!: le_add2) + done + + +text {* @{term COMP} case *} - (*Note that g is applied first to PREC f g y and then to y!*) - PREC_def "PREC f g l == case l of - [] => 0 - | x#l' => nat_rec (f l') (%y r. g (r#y#l')) x" +lemma COMP_map_aux: "fs \ lists (PRIMREC \ {f. \kf. \l. f l < ack (kf, list_add l)}) + ==> \k. \l. list_add (map (\f. f l) fs) < ack (k, list_add l)" + apply (erule lists.induct) + apply (rule_tac x = 0 in exI) + apply simp + apply safe + apply simp + apply (rule exI) + apply (blast intro: add_less_mono ack_add_bound less_trans) + done + +lemma COMP_case: + "\l. g l < ack (kg, list_add l) ==> + fs \ lists(PRIMREC Int {f. \kf. \l. f l < ack(kf, list_add l)}) + ==> \k. \l. COMP g fs l < ack(k, list_add l)" + apply (unfold COMP_def) + apply (frule Int_lower1 [THEN lists_mono, THEN subsetD]) + apply (erule COMP_map_aux [THEN exE]) + apply (rule exI) + apply (rule allI) + apply (drule spec)+ + apply (erule less_trans) + apply (blast intro: ack_less_mono2 ack_nest_bound less_trans) + done + + +text {* @{term PREC} case *} - -inductive PRIMREC - intrs - SC "SC : PRIMREC" - CONST "CONST k : PRIMREC" - PROJ "PROJ i : PRIMREC" - COMP "[| g: PRIMREC; fs: lists PRIMREC |] ==> COMP g fs : PRIMREC" - PREC "[| f: PRIMREC; g: PRIMREC |] ==> PREC f g: PRIMREC" - monos lists_mono +lemma PREC_case_aux: + "\l. f l + list_add l < ack (kf, list_add l) ==> + \l. g l + list_add l < ack (kg, list_add l) ==> + PREC f g l + list_add l < ack (Suc (kf + kg), list_add l)" + apply (unfold PREC_def) + apply (case_tac l) + apply simp_all + apply (blast intro: less_trans) + apply (erule ssubst) -- {* get rid of the needless assumption *} + apply (induct_tac a) + apply simp_all + txt {* base case *} + apply (blast intro: le_add1 [THEN le_imp_less_Suc, THEN ack_less_mono1] less_trans) + txt {* induction step *} + apply (rule Suc_leI [THEN le_less_trans]) + apply (rule le_refl [THEN add_le_mono, THEN le_less_trans]) + prefer 2 + apply (erule spec) + apply (simp add: le_add2) + txt {* final part of the simplification *} + apply simp + apply (rule le_add2 [THEN ack_le_mono1, THEN le_less_trans]) + apply (erule ack_less_mono2) + done + +lemma PREC_case: + "\l. f l < ack (kf, list_add l) ==> + \l. g l < ack (kg, list_add l) ==> + \k. \l. PREC f g l < ack (k, list_add l)" + apply (rule exI) + apply (rule allI) + apply (rule le_less_trans [OF le_add1 PREC_case_aux]) + apply (blast intro: ack_add_bound2)+ + done + +lemma ack_bounds_PRIMREC: "f \ PRIMREC ==> \k. \l. f l < ack (k, list_add l)" + apply (erule PRIMREC.induct) + apply (blast intro: SC_case CONST_case PROJ_case COMP_case PREC_case)+ + done + +lemma ack_not_PRIMREC: "(\l. case l of [] => 0 | x # l' => ack (x, x)) \ PRIMREC" + apply (rule notI) + apply (erule ack_bounds_PRIMREC [THEN exE]) + apply (rule less_irrefl) + apply (drule_tac x = "[x]" in spec) + apply simp + done end diff -r 6e6c8d1ec89e -r 23bf8d787b04 src/HOL/ex/Recdefs.ML --- a/src/HOL/ex/Recdefs.ML Thu Feb 01 20:48:58 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ -(* Title: HOL/ex/Recdefs.ML - ID: $Id$ - Author: Konrad Slind and Lawrence C Paulson - Copyright 1997 University of Cambridge - -A few proofs to demonstrate the functions defined in Recdefs.thy -Lemma statements from Konrad Slind's Web site -*) - -(** The silly g function: example of nested recursion **) - -Addsimps g.simps; - -Goal "g x < Suc x"; -by (induct_thm_tac g.induct "x" 1); -by Auto_tac; -qed "g_terminates"; - -Goal "g x = 0"; -by (induct_thm_tac g.induct "x" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates]))); -qed "g_zero"; - -(*** the contrived `mapf' ***) - -(* proving the termination condition: *) -val [tc] = mapf.tcs; -goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc)); -by (rtac allI 1); -by (case_tac "n=0" 1); -by (ALLGOALS Asm_simp_tac); -val lemma = result(); - -(* removing the termination condition from the generated thms: *) -val [mapf_0,mapf_Suc] = mapf.simps; -val mapf_Suc = lemma RS mapf_Suc; - -val mapf_induct = lemma RS mapf.induct; diff -r 6e6c8d1ec89e -r 23bf8d787b04 src/HOL/ex/Recdefs.thy --- a/src/HOL/ex/Recdefs.thy Thu Feb 01 20:48:58 2001 +0100 +++ b/src/HOL/ex/Recdefs.thy Thu Feb 01 20:51:13 2001 +0100 @@ -6,88 +6,126 @@ Examples of recdef definitions. Most, but not all, are handled automatically. *) -Recdefs = Main + +header {* Examples of recdef definitions *} + +theory Recdefs = Main: consts fact :: "nat => nat" -recdef fact "less_than" - "fact x = (if (x = 0) then 1 else x * fact (x - 1))" +recdef fact less_than + "fact x = (if x = 0 then 1 else x * fact (x - 1))" consts Fact :: "nat => nat" -recdef Fact "less_than" - "Fact 0 = 1" - "Fact (Suc x) = (Fact x * Suc x)" +recdef Fact less_than + "Fact 0 = 1" + "Fact (Suc x) = Fact x * Suc x" consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list" -recdef map2 "measure(%(f,l1,l2).size l1)" - "map2(f, [], []) = []" - "map2(f, h#t, []) = []" - "map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2)" +recdef map2 "measure(\(f, l1, l2). size l1)" + "map2 (f, [], []) = []" + "map2 (f, h # t, []) = []" + "map2 (f, h1 # t1, h2 # t2) = f h1 h2 # map2 (f, t1, t2)" -consts finiteRchain :: "(['a,'a] => bool) * 'a list => bool" -recdef finiteRchain "measure (%(R,l).size l)" - "finiteRchain(R, []) = True" - "finiteRchain(R, [x]) = True" - "finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst))" +consts finiteRchain :: "('a => 'a => bool) * 'a list => bool" +recdef finiteRchain "measure (\(R, l). size l)" + "finiteRchain(R, []) = True" + "finiteRchain(R, [x]) = True" + "finiteRchain(R, x # y # rst) = (R x y \ finiteRchain (R, y # rst))" -(*Not handled automatically: too complicated.*) +text {* Not handled automatically: too complicated. *} consts variant :: "nat * nat list => nat" -recdef variant "measure(%(n::nat, ns). size(filter(%y. n <= y) ns))" - "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)" +recdef variant "measure (\(n::nat, ns). size (filter (\y. n \ y) ns))" + "variant (x, L) = (if x mem L then variant (Suc x, L) else x)" consts gcd :: "nat * nat => nat" -recdef gcd "measure (%(x,y).x+y)" - "gcd (0,y) = y" - "gcd (Suc x, 0) = Suc x" - "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y) - else gcd(Suc x, y - x))" +recdef gcd "measure (\(x, y). x + y)" + "gcd (0, y) = y" + "gcd (Suc x, 0) = Suc x" + "gcd (Suc x, Suc y) = + (if y \ x then gcd (x - y, Suc y) else gcd (Suc x, y - x))" + + +text {* + \medskip The silly @{term g} function: example of nested recursion. + Not handled automatically. In fact, @{term g} is the zero constant + function. + *} -(*Not handled automatically. In fact, g is the zero constant function.*) -consts g :: "nat => nat" -recdef g "less_than" - "g 0 = 0" - "g(Suc x) = g(g x)" +consts g :: "nat => nat" +recdef g less_than + "g 0 = 0" + "g (Suc x) = g (g x)" + +lemma g_terminates: "g x < Suc x" + apply (induct x rule: g.induct) + apply (auto simp add: g.simps) + done + +lemma g_zero: "g x = 0" + apply (induct x rule: g.induct) + apply (simp_all add: g.simps g_terminates) + done + consts Div :: "nat * nat => nat * nat" -recdef Div "measure fst" - "Div(0,x) = (0,0)" - "Div(Suc x, y) = - (let (q,r) = Div(x,y) - in - if (y <= Suc r) then (Suc q,0) else (q, Suc r))" +recdef Div "measure fst" + "Div (0, x) = (0, 0)" + "Div (Suc x, y) = + (let (q, r) = Div (x, y) + in if y \ Suc r then (Suc q, 0) else (q, Suc r))" + +text {* + \medskip Not handled automatically. Should be the predecessor + function, but there is an unnecessary "looping" recursive call in + @{term "k 1"}. +*} -(*Not handled automatically. Should be the predecessor function, but there - is an unnecessary "looping" recursive call in k(1) *) -consts k :: "nat => nat" -recdef k "less_than" - "k 0 = 0" - "k (Suc n) = (let x = k 1 - in if (0=1) then k (Suc 1) else n)" +consts k :: "nat => nat" +recdef k less_than + "k 0 = 0" + "k (Suc n) = + (let x = k 1 + in if 0 = 1 then k (Suc 1) else n)" + +consts part :: "('a => bool) * 'a list * 'a list * 'a list => 'a list * 'a list" +recdef part "measure (\(P, l, l1, l2). size l)" + "part (P, [], l1, l2) = (l1, l2)" + "part (P, h # rst, l1, l2) = + (if P h then part (P, rst, h # l1, l2) + else part (P, rst, l1, h # l2))" -consts part :: "('a=>bool) * 'a list * 'a list * 'a list => 'a list * 'a list" -recdef part "measure (%(P,l,l1,l2).size l)" - "part(P, [], l1,l2) = (l1,l2)" - "part(P, h#rst, l1,l2) = - (if P h then part(P,rst, h#l1, l2) - else part(P,rst, l1, h#l2))" +consts fqsort :: "('a => 'a => bool) * 'a list => 'a list" +recdef fqsort "measure (size o snd)" + "fqsort (ord, []) = []" + "fqsort (ord, x # rst) = + (let (less, more) = part ((\y. ord y x), rst, ([], [])) + in fqsort (ord, less) @ [x] @ fqsort (ord, more))" + +text {* + \medskip Silly example which demonstrates the occasional need for + additional congruence rules (here: @{thm [source] map_cong}). If + the congruence rule is removed, an unprovable termination condition + is generated! Termination not proved automatically. TFL requires + @{term [source] "\x. mapf x"} instead of @{term [source] mapf}. +*} -consts fqsort :: "(['a,'a] => bool) * 'a list => 'a list" -recdef fqsort "measure (size o snd)" - "fqsort(ord,[]) = []" - "fqsort(ord, x#rst) = - (let (less,more) = part((%y. ord y x), rst, ([],[])) - in - fqsort(ord,less)@[x]@fqsort(ord,more))" +consts mapf :: "nat => nat list" +recdef mapf "measure (\m. m)" + "mapf 0 = []" + "mapf (Suc n) = concat (map (\x. mapf x) (replicate n n))" + (hints cong: map_cong) -(* silly example which demonstrates the occasional need for additional - congruence rules (here: map_cong from List). If the congruence rule is - removed, an unprovable termination condition is generated! - Termination not proved automatically; see the ML file. - TFL requires (%x.mapf x) instead of mapf. -*) -consts mapf :: nat => nat list -recdef mapf "measure(%m. m)" -congs map_cong -"mapf 0 = []" -"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))" +recdef_tc mapf_tc: mapf + apply (rule allI) + apply (case_tac "n = 0") + apply simp_all + done + +text {* Removing the termination condition from the generated thms: *} + +lemma "mapf (Suc n) = concat (map mapf (replicate n n))" + apply (simp add: mapf.simps mapf_tc) + done + +lemmas mapf_induct = mapf.induct [OF mapf_tc] end