# HG changeset patch
# User krauss
# Date 1298456216 -3600
# Node ID 81d64ec484278d99c547a281713194d29b06a071
# Parent  27afef7d6c371114ef82f0814329e0488fdd6e09
eliminated remdps in favor of List.remdups

diff -r 27afef7d6c37 -r 81d64ec48427 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- 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)))"
-(hints simp add: filter_length[rule_format])
-
-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"