converted to new-style theories;
authorwenzelm
Thu Feb 01 20:51:13 2001 +0100 (2001-02-01)
changeset 1102423bf8d787b04
parent 11023 6e6c8d1ec89e
child 11025 a70b796d9af8
converted to new-style theories;
src/HOL/IsaMakefile
src/HOL/ex/BT.ML
src/HOL/ex/BT.thy
src/HOL/ex/BinEx.ML
src/HOL/ex/BinEx.thy
src/HOL/ex/NatSum.ML
src/HOL/ex/NatSum.thy
src/HOL/ex/Primrec.ML
src/HOL/ex/Primrec.thy
src/HOL/ex/Recdefs.ML
src/HOL/ex/Recdefs.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Feb 01 20:48:58 2001 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Feb 01 20:51:13 2001 +0100
     1.3 @@ -484,13 +484,13 @@
     1.4  HOL-ex: HOL $(LOG)/HOL-ex.gz
     1.5  
     1.6  $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.ML ex/AVL.thy ex/Antiquote.thy \
     1.7 -  ex/BT.ML ex/BT.thy ex/BinEx.ML ex/BinEx.thy ex/Group.ML ex/Group.thy \
     1.8 +  ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy \
     1.9    ex/InSort.ML ex/InSort.thy ex/IntRing.ML ex/IntRing.thy \
    1.10    ex/Lagrange.ML ex/Lagrange.thy ex/LocaleGroup.ML ex/LocaleGroup.thy \
    1.11 -  ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.ML \
    1.12 -  ex/NatSum.thy ex/PER.thy ex/PiSets.ML ex/PiSets.thy ex/Primrec.ML \
    1.13 +  ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
    1.14 +  ex/NatSum.thy ex/PER.thy ex/PiSets.ML ex/PiSets.thy \
    1.15    ex/Primrec.thy ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
    1.16 -  ex/ROOT.ML ex/Recdefs.ML ex/Recdefs.thy ex/Records.thy ex/Ring.ML \
    1.17 +  ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/Ring.ML \
    1.18    ex/Ring.thy ex/StringEx.thy ex/Tarski.ML \
    1.19    ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML ex/mesontest2.ML \
    1.20    ex/mesontest2.thy ex/set.ML ex/set.thy ex/svc_test.ML ex/svc_test.thy
     2.1 --- a/src/HOL/ex/BT.ML	Thu Feb 01 20:48:58 2001 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,57 +0,0 @@
     2.4 -(*  Title:      HOL/ex/BT.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1995  University of Cambridge
     2.8 -
     2.9 -Datatype definition of binary trees
    2.10 -*)
    2.11 -
    2.12 -(** BT simplification **)
    2.13 -
    2.14 -Goal "n_leaves(reflect(t)) = n_leaves(t)";
    2.15 -by (induct_tac "t" 1);
    2.16 -by Auto_tac;
    2.17 -qed "n_leaves_reflect";
    2.18 -
    2.19 -Goal "n_nodes(reflect(t)) = n_nodes(t)";
    2.20 -by (induct_tac "t" 1);
    2.21 -by Auto_tac;
    2.22 -qed "n_nodes_reflect";
    2.23 -
    2.24 -(*The famous relationship between the numbers of leaves and nodes*)
    2.25 -Goal "n_leaves(t) = Suc(n_nodes(t))";
    2.26 -by (induct_tac "t" 1);
    2.27 -by Auto_tac;
    2.28 -qed "n_leaves_nodes";
    2.29 -
    2.30 -Goal "reflect(reflect(t))=t";
    2.31 -by (induct_tac "t" 1);
    2.32 -by Auto_tac;
    2.33 -qed "reflect_reflect_ident";
    2.34 -
    2.35 -Goal "bt_map f (reflect t) = reflect (bt_map f t)";
    2.36 -by (induct_tac "t" 1);
    2.37 -by (ALLGOALS Asm_simp_tac);
    2.38 -qed "bt_map_reflect";
    2.39 -
    2.40 -Goal "inorder (bt_map f t) = map f (inorder t)";
    2.41 -by (induct_tac "t" 1);
    2.42 -by (ALLGOALS Asm_simp_tac);
    2.43 -qed "inorder_bt_map";
    2.44 -
    2.45 -Goal "preorder (reflect t) = rev (postorder t)";
    2.46 -by (induct_tac "t" 1);
    2.47 -by (ALLGOALS Asm_simp_tac);
    2.48 -qed "preorder_reflect";
    2.49 -
    2.50 -Goal "inorder (reflect t) = rev (inorder t)";
    2.51 -by (induct_tac "t" 1);
    2.52 -by (ALLGOALS Asm_simp_tac);
    2.53 -qed "inorder_reflect";
    2.54 -
    2.55 -Goal "postorder (reflect t) = rev (preorder t)";
    2.56 -by (induct_tac "t" 1);
    2.57 -by (ALLGOALS Asm_simp_tac);
    2.58 -qed "postorder_reflect";
    2.59 -
    2.60 -
     3.1 --- a/src/HOL/ex/BT.thy	Thu Feb 01 20:48:58 2001 +0100
     3.2 +++ b/src/HOL/ex/BT.thy	Thu Feb 01 20:51:13 2001 +0100
     3.3 @@ -3,26 +3,29 @@
     3.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.5      Copyright   1995  University of Cambridge
     3.6  
     3.7 -Binary trees (based on the ZF version)
     3.8 +Binary trees (based on the ZF version).
     3.9  *)
    3.10  
    3.11 -BT = Main +
    3.12 +header {* Binary trees *}
    3.13 +
    3.14 +theory BT = Main:
    3.15  
    3.16 -datatype 'a bt = Lf
    3.17 -               | Br 'a ('a bt) ('a bt)
    3.18 -  
    3.19 +datatype 'a bt =
    3.20 +    Lf
    3.21 +  | Br 'a  "'a bt"  "'a bt"
    3.22 +
    3.23  consts
    3.24 -    n_nodes     :: 'a bt => nat
    3.25 -    n_leaves    :: 'a bt => nat
    3.26 -    reflect     :: 'a bt => 'a bt
    3.27 -    bt_map      :: ('a=>'b) => ('a bt => 'b bt)
    3.28 -    preorder    :: 'a bt => 'a list
    3.29 -    inorder     :: 'a bt => 'a list
    3.30 -    postorder   :: 'a bt => 'a list
    3.31 +  n_nodes :: "'a bt => nat"
    3.32 +  n_leaves :: "'a bt => nat"
    3.33 +  reflect :: "'a bt => 'a bt"
    3.34 +  bt_map :: "('a => 'b) => ('a bt => 'b bt)"
    3.35 +  preorder :: "'a bt => 'a list"
    3.36 +  inorder :: "'a bt => 'a list"
    3.37 +  postorder :: "'a bt => 'a list"
    3.38  
    3.39  primrec
    3.40    "n_nodes (Lf) = 0"
    3.41 -  "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
    3.42 +  "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
    3.43  
    3.44  primrec
    3.45    "n_leaves (Lf) = Suc 0"
    3.46 @@ -48,5 +51,56 @@
    3.47    "postorder (Lf) = []"
    3.48    "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
    3.49  
    3.50 +
    3.51 +text {* \medskip BT simplification *}
    3.52 +
    3.53 +lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
    3.54 +  apply (induct t)
    3.55 +   apply auto
    3.56 +  done
    3.57 +
    3.58 +lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
    3.59 +  apply (induct t)
    3.60 +   apply auto
    3.61 +  done
    3.62 +
    3.63 +text {*
    3.64 +  The famous relationship between the numbers of leaves and nodes.
    3.65 +*}
    3.66 +
    3.67 +lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
    3.68 +  apply (induct t)
    3.69 +   apply auto
    3.70 +  done
    3.71 +
    3.72 +lemma reflect_reflect_ident: "reflect (reflect t) = t"
    3.73 +  apply (induct t)
    3.74 +   apply auto
    3.75 +  done
    3.76 +
    3.77 +lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
    3.78 +  apply (induct t)
    3.79 +   apply simp_all
    3.80 +  done
    3.81 +
    3.82 +lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
    3.83 +  apply (induct t)
    3.84 +   apply simp_all
    3.85 +  done
    3.86 +
    3.87 +lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
    3.88 +  apply (induct t)
    3.89 +   apply simp_all
    3.90 +  done
    3.91 +
    3.92 +lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
    3.93 +  apply (induct t)
    3.94 +   apply simp_all
    3.95 +  done
    3.96 +
    3.97 +lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
    3.98 +  apply (induct t)
    3.99 +   apply simp_all
   3.100 +  done
   3.101 +
   3.102  end
   3.103 -
     4.1 --- a/src/HOL/ex/BinEx.ML	Thu Feb 01 20:48:58 2001 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,372 +0,0 @@
     4.4 -(*  Title:      HOL/ex/BinEx.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 -    Copyright   1998  University of Cambridge
     4.8 -
     4.9 -Examples of performing binary arithmetic by simplification
    4.10 -
    4.11 -Also a proof that binary arithmetic on normalized operands 
    4.12 -yields normalized results. 
    4.13 -*)
    4.14 -
    4.15 -(**** The Integers ****)
    4.16 -
    4.17 -(*** Addition ***)
    4.18 -
    4.19 -Goal "(#13::int)  +  #19 = #32";
    4.20 -by (Simp_tac 1);
    4.21 -result();
    4.22 -
    4.23 -Goal "(#1234::int)  +  #5678 = #6912";
    4.24 -by (Simp_tac 1);
    4.25 -result();
    4.26 -
    4.27 -Goal "(#1359::int)  +  #-2468 = #-1109";
    4.28 -by (Simp_tac 1);
    4.29 -result();
    4.30 -
    4.31 -Goal "(#93746::int) +  #-46375 = #47371";
    4.32 -by (Simp_tac 1);
    4.33 -result();
    4.34 -
    4.35 -(*** Negation ***)
    4.36 -
    4.37 -Goal "- (#65745::int) = #-65745";
    4.38 -by (Simp_tac 1);
    4.39 -result();
    4.40 -
    4.41 -Goal "- (#-54321::int) = #54321";
    4.42 -by (Simp_tac 1);
    4.43 -result();
    4.44 -
    4.45 -
    4.46 -(*** Multiplication ***)
    4.47 -
    4.48 -Goal "(#13::int)  *  #19 = #247";
    4.49 -by (Simp_tac 1);
    4.50 -result();
    4.51 -
    4.52 -Goal "(#-84::int)  *  #51 = #-4284";
    4.53 -by (Simp_tac 1);
    4.54 -result();
    4.55 -
    4.56 -Goal "(#255::int)  *  #255 = #65025";
    4.57 -by (Simp_tac 1);
    4.58 -result();
    4.59 -
    4.60 -Goal "(#1359::int)  *  #-2468 = #-3354012";
    4.61 -by (Simp_tac 1);
    4.62 -result();
    4.63 -
    4.64 -Goal "(#89::int) * #10 ~= #889";  
    4.65 -by (Simp_tac 1); 
    4.66 -result();
    4.67 -
    4.68 -Goal "(#13::int) < #18 - #4";  
    4.69 -by (Simp_tac 1); 
    4.70 -result();
    4.71 -
    4.72 -Goal "(#-345::int) < #-242 + #-100";  
    4.73 -by (Simp_tac 1); 
    4.74 -result();
    4.75 -
    4.76 -Goal "(#13557456::int) < #18678654";  
    4.77 -by (Simp_tac 1); 
    4.78 -result();
    4.79 -
    4.80 -Goal "(#999999::int) <= (#1000001 + #1)-#2";  
    4.81 -by (Simp_tac 1); 
    4.82 -result();
    4.83 -
    4.84 -Goal "(#1234567::int) <= #1234567";  
    4.85 -by (Simp_tac 1); 
    4.86 -result();
    4.87 -
    4.88 -
    4.89 -(*** Quotient and Remainder ***)
    4.90 -
    4.91 -Goal "(#10::int) div #3 = #3";
    4.92 -by (Simp_tac 1);
    4.93 -result();
    4.94 -
    4.95 -Goal "(#10::int) mod #3 = #1";
    4.96 -by (Simp_tac 1);
    4.97 -result();
    4.98 -
    4.99 -(** A negative divisor **)
   4.100 -
   4.101 -Goal "(#10::int) div #-3 = #-4";
   4.102 -by (Simp_tac 1);
   4.103 -result();
   4.104 -
   4.105 -Goal "(#10::int) mod #-3 = #-2";
   4.106 -by (Simp_tac 1);
   4.107 -result();
   4.108 -
   4.109 -(** A negative dividend
   4.110 -    [ The definition agrees with mathematical convention but not with
   4.111 -      the hardware of most computers ]
   4.112 -**)
   4.113 -
   4.114 -Goal "(#-10::int) div #3 = #-4";
   4.115 -by (Simp_tac 1);
   4.116 -result();
   4.117 -
   4.118 -Goal "(#-10::int) mod #3 = #2";
   4.119 -by (Simp_tac 1);
   4.120 -result();
   4.121 -
   4.122 -(** A negative dividend AND divisor **)
   4.123 -
   4.124 -Goal "(#-10::int) div #-3 = #3";
   4.125 -by (Simp_tac 1);
   4.126 -result();
   4.127 -
   4.128 -Goal "(#-10::int) mod #-3 = #-1";
   4.129 -by (Simp_tac 1);
   4.130 -result();
   4.131 -
   4.132 -(** A few bigger examples **)
   4.133 -
   4.134 -Goal "(#8452::int) mod #3 = #1";
   4.135 -by (Simp_tac 1);
   4.136 -result();
   4.137 -
   4.138 -Goal "(#59485::int) div #434 = #137";
   4.139 -by (Simp_tac 1);
   4.140 -result();
   4.141 -
   4.142 -Goal "(#1000006::int) mod #10 = #6";
   4.143 -by (Simp_tac 1);
   4.144 -result();
   4.145 -
   4.146 -
   4.147 -(** division by shifting **)
   4.148 -
   4.149 -Goal "#10000000 div #2 = (#5000000::int)";
   4.150 -by (Simp_tac 1);
   4.151 -result();
   4.152 -
   4.153 -Goal "#10000001 mod #2 = (#1::int)";
   4.154 -by (Simp_tac 1);
   4.155 -result();
   4.156 -
   4.157 -Goal "#10000055 div #32 = (#312501::int)";
   4.158 -by (Simp_tac 1);
   4.159 -
   4.160 -Goal "#10000055 mod #32 = (#23::int)";
   4.161 -by (Simp_tac 1);
   4.162 -
   4.163 -Goal "#100094 div #144 = (#695::int)";
   4.164 -by (Simp_tac 1);
   4.165 -result();
   4.166 -
   4.167 -Goal "#100094 mod #144 = (#14::int)";
   4.168 -by (Simp_tac 1);
   4.169 -result();
   4.170 -
   4.171 -
   4.172 -
   4.173 -(**** The Natural Numbers ****)
   4.174 -
   4.175 -(** Successor **)
   4.176 -
   4.177 -Goal "Suc #99999 = #100000";
   4.178 -by (asm_simp_tac (simpset() addsimps [Suc_nat_number_of]) 1);
   4.179 -	(*not a default rewrite since sometimes we want to have Suc(#nnn)*)
   4.180 -result();
   4.181 -
   4.182 -
   4.183 -(** Addition **)
   4.184 -
   4.185 -Goal "(#13::nat)  +  #19 = #32";
   4.186 -by (Simp_tac 1);
   4.187 -result();
   4.188 -
   4.189 -Goal "(#1234::nat)  +  #5678 = #6912";
   4.190 -by (Simp_tac 1);
   4.191 -result();
   4.192 -
   4.193 -Goal "(#973646::nat) +  #6475 = #980121";
   4.194 -by (Simp_tac 1);
   4.195 -result();
   4.196 -
   4.197 -
   4.198 -(** Subtraction **)
   4.199 -
   4.200 -Goal "(#32::nat)  -  #14 = #18";
   4.201 -by (Simp_tac 1);
   4.202 -result();
   4.203 -
   4.204 -Goal "(#14::nat)  -  #15 = #0";
   4.205 -by (Simp_tac 1);
   4.206 -result();
   4.207 -
   4.208 -Goal "(#14::nat)  -  #1576644 = #0";
   4.209 -by (Simp_tac 1);
   4.210 -result();
   4.211 -
   4.212 -Goal "(#48273776::nat)  -  #3873737 = #44400039";
   4.213 -by (Simp_tac 1);
   4.214 -result();
   4.215 -
   4.216 -
   4.217 -(** Multiplication **)
   4.218 -
   4.219 -Goal "(#12::nat) * #11 = #132";
   4.220 -by (Simp_tac 1);
   4.221 -result();
   4.222 -
   4.223 -Goal "(#647::nat) * #3643 = #2357021";
   4.224 -by (Simp_tac 1);
   4.225 -result();
   4.226 -
   4.227 -
   4.228 -(** Quotient and Remainder **)
   4.229 -
   4.230 -Goal "(#10::nat) div #3 = #3";
   4.231 -by (Simp_tac 1);
   4.232 -result();
   4.233 -
   4.234 -Goal "(#10::nat) mod #3 = #1";
   4.235 -by (Simp_tac 1);
   4.236 -result();
   4.237 -
   4.238 -Goal "(#10000::nat) div #9 = #1111";
   4.239 -by (Simp_tac 1);
   4.240 -result();
   4.241 -
   4.242 -Goal "(#10000::nat) mod #9 = #1";
   4.243 -by (Simp_tac 1);
   4.244 -result();
   4.245 -
   4.246 -Goal "(#10000::nat) div #16 = #625";
   4.247 -by (Simp_tac 1);
   4.248 -result();
   4.249 -
   4.250 -Goal "(#10000::nat) mod #16 = #0";
   4.251 -by (Simp_tac 1);
   4.252 -result();
   4.253 -
   4.254 -
   4.255 -(*** Testing the cancellation of complementary terms ***)
   4.256 -
   4.257 -Goal "y + (x + -x) = (#0::int) + y";
   4.258 -by (Simp_tac 1);
   4.259 -result();
   4.260 -
   4.261 -Goal "y + (-x + (- y + x)) = (#0::int)";
   4.262 -by (Simp_tac 1);
   4.263 -result();
   4.264 -
   4.265 -Goal "-x + (y + (- y + x)) = (#0::int)";
   4.266 -by (Simp_tac 1);
   4.267 -result();
   4.268 -
   4.269 -Goal "x + (x + (- x + (- x + (- y + - z)))) = (#0::int) - y - z";
   4.270 -by (Simp_tac 1);
   4.271 -result();
   4.272 -
   4.273 -Goal "x + x - x - x - y - z = (#0::int) - y - z";
   4.274 -by (Simp_tac 1);
   4.275 -result();
   4.276 -
   4.277 -Goal "x + y + z - (x + z) = y - (#0::int)";
   4.278 -by (Simp_tac 1);
   4.279 -result();
   4.280 -
   4.281 -Goal "x+(y+(y+(y+ (-x + -x)))) = (#0::int) + y - x + y + y";
   4.282 -by (Simp_tac 1);
   4.283 -result();
   4.284 -
   4.285 -Goal "x+(y+(y+(y+ (-y + -x)))) = y + (#0::int) + y";
   4.286 -by (Simp_tac 1);
   4.287 -result();
   4.288 -
   4.289 -Goal "x + y - x + z - x - y - z + x < (#1::int)";
   4.290 -by (Simp_tac 1);
   4.291 -result();
   4.292 -
   4.293 -
   4.294 -Addsimps normal.intrs;
   4.295 -
   4.296 -Goal "(w BIT b): normal ==> (w BIT b BIT c): normal";
   4.297 -by (case_tac "c" 1);
   4.298 -by Auto_tac;
   4.299 -qed "normal_BIT_I";
   4.300 -
   4.301 -Addsimps [normal_BIT_I];
   4.302 -
   4.303 -Goal "w BIT b: normal ==> w: normal";
   4.304 -by (etac normal.elim 1);
   4.305 -by Auto_tac;
   4.306 -qed "normal_BIT_D";
   4.307 -
   4.308 -Goal "w : normal --> NCons w b : normal";
   4.309 -by (induct_tac "w" 1);
   4.310 -by (auto_tac (claset(), simpset() addsimps [NCons_Pls, NCons_Min]));
   4.311 -qed_spec_mp "NCons_normal";
   4.312 -
   4.313 -Addsimps [NCons_normal];
   4.314 -
   4.315 -Goal "NCons w True ~= Pls";
   4.316 -by (induct_tac "w" 1);
   4.317 -by Auto_tac;
   4.318 -qed "NCons_True";
   4.319 -
   4.320 -Goal "NCons w False ~= Min";
   4.321 -by (induct_tac "w" 1);
   4.322 -by Auto_tac;
   4.323 -qed "NCons_False";
   4.324 -
   4.325 -Goal "w: normal ==> bin_succ w : normal";
   4.326 -by (etac normal.induct 1);
   4.327 -by (case_tac "w" 4);
   4.328 -by (auto_tac (claset(), simpset() addsimps [NCons_True, bin_succ_BIT]));
   4.329 -qed "bin_succ_normal";
   4.330 -
   4.331 -Goal "w: normal ==> bin_pred w : normal";
   4.332 -by (etac normal.induct 1);
   4.333 -by (case_tac "w" 3);
   4.334 -by (auto_tac (claset(), simpset() addsimps [NCons_False, bin_pred_BIT]));
   4.335 -qed "bin_pred_normal";
   4.336 -
   4.337 -Addsimps [bin_succ_normal, bin_pred_normal];
   4.338 -
   4.339 -Goal "w : normal --> (ALL z. z: normal --> bin_add w z : normal)";
   4.340 -by (induct_tac "w" 1);
   4.341 -by (Simp_tac 1);
   4.342 -by (Simp_tac 1);
   4.343 -by (rtac impI 1);
   4.344 -by (rtac allI 1);
   4.345 -by (induct_tac "z" 1);
   4.346 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_add_BIT])));
   4.347 -by (safe_tac (claset() addSDs [normal_BIT_D]));
   4.348 -by (ALLGOALS Asm_simp_tac);
   4.349 -qed_spec_mp "bin_add_normal";
   4.350 -
   4.351 -Goal "w: normal ==> (w = Pls) = (number_of w = (#0::int))";
   4.352 -by (etac normal.induct 1);
   4.353 -by Auto_tac;
   4.354 -qed "normal_Pls_eq_0";
   4.355 -
   4.356 -Goal "w : normal ==> bin_minus w : normal";
   4.357 -by (etac normal.induct 1);
   4.358 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_BIT])));
   4.359 -by (resolve_tac normal.intrs 1);
   4.360 -by (assume_tac 1);
   4.361 -by (asm_full_simp_tac (simpset() addsimps [normal_Pls_eq_0]) 1);
   4.362 -by (asm_full_simp_tac 
   4.363 -    (simpset_of Int.thy 
   4.364 -     addsimps [number_of_minus, iszero_def, 
   4.365 -	       read_instantiate [("y","int 0")] zminus_equation]) 1);
   4.366 -by (etac not_sym 1);
   4.367 -qed "bin_minus_normal";
   4.368 -
   4.369 -Goal "w : normal ==> z: normal --> bin_mult w z : normal";
   4.370 -by (etac normal.induct 1);
   4.371 -by (ALLGOALS
   4.372 -    (asm_simp_tac (simpset() addsimps [bin_minus_normal, bin_mult_BIT])));
   4.373 -by (safe_tac (claset() addSDs [normal_BIT_D]));
   4.374 -by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1);
   4.375 -qed_spec_mp "bin_mult_normal";
     5.1 --- a/src/HOL/ex/BinEx.thy	Thu Feb 01 20:48:58 2001 +0100
     5.2 +++ b/src/HOL/ex/BinEx.thy	Thu Feb 01 20:51:13 2001 +0100
     5.3 @@ -2,26 +2,328 @@
     5.4      ID:         $Id$
     5.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.6      Copyright   1998  University of Cambridge
     5.7 -
     5.8 -Definition of normal form for proving that binary arithmetic on
     5.9 -normalized operands yields normalized results.
    5.10 -
    5.11 -Normal means no leading 0s on positive numbers and no leading 1s on negatives.
    5.12  *)
    5.13  
    5.14 -BinEx = Main +
    5.15 +header {* Binary arithmetic examples *}
    5.16 +
    5.17 +theory BinEx = Main:
    5.18 +
    5.19 +subsection {* The Integers *}
    5.20 +
    5.21 +text {* Addition *}
    5.22 +
    5.23 +lemma "(#13::int) + #19 = #32"
    5.24 +  by simp
    5.25 +
    5.26 +lemma "(#1234::int) + #5678 = #6912"
    5.27 +  by simp
    5.28 +
    5.29 +lemma "(#1359::int) + #-2468 = #-1109"
    5.30 +  by simp
    5.31 +
    5.32 +lemma "(#93746::int) + #-46375 = #47371"
    5.33 +  by simp
    5.34 +
    5.35 +
    5.36 +text {* \medskip Negation *}
    5.37 +
    5.38 +lemma "- (#65745::int) = #-65745"
    5.39 +  by simp
    5.40 +
    5.41 +lemma "- (#-54321::int) = #54321"
    5.42 +  by simp
    5.43 +
    5.44 +
    5.45 +text {* \medskip Multiplication *}
    5.46 +
    5.47 +lemma "(#13::int) * #19 = #247"
    5.48 +  by simp
    5.49 +
    5.50 +lemma "(#-84::int) * #51 = #-4284"
    5.51 +  by simp
    5.52 +
    5.53 +lemma "(#255::int) * #255 = #65025"
    5.54 +  by simp
    5.55 +
    5.56 +lemma "(#1359::int) * #-2468 = #-3354012"
    5.57 +  by simp
    5.58 +
    5.59 +lemma "(#89::int) * #10 \<noteq> #889"
    5.60 +  by simp
    5.61 +
    5.62 +lemma "(#13::int) < #18 - #4"
    5.63 +  by simp
    5.64 +
    5.65 +lemma "(#-345::int) < #-242 + #-100"
    5.66 +  by simp
    5.67 +
    5.68 +lemma "(#13557456::int) < #18678654"
    5.69 +  by simp
    5.70 +
    5.71 +lemma "(#999999::int) \<le> (#1000001 + #1) - #2"
    5.72 +  by simp
    5.73 +
    5.74 +lemma "(#1234567::int) \<le> #1234567"
    5.75 +  by simp
    5.76 +
    5.77 +
    5.78 +text {* \medskip Quotient and Remainder *}
    5.79 +
    5.80 +lemma "(#10::int) div #3 = #3"
    5.81 +  by simp
    5.82 +
    5.83 +lemma "(#10::int) mod #3 = #1"
    5.84 +  by simp
    5.85 +
    5.86 +text {* A negative divisor *}
    5.87 +
    5.88 +lemma "(#10::int) div #-3 = #-4"
    5.89 +  by simp
    5.90 +
    5.91 +lemma "(#10::int) mod #-3 = #-2"
    5.92 +  by simp
    5.93  
    5.94 -consts normal :: bin set
    5.95 -  
    5.96 -inductive "normal"
    5.97 -  intrs 
    5.98 +text {*
    5.99 +  A negative dividend\footnote{The definition agrees with mathematical
   5.100 +  convention but not with the hardware of most computers}
   5.101 +*}
   5.102 +
   5.103 +lemma "(#-10::int) div #3 = #-4"
   5.104 +  by simp
   5.105 +
   5.106 +lemma "(#-10::int) mod #3 = #2"
   5.107 +  by simp
   5.108 +
   5.109 +text {* A negative dividend \emph{and} divisor *}
   5.110 +
   5.111 +lemma "(#-10::int) div #-3 = #3"
   5.112 +  by simp
   5.113 +
   5.114 +lemma "(#-10::int) mod #-3 = #-1"
   5.115 +  by simp
   5.116 +
   5.117 +text {* A few bigger examples *}
   5.118 +
   5.119 +lemma "(#8452::int) mod #3 = #1"
   5.120 +  by simp
   5.121 +
   5.122 +lemma "(#59485::int) div #434 = #137"
   5.123 +  by simp
   5.124 +
   5.125 +lemma "(#1000006::int) mod #10 = #6"
   5.126 +  by simp
   5.127 +
   5.128 +
   5.129 +text {* \medskip Division by shifting *}
   5.130 +
   5.131 +lemma "#10000000 div #2 = (#5000000::int)"
   5.132 +  by simp
   5.133 +
   5.134 +lemma "#10000001 mod #2 = (#1::int)"
   5.135 +  by simp
   5.136 +
   5.137 +lemma "#10000055 div #32 = (#312501::int)"
   5.138 +  by simp
   5.139 +
   5.140 +lemma "#10000055 mod #32 = (#23::int)"
   5.141 +  by simp
   5.142 +
   5.143 +lemma "#100094 div #144 = (#695::int)"
   5.144 +  by simp
   5.145 +
   5.146 +lemma "#100094 mod #144 = (#14::int)"
   5.147 +  by simp
   5.148 +
   5.149 +
   5.150 +subsection {* The Natural Numbers *}
   5.151 +
   5.152 +text {* Successor *}
   5.153 +
   5.154 +lemma "Suc #99999 = #100000"
   5.155 +  by (simp add: Suc_nat_number_of)
   5.156 +    -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *}
   5.157 +
   5.158 +
   5.159 +text {* \medskip Addition *}
   5.160 +
   5.161 +lemma "(#13::nat) + #19 = #32"
   5.162 +  by simp
   5.163 +
   5.164 +lemma "(#1234::nat) + #5678 = #6912"
   5.165 +  by simp
   5.166 +
   5.167 +lemma "(#973646::nat) + #6475 = #980121"
   5.168 +  by simp
   5.169 +
   5.170 +
   5.171 +text {* \medskip Subtraction *}
   5.172 +
   5.173 +lemma "(#32::nat) - #14 = #18"
   5.174 +  by simp
   5.175 +
   5.176 +lemma "(#14::nat) - #15 = #0"
   5.177 +  by simp
   5.178  
   5.179 -    Pls  "Pls: normal"
   5.180 +lemma "(#14::nat) - #1576644 = #0"
   5.181 +  by simp
   5.182 +
   5.183 +lemma "(#48273776::nat) - #3873737 = #44400039"
   5.184 +  by simp
   5.185 +
   5.186 +
   5.187 +text {* \medskip Multiplication *}
   5.188 +
   5.189 +lemma "(#12::nat) * #11 = #132"
   5.190 +  by simp
   5.191 +
   5.192 +lemma "(#647::nat) * #3643 = #2357021"
   5.193 +  by simp
   5.194 +
   5.195 +
   5.196 +text {* \medskip Quotient and Remainder *}
   5.197 +
   5.198 +lemma "(#10::nat) div #3 = #3"
   5.199 +  by simp
   5.200 +
   5.201 +lemma "(#10::nat) mod #3 = #1"
   5.202 +  by simp
   5.203 +
   5.204 +lemma "(#10000::nat) div #9 = #1111"
   5.205 +  by simp
   5.206 +
   5.207 +lemma "(#10000::nat) mod #9 = #1"
   5.208 +  by simp
   5.209 +
   5.210 +lemma "(#10000::nat) div #16 = #625"
   5.211 +  by simp
   5.212 +
   5.213 +lemma "(#10000::nat) mod #16 = #0"
   5.214 +  by simp
   5.215 +
   5.216  
   5.217 -    Min  "Min: normal"
   5.218 +text {* \medskip Testing the cancellation of complementary terms *}
   5.219 +
   5.220 +lemma "y + (x + -x) = (#0::int) + y"
   5.221 +  by simp
   5.222 +
   5.223 +lemma "y + (-x + (- y + x)) = (#0::int)"
   5.224 +  by simp
   5.225 +
   5.226 +lemma "-x + (y + (- y + x)) = (#0::int)"
   5.227 +  by simp
   5.228 +
   5.229 +lemma "x + (x + (- x + (- x + (- y + - z)))) = (#0::int) - y - z"
   5.230 +  by simp
   5.231 +
   5.232 +lemma "x + x - x - x - y - z = (#0::int) - y - z"
   5.233 +  by simp
   5.234 +
   5.235 +lemma "x + y + z - (x + z) = y - (#0::int)"
   5.236 +  by simp
   5.237 +
   5.238 +lemma "x + (y + (y + (y + (-x + -x)))) = (#0::int) + y - x + y + y"
   5.239 +  by simp
   5.240 +
   5.241 +lemma "x + (y + (y + (y + (-y + -x)))) = y + (#0::int) + y"
   5.242 +  by simp
   5.243 +
   5.244 +lemma "x + y - x + z - x - y - z + x < (#1::int)"
   5.245 +  by simp
   5.246 +
   5.247 +
   5.248 +subsection {* Normal form of bit strings *}
   5.249 +
   5.250 +text {*
   5.251 +  Definition of normal form for proving that binary arithmetic on
   5.252 +  normalized operands yields normalized results.  Normal means no
   5.253 +  leading 0s on positive numbers and no leading 1s on negatives.
   5.254 +*}
   5.255  
   5.256 -    BIT_F  "[| w: normal; w ~= Pls |] ==> w BIT False : normal"
   5.257 +consts normal :: "bin set"
   5.258 +inductive "normal"
   5.259 +  intros [simp]
   5.260 +    Pls: "Pls: normal"
   5.261 +    Min: "Min: normal"
   5.262 +    BIT_F: "w: normal ==> w \<noteq> Pls ==> w BIT False : normal"
   5.263 +    BIT_T: "w: normal ==> w \<noteq> Min ==> w BIT True : normal"
   5.264 +
   5.265 +text {*
   5.266 +  \medskip Binary arithmetic on normalized operands yields normalized
   5.267 +  results.
   5.268 +*}
   5.269 +
   5.270 +lemma normal_BIT_I [simp]: "w BIT b \<in> normal ==> w BIT b BIT c \<in> normal"
   5.271 +  apply (case_tac c)
   5.272 +   apply auto
   5.273 +  done
   5.274 +
   5.275 +lemma normal_BIT_D: "w BIT b \<in> normal ==> w \<in> normal"
   5.276 +  apply (erule normal.cases)
   5.277 +     apply auto
   5.278 +  done
   5.279 +
   5.280 +lemma NCons_normal [simp]: "w \<in> normal ==> NCons w b \<in> normal"
   5.281 +  apply (induct w)
   5.282 +    apply (auto simp add: NCons_Pls NCons_Min)
   5.283 +  done
   5.284 +
   5.285 +lemma NCons_True: "NCons w True \<noteq> Pls"
   5.286 +  apply (induct w)
   5.287 +    apply auto
   5.288 +  done
   5.289 +
   5.290 +lemma NCons_False: "NCons w False \<noteq> Min"
   5.291 +  apply (induct w)
   5.292 +    apply auto
   5.293 +  done
   5.294  
   5.295 -    BIT_T  "[| w: normal; w ~= Min |] ==> w BIT True : normal"
   5.296 +lemma bin_succ_normal [simp]: "w \<in> normal ==> bin_succ w \<in> normal"
   5.297 +  apply (erule normal.induct)
   5.298 +     apply (case_tac [4] w)
   5.299 +  apply (auto simp add: NCons_True bin_succ_BIT)
   5.300 +  done
   5.301 +
   5.302 +lemma bin_pred_normal [simp]: "w \<in> normal ==> bin_pred w \<in> normal"
   5.303 +  apply (erule normal.induct)
   5.304 +     apply (case_tac [3] w)
   5.305 +  apply (auto simp add: NCons_False bin_pred_BIT)
   5.306 +  done
   5.307 +
   5.308 +lemma bin_add_normal [rule_format]:
   5.309 +  "w \<in> normal --> (\<forall>z. z \<in> normal --> bin_add w z \<in> normal)"
   5.310 +  apply (induct w)
   5.311 +    apply simp
   5.312 +   apply simp
   5.313 +  apply (rule impI)
   5.314 +  apply (rule allI)
   5.315 +  apply (induct_tac z)
   5.316 +    apply (simp_all add: bin_add_BIT)
   5.317 +  apply (safe dest!: normal_BIT_D)
   5.318 +    apply simp_all
   5.319 +  done
   5.320 +
   5.321 +lemma normal_Pls_eq_0: "w \<in> normal ==> (w = Pls) = (number_of w = (#0::int))"
   5.322 +  apply (erule normal.induct)
   5.323 +     apply auto
   5.324 +  done
   5.325 +
   5.326 +lemma bin_minus_normal: "w \<in> normal ==> bin_minus w \<in> normal"
   5.327 +  apply (erule normal.induct)
   5.328 +     apply (simp_all add: bin_minus_BIT)
   5.329 +  apply (rule normal.intros)
   5.330 +  apply assumption
   5.331 +  apply (simp add: normal_Pls_eq_0)
   5.332 +  apply (simp only: number_of_minus iszero_def zminus_equation [of _ "int 0"])
   5.333 +  apply (rule not_sym)
   5.334 +  apply simp
   5.335 +  done
   5.336 +
   5.337 +lemma bin_mult_normal [rule_format]:
   5.338 +    "w \<in> normal ==> z \<in> normal --> bin_mult w z \<in> normal"
   5.339 +  apply (erule normal.induct)
   5.340 +     apply (simp_all add: bin_minus_normal bin_mult_BIT)
   5.341 +  apply (safe dest!: normal_BIT_D)
   5.342 +  apply (simp add: bin_add_normal)
   5.343 +  done
   5.344  
   5.345  end
     6.1 --- a/src/HOL/ex/NatSum.ML	Thu Feb 01 20:48:58 2001 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,96 +0,0 @@
     6.4 -(*  Title:      HOL/ex/NatSum.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Tobias Nipkow
     6.7 -    Copyright   1994 TU Muenchen
     6.8 -
     6.9 -Summing natural numbers, squares, cubes, etc.
    6.10 -
    6.11 -Originally demonstrated permutative rewriting, but add_ac is no longer needed
    6.12 -  thanks to new simprocs.
    6.13 -
    6.14 -Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
    6.15 -  http://www.research.att.com/~njas/sequences/
    6.16 -*)
    6.17 -
    6.18 -Addsimps [lessThan_Suc, atMost_Suc];
    6.19 -Addsimps [add_mult_distrib, add_mult_distrib2];
    6.20 -Addsimps [diff_mult_distrib, diff_mult_distrib2];
    6.21 -
    6.22 -(*The sum of the first n odd numbers equals n squared.*)
    6.23 -Goal "setsum (%i. Suc(i+i)) (lessThan n) = n*n";
    6.24 -by (induct_tac "n" 1);
    6.25 -by Auto_tac;
    6.26 -qed "sum_of_odds";
    6.27 -
    6.28 -(*The sum of the first n odd squares*)
    6.29 -Goal "#3 * setsum (%i. Suc(i+i)*Suc(i+i)) (lessThan n) = n * (#4*n*n - #1)";
    6.30 -by (induct_tac "n" 1);
    6.31 -(*This removes the -#1 from the inductive step*)
    6.32 -by (case_tac "n" 2);
    6.33 -by Auto_tac;
    6.34 -qed "sum_of_odd_squares";
    6.35 -
    6.36 -(*The sum of the first n odd cubes*)
    6.37 -Goal "setsum (%i. Suc(i+i)*Suc(i+i)*Suc(i+i)) (lessThan n) = n * n * (#2*n*n - #1)";
    6.38 -by (induct_tac "n" 1);
    6.39 -(*This removes the -#1 from the inductive step*)
    6.40 -by (case_tac "n" 2);
    6.41 -by Auto_tac;
    6.42 -qed "sum_of_odd_cubes";
    6.43 -
    6.44 -(*The sum of the first n positive integers equals n(n+1)/2.*)
    6.45 -Goal "#2 * setsum id (atMost n) = n*Suc(n)";
    6.46 -by (induct_tac "n" 1);
    6.47 -by Auto_tac;
    6.48 -qed "sum_of_naturals";
    6.49 -
    6.50 -Goal "#6 * setsum (%i. i*i) (atMost n) = n * Suc(n) * Suc(#2*n)";
    6.51 -by (induct_tac "n" 1);
    6.52 -by Auto_tac;
    6.53 -qed "sum_of_squares";
    6.54 -
    6.55 -Goal "#4 * setsum (%i. i*i*i) (atMost n) = n * n * Suc(n) * Suc(n)";
    6.56 -by (induct_tac "n" 1);
    6.57 -by Auto_tac;
    6.58 -qed "sum_of_cubes";
    6.59 -
    6.60 -(** Sum of fourth powers: two versions **)
    6.61 -
    6.62 -Goal "#30 * setsum (%i. i*i*i*i) (atMost n) = \
    6.63 -\     n * Suc(n) * Suc(#2*n) * (#3*n*n + #3*n - #1)";
    6.64 -by (induct_tac "n" 1);
    6.65 -by Auto_tac;
    6.66 -(*Eliminates the subtraction*)
    6.67 -by (case_tac "n" 1);
    6.68 -by (ALLGOALS Asm_simp_tac);
    6.69 -qed "sum_of_fourth_powers";
    6.70 -
    6.71 -(*Alternative proof, with a change of variables and much more subtraction, 
    6.72 -  performed using the integers.*)
    6.73 -
    6.74 -Addsimps [zmult_int RS sym, zadd_zmult_distrib, zadd_zmult_distrib2, 
    6.75 -	  zdiff_zmult_distrib, zdiff_zmult_distrib2];
    6.76 -
    6.77 -Goal "#30 * int (setsum (%i. i*i*i*i) (lessThan m)) = \
    6.78 -\         int m * (int m - #1) * (int (#2*m) - #1) * \
    6.79 -\         (int (#3*m*m) - int(#3*m) - #1)";
    6.80 -by (induct_tac "m" 1);
    6.81 -by (ALLGOALS Asm_simp_tac);
    6.82 -qed "int_sum_of_fourth_powers";
    6.83 -
    6.84 -(** Sums of geometric series: 2, 3 and the general case **)
    6.85 -
    6.86 -Goal "setsum (%i. #2^i) (lessThan n) = #2^n - 1";
    6.87 -by (induct_tac "n" 1);
    6.88 -by Auto_tac;
    6.89 -qed "sum_of_2_powers";
    6.90 -
    6.91 -Goal "#2 * setsum (%i. #3^i) (lessThan n) = #3^n - 1";
    6.92 -by (induct_tac "n" 1);
    6.93 -by Auto_tac;
    6.94 -qed "sum_of_3_powers";
    6.95 -
    6.96 -Goal "0<k ==> (k-1) * setsum (%i. k^i) (lessThan n) = k^n - 1";
    6.97 -by (induct_tac "n" 1);
    6.98 -by Auto_tac;
    6.99 -qed "sum_of_powers";
     7.1 --- a/src/HOL/ex/NatSum.thy	Thu Feb 01 20:48:58 2001 +0100
     7.2 +++ b/src/HOL/ex/NatSum.thy	Thu Feb 01 20:51:13 2001 +0100
     7.3 @@ -1,1 +1,132 @@
     7.4 -NatSum = Main
     7.5 +(*  Title:      HOL/ex/NatSum.ML
     7.6 +    ID:         $Id$
     7.7 +    Author:     Tobias Nipkow
     7.8 +    Copyright   1994 TU Muenchen
     7.9 +
    7.10 +Summing natural numbers, squares, cubes, etc.
    7.11 +
    7.12 +Originally demonstrated permutative rewriting, but add_ac is no longer
    7.13 +needed thanks to new simprocs.
    7.14 +
    7.15 +Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
    7.16 +http://www.research.att.com/~njas/sequences/
    7.17 +*)
    7.18 +
    7.19 +header {* Summing natural numbers *}
    7.20 +
    7.21 +theory NatSum = Main:
    7.22 +
    7.23 +declare lessThan_Suc [simp] atMost_Suc [simp]
    7.24 +declare add_mult_distrib [simp] add_mult_distrib2 [simp]
    7.25 +declare diff_mult_distrib [simp] diff_mult_distrib2 [simp]
    7.26 +
    7.27 +text {*
    7.28 +  \medskip The sum of the first @{term n} odd numbers equals @{term n}
    7.29 +  squared.
    7.30 +*}
    7.31 +
    7.32 +lemma sum_of_odds: "setsum (\<lambda>i. Suc (i + i)) (lessThan n) = n * n"
    7.33 +  apply (induct n)
    7.34 +   apply auto
    7.35 +  done
    7.36 +
    7.37 +
    7.38 +text {*
    7.39 +  \medskip The sum of the first @{text n} odd squares.
    7.40 +*}
    7.41 +
    7.42 +lemma sum_of_odd_squares:
    7.43 +  "#3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) = n * (#4 * n * n - #1)"
    7.44 +  apply (induct n)
    7.45 +  txt {* This removes the @{term "-#1"} from the inductive step *}
    7.46 +   apply (case_tac [2] n)
    7.47 +    apply auto
    7.48 +  done
    7.49 +
    7.50 +
    7.51 +text {*
    7.52 +  \medskip The sum of the first @{term n} odd cubes
    7.53 +*}
    7.54 +
    7.55 +lemma sum_of_odd_cubes:
    7.56 +  "setsum (\<lambda>i. Suc (i + i) * Suc (i + i) * Suc (i + i)) (lessThan n) =
    7.57 +    n * n * (#2 * n * n - #1)"
    7.58 +  apply (induct "n")
    7.59 +  txt {* This removes the @{term "-#1"} from the inductive step *}
    7.60 +   apply (case_tac [2] "n")
    7.61 +    apply auto
    7.62 +  done
    7.63 +
    7.64 +text {*
    7.65 +  \medskip The sum of the first @{term n} positive integers equals
    7.66 +  @{text "n (n + 1) / 2"}.*}
    7.67 +
    7.68 +lemma sum_of_naturals: "#2 * setsum id (atMost n) = n * Suc n"
    7.69 +  apply (induct n)
    7.70 +   apply auto
    7.71 +  done
    7.72 +
    7.73 +lemma sum_of_squares: "#6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)"
    7.74 +  apply (induct n)
    7.75 +   apply auto
    7.76 +  done
    7.77 +
    7.78 +lemma sum_of_cubes: "#4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
    7.79 +  apply (induct n)
    7.80 +   apply auto
    7.81 +  done
    7.82 +
    7.83 +
    7.84 +text {*
    7.85 +  \medskip Sum of fourth powers: two versions.
    7.86 +*}
    7.87 +
    7.88 +lemma sum_of_fourth_powers:
    7.89 +  "#30 * setsum (\<lambda>i. i * i * i * i) (atMost n) =
    7.90 +    n * Suc n * Suc (#2 * n) * (#3 * n * n + #3 * n - #1)"
    7.91 +  apply (induct n)
    7.92 +   apply auto
    7.93 +  txt {* Eliminates the subtraction *}
    7.94 +  apply (case_tac n)
    7.95 +   apply simp_all
    7.96 +  done
    7.97 +
    7.98 +text {*
    7.99 +  Alternative proof, with a change of variables and much more
   7.100 +  subtraction, performed using the integers. *}
   7.101 +
   7.102 +declare
   7.103 +  zmult_int [symmetric, simp]
   7.104 +  zadd_zmult_distrib [simp]
   7.105 +  zadd_zmult_distrib2 [simp]
   7.106 +  zdiff_zmult_distrib [simp]
   7.107 +  zdiff_zmult_distrib2 [simp]
   7.108 +
   7.109 +lemma int_sum_of_fourth_powers:
   7.110 +  "#30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) =
   7.111 +    int m * (int m - #1) * (int (#2 * m) - #1) *
   7.112 +    (int (#3 * m * m) - int (#3 * m) - #1)"
   7.113 +  apply (induct m)
   7.114 +   apply simp_all
   7.115 +  done
   7.116 +
   7.117 +
   7.118 +text {*
   7.119 +  \medskip Sums of geometric series: 2, 3 and the general case *}
   7.120 +
   7.121 +lemma sum_of_2_powers: "setsum (\<lambda>i. #2^i) (lessThan n) = #2^n - 1"
   7.122 +  apply (induct n)
   7.123 +   apply auto
   7.124 +  done
   7.125 +
   7.126 +lemma sum_of_3_powers: "#2 * setsum (\<lambda>i. #3^i) (lessThan n) = #3^n - 1"
   7.127 +  apply (induct n)
   7.128 +   apply auto
   7.129 +  done
   7.130 +
   7.131 +lemma sum_of_powers: "0 < k ==> (k - 1) * setsum (\<lambda>i. k^i) (lessThan n) = k^n - 1"
   7.132 +  apply (induct n)
   7.133 +   apply auto
   7.134 +  done
   7.135 +
   7.136 +end
     8.1 --- a/src/HOL/ex/Primrec.ML	Thu Feb 01 20:48:58 2001 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,270 +0,0 @@
     8.4 -(*  Title:      HOL/ex/Primrec
     8.5 -    ID:         $Id$
     8.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   1997  University of Cambridge
     8.8 -
     8.9 -Primitive Recursive Functions
    8.10 -
    8.11 -Proof adopted from
    8.12 -Nora Szasz, 
    8.13 -A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
    8.14 -In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
    8.15 -
    8.16 -See also E. Mendelson, Introduction to Mathematical Logic.
    8.17 -(Van Nostrand, 1964), page 250, exercise 11.
    8.18 -*)
    8.19 -
    8.20 -
    8.21 -(** Useful special cases of evaluation ***)
    8.22 -
    8.23 -Goalw [SC_def] "SC (x#l) = Suc x";
    8.24 -by (Asm_simp_tac 1);
    8.25 -qed "SC";
    8.26 -
    8.27 -Goalw [CONST_def] "CONST k l = k";
    8.28 -by (Asm_simp_tac 1);
    8.29 -qed "CONST";
    8.30 -
    8.31 -Goalw [PROJ_def] "PROJ(0) (x#l) = x";
    8.32 -by (Asm_simp_tac 1);
    8.33 -qed "PROJ_0";
    8.34 -
    8.35 -Goalw [COMP_def] "COMP g [f] l = g [f l]";
    8.36 -by (Asm_simp_tac 1);
    8.37 -qed "COMP_1";
    8.38 -
    8.39 -Goalw [PREC_def] "PREC f g (0#l) = f l";
    8.40 -by (Asm_simp_tac 1);
    8.41 -qed "PREC_0";
    8.42 -
    8.43 -Goalw [PREC_def] "PREC f g (Suc x # l) = g (PREC f g (x#l) # x # l)";
    8.44 -by (Asm_simp_tac 1);
    8.45 -qed "PREC_Suc";
    8.46 -
    8.47 -Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc];
    8.48 -
    8.49 -
    8.50 -(*PROPERTY A 4*)
    8.51 -Goal "j < ack(i,j)";
    8.52 -by (induct_thm_tac ack.induct "i j" 1);
    8.53 -by (ALLGOALS Asm_simp_tac);
    8.54 -qed "less_ack2";
    8.55 -
    8.56 -AddIffs [less_ack2];
    8.57 -
    8.58 -(*PROPERTY A 5-, the single-step lemma*)
    8.59 -Goal "ack(i,j) < ack(i, Suc(j))";
    8.60 -by (induct_thm_tac ack.induct "i j" 1);
    8.61 -by (ALLGOALS Asm_simp_tac);
    8.62 -qed "ack_less_ack_Suc2";
    8.63 -
    8.64 -AddIffs [ack_less_ack_Suc2];
    8.65 -
    8.66 -(*PROPERTY A 5, monotonicity for < *)
    8.67 -Goal "j<k --> ack(i,j) < ack(i,k)";
    8.68 -by (induct_thm_tac ack.induct "i k" 1);
    8.69 -by (ALLGOALS Asm_simp_tac);
    8.70 -by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1);
    8.71 -qed_spec_mp "ack_less_mono2";
    8.72 -
    8.73 -(*PROPERTY A 5', monotonicity for<=*)
    8.74 -Goal "j<=k ==> ack(i,j)<=ack(i,k)";
    8.75 -by (full_simp_tac (simpset() addsimps [order_le_less]) 1);
    8.76 -by (blast_tac (claset() addIs [ack_less_mono2]) 1);
    8.77 -qed "ack_le_mono2";
    8.78 -
    8.79 -(*PROPERTY A 6*)
    8.80 -Goal "ack(i, Suc(j)) <= ack(Suc(i), j)";
    8.81 -by (induct_tac "j" 1);
    8.82 -by (ALLGOALS Asm_simp_tac);
    8.83 -by (blast_tac (claset() addIs [ack_le_mono2, less_ack2 RS Suc_leI, 
    8.84 -			      le_trans]) 1);
    8.85 -qed "ack2_le_ack1";
    8.86 -
    8.87 -AddIffs [ack2_le_ack1];
    8.88 -
    8.89 -(*PROPERTY A 7-, the single-step lemma*)
    8.90 -Goal "ack(i,j) < ack(Suc(i),j)";
    8.91 -by (blast_tac (claset() addIs [ack_less_mono2, less_le_trans]) 1);
    8.92 -qed "ack_less_ack_Suc1";
    8.93 -
    8.94 -AddIffs [ack_less_ack_Suc1];
    8.95 -
    8.96 -(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
    8.97 -Goal "i < ack(i,j)";
    8.98 -by (induct_tac "i" 1);
    8.99 -by (ALLGOALS Asm_simp_tac);
   8.100 -by (blast_tac (claset() addIs [Suc_leI, le_less_trans]) 1);
   8.101 -qed "less_ack1";
   8.102 -AddIffs [less_ack1];
   8.103 -
   8.104 -(*PROPERTY A 8*)
   8.105 -Goal "ack(1,j) = j + #2";
   8.106 -by (induct_tac "j" 1);
   8.107 -by (ALLGOALS Asm_simp_tac);
   8.108 -qed "ack_1";
   8.109 -Addsimps [ack_1];
   8.110 -
   8.111 -(*PROPERTY A 9.  The unary 1 and 2 in ack is essential for the rewriting.*)
   8.112 -Goal "ack(2,j) = #2*j + #3";
   8.113 -by (induct_tac "j" 1);
   8.114 -by (ALLGOALS Asm_simp_tac);
   8.115 -qed "ack_2";
   8.116 -Addsimps [ack_2];
   8.117 -
   8.118 -
   8.119 -(*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*)
   8.120 -Goal "ack(i,k) < ack(Suc(i+i'),k)";
   8.121 -by (induct_thm_tac ack.induct "i k" 1);
   8.122 -by (ALLGOALS Asm_full_simp_tac);
   8.123 -by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2);
   8.124 -by (induct_thm_tac ack.induct "i' n" 1);
   8.125 -by (ALLGOALS Asm_simp_tac);
   8.126 -by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1);
   8.127 -by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1);
   8.128 -val lemma = result();
   8.129 -
   8.130 -Goal "i<j ==> ack(i,k) < ack(j,k)";
   8.131 -by (dtac less_imp_Suc_add 1);
   8.132 -by (blast_tac (claset() addSIs [lemma]) 1);
   8.133 -qed "ack_less_mono1";
   8.134 -
   8.135 -(*PROPERTY A 7', monotonicity for<=*)
   8.136 -Goal "i<=j ==> ack(i,k)<=ack(j,k)";
   8.137 -by (full_simp_tac (simpset() addsimps [order_le_less]) 1);
   8.138 -by (blast_tac (claset() addIs [ack_less_mono1]) 1);
   8.139 -qed "ack_le_mono1";
   8.140 -
   8.141 -(*PROPERTY A 10*)
   8.142 -Goal "ack(i1, ack(i2,j)) < ack(#2 + (i1+i2), j)";
   8.143 -by (simp_tac numeral_ss 1);
   8.144 -by (rtac (ack2_le_ack1 RSN (2,less_le_trans)) 1);
   8.145 -by (Asm_simp_tac 1);
   8.146 -by (rtac (le_add1 RS ack_le_mono1 RS le_less_trans) 1);
   8.147 -by (rtac (ack_less_mono1 RS ack_less_mono2) 1);
   8.148 -by (simp_tac (simpset() addsimps [le_imp_less_Suc, le_add2]) 1);
   8.149 -qed "ack_nest_bound";
   8.150 -
   8.151 -(*PROPERTY A 11*)
   8.152 -Goal "ack(i1,j) + ack(i2,j) < ack(#4 + (i1 + i2), j)";
   8.153 -by (res_inst_tac [("j", "ack(2, ack(i1 + i2, j))")] less_trans 1);
   8.154 -by (Asm_simp_tac 1);
   8.155 -by (rtac (ack_nest_bound RS less_le_trans) 2);
   8.156 -by (asm_simp_tac (simpset() addsimps [Suc3_eq_add_3]) 2);
   8.157 -by (cut_inst_tac [("i","i1"), ("m1","i2"), ("k","j")] 
   8.158 -    (le_add1 RS ack_le_mono1) 1);
   8.159 -by (cut_inst_tac [("i","i2"), ("m1","i1"), ("k","j")] 
   8.160 -    (le_add2 RS ack_le_mono1) 1);
   8.161 -by Auto_tac;
   8.162 -qed "ack_add_bound";
   8.163 -
   8.164 -(*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
   8.165 -  used k+4.  Quantified version must be nested EX k'. ALL i,j... *)
   8.166 -Goal "i < ack(k,j) ==> i+j < ack(#4 + k, j)";
   8.167 -by (res_inst_tac [("j", "ack(k,j) + ack(0,j)")] less_trans 1);
   8.168 -by (rtac (ack_add_bound RS less_le_trans) 2);
   8.169 -by (Asm_simp_tac 2);
   8.170 -by (REPEAT (ares_tac ([add_less_mono, less_ack2]) 1));
   8.171 -qed "ack_add_bound2";
   8.172 -
   8.173 -
   8.174 -(*** Inductive definition of the PR functions ***)
   8.175 -
   8.176 -(*** MAIN RESULT ***)
   8.177 -
   8.178 -Goalw [SC_def] "SC l < ack(1, list_add l)";
   8.179 -by (induct_tac "l" 1);
   8.180 -by (ALLGOALS (simp_tac (simpset() addsimps [le_add1, le_imp_less_Suc])));
   8.181 -qed "SC_case";
   8.182 -
   8.183 -Goal "CONST k l < ack(k, list_add l)";
   8.184 -by (Simp_tac 1);
   8.185 -qed "CONST_case";
   8.186 -
   8.187 -Goalw [PROJ_def] "ALL i. PROJ i l < ack(0, list_add l)";
   8.188 -by (Simp_tac 1);
   8.189 -by (induct_tac "l" 1);
   8.190 -by (ALLGOALS Asm_simp_tac);
   8.191 -by (rtac allI 1);
   8.192 -by (case_tac "i" 1);
   8.193 -by (asm_simp_tac (simpset() addsimps [le_add1, le_imp_less_Suc]) 1);
   8.194 -by (Asm_simp_tac 1);
   8.195 -by (blast_tac (claset() addIs [less_le_trans] 
   8.196 -                       addSIs [le_add2]) 1);
   8.197 -qed_spec_mp "PROJ_case";
   8.198 -
   8.199 -(** COMP case **)
   8.200 -
   8.201 -Goal "fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
   8.202 -\     ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)";
   8.203 -by (etac lists.induct 1);
   8.204 -by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1);
   8.205 -by Safe_tac;
   8.206 -by (Asm_simp_tac 1);
   8.207 -by (rtac exI 1);
   8.208 -by (blast_tac (claset() addIs [add_less_mono, ack_add_bound, less_trans]) 1);
   8.209 -qed "COMP_map_lemma";
   8.210 -
   8.211 -Goalw [COMP_def]
   8.212 - "[| ALL l. g l < ack(kg, list_add l);           \
   8.213 -\    fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
   8.214 -\ |] ==> EX k. ALL l. COMP g fs  l < ack(k, list_add l)";
   8.215 -by (forward_tac [impOfSubs (Int_lower1 RS lists_mono)] 1);
   8.216 -by (etac (COMP_map_lemma RS exE) 1);
   8.217 -by (rtac exI 1);
   8.218 -by (rtac allI 1);
   8.219 -by (REPEAT (dtac spec 1));
   8.220 -by (etac less_trans 1);
   8.221 -by (blast_tac (claset() addIs [ack_less_mono2, ack_nest_bound, less_trans]) 1);
   8.222 -qed "COMP_case";
   8.223 -
   8.224 -(** PREC case **)
   8.225 -
   8.226 -Goalw [PREC_def]
   8.227 - "[| ALL l. f l + list_add l < ack(kf, list_add l); \
   8.228 -\    ALL l. g l + list_add l < ack(kg, list_add l)  \
   8.229 -\ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)";
   8.230 -by (case_tac "l" 1);
   8.231 -by (ALLGOALS Asm_simp_tac);
   8.232 -by (blast_tac (claset() addIs [less_trans]) 1);
   8.233 -by (etac ssubst 1);  (*get rid of the needless assumption*)
   8.234 -by (induct_tac "a" 1);
   8.235 -by (ALLGOALS Asm_simp_tac);
   8.236 -(*base case*)
   8.237 -by (blast_tac (claset() addIs [le_add1 RS le_imp_less_Suc RS ack_less_mono1, 
   8.238 -			      less_trans]) 1);
   8.239 -(*induction step*)
   8.240 -by (rtac (Suc_leI RS le_less_trans) 1);
   8.241 -by (rtac (le_refl RS add_le_mono RS le_less_trans) 1);
   8.242 -by (etac spec 2);
   8.243 -by (asm_simp_tac (simpset() addsimps [le_add2]) 1);
   8.244 -(*final part of the simplification*)
   8.245 -by (Asm_simp_tac 1);
   8.246 -by (rtac (le_add2 RS ack_le_mono1 RS le_less_trans) 1);
   8.247 -by (etac ack_less_mono2 1);
   8.248 -qed "PREC_case_lemma";
   8.249 -
   8.250 -Goal "[| ALL l. f l < ack(kf, list_add l);        \
   8.251 -\        ALL l. g l < ack(kg, list_add l)         \
   8.252 -\     |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)";
   8.253 -by (rtac exI 1);
   8.254 -by (rtac allI 1);
   8.255 -by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1);
   8.256 -by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1));
   8.257 -qed "PREC_case";
   8.258 -
   8.259 -Goal "f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)";
   8.260 -by (etac PRIMREC.induct 1);
   8.261 -by (ALLGOALS 
   8.262 -    (blast_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, 
   8.263 -			       PREC_case])));
   8.264 -qed "ack_bounds_PRIMREC";
   8.265 -
   8.266 -Goal "(%l. case l of [] => 0 | x#l' => ack(x,x)) ~: PRIMREC";
   8.267 -by (rtac notI 1);
   8.268 -by (etac (ack_bounds_PRIMREC RS exE) 1);
   8.269 -by (rtac less_irrefl 1);
   8.270 -by (dres_inst_tac [("x", "[x]")] spec 1);
   8.271 -by (Asm_full_simp_tac 1);
   8.272 -qed "ack_not_PRIMREC";
   8.273 -
     9.1 --- a/src/HOL/ex/Primrec.thy	Thu Feb 01 20:48:58 2001 +0100
     9.2 +++ b/src/HOL/ex/Primrec.thy	Thu Feb 01 20:51:13 2001 +0100
     9.3 @@ -1,72 +1,348 @@
     9.4 -(*  Title:      HOL/ex/Primrec
     9.5 +(*  Title:      HOL/ex/Primrec.thy
     9.6      ID:         $Id$
     9.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.8      Copyright   1997  University of Cambridge
     9.9  
    9.10 -Primitive Recursive Functions
    9.11 -
    9.12 -Proof adopted from
    9.13 -Nora Szasz, 
    9.14 -A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
    9.15 -In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
    9.16 -
    9.17 -See also E. Mendelson, Introduction to Mathematical Logic.
    9.18 -(Van Nostrand, 1964), page 250, exercise 11.
    9.19 -
    9.20 -Demonstrates recursive definitions, the TFL package
    9.21 +Primitive Recursive Functions.  Demonstrates recursive definitions,
    9.22 +the TFL package.
    9.23  *)
    9.24  
    9.25 -Primrec = Main +
    9.26 +header {* Primitive Recursive Functions *}
    9.27 +
    9.28 +theory Primrec = Main:
    9.29 +
    9.30 +text {*
    9.31 +  Proof adopted from
    9.32 +
    9.33 +  Nora Szasz, A Machine Checked Proof that Ackermann's Function is not
    9.34 +  Primitive Recursive, In: Huet \& Plotkin, eds., Logical Environments
    9.35 +  (CUP, 1993), 317-338.
    9.36 +
    9.37 +  See also E. Mendelson, Introduction to Mathematical Logic.  (Van
    9.38 +  Nostrand, 1964), page 250, exercise 11.
    9.39 +  \medskip
    9.40 +*}
    9.41 +
    9.42 +consts ack :: "nat * nat => nat"
    9.43 +recdef ack  "less_than <*lex*> less_than"
    9.44 +  "ack (0, n) =  Suc n"
    9.45 +  "ack (Suc m, 0) = ack (m, 1)"
    9.46 +  "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"
    9.47 +
    9.48 +consts list_add :: "nat list => nat"
    9.49 +primrec
    9.50 +  "list_add [] = 0"
    9.51 +  "list_add (m # ms) = m + list_add ms"
    9.52 +
    9.53 +consts zeroHd :: "nat list => nat"
    9.54 +primrec
    9.55 +  "zeroHd [] = 0"
    9.56 +  "zeroHd (m # ms) = m"
    9.57 +
    9.58 +
    9.59 +text {* The set of primitive recursive functions of type @{typ "nat list => nat"}. *}
    9.60 +
    9.61 +constdefs
    9.62 +  SC :: "nat list => nat"
    9.63 +  "SC l == Suc (zeroHd l)"
    9.64  
    9.65 -consts ack  :: "nat * nat => nat"
    9.66 -recdef ack "less_than <*lex*> less_than"
    9.67 -    "ack (0,n) =  Suc n"
    9.68 -    "ack (Suc m,0) = (ack (m, 1))"
    9.69 -    "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"
    9.70 +  CONST :: "nat => nat list => nat"
    9.71 +  "CONST k l == k"
    9.72 +
    9.73 +  PROJ :: "nat => nat list => nat"
    9.74 +  "PROJ i l == zeroHd (drop i l)"
    9.75 +
    9.76 +  COMP :: "(nat list => nat) => (nat list => nat) list => nat list => nat"
    9.77 +  "COMP g fs l == g (map (\<lambda>f. f l) fs)"
    9.78 +
    9.79 +  PREC :: "(nat list => nat) => (nat list => nat) => nat list => nat"
    9.80 +  "PREC f g l ==
    9.81 +    case l of
    9.82 +      [] => 0
    9.83 +    | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x"
    9.84 +  -- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *}
    9.85 +
    9.86 +consts PRIMREC :: "(nat list => nat) set"
    9.87 +inductive PRIMREC
    9.88 +  intros
    9.89 +    SC: "SC \<in> PRIMREC"
    9.90 +    CONST: "CONST k \<in> PRIMREC"
    9.91 +    PROJ: "PROJ i \<in> PRIMREC"
    9.92 +    COMP: "g \<in> PRIMREC ==> fs \<in> lists PRIMREC ==> COMP g fs \<in> PRIMREC"
    9.93 +    PREC: "f \<in> PRIMREC ==> g \<in> PRIMREC ==> PREC f g \<in> PRIMREC"
    9.94 +
    9.95 +
    9.96 +text {* Useful special cases of evaluation *}
    9.97 +
    9.98 +lemma SC [simp]: "SC (x # l) = Suc x"
    9.99 +  apply (simp add: SC_def)
   9.100 +  done
   9.101 +
   9.102 +lemma CONST [simp]: "CONST k l = k"
   9.103 +  apply (simp add: CONST_def)
   9.104 +  done
   9.105 +
   9.106 +lemma PROJ_0 [simp]: "PROJ 0 (x # l) = x"
   9.107 +  apply (simp add: PROJ_def)
   9.108 +  done
   9.109 +
   9.110 +lemma COMP_1 [simp]: "COMP g [f] l = g [f l]"
   9.111 +  apply (simp add: COMP_def)
   9.112 +  done
   9.113  
   9.114 -consts  list_add :: nat list => nat
   9.115 -primrec
   9.116 -  "list_add []     = 0"
   9.117 -  "list_add (m#ms) = m + list_add ms"
   9.118 +lemma PREC_0 [simp]: "PREC f g (0 # l) = f l"
   9.119 +  apply (simp add: PREC_def)
   9.120 +  done
   9.121 +
   9.122 +lemma PREC_Suc [simp]: "PREC f g (Suc x # l) = g (PREC f g (x # l) # x # l)"
   9.123 +  apply (simp add: PREC_def)
   9.124 +  done
   9.125 +
   9.126 +
   9.127 +text {* PROPERTY A 4 *}
   9.128 +
   9.129 +lemma less_ack2 [iff]: "j < ack (i, j)"
   9.130 +  apply (induct i j rule: ack.induct)
   9.131 +    apply simp_all
   9.132 +  done
   9.133 +
   9.134 +
   9.135 +text {* PROPERTY A 5-, the single-step lemma *}
   9.136 +
   9.137 +lemma ack_less_ack_Suc2 [iff]: "ack(i, j) < ack (i, Suc j)"
   9.138 +  apply (induct i j rule: ack.induct)
   9.139 +    apply simp_all
   9.140 +  done
   9.141 +
   9.142 +
   9.143 +text {* PROPERTY A 5, monotonicity for @{text "<"} *}
   9.144 +
   9.145 +lemma ack_less_mono2: "j < k ==> ack (i, j) < ack (i, k)"
   9.146 +  apply (induct i k rule: ack.induct)
   9.147 +    apply simp_all
   9.148 +  apply (blast elim!: less_SucE intro: less_trans)
   9.149 +  done
   9.150 +
   9.151 +
   9.152 +text {* PROPERTY A 5', monotonicity for @{text \<le>} *}
   9.153 +
   9.154 +lemma ack_le_mono2: "j \<le> k ==> ack (i, j) \<le> ack (i, k)"
   9.155 +  apply (simp add: order_le_less)
   9.156 +  apply (blast intro: ack_less_mono2)
   9.157 +  done
   9.158  
   9.159 -consts  zeroHd  :: nat list => nat
   9.160 -primrec
   9.161 -  "zeroHd []     = 0"
   9.162 -  "zeroHd (m#ms) = m"
   9.163 +
   9.164 +text {* PROPERTY A 6 *}
   9.165 +
   9.166 +lemma ack2_le_ack1 [iff]: "ack (i, Suc j) \<le> ack (Suc i, j)"
   9.167 +  apply (induct j)
   9.168 +   apply simp_all
   9.169 +  apply (blast intro: ack_le_mono2 less_ack2 [THEN Suc_leI] le_trans)
   9.170 +  done
   9.171 +
   9.172 +
   9.173 +text {* PROPERTY A 7-, the single-step lemma *}
   9.174 +
   9.175 +lemma ack_less_ack_Suc1 [iff]: "ack (i, j) < ack (Suc i, j)"
   9.176 +  apply (blast intro: ack_less_mono2 less_le_trans)
   9.177 +  done
   9.178 +
   9.179 +
   9.180 +text {* PROPERTY A 4'? Extra lemma needed for @{term CONST} case, constant functions *}
   9.181 +
   9.182 +lemma less_ack1 [iff]: "i < ack (i, j)"
   9.183 +  apply (induct i)
   9.184 +   apply simp_all
   9.185 +  apply (blast intro: Suc_leI le_less_trans)
   9.186 +  done
   9.187 +
   9.188 +
   9.189 +text {* PROPERTY A 8 *}
   9.190 +
   9.191 +lemma ack_1 [simp]: "ack (1, j) = j + #2"
   9.192 +  apply (induct j)
   9.193 +   apply simp_all
   9.194 +  done
   9.195 +
   9.196 +
   9.197 +text {* PROPERTY A 9.  The unary @{term 1} and @{term 2} in @{term
   9.198 +  ack} is essential for the rewriting. *}
   9.199 +
   9.200 +lemma ack_2 [simp]: "ack (2, j) = #2 * j + #3"
   9.201 +  apply (induct j)
   9.202 +   apply simp_all
   9.203 +  done
   9.204  
   9.205  
   9.206 -(** The set of primitive recursive functions of type  nat list => nat **)
   9.207 -consts
   9.208 -    PRIMREC :: (nat list => nat) set
   9.209 -    SC      :: nat list => nat
   9.210 -    CONST   :: [nat, nat list] => nat
   9.211 -    PROJ    :: [nat, nat list] => nat
   9.212 -    COMP    :: [nat list => nat, (nat list => nat)list, nat list] => nat
   9.213 -    PREC    :: [nat list => nat, nat list => nat, nat list] => nat
   9.214 +text {* PROPERTY A 7, monotonicity for @{text "<"} [not clear why
   9.215 +  @{thm [source] ack_1} is now needed first!] *}
   9.216 +
   9.217 +lemma ack_less_mono1_aux: "ack (i, k) < ack (Suc (i +i'), k)"
   9.218 +  apply (induct i k rule: ack.induct)
   9.219 +    apply simp_all
   9.220 +   prefer 2
   9.221 +   apply (blast intro: less_trans ack_less_mono2)
   9.222 +  apply (induct_tac i' n rule: ack.induct)
   9.223 +    apply simp_all
   9.224 +  apply (blast intro: Suc_leI [THEN le_less_trans] ack_less_mono2)
   9.225 +  done
   9.226 +
   9.227 +lemma ack_less_mono1: "i < j ==> ack (i, k) < ack (j, k)"
   9.228 +  apply (drule less_imp_Suc_add)
   9.229 +  apply (blast intro!: ack_less_mono1_aux)
   9.230 +  done
   9.231 +
   9.232 +
   9.233 +text {* PROPERTY A 7', monotonicity for @{text "\<le>"} *}
   9.234 +
   9.235 +lemma ack_le_mono1: "i \<le> j ==> ack (i, k) \<le> ack (j, k)"
   9.236 +  apply (simp add: order_le_less)
   9.237 +  apply (blast intro: ack_less_mono1)
   9.238 +  done
   9.239 +
   9.240 +
   9.241 +text {* PROPERTY A 10 *}
   9.242 +
   9.243 +lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (#2 + (i1 + i2), j)"
   9.244 +  apply (simp add: numerals)
   9.245 +  apply (rule ack2_le_ack1 [THEN [2] less_le_trans])
   9.246 +  apply simp
   9.247 +  apply (rule le_add1 [THEN ack_le_mono1, THEN le_less_trans])
   9.248 +  apply (rule ack_less_mono1 [THEN ack_less_mono2])
   9.249 +  apply (simp add: le_imp_less_Suc le_add2)
   9.250 +  done
   9.251 +
   9.252  
   9.253 -defs
   9.254 +text {* PROPERTY A 11 *}
   9.255  
   9.256 -  SC_def    "SC l        == Suc (zeroHd l)"
   9.257 +lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (#4 + (i1 + i2), j)"
   9.258 +  apply (rule_tac j = "ack (2, ack (i1 + i2, j))" in less_trans)
   9.259 +   prefer 2
   9.260 +   apply (rule ack_nest_bound [THEN less_le_trans])
   9.261 +   apply (simp add: Suc3_eq_add_3)
   9.262 +  apply simp
   9.263 +  apply (cut_tac i = i1 and m1 = i2 and k = j in le_add1 [THEN ack_le_mono1])
   9.264 +  apply (cut_tac i = "i2" and m1 = i1 and k = j in le_add2 [THEN ack_le_mono1])
   9.265 +  apply auto
   9.266 +  done
   9.267 +
   9.268 +
   9.269 +text {* PROPERTY A 12.  Article uses existential quantifier but the ALF proof
   9.270 +  used @{text "k + 4"}.  Quantified version must be nested @{text
   9.271 +  "\<exists>k'. \<forall>i j. ..."} *}
   9.272  
   9.273 -  CONST_def "CONST k l   == k"
   9.274 +lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (#4 + k, j)"
   9.275 +  apply (rule_tac j = "ack (k, j) + ack (0, j)" in less_trans)
   9.276 +   prefer 2
   9.277 +   apply (rule ack_add_bound [THEN less_le_trans])
   9.278 +   apply simp
   9.279 +  apply (rule add_less_mono less_ack2 | assumption)+
   9.280 +  done
   9.281 +
   9.282 +
   9.283 +
   9.284 +text {* Inductive definition of the @{term PR} functions *}
   9.285  
   9.286 -  PROJ_def  "PROJ i l    == zeroHd (drop i l)"
   9.287 +text {* MAIN RESULT *}
   9.288 +
   9.289 +lemma SC_case: "SC l < ack (1, list_add l)"
   9.290 +  apply (unfold SC_def)
   9.291 +  apply (induct l)
   9.292 +  apply (simp_all add: le_add1 le_imp_less_Suc)
   9.293 +  done
   9.294 +
   9.295 +lemma CONST_case: "CONST k l < ack (k, list_add l)"
   9.296 +  apply simp
   9.297 +  done
   9.298  
   9.299 -  COMP_def  "COMP g fs l == g (map (%f. f l) fs)"
   9.300 +lemma PROJ_case [rule_format]: "\<forall>i. PROJ i l < ack (0, list_add l)"
   9.301 +  apply (simp add: PROJ_def)
   9.302 +  apply (induct l)
   9.303 +   apply simp_all
   9.304 +  apply (rule allI)
   9.305 +  apply (case_tac i)
   9.306 +  apply (simp (no_asm_simp) add: le_add1 le_imp_less_Suc)
   9.307 +  apply (simp (no_asm_simp))
   9.308 +  apply (blast intro: less_le_trans intro!: le_add2)
   9.309 +  done
   9.310 +
   9.311 +
   9.312 +text {* @{term COMP} case *}
   9.313  
   9.314 -  (*Note that g is applied first to PREC f g y and then to y!*)
   9.315 -  PREC_def  "PREC f g l == case l of
   9.316 -                             []   => 0
   9.317 -                           | x#l' => nat_rec (f l') (%y r. g (r#y#l')) x"
   9.318 +lemma COMP_map_aux: "fs \<in> lists (PRIMREC \<inter> {f. \<exists>kf. \<forall>l. f l < ack (kf, list_add l)})
   9.319 +  ==> \<exists>k. \<forall>l. list_add (map (\<lambda>f. f l) fs) < ack (k, list_add l)"
   9.320 +  apply (erule lists.induct)
   9.321 +  apply (rule_tac x = 0 in exI)
   9.322 +   apply simp
   9.323 +  apply safe
   9.324 +  apply simp
   9.325 +  apply (rule exI)
   9.326 +  apply (blast intro: add_less_mono ack_add_bound less_trans)
   9.327 +  done
   9.328 +
   9.329 +lemma COMP_case:
   9.330 +  "\<forall>l. g l < ack (kg, list_add l) ==>
   9.331 +  fs \<in> lists(PRIMREC Int {f. \<exists>kf. \<forall>l. f l < ack(kf, list_add l)})
   9.332 +  ==> \<exists>k. \<forall>l. COMP g fs  l < ack(k, list_add l)"
   9.333 +  apply (unfold COMP_def)
   9.334 +  apply (frule Int_lower1 [THEN lists_mono, THEN subsetD])
   9.335 +  apply (erule COMP_map_aux [THEN exE])
   9.336 +  apply (rule exI)
   9.337 +  apply (rule allI)
   9.338 +  apply (drule spec)+
   9.339 +  apply (erule less_trans)
   9.340 +  apply (blast intro: ack_less_mono2 ack_nest_bound less_trans)
   9.341 +  done
   9.342 +
   9.343 +
   9.344 +text {* @{term PREC} case *}
   9.345  
   9.346 -  
   9.347 -inductive PRIMREC
   9.348 -  intrs
   9.349 -    SC       "SC : PRIMREC"
   9.350 -    CONST    "CONST k : PRIMREC"
   9.351 -    PROJ     "PROJ i : PRIMREC"
   9.352 -    COMP     "[| g: PRIMREC; fs: lists PRIMREC |] ==> COMP g fs : PRIMREC"
   9.353 -    PREC     "[| f: PRIMREC; g: PRIMREC |] ==> PREC f g: PRIMREC"
   9.354 -  monos      lists_mono
   9.355 +lemma PREC_case_aux:
   9.356 +  "\<forall>l. f l + list_add l < ack (kf, list_add l) ==>
   9.357 +    \<forall>l. g l + list_add l < ack (kg, list_add l) ==>
   9.358 +    PREC f g l + list_add l < ack (Suc (kf + kg), list_add l)"
   9.359 +  apply (unfold PREC_def)
   9.360 +  apply (case_tac l)
   9.361 +   apply simp_all
   9.362 +   apply (blast intro: less_trans)
   9.363 +  apply (erule ssubst) -- {* get rid of the needless assumption *}
   9.364 +  apply (induct_tac a)
   9.365 +   apply simp_all
   9.366 +   txt {* base case *}
   9.367 +   apply (blast intro: le_add1 [THEN le_imp_less_Suc, THEN ack_less_mono1] less_trans)
   9.368 +  txt {* induction step *}
   9.369 +  apply (rule Suc_leI [THEN le_less_trans])
   9.370 +   apply (rule le_refl [THEN add_le_mono, THEN le_less_trans])
   9.371 +    prefer 2
   9.372 +    apply (erule spec)
   9.373 +   apply (simp add: le_add2)
   9.374 +  txt {* final part of the simplification *}
   9.375 +  apply simp
   9.376 +  apply (rule le_add2 [THEN ack_le_mono1, THEN le_less_trans])
   9.377 +  apply (erule ack_less_mono2)
   9.378 +  done
   9.379 +
   9.380 +lemma PREC_case:
   9.381 +  "\<forall>l. f l < ack (kf, list_add l) ==>
   9.382 +    \<forall>l. g l < ack (kg, list_add l) ==>
   9.383 +    \<exists>k. \<forall>l. PREC f g l < ack (k, list_add l)"
   9.384 +  apply (rule exI)
   9.385 +  apply (rule allI)
   9.386 +  apply (rule le_less_trans [OF le_add1 PREC_case_aux])
   9.387 +   apply (blast intro: ack_add_bound2)+
   9.388 +  done
   9.389 +
   9.390 +lemma ack_bounds_PRIMREC: "f \<in> PRIMREC ==> \<exists>k. \<forall>l. f l < ack (k, list_add l)"
   9.391 +  apply (erule PRIMREC.induct)
   9.392 +      apply (blast intro: SC_case CONST_case PROJ_case COMP_case PREC_case)+
   9.393 +  done
   9.394 +
   9.395 +lemma ack_not_PRIMREC: "(\<lambda>l. case l of [] => 0 | x # l' => ack (x, x)) \<notin> PRIMREC"
   9.396 +  apply (rule notI)
   9.397 +  apply (erule ack_bounds_PRIMREC [THEN exE])
   9.398 +  apply (rule less_irrefl)
   9.399 +  apply (drule_tac x = "[x]" in spec)
   9.400 +  apply simp
   9.401 +  done
   9.402  
   9.403  end
    10.1 --- a/src/HOL/ex/Recdefs.ML	Thu Feb 01 20:48:58 2001 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,38 +0,0 @@
    10.4 -(*  Title:      HOL/ex/Recdefs.ML
    10.5 -    ID:         $Id$
    10.6 -    Author:     Konrad Slind and Lawrence C Paulson
    10.7 -    Copyright   1997  University of Cambridge
    10.8 -
    10.9 -A few proofs to demonstrate the functions defined in Recdefs.thy
   10.10 -Lemma statements from Konrad Slind's Web site
   10.11 -*)
   10.12 -
   10.13 -(** The silly g function: example of nested recursion **)
   10.14 -
   10.15 -Addsimps g.simps;
   10.16 -
   10.17 -Goal "g x < Suc x";
   10.18 -by (induct_thm_tac g.induct "x" 1);
   10.19 -by Auto_tac;
   10.20 -qed "g_terminates";
   10.21 -
   10.22 -Goal "g x = 0";
   10.23 -by (induct_thm_tac g.induct "x" 1);
   10.24 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
   10.25 -qed "g_zero";
   10.26 -
   10.27 -(*** the contrived `mapf' ***)
   10.28 -
   10.29 -(* proving the termination condition: *)
   10.30 -val [tc] = mapf.tcs;
   10.31 -goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
   10.32 -by (rtac allI 1);
   10.33 -by (case_tac "n=0" 1);
   10.34 -by (ALLGOALS Asm_simp_tac);
   10.35 -val lemma = result();
   10.36 -
   10.37 -(* removing the termination condition from the generated thms: *)
   10.38 -val [mapf_0,mapf_Suc] = mapf.simps;
   10.39 -val mapf_Suc = lemma RS mapf_Suc;
   10.40 -
   10.41 -val mapf_induct = lemma RS mapf.induct;
    11.1 --- a/src/HOL/ex/Recdefs.thy	Thu Feb 01 20:48:58 2001 +0100
    11.2 +++ b/src/HOL/ex/Recdefs.thy	Thu Feb 01 20:51:13 2001 +0100
    11.3 @@ -6,88 +6,126 @@
    11.4  Examples of recdef definitions.  Most, but not all, are handled automatically.
    11.5  *)
    11.6  
    11.7 -Recdefs = Main +
    11.8 +header {* Examples of recdef definitions *}
    11.9 +
   11.10 +theory Recdefs = Main:
   11.11  
   11.12  consts fact :: "nat => nat"
   11.13 -recdef fact "less_than"
   11.14 -    "fact x = (if (x = 0) then 1 else x * fact (x - 1))"
   11.15 +recdef fact  less_than
   11.16 +  "fact x = (if x = 0 then 1 else x * fact (x - 1))"
   11.17  
   11.18  consts Fact :: "nat => nat"
   11.19 -recdef Fact "less_than"
   11.20 -    "Fact 0 = 1"
   11.21 -    "Fact (Suc x) = (Fact x * Suc x)"
   11.22 +recdef Fact  less_than
   11.23 +  "Fact 0 = 1"
   11.24 +  "Fact (Suc x) = Fact x * Suc x"
   11.25  
   11.26  consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
   11.27 -recdef map2 "measure(%(f,l1,l2).size l1)"
   11.28 -    "map2(f, [], [])  = []"
   11.29 -    "map2(f, h#t, []) = []"
   11.30 -    "map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2)"
   11.31 +recdef map2  "measure(\<lambda>(f, l1, l2). size l1)"
   11.32 +  "map2 (f, [], [])  = []"
   11.33 +  "map2 (f, h # t, []) = []"
   11.34 +  "map2 (f, h1 # t1, h2 # t2) = f h1 h2 # map2 (f, t1, t2)"
   11.35  
   11.36 -consts finiteRchain :: "(['a,'a] => bool) * 'a list => bool"
   11.37 -recdef finiteRchain "measure (%(R,l).size l)"
   11.38 -    "finiteRchain(R,  []) = True"
   11.39 -    "finiteRchain(R, [x]) = True"
   11.40 -    "finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst))"
   11.41 +consts finiteRchain :: "('a => 'a => bool) * 'a list => bool"
   11.42 +recdef finiteRchain  "measure (\<lambda>(R, l). size l)"
   11.43 +  "finiteRchain(R,  []) = True"
   11.44 +  "finiteRchain(R, [x]) = True"
   11.45 +  "finiteRchain(R, x # y # rst) = (R x y \<and> finiteRchain (R, y # rst))"
   11.46  
   11.47 -(*Not handled automatically: too complicated.*)
   11.48 +text {* Not handled automatically: too complicated. *}
   11.49  consts variant :: "nat * nat list => nat"
   11.50 -recdef variant "measure(%(n::nat, ns). size(filter(%y. n <= y) ns))"
   11.51 -    "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)"
   11.52 +recdef variant  "measure (\<lambda>(n::nat, ns). size (filter (\<lambda>y. n \<le> y) ns))"
   11.53 +  "variant (x, L) = (if x mem L then variant (Suc x, L) else x)"
   11.54  
   11.55  consts gcd :: "nat * nat => nat"
   11.56 -recdef gcd "measure (%(x,y).x+y)"
   11.57 -    "gcd (0,y)          = y"
   11.58 -    "gcd (Suc x, 0)     = Suc x"
   11.59 -    "gcd (Suc x, Suc y) = (if (y <= x) then gcd(x - y, Suc y)  
   11.60 -                                       else gcd(Suc x, y - x))"
   11.61 +recdef gcd  "measure (\<lambda>(x, y). x + y)"
   11.62 +  "gcd (0, y) = y"
   11.63 +  "gcd (Suc x, 0) = Suc x"
   11.64 +  "gcd (Suc x, Suc y) =
   11.65 +    (if y \<le> x then gcd (x - y, Suc y) else gcd (Suc x, y - x))"
   11.66 +
   11.67 +
   11.68 +text {*
   11.69 +  \medskip The silly @{term g} function: example of nested recursion.
   11.70 +  Not handled automatically.  In fact, @{term g} is the zero constant
   11.71 +  function.
   11.72 + *}
   11.73  
   11.74 -(*Not handled automatically.  In fact, g is the zero constant function.*)
   11.75 -consts g   :: "nat => nat"
   11.76 -recdef g "less_than"
   11.77 -    "g 0 = 0"
   11.78 -    "g(Suc x) = g(g x)"
   11.79 +consts g :: "nat => nat"
   11.80 +recdef g  less_than
   11.81 +  "g 0 = 0"
   11.82 +  "g (Suc x) = g (g x)"
   11.83 +
   11.84 +lemma g_terminates: "g x < Suc x"
   11.85 +  apply (induct x rule: g.induct)
   11.86 +   apply (auto simp add: g.simps)
   11.87 +  done
   11.88 +
   11.89 +lemma g_zero: "g x = 0"
   11.90 +  apply (induct x rule: g.induct)
   11.91 +   apply (simp_all add: g.simps g_terminates)
   11.92 +  done
   11.93 +
   11.94  
   11.95  consts Div :: "nat * nat => nat * nat"
   11.96 -recdef Div "measure fst"
   11.97 -    "Div(0,x)      = (0,0)"
   11.98 -    "Div(Suc x, y) =      
   11.99 -         (let (q,r) = Div(x,y)
  11.100 -          in                      
  11.101 -          if (y <= Suc r) then (Suc q,0) else (q, Suc r))"
  11.102 +recdef Div  "measure fst"
  11.103 +  "Div (0, x) = (0, 0)"
  11.104 +  "Div (Suc x, y) =
  11.105 +    (let (q, r) = Div (x, y)
  11.106 +    in if y \<le> Suc r then (Suc q, 0) else (q, Suc r))"
  11.107 +
  11.108 +text {*
  11.109 +  \medskip Not handled automatically.  Should be the predecessor
  11.110 +  function, but there is an unnecessary "looping" recursive call in
  11.111 +  @{term "k 1"}.
  11.112 +*}
  11.113  
  11.114 -(*Not handled automatically.  Should be the predecessor function, but there
  11.115 -  is an unnecessary "looping" recursive call in k(1) *)
  11.116 -consts k   :: "nat => nat"
  11.117 -recdef k "less_than"
  11.118 -    "k 0 = 0"
  11.119 -    "k (Suc n) = (let x = k 1  
  11.120 -                  in if (0=1) then k (Suc 1) else n)"
  11.121 +consts k :: "nat => nat"
  11.122 +recdef k  less_than
  11.123 +  "k 0 = 0"
  11.124 +  "k (Suc n) =
  11.125 +   (let x = k 1
  11.126 +    in if 0 = 1 then k (Suc 1) else n)"
  11.127 +
  11.128 +consts part :: "('a => bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
  11.129 +recdef part  "measure (\<lambda>(P, l, l1, l2). size l)"
  11.130 +  "part (P, [], l1, l2) = (l1, l2)"
  11.131 +  "part (P, h # rst, l1, l2) =
  11.132 +    (if P h then part (P, rst, h # l1, l2)
  11.133 +    else part (P, rst, l1, h # l2))"
  11.134  
  11.135 -consts part :: "('a=>bool) * 'a list * 'a list * 'a list => 'a list * 'a list"
  11.136 -recdef part "measure (%(P,l,l1,l2).size l)"
  11.137 -    "part(P, [], l1,l2) = (l1,l2)"
  11.138 -    "part(P, h#rst, l1,l2) =  
  11.139 -        (if P h then part(P,rst, h#l1,  l2)  
  11.140 -                else part(P,rst,  l1,  h#l2))"
  11.141 +consts fqsort :: "('a => 'a => bool) * 'a list => 'a list"
  11.142 +recdef fqsort  "measure (size o snd)"
  11.143 +  "fqsort (ord, []) = []"
  11.144 +  "fqsort (ord, x # rst) =
  11.145 +  (let (less, more) = part ((\<lambda>y. ord y x), rst, ([], []))
  11.146 +  in fqsort (ord, less) @ [x] @ fqsort (ord, more))"
  11.147 +
  11.148 +text {*
  11.149 +  \medskip Silly example which demonstrates the occasional need for
  11.150 +  additional congruence rules (here: @{thm [source] map_cong}).  If
  11.151 +  the congruence rule is removed, an unprovable termination condition
  11.152 +  is generated!  Termination not proved automatically.  TFL requires
  11.153 +  @{term [source] "\<lambda>x. mapf x"} instead of @{term [source] mapf}.
  11.154 +*}
  11.155  
  11.156 -consts fqsort :: "(['a,'a] => bool) * 'a list => 'a list"
  11.157 -recdef fqsort "measure (size o snd)"
  11.158 -    "fqsort(ord,[]) = []"
  11.159 -    "fqsort(ord, x#rst) =    
  11.160 -     (let (less,more) = part((%y. ord y x), rst, ([],[]))
  11.161 -      in  
  11.162 -      fqsort(ord,less)@[x]@fqsort(ord,more))"
  11.163 +consts mapf :: "nat => nat list"
  11.164 +recdef mapf  "measure (\<lambda>m. m)"
  11.165 +  "mapf 0 = []"
  11.166 +  "mapf (Suc n) = concat (map (\<lambda>x. mapf x) (replicate n n))"
  11.167 +  (hints cong: map_cong)
  11.168  
  11.169 -(* silly example which demonstrates the occasional need for additional
  11.170 -   congruence rules (here: map_cong from List). If the congruence rule is
  11.171 -   removed, an unprovable termination condition is generated!
  11.172 -   Termination not proved automatically; see the ML file.
  11.173 -   TFL requires (%x.mapf x) instead of mapf.
  11.174 -*)
  11.175 -consts mapf :: nat => nat list
  11.176 -recdef mapf "measure(%m. m)"
  11.177 -congs map_cong
  11.178 -"mapf 0 = []"
  11.179 -"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"
  11.180 +recdef_tc mapf_tc: mapf
  11.181 +  apply (rule allI)
  11.182 +  apply (case_tac "n = 0")
  11.183 +   apply simp_all
  11.184 +  done
  11.185 +
  11.186 +text {* Removing the termination condition from the generated thms: *}
  11.187 +
  11.188 +lemma "mapf (Suc n) = concat (map mapf (replicate n n))"
  11.189 +  apply (simp add: mapf.simps mapf_tc)
  11.190 +  done
  11.191 +
  11.192 +lemmas mapf_induct = mapf.induct [OF mapf_tc]
  11.193  
  11.194  end