# HG changeset patch
# User krauss
# Date 1298454537 -3600
# Node ID c118ae98dfbf8132b1ec0ee0873177de867afc77
# Parent  7fe10daa43330e71f5d6852efa34ae2efacad68f
recdef -> fun

diff -r 7fe10daa4333 -r c118ae98dfbf src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Feb 22 21:54:56 2011 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 23 10:48:57 2011 +0100
@@ -85,27 +85,23 @@
   using nb le bnd
   by (induct t rule: tm.induct , auto)
 
-consts 
-  incrtm0:: "tm \<Rightarrow> tm"
-  decrtm0:: "tm \<Rightarrow> tm" 
-
-recdef decrtm0 "measure size"
+fun decrtm0:: "tm \<Rightarrow> tm" where
   "decrtm0 (Bound n) = Bound (n - 1)"
-  "decrtm0 (Neg a) = Neg (decrtm0 a)"
-  "decrtm0 (Add a b) = Add (decrtm0 a) (decrtm0 b)"
-  "decrtm0 (Sub a b) = Sub (decrtm0 a) (decrtm0 b)"
-  "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
-  "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
-  "decrtm0 a = a"
+| "decrtm0 (Neg a) = Neg (decrtm0 a)"
+| "decrtm0 (Add a b) = Add (decrtm0 a) (decrtm0 b)"
+| "decrtm0 (Sub a b) = Sub (decrtm0 a) (decrtm0 b)"
+| "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
+| "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
+| "decrtm0 a = a"
 
-recdef incrtm0 "measure size"
+fun incrtm0:: "tm \<Rightarrow> tm" where
   "incrtm0 (Bound n) = Bound (n + 1)"
-  "incrtm0 (Neg a) = Neg (incrtm0 a)"
-  "incrtm0 (Add a b) = Add (incrtm0 a) (incrtm0 b)"
-  "incrtm0 (Sub a b) = Sub (incrtm0 a) (incrtm0 b)"
-  "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
-  "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
-  "incrtm0 a = a"
+| "incrtm0 (Neg a) = Neg (incrtm0 a)"
+| "incrtm0 (Add a b) = Add (incrtm0 a) (incrtm0 b)"
+| "incrtm0 (Sub a b) = Sub (incrtm0 a) (incrtm0 b)"
+| "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
+| "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
+| "incrtm0 a = a"
 
 lemma decrtm0: assumes nb: "tmbound0 t"
   shows "Itm vs (x#bs) t = Itm vs bs (decrtm0 t)"
@@ -213,9 +209,7 @@
   (* Simplification *)
 
 consts
-  simptm:: "tm \<Rightarrow> tm"
   tmadd:: "tm \<times> tm \<Rightarrow> tm"
-  tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm"
 recdef tmadd "measure (\<lambda> (t,s). size t + size s)"
   "tmadd (CNP n1 c1 r1,CNP n2 c2 r2) =
   (if n1=n2 then 
@@ -245,10 +239,10 @@
 
 lemma tmadd_allpolys_npoly[simp]: "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd(t,s))" by (induct t s rule: tmadd.induct, simp_all add: Let_def polyadd_norm)
 
-recdef tmmul "measure size"
+fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm" where
   "tmmul (CP j) = (\<lambda> i. CP (i *\<^sub>p j))"
-  "tmmul (CNP n c a) = (\<lambda> i. CNP n (i *\<^sub>p c) (tmmul a i))"
-  "tmmul t = (\<lambda> i. Mul i t)"
+| "tmmul (CNP n c a) = (\<lambda> i. CNP n (i *\<^sub>p c) (tmmul a i))"
+| "tmmul t = (\<lambda> i. Mul i t)"
 
 lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)"
 by (induct t arbitrary: i rule: tmmul.induct, simp_all add: field_simps)
@@ -306,14 +300,14 @@
   shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)" 
   unfolding tmsub_def by (simp add: isnpoly_def)
 
-recdef simptm "measure size"
+fun simptm:: "tm \<Rightarrow> tm" where
   "simptm (CP j) = CP (polynate j)"
-  "simptm (Bound n) = CNP n 1\<^sub>p (CP 0\<^sub>p)"
-  "simptm (Neg t) = tmneg (simptm t)"
-  "simptm (Add t s) = tmadd (simptm t,simptm s)"
-  "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
-  "simptm (Mul i t) = (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
-  "simptm (CNP n c t) = (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"
+| "simptm (Bound n) = CNP n 1\<^sub>p (CP 0\<^sub>p)"
+| "simptm (Neg t) = tmneg (simptm t)"
+| "simptm (Add t s) = tmadd (simptm t,simptm s)"
+| "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
+| "simptm (Mul i t) = (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
+| "simptm (CNP n c t) = (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"
 
 lemma polynate_stupid: 
   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"