author krauss Wed Feb 23 11:16:56 2011 +0100 (2011-02-23) changeset 41823 81d64ec48427 parent 41822 27afef7d6c37 child 41825 49d5af6a3d1b
eliminated remdps in favor of List.remdups
```     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.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"
```