fix HOL/ex/LexOrds.thy; add to regression
authorkrauss
Tue Aug 05 14:40:48 2008 +0200 (2008-08-05)
changeset 27742df552e6027cf
parent 27741 d2523b72ed44
child 27743 7420e78f1541
fix HOL/ex/LexOrds.thy; add to regression
src/HOL/IsaMakefile
src/HOL/ex/LexOrds.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Aug 05 13:31:38 2008 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Aug 05 14:40:48 2008 +0200
     1.3 @@ -766,7 +766,7 @@
     1.4    ex/Binary.thy ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy	\
     1.5    ex/Induction_Scheme.thy ex/InductiveInvariant.thy			\
     1.6    ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
     1.7 -  ex/Lagrange.thy ex/Locales.thy ex/LocaleTest2.thy ex/MT.thy		\
     1.8 +  ex/Lagrange.thy ex/LexOrds.thy ex/Locales.thy ex/LocaleTest2.thy ex/MT.thy		\
     1.9    ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy	\
    1.10    ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy ex/Puzzle.thy		\
    1.11    ex/Quickcheck_Examples.thy ex/Reflection.thy ex/reflection_data.ML	\
     2.1 --- a/src/HOL/ex/LexOrds.thy	Tue Aug 05 13:31:38 2008 +0200
     2.2 +++ b/src/HOL/ex/LexOrds.thy	Tue Aug 05 14:40:48 2008 +0200
     2.3 @@ -1,9 +1,9 @@
     2.4  (* Title:       HOL/ex/LexOrds.thy
     2.5 -   ID:
     2.6 +   ID:          $Id$
     2.7     Author:      Lukas Bulwahn, TU Muenchen
     2.8 +*)
     2.9  
    2.10 -Examples for functions whose termination is proven by lexicographic order.
    2.11 -*)
    2.12 +header {* Examples and regression tests for method lexicographic order. *}
    2.13   
    2.14  theory LexOrds
    2.15  imports Main
    2.16 @@ -13,12 +13,12 @@
    2.17  
    2.18  fun identity :: "nat \<Rightarrow> nat"
    2.19  where
    2.20 -"identity n = n"
    2.21 +  "identity n = n"
    2.22  
    2.23  fun yaSuc :: "nat \<Rightarrow> nat"
    2.24  where 
    2.25    "yaSuc 0 = 0"
    2.26 -  "yaSuc (Suc n) = Suc (yaSuc n)"
    2.27 +| "yaSuc (Suc n) = Suc (yaSuc n)"
    2.28  
    2.29  
    2.30  subsection {* Examples on natural numbers *}
    2.31 @@ -26,39 +26,39 @@
    2.32  fun bin :: "(nat * nat) \<Rightarrow> nat"
    2.33  where
    2.34    "bin (0, 0) = 1"
    2.35 -  "bin (Suc n, 0) = 0"
    2.36 -  "bin (0, Suc m) = 0"
    2.37 -  "bin (Suc n, Suc m) = bin (n, m) + bin (Suc n, m)"
    2.38 +| "bin (Suc n, 0) = 0"
    2.39 +| "bin (0, Suc m) = 0"
    2.40 +| "bin (Suc n, Suc m) = bin (n, m) + bin (Suc n, m)"
    2.41  
    2.42  
    2.43  fun t :: "(nat * nat) \<Rightarrow> nat"
    2.44  where
    2.45    "t (0,n) = 0"
    2.46 -  "t (n,0) = 0"
    2.47 -  "t (Suc n, Suc m) = (if (n mod 2 = 0) then (t (Suc n, m)) else (t (n, Suc m)))" 
    2.48 +| "t (n,0) = 0"
    2.49 +| "t (Suc n, Suc m) = (if (n mod 2 = 0) then (t (Suc n, m)) else (t (n, Suc m)))" 
    2.50  
    2.51  
    2.52  fun k :: "(nat * nat) * (nat * nat) \<Rightarrow> nat"
    2.53  where
    2.54    "k ((0,0),(0,0)) = 0"
    2.55 -  "k ((Suc z, y), (u,v)) = k((z, y), (u, v))" (* z is descending *)
    2.56 -  "k ((0, Suc y), (u,v)) = k((1, y), (u, v))" (* y is descending *)
    2.57 -  "k ((0,0), (Suc u, v)) = k((1, 1), (u, v))" (* u is descending *)
    2.58 -  "k ((0,0), (0, Suc v)) = k((1,1), (1,v))"   (* v is descending *)
    2.59 +| "k ((Suc z, y), (u,v)) = k((z, y), (u, v))" (* z is descending *)
    2.60 +| "k ((0, Suc y), (u,v)) = k((1, y), (u, v))" (* y is descending *)
    2.61 +| "k ((0,0), (Suc u, v)) = k((1, 1), (u, v))" (* u is descending *)
    2.62 +| "k ((0,0), (0, Suc v)) = k((1,1), (1,v))"   (* v is descending *)
    2.63  
    2.64  
    2.65  fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    2.66  where
    2.67    "gcd2 x 0 = x"
    2.68 -  "gcd2 0 y = y"
    2.69 -  "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
    2.70 +| "gcd2 0 y = y"
    2.71 +| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
    2.72                                      else gcd2 (x - y) (Suc y))"
    2.73  
    2.74  fun ack :: "(nat * nat) \<Rightarrow> nat"
    2.75  where
    2.76    "ack (0, m) = Suc m"
    2.77 -  "ack (Suc n, 0) = ack(n, 1)"
    2.78 -  "ack (Suc n, Suc m) = ack (n, ack (Suc n, m))"
    2.79 +| "ack (Suc n, 0) = ack(n, 1)"
    2.80 +| "ack (Suc n, Suc m) = ack (n, ack (Suc n, m))"
    2.81  
    2.82  
    2.83  fun greedy :: "nat * nat * nat * nat * nat => nat"
    2.84 @@ -74,21 +74,21 @@
    2.85    (if (a < 80) then greedy (a, Suc b, Suc c, d, Suc e) else
    2.86    (if (a < 90) then greedy (Suc a, Suc b, Suc c, d, e) else
    2.87    greedy (Suc a, Suc b, Suc c, d, e))))))))))"
    2.88 -  "greedy (a, b, c, d, e) = 0"
    2.89 +| "greedy (a, b, c, d, e) = 0"
    2.90  
    2.91  
    2.92  fun blowup :: "nat => nat => nat => nat => nat => nat => nat => nat => nat => nat"
    2.93  where
    2.94    "blowup 0 0 0 0 0 0 0 0 0 = 0"
    2.95 -  "blowup 0 0 0 0 0 0 0 0 (Suc i) = Suc (blowup i i i i i i i i i)"
    2.96 -  "blowup 0 0 0 0 0 0 0 (Suc h) i = Suc (blowup h h h h h h h h i)"
    2.97 -  "blowup 0 0 0 0 0 0 (Suc g) h i = Suc (blowup g g g g g g g h i)"
    2.98 -  "blowup 0 0 0 0 0 (Suc f) g h i = Suc (blowup f f f f f f g h i)"
    2.99 -  "blowup 0 0 0 0 (Suc e) f g h i = Suc (blowup e e e e e f g h i)"
   2.100 -  "blowup 0 0 0 (Suc d) e f g h i = Suc (blowup d d d d e f g h i)"
   2.101 -  "blowup 0 0 (Suc c) d e f g h i = Suc (blowup c c c d e f g h i)"
   2.102 -  "blowup 0 (Suc b) c d e f g h i = Suc (blowup b b c d e f g h i)"
   2.103 -  "blowup (Suc a) b c d e f g h i = Suc (blowup a b c d e f g h i)"
   2.104 +| "blowup 0 0 0 0 0 0 0 0 (Suc i) = Suc (blowup i i i i i i i i i)"
   2.105 +| "blowup 0 0 0 0 0 0 0 (Suc h) i = Suc (blowup h h h h h h h h i)"
   2.106 +| "blowup 0 0 0 0 0 0 (Suc g) h i = Suc (blowup g g g g g g g h i)"
   2.107 +| "blowup 0 0 0 0 0 (Suc f) g h i = Suc (blowup f f f f f f g h i)"
   2.108 +| "blowup 0 0 0 0 (Suc e) f g h i = Suc (blowup e e e e e f g h i)"
   2.109 +| "blowup 0 0 0 (Suc d) e f g h i = Suc (blowup d d d d e f g h i)"
   2.110 +| "blowup 0 0 (Suc c) d e f g h i = Suc (blowup c c c d e f g h i)"
   2.111 +| "blowup 0 (Suc b) c d e f g h i = Suc (blowup b b c d e f g h i)"
   2.112 +| "blowup (Suc a) b c d e f g h i = Suc (blowup a b c d e f g h i)"
   2.113  
   2.114    
   2.115  subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *}
   2.116 @@ -98,9 +98,9 @@
   2.117  fun g_tree :: "tree * tree \<Rightarrow> tree"
   2.118  where
   2.119    "g_tree (Node, Node) = Node"
   2.120 -  "g_tree (Node, Branch a b) = Branch Node (g_tree (a,b))"
   2.121 -  "g_tree (Branch a b, Node) = Branch (g_tree (a,Node)) b"
   2.122 -  "g_tree (Branch a b, Branch c d) = Branch (g_tree (a,c)) (g_tree (b,d))"
   2.123 +| "g_tree (Node, Branch a b) = Branch Node (g_tree (a,b))"
   2.124 +| "g_tree (Branch a b, Node) = Branch (g_tree (a,Node)) b"
   2.125 +| "g_tree (Branch a b, Branch c d) = Branch (g_tree (a,c)) (g_tree (b,d))"
   2.126  
   2.127  
   2.128  fun acklist :: "'a list * 'a list \<Rightarrow> 'a list"
   2.129 @@ -123,8 +123,8 @@
   2.130  fun sizechange_f :: "'a list => 'a list => 'a list" and
   2.131  sizechange_g :: "'a list => 'a list => 'a list => 'a list"
   2.132  where
   2.133 -"sizechange_f i x = (if i=[] then x else sizechange_g (tl i) x i)"
   2.134 -"sizechange_g a b c = sizechange_f a (b @ c)"
   2.135 +  "sizechange_f i x = (if i=[] then x else sizechange_g (tl i) x i)"
   2.136 +| "sizechange_g a b c = sizechange_f a (b @ c)"
   2.137  
   2.138  
   2.139  fun
   2.140 @@ -133,8 +133,8 @@
   2.141    oprod :: "nat => nat => nat => nat"
   2.142  where
   2.143    "prod x y z = (if y mod 2 = 0 then eprod x y z else oprod x y z)"
   2.144 -  "oprod x y z = eprod x (y - 1) (z+x)"
   2.145 -  "eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)"
   2.146 +| "oprod x y z = eprod x (y - 1) (z+x)"
   2.147 +| "eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)"
   2.148  
   2.149  
   2.150  fun
   2.151 @@ -152,14 +152,6 @@
   2.152       (if n < m then coast n (m - 1) (c + n)
   2.153                 else pedal n m (c + n))"
   2.154  
   2.155 -fun ack1 :: "nat => nat => nat"
   2.156 -  and ack2 :: "nat => nat => nat"
   2.157 -  where
   2.158 -  "ack1 0 m = m+1" |
   2.159 -  "ack1 (Suc n) m = ack2 n m" |
   2.160 -  "ack2 n 0 = ack1 n 1" |
   2.161 -  "ack2 n (Suc m) = ack1 n (ack2 n (Suc m))"
   2.162 -
   2.163  
   2.164  subsection {*Examples for an unprovable termination *}
   2.165  
   2.166 @@ -174,9 +166,9 @@
   2.167  function term_but_no_prove :: "nat * nat \<Rightarrow> nat"
   2.168  where
   2.169    "term_but_no_prove (0,0) = 1"
   2.170 -  "term_but_no_prove (0, Suc b) = 0"
   2.171 -  "term_but_no_prove (Suc a, 0) = 0"
   2.172 -  "term_but_no_prove (Suc a, Suc b) = term_but_no_prove (b, a)"
   2.173 +| "term_but_no_prove (0, Suc b) = 0"
   2.174 +| "term_but_no_prove (Suc a, 0) = 0"
   2.175 +| "term_but_no_prove (Suc a, Suc b) = term_but_no_prove (b, a)"
   2.176  by pat_completeness auto
   2.177  (* termination by lexicographic_order *)
   2.178  
     3.1 --- a/src/HOL/ex/ROOT.ML	Tue Aug 05 13:31:38 2008 +0200
     3.2 +++ b/src/HOL/ex/ROOT.ML	Tue Aug 05 14:40:48 2008 +0200
     3.3 @@ -58,7 +58,8 @@
     3.4    "Classical",
     3.5    "set",
     3.6    "Meson_Test",
     3.7 -  "Code_Antiq"
     3.8 +  "Code_Antiq",
     3.9 +  "LexOrds"
    3.10  ];
    3.11  
    3.12  setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical";