more recdef (and old primrec) hunting
authorkrauss
Mon Mar 01 17:05:57 2010 +0100 (2010-03-01)
changeset 35419d78659d1723e
parent 35418 83b0f75810f0
child 35420 70395c8e8c07
more recdef (and old primrec) hunting
src/HOL/Hoare/Pointer_Examples.thy
src/HOL/Hoare/Pointers0.thy
src/HOL/Induct/Tree.thy
src/HOL/ex/ReflectionEx.thy
src/HOL/ex/ThreeDivides.thy
     1.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Mon Mar 01 16:42:45 2010 +0100
     1.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Mon Mar 01 17:05:57 2010 +0100
     1.3 @@ -222,13 +222,11 @@
     1.4  definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
     1.5  "cand P Q == if P then Q else False"
     1.6  
     1.7 -consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
     1.8 -
     1.9 -recdef merge "measure(%(xs,ys,f). size xs + size ys)"
    1.10 +fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
    1.11  "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
    1.12 -                                else y # merge(x#xs,ys,f))"
    1.13 -"merge(x#xs,[],f) = x # merge(xs,[],f)"
    1.14 -"merge([],y#ys,f) = y # merge([],ys,f)"
    1.15 +                                else y # merge(x#xs,ys,f))" |
    1.16 +"merge(x#xs,[],f) = x # merge(xs,[],f)" |
    1.17 +"merge([],y#ys,f) = y # merge([],ys,f)" |
    1.18  "merge([],[],f) = []"
    1.19  
    1.20  text{* Simplifies the proof a little: *}
     2.1 --- a/src/HOL/Hoare/Pointers0.thy	Mon Mar 01 16:42:45 2010 +0100
     2.2 +++ b/src/HOL/Hoare/Pointers0.thy	Mon Mar 01 17:05:57 2010 +0100
     2.3 @@ -320,13 +320,11 @@
     2.4  
     2.5  text"This is still a bit rough, especially the proof."
     2.6  
     2.7 -consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
     2.8 -
     2.9 -recdef merge "measure(%(xs,ys,f). size xs + size ys)"
    2.10 +fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
    2.11  "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
    2.12 -                                else y # merge(x#xs,ys,f))"
    2.13 -"merge(x#xs,[],f) = x # merge(xs,[],f)"
    2.14 -"merge([],y#ys,f) = y # merge([],ys,f)"
    2.15 +                                else y # merge(x#xs,ys,f))" |
    2.16 +"merge(x#xs,[],f) = x # merge(xs,[],f)" |
    2.17 +"merge([],y#ys,f) = y # merge([],ys,f)" |
    2.18  "merge([],[],f) = []"
    2.19  
    2.20  lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"
     3.1 --- a/src/HOL/Induct/Tree.thy	Mon Mar 01 16:42:45 2010 +0100
     3.2 +++ b/src/HOL/Induct/Tree.thy	Mon Mar 01 17:05:57 2010 +0100
     3.3 @@ -13,20 +13,20 @@
     3.4      Atom 'a
     3.5    | Branch "nat => 'a tree"
     3.6  
     3.7 -consts
     3.8 +primrec
     3.9    map_tree :: "('a => 'b) => 'a tree => 'b tree"
    3.10 -primrec
    3.11 +where
    3.12    "map_tree f (Atom a) = Atom (f a)"
    3.13 -  "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
    3.14 +| "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
    3.15  
    3.16  lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
    3.17    by (induct t) simp_all
    3.18  
    3.19 -consts
    3.20 +primrec
    3.21    exists_tree :: "('a => bool) => 'a tree => bool"
    3.22 -primrec
    3.23 +where
    3.24    "exists_tree P (Atom a) = P a"
    3.25 -  "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
    3.26 +| "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
    3.27  
    3.28  lemma exists_map:
    3.29    "(!!x. P x ==> Q (f x)) ==>
    3.30 @@ -39,23 +39,23 @@
    3.31  datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
    3.32  
    3.33  text{*Addition of ordinals*}
    3.34 -consts
    3.35 +primrec
    3.36    add :: "[brouwer,brouwer] => brouwer"
    3.37 -primrec
    3.38 +where
    3.39    "add i Zero = i"
    3.40 -  "add i (Succ j) = Succ (add i j)"
    3.41 -  "add i (Lim f) = Lim (%n. add i (f n))"
    3.42 +| "add i (Succ j) = Succ (add i j)"
    3.43 +| "add i (Lim f) = Lim (%n. add i (f n))"
    3.44  
    3.45  lemma add_assoc: "add (add i j) k = add i (add j k)"
    3.46    by (induct k) auto
    3.47  
    3.48  text{*Multiplication of ordinals*}
    3.49 -consts
    3.50 +primrec
    3.51    mult :: "[brouwer,brouwer] => brouwer"
    3.52 -primrec
    3.53 +where
    3.54    "mult i Zero = Zero"
    3.55 -  "mult i (Succ j) = add (mult i j) i"
    3.56 -  "mult i (Lim f) = Lim (%n. mult i (f n))"
    3.57 +| "mult i (Succ j) = add (mult i j) i"
    3.58 +| "mult i (Lim f) = Lim (%n. mult i (f n))"
    3.59  
    3.60  lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
    3.61    by (induct k) (auto simp add: add_assoc)
    3.62 @@ -83,7 +83,7 @@
    3.63  lemma wf_brouwer_pred: "wf brouwer_pred"
    3.64    by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
    3.65  
    3.66 -lemma wf_brouwer_order: "wf brouwer_order"
    3.67 +lemma wf_brouwer_order[simp]: "wf brouwer_order"
    3.68    by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred])
    3.69  
    3.70  lemma [simp]: "(j, Succ j) : brouwer_order"
    3.71 @@ -92,14 +92,16 @@
    3.72  lemma [simp]: "(f n, Lim f) : brouwer_order"
    3.73    by(auto simp add: brouwer_order_def brouwer_pred_def)
    3.74  
    3.75 -text{*Example of a recdef*}
    3.76 -consts
    3.77 +text{*Example of a general function*}
    3.78 +
    3.79 +function
    3.80    add2 :: "(brouwer*brouwer) => brouwer"
    3.81 -recdef add2 "inv_image brouwer_order (\<lambda> (x,y). y)"
    3.82 +where
    3.83    "add2 (i, Zero) = i"
    3.84 -  "add2 (i, (Succ j)) = Succ (add2 (i, j))"
    3.85 -  "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
    3.86 -  (hints recdef_wf: wf_brouwer_order)
    3.87 +| "add2 (i, (Succ j)) = Succ (add2 (i, j))"
    3.88 +| "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
    3.89 +by pat_completeness auto
    3.90 +termination by (relation "inv_image brouwer_order snd") auto
    3.91  
    3.92  lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
    3.93    by (induct k) auto
     4.1 --- a/src/HOL/ex/ReflectionEx.thy	Mon Mar 01 16:42:45 2010 +0100
     4.2 +++ b/src/HOL/ex/ReflectionEx.thy	Mon Mar 01 17:05:57 2010 +0100
     4.3 @@ -69,28 +69,29 @@
     4.4  oops
     4.5  
     4.6    text{* Let's perform NNF. This is a version that tends to generate disjunctions *}
     4.7 -consts fmsize :: "fm \<Rightarrow> nat"
     4.8 -primrec
     4.9 +primrec fmsize :: "fm \<Rightarrow> nat" where
    4.10    "fmsize (At n) = 1"
    4.11 -  "fmsize (NOT p) = 1 + fmsize p"
    4.12 -  "fmsize (And p q) = 1 + fmsize p + fmsize q"
    4.13 -  "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    4.14 -  "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
    4.15 -  "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
    4.16 +| "fmsize (NOT p) = 1 + fmsize p"
    4.17 +| "fmsize (And p q) = 1 + fmsize p + fmsize q"
    4.18 +| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    4.19 +| "fmsize (Imp p q) = 2 + fmsize p + fmsize q"
    4.20 +| "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q"
    4.21 +
    4.22 +lemma [measure_function]: "is_measure fmsize" ..
    4.23  
    4.24 -consts nnf :: "fm \<Rightarrow> fm"
    4.25 -recdef nnf "measure fmsize"
    4.26 +fun nnf :: "fm \<Rightarrow> fm"
    4.27 +where
    4.28    "nnf (At n) = At n"
    4.29 -  "nnf (And p q) = And (nnf p) (nnf q)"
    4.30 -  "nnf (Or p q) = Or (nnf p) (nnf q)"
    4.31 -  "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
    4.32 -  "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
    4.33 -  "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
    4.34 -  "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
    4.35 -  "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
    4.36 -  "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
    4.37 -  "nnf (NOT (NOT p)) = nnf p"
    4.38 -  "nnf (NOT p) = NOT p"
    4.39 +| "nnf (And p q) = And (nnf p) (nnf q)"
    4.40 +| "nnf (Or p q) = Or (nnf p) (nnf q)"
    4.41 +| "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
    4.42 +| "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))"
    4.43 +| "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))"
    4.44 +| "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))"
    4.45 +| "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))"
    4.46 +| "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))"
    4.47 +| "nnf (NOT (NOT p)) = nnf p"
    4.48 +| "nnf (NOT p) = NOT p"
    4.49  
    4.50    text{* The correctness theorem of nnf: it preserves the semantics of fm *}
    4.51  lemma nnf[reflection]: "Ifm (nnf p) vs = Ifm p vs"
    4.52 @@ -113,22 +114,22 @@
    4.53  datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
    4.54  
    4.55  text{* This is just technical to make recursive definitions easier. *}
    4.56 -consts num_size :: "num \<Rightarrow> nat" 
    4.57 -primrec 
    4.58 +primrec num_size :: "num \<Rightarrow> nat" 
    4.59 +where
    4.60    "num_size (C c) = 1"
    4.61 -  "num_size (Var n) = 1"
    4.62 -  "num_size (Add a b) = 1 + num_size a + num_size b"
    4.63 -  "num_size (Mul c a) = 1 + num_size a"
    4.64 -  "num_size (CN n c a) = 4 + num_size a "
    4.65 +| "num_size (Var n) = 1"
    4.66 +| "num_size (Add a b) = 1 + num_size a + num_size b"
    4.67 +| "num_size (Mul c a) = 1 + num_size a"
    4.68 +| "num_size (CN n c a) = 4 + num_size a "
    4.69  
    4.70    text{* The semantics of num *}
    4.71 -consts Inum:: "num \<Rightarrow> nat list \<Rightarrow> nat"
    4.72 -primrec 
    4.73 +primrec Inum:: "num \<Rightarrow> nat list \<Rightarrow> nat"
    4.74 +where
    4.75    Inum_C  : "Inum (C i) vs = i"
    4.76 -  Inum_Var: "Inum (Var n) vs = vs!n"
    4.77 -  Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs "
    4.78 -  Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs "
    4.79 -  Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs "
    4.80 +| Inum_Var: "Inum (Var n) vs = vs!n"
    4.81 +| Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs "
    4.82 +| Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs "
    4.83 +| Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs "
    4.84  
    4.85  
    4.86    text{* Let's reify some nat expressions \dots *}
    4.87 @@ -168,39 +169,41 @@
    4.88    apply (reify Inum_eqs' ("1 * (2*x + (y::nat) + 0 + 1)"))
    4.89  oops
    4.90  text{* Okay, let's try reflection. Some simplifications on num follow. You can skim until the main theorem @{text linum} *}
    4.91 -consts lin_add :: "num \<times> num \<Rightarrow> num"
    4.92 -recdef lin_add "measure (\<lambda>(x,y). ((size x) + (size y)))"
    4.93 -  "lin_add (CN n1 c1 r1,CN n2 c2 r2) =
    4.94 +fun lin_add :: "num \<Rightarrow> num \<Rightarrow> num"
    4.95 +where
    4.96 +  "lin_add (CN n1 c1 r1) (CN n2 c2 r2) =
    4.97    (if n1=n2 then 
    4.98    (let c = c1 + c2
    4.99 -  in (if c=0 then lin_add(r1,r2) else CN n1 c (lin_add (r1,r2))))
   4.100 -  else if n1 \<le> n2 then (CN n1 c1 (lin_add (r1,CN n2 c2 r2))) 
   4.101 -  else (CN n2 c2 (lin_add (CN n1 c1 r1,r2))))"
   4.102 -  "lin_add (CN n1 c1 r1,t) = CN n1 c1 (lin_add (r1, t))"  
   4.103 -  "lin_add (t,CN n2 c2 r2) = CN n2 c2 (lin_add (t,r2))" 
   4.104 -  "lin_add (C b1, C b2) = C (b1+b2)"
   4.105 -  "lin_add (a,b) = Add a b"
   4.106 -lemma lin_add: "Inum (lin_add (t,s)) bs = Inum (Add t s) bs"
   4.107 +  in (if c=0 then lin_add r1 r2 else CN n1 c (lin_add r1 r2)))
   4.108 +  else if n1 \<le> n2 then (CN n1 c1 (lin_add r1 (CN n2 c2 r2))) 
   4.109 +  else (CN n2 c2 (lin_add (CN n1 c1 r1) r2)))"
   4.110 +| "lin_add (CN n1 c1 r1) t = CN n1 c1 (lin_add r1 t)"  
   4.111 +| "lin_add t (CN n2 c2 r2) = CN n2 c2 (lin_add t r2)" 
   4.112 +| "lin_add (C b1) (C b2) = C (b1+b2)"
   4.113 +| "lin_add a b = Add a b"
   4.114 +lemma lin_add: "Inum (lin_add t s) bs = Inum (Add t s) bs"
   4.115  apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
   4.116  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
   4.117  by (case_tac "n1 = n2", simp_all add: algebra_simps)
   4.118  
   4.119 -consts lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
   4.120 -recdef lin_mul "measure size "
   4.121 -  "lin_mul (C j) = (\<lambda> i. C (i*j))"
   4.122 -  "lin_mul (CN n c a) = (\<lambda> i. if i=0 then (C 0) else CN n (i*c) (lin_mul a i))"
   4.123 -  "lin_mul t = (\<lambda> i. Mul i t)"
   4.124 +fun lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
   4.125 +where
   4.126 +  "lin_mul (C j) i = C (i*j)"
   4.127 +| "lin_mul (CN n c a) i = (if i=0 then (C 0) else CN n (i*c) (lin_mul a i))"
   4.128 +| "lin_mul t i = (Mul i t)"
   4.129  
   4.130  lemma lin_mul: "Inum (lin_mul t i) bs = Inum (Mul i t) bs"
   4.131 -by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: algebra_simps)
   4.132 +by (induct t i rule: lin_mul.induct, auto simp add: algebra_simps)
   4.133  
   4.134 -consts linum:: "num \<Rightarrow> num"
   4.135 -recdef linum "measure num_size"
   4.136 +lemma [measure_function]: "is_measure num_size" ..
   4.137 +
   4.138 +fun linum:: "num \<Rightarrow> num"
   4.139 +where
   4.140    "linum (C b) = C b"
   4.141 -  "linum (Var n) = CN n 1 (C 0)"
   4.142 -  "linum (Add t s) = lin_add (linum t, linum s)"
   4.143 -  "linum (Mul c t) = lin_mul (linum t) c"
   4.144 -  "linum (CN n c t) = lin_add (linum (Mul c (Var n)),linum t)"
   4.145 +| "linum (Var n) = CN n 1 (C 0)"
   4.146 +| "linum (Add t s) = lin_add (linum t) (linum s)"
   4.147 +| "linum (Mul c t) = lin_mul (linum t) c"
   4.148 +| "linum (CN n c t) = lin_add (linum (Mul c (Var n))) (linum t)"
   4.149  
   4.150  lemma linum[reflection] : "Inum (linum t) bs = Inum t bs"
   4.151  by (induct t rule: linum.induct, simp_all add: lin_mul lin_add)
   4.152 @@ -214,30 +217,32 @@
   4.153  
   4.154  datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
   4.155    Conj aform aform | Disj aform aform | NEG aform | T | F
   4.156 -consts linaformsize:: "aform \<Rightarrow> nat"
   4.157 -recdef linaformsize "measure size"
   4.158 +
   4.159 +primrec linaformsize:: "aform \<Rightarrow> nat"
   4.160 +where
   4.161    "linaformsize T = 1"
   4.162 -  "linaformsize F = 1"
   4.163 -  "linaformsize (Lt a b) = 1"
   4.164 -  "linaformsize (Ge a b) = 1"
   4.165 -  "linaformsize (Eq a b) = 1"
   4.166 -  "linaformsize (NEq a b) = 1"
   4.167 -  "linaformsize (NEG p) = 2 + linaformsize p"
   4.168 -  "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
   4.169 -  "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
   4.170 +| "linaformsize F = 1"
   4.171 +| "linaformsize (Lt a b) = 1"
   4.172 +| "linaformsize (Ge a b) = 1"
   4.173 +| "linaformsize (Eq a b) = 1"
   4.174 +| "linaformsize (NEq a b) = 1"
   4.175 +| "linaformsize (NEG p) = 2 + linaformsize p"
   4.176 +| "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q"
   4.177 +| "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
   4.178  
   4.179 +lemma [measure_function]: "is_measure linaformsize" ..
   4.180  
   4.181 -consts is_aform :: "aform => nat list => bool"
   4.182 -primrec
   4.183 +primrec is_aform :: "aform => nat list => bool"
   4.184 +where
   4.185    "is_aform T vs = True"
   4.186 -  "is_aform F vs = False"
   4.187 -  "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
   4.188 -  "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
   4.189 -  "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
   4.190 -  "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
   4.191 -  "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
   4.192 -  "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
   4.193 -  "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
   4.194 +| "is_aform F vs = False"
   4.195 +| "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
   4.196 +| "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
   4.197 +| "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
   4.198 +| "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
   4.199 +| "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
   4.200 +| "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
   4.201 +| "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
   4.202  
   4.203    text{* Let's reify and do reflection *}
   4.204  lemma "(3::nat)*x + t < 0 \<and> (2 * x + y \<noteq> 17)"
   4.205 @@ -250,24 +255,25 @@
   4.206  oops
   4.207  
   4.208    text{* For reflection we now define a simple transformation on aform: NNF + linum on atoms *}
   4.209 -consts linaform:: "aform \<Rightarrow> aform"
   4.210 -recdef linaform "measure linaformsize"
   4.211 +
   4.212 +fun linaform:: "aform \<Rightarrow> aform"
   4.213 +where
   4.214    "linaform (Lt s t) = Lt (linum s) (linum t)"
   4.215 -  "linaform (Eq s t) = Eq (linum s) (linum t)"
   4.216 -  "linaform (Ge s t) = Ge (linum s) (linum t)"
   4.217 -  "linaform (NEq s t) = NEq (linum s) (linum t)"
   4.218 -  "linaform (Conj p q) = Conj (linaform p) (linaform q)"
   4.219 -  "linaform (Disj p q) = Disj (linaform p) (linaform q)"
   4.220 -  "linaform (NEG T) = F"
   4.221 -  "linaform (NEG F) = T"
   4.222 -  "linaform (NEG (Lt a b)) = Ge a b"
   4.223 -  "linaform (NEG (Ge a b)) = Lt a b"
   4.224 -  "linaform (NEG (Eq a b)) = NEq a b"
   4.225 -  "linaform (NEG (NEq a b)) = Eq a b"
   4.226 -  "linaform (NEG (NEG p)) = linaform p"
   4.227 -  "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
   4.228 -  "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
   4.229 -  "linaform p = p"
   4.230 +| "linaform (Eq s t) = Eq (linum s) (linum t)"
   4.231 +| "linaform (Ge s t) = Ge (linum s) (linum t)"
   4.232 +| "linaform (NEq s t) = NEq (linum s) (linum t)"
   4.233 +| "linaform (Conj p q) = Conj (linaform p) (linaform q)"
   4.234 +| "linaform (Disj p q) = Disj (linaform p) (linaform q)"
   4.235 +| "linaform (NEG T) = F"
   4.236 +| "linaform (NEG F) = T"
   4.237 +| "linaform (NEG (Lt a b)) = Ge a b"
   4.238 +| "linaform (NEG (Ge a b)) = Lt a b"
   4.239 +| "linaform (NEG (Eq a b)) = NEq a b"
   4.240 +| "linaform (NEG (NEq a b)) = Eq a b"
   4.241 +| "linaform (NEG (NEG p)) = linaform p"
   4.242 +| "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))"
   4.243 +| "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
   4.244 +| "linaform p = p"
   4.245  
   4.246  lemma linaform: "is_aform (linaform p) vs = is_aform p vs"
   4.247    by (induct p rule: linaform.induct) (auto simp add: linum)
   4.248 @@ -283,11 +289,11 @@
   4.249  
   4.250  text{* We now give an example where Interpretaions have 0 or more than only one envornement of different types and show that automatic reification also deals with binding *}
   4.251  datatype rb = BC bool| BAnd rb rb | BOr rb rb
   4.252 -consts Irb :: "rb \<Rightarrow> bool"
   4.253 -primrec
   4.254 +primrec Irb :: "rb \<Rightarrow> bool"
   4.255 +where
   4.256    "Irb (BC p) = p"
   4.257 -  "Irb (BAnd s t) = (Irb s \<and> Irb t)"
   4.258 -  "Irb (BOr s t) = (Irb s \<or> Irb t)"
   4.259 +| "Irb (BAnd s t) = (Irb s \<and> Irb t)"
   4.260 +| "Irb (BOr s t) = (Irb s \<or> Irb t)"
   4.261  
   4.262  lemma "A \<and> (B \<or> D \<and> B) \<and> A \<and> (B \<or> D \<and> B) \<or> A \<and> (B \<or> D \<and> B) \<or> A \<and> (B \<or> D \<and> B)"
   4.263  apply (reify Irb.simps)
   4.264 @@ -295,14 +301,14 @@
   4.265  
   4.266  
   4.267  datatype rint = IC int| IVar nat | IAdd rint rint | IMult rint rint | INeg rint | ISub rint rint
   4.268 -consts Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
   4.269 -primrec
   4.270 -Irint_Var: "Irint (IVar n) vs = vs!n"
   4.271 -Irint_Neg: "Irint (INeg t) vs = - Irint t vs"
   4.272 -Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs"
   4.273 -Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs"
   4.274 -Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs"
   4.275 -Irint_C: "Irint (IC i) vs = i"
   4.276 +primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
   4.277 +where
   4.278 +  Irint_Var: "Irint (IVar n) vs = vs!n"
   4.279 +| Irint_Neg: "Irint (INeg t) vs = - Irint t vs"
   4.280 +| Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs"
   4.281 +| Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs"
   4.282 +| Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs"
   4.283 +| Irint_C: "Irint (IC i) vs = i"
   4.284  lemma Irint_C0: "Irint (IC 0) vs = 0"
   4.285    by simp
   4.286  lemma Irint_C1: "Irint (IC 1) vs = 1"
   4.287 @@ -314,12 +320,12 @@
   4.288    apply (reify Irint_simps ("(3::int) * x + y*y - 9 + (- z)"))
   4.289    oops
   4.290  datatype rlist = LVar nat| LEmpty| LCons rint rlist | LAppend rlist rlist
   4.291 -consts Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> (int list)"
   4.292 -primrec
   4.293 +primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> (int list)"
   4.294 +where
   4.295    "Irlist (LEmpty) is vs = []"
   4.296 -  "Irlist (LVar n) is vs = vs!n"
   4.297 -  "Irlist (LCons i t) is vs = ((Irint i is)#(Irlist t is vs))"
   4.298 -  "Irlist (LAppend s t) is vs = (Irlist s is vs) @ (Irlist t is vs)"
   4.299 +| "Irlist (LVar n) is vs = vs!n"
   4.300 +| "Irlist (LCons i t) is vs = ((Irint i is)#(Irlist t is vs))"
   4.301 +| "Irlist (LAppend s t) is vs = (Irlist s is vs) @ (Irlist t is vs)"
   4.302  lemma "[(1::int)] = []"
   4.303    apply (reify Irlist.simps Irint_simps ("[1]:: int list"))
   4.304    oops
   4.305 @@ -329,16 +335,16 @@
   4.306    oops
   4.307  
   4.308  datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat | NNeg rnat | NSub rnat rnat | Nlgth rlist
   4.309 -consts Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> nat"
   4.310 -primrec
   4.311 -Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)"
   4.312 -Irnat_Var: "Irnat (NVar n) is ls vs = vs!n"
   4.313 -Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
   4.314 -Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
   4.315 -Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
   4.316 -Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"
   4.317 -Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)"
   4.318 -Irnat_C: "Irnat (NC i) is ls vs = i"
   4.319 +primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> nat"
   4.320 +where
   4.321 +  Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)"
   4.322 +| Irnat_Var: "Irnat (NVar n) is ls vs = vs!n"
   4.323 +| Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
   4.324 +| Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
   4.325 +| Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
   4.326 +| Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"
   4.327 +| Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)"
   4.328 +| Irnat_C: "Irnat (NC i) is ls vs = i"
   4.329  lemma Irnat_C0: "Irnat (NC 0) is ls vs = 0"
   4.330  by simp
   4.331  lemma Irnat_C1: "Irnat (NC 1) is ls vs = 1"
   4.332 @@ -356,26 +362,26 @@
   4.333    | RNEX rifm | RIEX rifm| RLEX rifm | RNALL rifm | RIALL rifm| RLALL rifm
   4.334    | RBEX rifm | RBALL rifm
   4.335  
   4.336 -consts Irifm :: "rifm \<Rightarrow> bool list \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> bool"
   4.337 -primrec
   4.338 -"Irifm RT ps is ls ns = True"
   4.339 -"Irifm RF ps is ls ns = False"
   4.340 -"Irifm (RVar n) ps is ls ns = ps!n"
   4.341 -"Irifm (RNLT s t) ps is ls ns = (Irnat s is ls ns < Irnat t is ls ns)"
   4.342 -"Irifm (RNILT s t) ps is ls ns = (int (Irnat s is ls ns) < Irint t is)"
   4.343 -"Irifm (RNEQ s t) ps is ls ns = (Irnat s is ls ns = Irnat t is ls ns)"
   4.344 -"Irifm (RAnd p q) ps is ls ns = (Irifm p ps is ls ns \<and> Irifm q ps is ls ns)"
   4.345 -"Irifm (ROr p q) ps is ls ns = (Irifm p ps is ls ns \<or> Irifm q ps is ls ns)"
   4.346 -"Irifm (RImp p q) ps is ls ns = (Irifm p ps is ls ns \<longrightarrow> Irifm q ps is ls ns)"
   4.347 -"Irifm (RIff p q) ps is ls ns = (Irifm p ps is ls ns = Irifm q ps is ls ns)"
   4.348 -"Irifm (RNEX p) ps is ls ns =  (\<exists>x. Irifm p ps is ls (x#ns))"
   4.349 -"Irifm (RIEX p) ps is ls ns =  (\<exists>x. Irifm p ps (x#is) ls ns)"
   4.350 -"Irifm (RLEX p) ps is ls ns =  (\<exists>x. Irifm p ps is (x#ls) ns)"
   4.351 -"Irifm (RBEX p) ps is ls ns =  (\<exists>x. Irifm p (x#ps) is ls ns)"
   4.352 -"Irifm (RNALL p) ps is ls ns = (\<forall>x. Irifm p ps is ls (x#ns))"
   4.353 -"Irifm (RIALL p) ps is ls ns = (\<forall>x. Irifm p ps (x#is) ls ns)"
   4.354 -"Irifm (RLALL p) ps is ls ns = (\<forall>x. Irifm p ps is (x#ls) ns)"
   4.355 -"Irifm (RBALL p) ps is ls ns = (\<forall>x. Irifm p (x#ps) is ls ns)"
   4.356 +primrec Irifm :: "rifm \<Rightarrow> bool list \<Rightarrow> int list \<Rightarrow> (int list) list \<Rightarrow> nat list \<Rightarrow> bool"
   4.357 +where
   4.358 +  "Irifm RT ps is ls ns = True"
   4.359 +| "Irifm RF ps is ls ns = False"
   4.360 +| "Irifm (RVar n) ps is ls ns = ps!n"
   4.361 +| "Irifm (RNLT s t) ps is ls ns = (Irnat s is ls ns < Irnat t is ls ns)"
   4.362 +| "Irifm (RNILT s t) ps is ls ns = (int (Irnat s is ls ns) < Irint t is)"
   4.363 +| "Irifm (RNEQ s t) ps is ls ns = (Irnat s is ls ns = Irnat t is ls ns)"
   4.364 +| "Irifm (RAnd p q) ps is ls ns = (Irifm p ps is ls ns \<and> Irifm q ps is ls ns)"
   4.365 +| "Irifm (ROr p q) ps is ls ns = (Irifm p ps is ls ns \<or> Irifm q ps is ls ns)"
   4.366 +| "Irifm (RImp p q) ps is ls ns = (Irifm p ps is ls ns \<longrightarrow> Irifm q ps is ls ns)"
   4.367 +| "Irifm (RIff p q) ps is ls ns = (Irifm p ps is ls ns = Irifm q ps is ls ns)"
   4.368 +| "Irifm (RNEX p) ps is ls ns =  (\<exists>x. Irifm p ps is ls (x#ns))"
   4.369 +| "Irifm (RIEX p) ps is ls ns =  (\<exists>x. Irifm p ps (x#is) ls ns)"
   4.370 +| "Irifm (RLEX p) ps is ls ns =  (\<exists>x. Irifm p ps is (x#ls) ns)"
   4.371 +| "Irifm (RBEX p) ps is ls ns =  (\<exists>x. Irifm p (x#ps) is ls ns)"
   4.372 +| "Irifm (RNALL p) ps is ls ns = (\<forall>x. Irifm p ps is ls (x#ns))"
   4.373 +| "Irifm (RIALL p) ps is ls ns = (\<forall>x. Irifm p ps (x#is) ls ns)"
   4.374 +| "Irifm (RLALL p) ps is ls ns = (\<forall>x. Irifm p ps is (x#ls) ns)"
   4.375 +| "Irifm (RBALL p) ps is ls ns = (\<forall>x. Irifm p (x#ps) is ls ns)"
   4.376  
   4.377  lemma " \<forall>x. \<exists>n. ((Suc n) * length (([(3::int) * x + (f t)*y - 9 + (- z)] @ []) @ xs) = length xs) \<and> m < 5*n - length (xs @ [2,3,4,x*z + 8 - y]) \<longrightarrow> (\<exists>p. \<forall>q. p \<and> q \<longrightarrow> r)"
   4.378    apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
   4.379 @@ -385,28 +391,28 @@
   4.380  (* An example for equations containing type variables *)
   4.381  datatype prod = Zero | One | Var nat | Mul prod prod 
   4.382    | Pw prod nat | PNM nat nat prod
   4.383 -consts Iprod :: " prod \<Rightarrow> ('a::{linordered_idom}) list \<Rightarrow>'a" 
   4.384 -primrec
   4.385 +primrec Iprod :: " prod \<Rightarrow> ('a::{linordered_idom}) list \<Rightarrow>'a" 
   4.386 +where
   4.387    "Iprod Zero vs = 0"
   4.388 -  "Iprod One vs = 1"
   4.389 -  "Iprod (Var n) vs = vs!n"
   4.390 -  "Iprod (Mul a b) vs = (Iprod a vs * Iprod b vs)"
   4.391 -  "Iprod (Pw a n) vs = ((Iprod a vs) ^ n)"
   4.392 -  "Iprod (PNM n k t) vs = (vs ! n)^k * Iprod t vs"
   4.393 +| "Iprod One vs = 1"
   4.394 +| "Iprod (Var n) vs = vs!n"
   4.395 +| "Iprod (Mul a b) vs = (Iprod a vs * Iprod b vs)"
   4.396 +| "Iprod (Pw a n) vs = ((Iprod a vs) ^ n)"
   4.397 +| "Iprod (PNM n k t) vs = (vs ! n)^k * Iprod t vs"
   4.398  consts prodmul:: "prod \<times> prod \<Rightarrow> prod"
   4.399  datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
   4.400    | Or sgn sgn | And sgn sgn
   4.401  
   4.402 -consts Isgn :: " sgn \<Rightarrow> ('a::{linordered_idom}) list \<Rightarrow>bool"
   4.403 -primrec 
   4.404 +primrec Isgn :: " sgn \<Rightarrow> ('a::{linordered_idom}) list \<Rightarrow>bool"
   4.405 +where 
   4.406    "Isgn Tr vs = True"
   4.407 -  "Isgn F vs = False"
   4.408 -  "Isgn (ZeroEq t) vs = (Iprod t vs = 0)"
   4.409 -  "Isgn (NZeroEq t) vs = (Iprod t vs \<noteq> 0)"
   4.410 -  "Isgn (Pos t) vs = (Iprod t vs > 0)"
   4.411 -  "Isgn (Neg t) vs = (Iprod t vs < 0)"
   4.412 -  "Isgn (And p q) vs = (Isgn p vs \<and> Isgn q vs)"
   4.413 -  "Isgn (Or p q) vs = (Isgn p vs \<or> Isgn q vs)"
   4.414 +| "Isgn F vs = False"
   4.415 +| "Isgn (ZeroEq t) vs = (Iprod t vs = 0)"
   4.416 +| "Isgn (NZeroEq t) vs = (Iprod t vs \<noteq> 0)"
   4.417 +| "Isgn (Pos t) vs = (Iprod t vs > 0)"
   4.418 +| "Isgn (Neg t) vs = (Iprod t vs < 0)"
   4.419 +| "Isgn (And p q) vs = (Isgn p vs \<and> Isgn q vs)"
   4.420 +| "Isgn (Or p q) vs = (Isgn p vs \<or> Isgn q vs)"
   4.421  
   4.422  lemmas eqs = Isgn.simps Iprod.simps
   4.423  
     5.1 --- a/src/HOL/ex/ThreeDivides.thy	Mon Mar 01 16:42:45 2010 +0100
     5.2 +++ b/src/HOL/ex/ThreeDivides.thy	Mon Mar 01 17:05:57 2010 +0100
     5.3 @@ -149,10 +149,10 @@
     5.4  The function @{text "nlen"} returns the number of digits in a natural
     5.5  number n. *}
     5.6  
     5.7 -consts nlen :: "nat \<Rightarrow> nat"
     5.8 -recdef nlen "measure id"
     5.9 +fun nlen :: "nat \<Rightarrow> nat"
    5.10 +where
    5.11    "nlen 0 = 0"
    5.12 -  "nlen x = 1 + nlen (x div 10)"
    5.13 +| "nlen x = 1 + nlen (x div 10)"
    5.14  
    5.15  text {* The function @{text "sumdig"} returns the sum of all digits in
    5.16  some number n. *}