src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
 changeset 41849 1a65b780bd56 parent 41842 d8f76db6a207 child 42284 326f57825e1a
```     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 25 14:25:52 2011 +0100
1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 25 20:07:48 2011 +0100
1.3 @@ -5,9 +5,7 @@
1.4  header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
1.5
1.6  theory Parametric_Ferrante_Rackoff
1.7 -imports
1.8 -  Reflected_Multivariate_Polynomial
1.9 -  Dense_Linear_Order
1.10 +imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library
1.11    "~~/src/HOL/Library/Efficient_Nat"
1.12  begin
1.13
1.14 @@ -2440,34 +2438,6 @@
1.15  from fr_eq[OF lp, of vs bs x, simplified th'] show ?thesis .
1.16  qed
1.17
1.18 -text {* Rest of the implementation *}
1.19 -
1.20 -primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
1.21 -  "alluopairs [] = []"
1.22 -| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
1.23 -
1.24 -lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
1.25 -by (induct xs, auto)
1.26 -
1.27 -lemma alluopairs_set:
1.28 -  "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "
1.29 -by (induct xs, auto)
1.30 -
1.31 -lemma alluopairs_ex:
1.32 -  assumes Pc: "\<forall> x \<in> set xs. \<forall>y\<in> set xs. P x y = P y x"
1.33 -  shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
1.34 -proof
1.35 -  assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"
1.36 -  then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y"  by blast
1.37 -  from alluopairs_set[OF x y] P Pc x y show"\<exists>(x, y)\<in>set (alluopairs xs). P x y"
1.38 -    by auto
1.39 -next
1.40 -  assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"
1.41 -  then obtain "x" and "y"  where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+
1.42 -  from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast
1.43 -  with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
1.44 -qed
1.45 -
1.46  lemma simpfm_lin:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.47    shows "qfree p \<Longrightarrow> islin (simpfm p)"
1.48    by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)
1.49 @@ -2516,7 +2486,7 @@
1.50    from decr0_qf[OF th1] have thqf: "qfree (ferrack p)" by (simp add: ferrack_def Let_def)
1.51    have "?lhs \<longleftrightarrow> (\<exists>x. Ifm vs (x#bs) ?q)" by simp
1.52    also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> (\<exists>(c, t)\<in>set ?U. \<exists>(d, s)\<in>set ?U. ?I (msubst (simpfm p) ((c, t), d, s)))" using fr_eq_msubst[OF lq, of vs bs x] by simp
1.53 -  also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> (\<exists> (x,y) \<in> set ?Up. ?I ((simpfm o (msubst ?q)) (x,y)))" using alluopairs_ex[OF th0] by simp
1.54 +  also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> (\<exists> (x,y) \<in> set ?Up. ?I ((simpfm o (msubst ?q)) (x,y)))" using alluopairs_bex[OF th0] by simp
1.55    also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (evaldjf (simpfm o (msubst ?q)) ?Up)"