--- 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
--- 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";
-
-
--- 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
-
--- 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";
--- 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 \<noteq> #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) \<le> (#1000001 + #1) - #2"
+ by simp
+
+lemma "(#1234567::int) \<le> #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 \<noteq> Pls ==> w BIT False : normal"
+ BIT_T: "w: normal ==> w \<noteq> Min ==> w BIT True : normal"
+
+text {*
+ \medskip Binary arithmetic on normalized operands yields normalized
+ results.
+*}
+
+lemma normal_BIT_I [simp]: "w BIT b \<in> normal ==> w BIT b BIT c \<in> normal"
+ apply (case_tac c)
+ apply auto
+ done
+
+lemma normal_BIT_D: "w BIT b \<in> normal ==> w \<in> normal"
+ apply (erule normal.cases)
+ apply auto
+ done
+
+lemma NCons_normal [simp]: "w \<in> normal ==> NCons w b \<in> normal"
+ apply (induct w)
+ apply (auto simp add: NCons_Pls NCons_Min)
+ done
+
+lemma NCons_True: "NCons w True \<noteq> Pls"
+ apply (induct w)
+ apply auto
+ done
+
+lemma NCons_False: "NCons w False \<noteq> Min"
+ apply (induct w)
+ apply auto
+ done
- BIT_T "[| w: normal; w ~= Min |] ==> w BIT True : normal"
+lemma bin_succ_normal [simp]: "w \<in> normal ==> bin_succ w \<in> 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 \<in> normal ==> bin_pred w \<in> 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 \<in> normal --> (\<forall>z. z \<in> normal --> bin_add w z \<in> 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 \<in> normal ==> (w = Pls) = (number_of w = (#0::int))"
+ apply (erule normal.induct)
+ apply auto
+ done
+
+lemma bin_minus_normal: "w \<in> normal ==> bin_minus w \<in> 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 \<in> normal ==> z \<in> normal --> bin_mult w z \<in> 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
--- 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 ==> (k-1) * setsum (%i. k^i) (lessThan n) = k^n - 1";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_powers";
--- 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 (\<lambda>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 (\<lambda>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 (\<lambda>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 (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)"
+ apply (induct n)
+ apply auto
+ done
+
+lemma sum_of_cubes: "#4 * setsum (\<lambda>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 (\<lambda>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 (\<lambda>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 (\<lambda>i. #2^i) (lessThan n) = #2^n - 1"
+ apply (induct n)
+ apply auto
+ done
+
+lemma sum_of_3_powers: "#2 * setsum (\<lambda>i. #3^i) (lessThan n) = #3^n - 1"
+ apply (induct n)
+ apply auto
+ done
+
+lemma sum_of_powers: "0 < k ==> (k - 1) * setsum (\<lambda>i. k^i) (lessThan n) = k^n - 1"
+ apply (induct n)
+ apply auto
+ done
+
+end
--- 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<k --> 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<j ==> 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";
-
--- 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 (\<lambda>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') (\<lambda>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 \<in> PRIMREC"
+ CONST: "CONST k \<in> PRIMREC"
+ PROJ: "PROJ i \<in> PRIMREC"
+ COMP: "g \<in> PRIMREC ==> fs \<in> lists PRIMREC ==> COMP g fs \<in> PRIMREC"
+ PREC: "f \<in> PRIMREC ==> g \<in> PRIMREC ==> PREC f g \<in> 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 \<le>} *}
+
+lemma ack_le_mono2: "j \<le> k ==> ack (i, j) \<le> 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) \<le> 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 "\<le>"} *}
+
+lemma ack_le_mono1: "i \<le> j ==> ack (i, k) \<le> 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
+ "\<exists>k'. \<forall>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]: "\<forall>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 \<in> lists (PRIMREC \<inter> {f. \<exists>kf. \<forall>l. f l < ack (kf, list_add l)})
+ ==> \<exists>k. \<forall>l. list_add (map (\<lambda>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:
+ "\<forall>l. g l < ack (kg, list_add l) ==>
+ fs \<in> lists(PRIMREC Int {f. \<exists>kf. \<forall>l. f l < ack(kf, list_add l)})
+ ==> \<exists>k. \<forall>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:
+ "\<forall>l. f l + list_add l < ack (kf, list_add l) ==>
+ \<forall>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:
+ "\<forall>l. f l < ack (kf, list_add l) ==>
+ \<forall>l. g l < ack (kg, list_add l) ==>
+ \<exists>k. \<forall>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 \<in> PRIMREC ==> \<exists>k. \<forall>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: "(\<lambda>l. case l of [] => 0 | x # l' => ack (x, x)) \<notin> 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
--- 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;
--- 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(\<lambda>(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 (\<lambda>(R, l). size l)"
+ "finiteRchain(R, []) = True"
+ "finiteRchain(R, [x]) = True"
+ "finiteRchain(R, x # y # rst) = (R x y \<and> 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 (\<lambda>(n::nat, ns). size (filter (\<lambda>y. n \<le> 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 (\<lambda>(x, y). x + y)"
+ "gcd (0, y) = y"
+ "gcd (Suc x, 0) = Suc x"
+ "gcd (Suc x, Suc y) =
+ (if y \<le> 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 \<le> 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 (\<lambda>(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 ((\<lambda>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] "\<lambda>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 (\<lambda>m. m)"
+ "mapf 0 = []"
+ "mapf (Suc n) = concat (map (\<lambda>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