author krauss Mon Mar 01 17:05:57 2010 +0100 (2010-03-01) changeset 35419 d78659d1723e parent 35418 83b0f75810f0 child 35420 70395c8e8c07
more recdef (and old primrec) hunting
 src/HOL/Hoare/Pointer_Examples.thy file | annotate | diff | revisions src/HOL/Hoare/Pointers0.thy file | annotate | diff | revisions src/HOL/Induct/Tree.thy file | annotate | diff | revisions src/HOL/ex/ReflectionEx.thy file | annotate | diff | revisions src/HOL/ex/ThreeDivides.thy file | annotate | diff | revisions
```     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.34 -consts
3.35 +primrec
3.36    add :: "[brouwer,brouwer] => brouwer"
3.37 -primrec
3.38 +where
3.39    "add i Zero = i"
3.41 -  "add i (Lim f) = Lim (%n. add i (f n))"
3.43 +| "add i (Lim f) = Lim (%n. add i (f n))"
3.44
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.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.85 -  "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
3.86 -  (hints recdef_wf: wf_brouwer_order)
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.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.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.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.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 (":: 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. *}
```
{"ft_lang_label":"__label__en","ft_lang_prob":0.51850903,"math_prob":0.9967536,"size":27314,"snap":"2019-51-2020-05","text_gpt3_token_len":11710,"char_repetition_ratio":0.19271329,"word_repetition_ratio":0.3596587,"special_character_ratio":0.49337336,"punctuation_ratio":0.15539612,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9972328,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-01-21T12:35:47Z\",\"WARC-Record-ID\":\"<urn:uuid:8036743f-1fca-4f56-8290-58135b32cfc7>\",\"Content-Length\":\"84706\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:4da82c32-f595-449c-9d75-1d455e1213f8>\",\"WARC-Concurrent-To\":\"<urn:uuid:67f7940c-6ac9-44ea-8894-f7d28b86ad12>\",\"WARC-IP-Address\":\"131.159.46.82\",\"WARC-Target-URI\":\"https://isabelle.in.tum.de/repos/isabelle/rev/d78659d1723e\",\"WARC-Payload-Digest\":\"sha1:ATPPJLZBMC3NGXWMQWJUAMFUUR6RGK2J\",\"WARC-Block-Digest\":\"sha1:PE4DE2TMDD5PRU7O7HYU4UFFRW7YHLYW\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-05/CC-MAIN-2020-05_segments_1579250603761.28_warc_CC-MAIN-20200121103642-20200121132642-00011.warc.gz\"}"}