src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
 changeset 41823 81d64ec48427 parent 41822 27afef7d6c37 child 41838 c845adaecf98
```--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 23 11:15:06 2011 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 23 11:16:56 2011 +0100
@@ -2475,16 +2475,6 @@
lemma filter_length: "length (List.filter P xs) < Suc (length xs)"
apply (induct xs, auto) done

-consts remdps:: "'a list \<Rightarrow> 'a list"
-
-recdef remdps "measure size"
-  "remdps [] = []"
-  "remdps (x#xs) = (x#(remdps (List.filter (\<lambda> y. y \<noteq> x) xs)))"
-
-lemma remdps_set[simp]: "set (remdps xs) = set xs"
-  by (induct xs rule: remdps.induct, auto)
-
lemma simpfm_lin:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)
@@ -2492,7 +2482,7 @@
definition
"ferrack p \<equiv> let q = simpfm p ; mp = minusinf q ; pp = plusinf q
in if (mp = T \<or> pp = T) then T
-     else (let U = alluopairs (remdps (uset  q))
+     else (let U = alluopairs (remdups (uset  q))
in decr0 (disj mp (disj pp (evaldjf (simpfm o (msubst q)) U ))))"

lemma ferrack:
@@ -2504,7 +2494,7 @@
let ?N = "\<lambda> t. Ipoly vs t"
let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
let ?q = "simpfm p"
-  let ?U = "remdps(uset ?q)"
+  let ?U = "remdups(uset ?q)"
let ?Up = "alluopairs ?U"
let ?mp = "minusinf ?q"
let ?pp = "plusinf ?q"
@@ -2793,7 +2783,7 @@
definition
"ferrack2 p \<equiv> let q = simpfm p ; mp = minusinf q ; pp = plusinf q
in if (mp = T \<or> pp = T) then T
-  else (let U = remdps (uset  q)
+  else (let U = remdups (uset  q)
in decr0 (list_disj [mp, pp, simpfm (subst0 (CP 0\<^sub>p) q), evaldjf (\<lambda>(c,t). msubst2 q (c *\<^sub>p C (-2, 1)) t) U,
evaldjf (\<lambda>((b,a),(d,c)). msubst2 q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) (alluopairs U)]))"

@@ -2808,7 +2798,7 @@
let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
let ?q = "simpfm p"
let ?qz = "subst0 (CP 0\<^sub>p) ?q"
-  let ?U = "remdps(uset ?q)"
+  let ?U = "remdups(uset ?q)"
let ?Up = "alluopairs ?U"
let ?mp = "minusinf ?q"
let ?pp = "plusinf ?q"```