eliminated remdps in favor of List.remdups
authorkrauss
Wed Feb 23 11:16:56 2011 +0100 (2011-02-23)
changeset 4182381d64ec48427
parent 41822 27afef7d6c37
child 41825 49d5af6a3d1b
eliminated remdps in favor of List.remdups
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 23 11:15:06 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 23 11:16:56 2011 +0100
     1.3 @@ -2475,16 +2475,6 @@
     1.4  lemma filter_length: "length (List.filter P xs) < Suc (length xs)"
     1.5    apply (induct xs, auto) done
     1.6  
     1.7 -consts remdps:: "'a list \<Rightarrow> 'a list"
     1.8 -
     1.9 -recdef remdps "measure size"
    1.10 -  "remdps [] = []"
    1.11 -  "remdps (x#xs) = (x#(remdps (List.filter (\<lambda> y. y \<noteq> x) xs)))"
    1.12 -(hints simp add: filter_length[rule_format])
    1.13 -
    1.14 -lemma remdps_set[simp]: "set (remdps xs) = set xs"
    1.15 -  by (induct xs rule: remdps.induct, auto)
    1.16 -
    1.17  lemma simpfm_lin:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.18    shows "qfree p \<Longrightarrow> islin (simpfm p)"
    1.19    by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)
    1.20 @@ -2492,7 +2482,7 @@
    1.21  definition 
    1.22    "ferrack p \<equiv> let q = simpfm p ; mp = minusinf q ; pp = plusinf q
    1.23    in if (mp = T \<or> pp = T) then T 
    1.24 -     else (let U = alluopairs (remdps (uset  q))
    1.25 +     else (let U = alluopairs (remdups (uset  q))
    1.26             in decr0 (disj mp (disj pp (evaldjf (simpfm o (msubst q)) U ))))"
    1.27  
    1.28  lemma ferrack: 
    1.29 @@ -2504,7 +2494,7 @@
    1.30    let ?N = "\<lambda> t. Ipoly vs t"
    1.31    let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
    1.32    let ?q = "simpfm p" 
    1.33 -  let ?U = "remdps(uset ?q)"
    1.34 +  let ?U = "remdups(uset ?q)"
    1.35    let ?Up = "alluopairs ?U"
    1.36    let ?mp = "minusinf ?q"
    1.37    let ?pp = "plusinf ?q"
    1.38 @@ -2793,7 +2783,7 @@
    1.39  definition 
    1.40  "ferrack2 p \<equiv> let q = simpfm p ; mp = minusinf q ; pp = plusinf q
    1.41   in if (mp = T \<or> pp = T) then T 
    1.42 -  else (let U = remdps (uset  q)
    1.43 +  else (let U = remdups (uset  q)
    1.44      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, 
    1.45     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)]))"
    1.46  
    1.47 @@ -2808,7 +2798,7 @@
    1.48    let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
    1.49    let ?q = "simpfm p" 
    1.50    let ?qz = "subst0 (CP 0\<^sub>p) ?q"
    1.51 -  let ?U = "remdps(uset ?q)"
    1.52 +  let ?U = "remdups(uset ?q)"
    1.53    let ?Up = "alluopairs ?U"
    1.54    let ?mp = "minusinf ?q"
    1.55    let ?pp = "plusinf ?q"