src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 41821 c118ae98dfbf
parent 41816 7a55699805dc
child 41822 27afef7d6c37
     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.57  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)
    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)"
    1.78 -  "simptm (Add t s) = tmadd (simptm t,simptm s)"
    1.79 -  "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
    1.80 -  "simptm (Mul i t) = (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
    1.81 -  "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))"
    1.82 +| "simptm (Bound n) = CNP n 1\<^sub>p (CP 0\<^sub>p)"
    1.83 +| "simptm (Neg t) = tmneg (simptm t)"
    1.84 +| "simptm (Add t s) = tmadd (simptm t,simptm s)"
    1.85 +| "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
    1.86 +| "simptm (Mul i t) = (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
    1.87 +| "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))"
    1.88  
    1.89  lemma polynate_stupid: 
    1.90    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"