author krauss Wed Feb 23 10:48:57 2011 +0100 (2011-02-23) changeset 41821 c118ae98dfbf parent 41820 7fe10daa4333 child 41822 27afef7d6c37 child 41824 1b447261865e
recdef -> fun
```     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Feb 22 21:54:56 2011 +0100
1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 23 10:48:57 2011 +0100
1.3 @@ -85,27 +85,23 @@
1.4    using nb le bnd
1.5    by (induct t rule: tm.induct , auto)
1.6
1.7 -consts
1.8 -  incrtm0:: "tm \<Rightarrow> tm"
1.9 -  decrtm0:: "tm \<Rightarrow> tm"
1.10 -
1.11 -recdef decrtm0 "measure size"
1.12 +fun decrtm0:: "tm \<Rightarrow> tm" where
1.13    "decrtm0 (Bound n) = Bound (n - 1)"
1.14 -  "decrtm0 (Neg a) = Neg (decrtm0 a)"
1.15 -  "decrtm0 (Add a b) = Add (decrtm0 a) (decrtm0 b)"
1.16 -  "decrtm0 (Sub a b) = Sub (decrtm0 a) (decrtm0 b)"
1.17 -  "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
1.18 -  "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
1.19 -  "decrtm0 a = a"
1.20 +| "decrtm0 (Neg a) = Neg (decrtm0 a)"
1.21 +| "decrtm0 (Add a b) = Add (decrtm0 a) (decrtm0 b)"
1.22 +| "decrtm0 (Sub a b) = Sub (decrtm0 a) (decrtm0 b)"
1.23 +| "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
1.24 +| "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
1.25 +| "decrtm0 a = a"
1.26
1.27 -recdef incrtm0 "measure size"
1.28 +fun incrtm0:: "tm \<Rightarrow> tm" where
1.29    "incrtm0 (Bound n) = Bound (n + 1)"
1.30 -  "incrtm0 (Neg a) = Neg (incrtm0 a)"
1.31 -  "incrtm0 (Add a b) = Add (incrtm0 a) (incrtm0 b)"
1.32 -  "incrtm0 (Sub a b) = Sub (incrtm0 a) (incrtm0 b)"
1.33 -  "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
1.34 -  "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
1.35 -  "incrtm0 a = a"
1.36 +| "incrtm0 (Neg a) = Neg (incrtm0 a)"
1.37 +| "incrtm0 (Add a b) = Add (incrtm0 a) (incrtm0 b)"
1.38 +| "incrtm0 (Sub a b) = Sub (incrtm0 a) (incrtm0 b)"
1.39 +| "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
1.40 +| "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
1.41 +| "incrtm0 a = a"
1.42
1.43  lemma decrtm0: assumes nb: "tmbound0 t"
1.44    shows "Itm vs (x#bs) t = Itm vs bs (decrtm0 t)"
1.45 @@ -213,9 +209,7 @@
1.46    (* Simplification *)
1.47
1.48  consts
1.49 -  simptm:: "tm \<Rightarrow> tm"
1.50    tmadd:: "tm \<times> tm \<Rightarrow> tm"
1.51 -  tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm"
1.52  recdef tmadd "measure (\<lambda> (t,s). size t + size s)"
1.53    "tmadd (CNP n1 c1 r1,CNP n2 c2 r2) =
1.54    (if n1=n2 then
1.55 @@ -245,10 +239,10 @@
1.56
1.58
1.59 -recdef tmmul "measure size"
1.60 +fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm" where
1.61    "tmmul (CP j) = (\<lambda> i. CP (i *\<^sub>p j))"
1.62 -  "tmmul (CNP n c a) = (\<lambda> i. CNP n (i *\<^sub>p c) (tmmul a i))"
1.63 -  "tmmul t = (\<lambda> i. Mul i t)"
1.64 +| "tmmul (CNP n c a) = (\<lambda> i. CNP n (i *\<^sub>p c) (tmmul a i))"
1.65 +| "tmmul t = (\<lambda> i. Mul i t)"
1.66
1.67  lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)"
1.68  by (induct t arbitrary: i rule: tmmul.induct, simp_all add: field_simps)
1.69 @@ -306,14 +300,14 @@
1.70    shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
1.71    unfolding tmsub_def by (simp add: isnpoly_def)
1.72
1.73 -recdef simptm "measure size"
1.74 +fun simptm:: "tm \<Rightarrow> tm" where
1.75    "simptm (CP j) = CP (polynate j)"
1.76 -  "simptm (Bound n) = CNP n 1\<^sub>p (CP 0\<^sub>p)"
1.77 -  "simptm (Neg t) = tmneg (simptm t)"