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)" 
    1.56      by (simp add: evaldjf_ex)
    1.57    also have "\<dots> \<longleftrightarrow> ?I (disj ?mp (disj ?pp (evaldjf (simpfm o (msubst ?q)) ?Up)))" by simp
    1.58 @@ -2857,7 +2827,7 @@
    1.59    also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (subst0 (CP 0\<^sub>p) ?q) \<or> (\<exists>(n,t) \<in> set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \<or> (\<exists> x\<in>set ?U. \<exists> y \<in>set ?U. ?I (?s (x,y)))"
    1.60      by (simp add: split_def)
    1.61    also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (subst0 (CP 0\<^sub>p) ?q) \<or> (\<exists>(n,t) \<in> set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \<or> (\<exists> (x,y) \<in> set ?Up. ?I (?s (x,y)))"
    1.62 -    using alluopairs_ex[OF th0] by simp 
    1.63 +    using alluopairs_bex[OF th0] by simp 
    1.64    also have "\<dots> \<longleftrightarrow> ?I ?R" 
    1.65      by (simp add: list_disj_def evaldjf_ex split_def)
    1.66    also have "\<dots> \<longleftrightarrow> ?rhs"