src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 61424 c3658c18b7bc
parent 60754 02924903a6fd
child 61586 5197a2ecb658
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -2608,7 +2608,7 @@
     1.4  section \<open>First implementation : Naive by encoding all case splits locally\<close>
     1.5  
     1.6  definition "msubsteq c t d s a r =
     1.7 -  evaldjf (split conj)
     1.8 +  evaldjf (case_prod conj)
     1.9    [(let cd = c *\<^sub>p d
    1.10      in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
    1.11     (conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
    1.12 @@ -2626,7 +2626,7 @@
    1.13        in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
    1.14       (conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
    1.15       (conj (NEq (CP c)) (Eq (CP d)), Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
    1.16 -     (conj (Eq (CP c)) (Eq (CP d)), Eq r)]. bound0 (split conj x)"
    1.17 +     (conj (Eq (CP c)) (Eq (CP d)), Eq r)]. bound0 (case_prod conj x)"
    1.18      using lp by (simp add: Let_def t s)
    1.19    from evaldjf_bound0[OF th] show ?thesis
    1.20      by (simp add: msubsteq_def)
    1.21 @@ -2715,7 +2715,7 @@
    1.22  
    1.23  
    1.24  definition "msubstneq c t d s a r =
    1.25 -  evaldjf (split conj)
    1.26 +  evaldjf (case_prod conj)
    1.27    [(let cd = c *\<^sub>p d
    1.28      in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
    1.29     (conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
    1.30 @@ -2733,7 +2733,7 @@
    1.31       in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
    1.32      (conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
    1.33      (conj (NEq (CP c)) (Eq (CP d)), NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
    1.34 -    (conj (Eq (CP c)) (Eq (CP d)), NEq r)]. bound0 (split conj x)"
    1.35 +    (conj (Eq (CP c)) (Eq (CP d)), NEq r)]. bound0 (case_prod conj x)"
    1.36      using lp by (simp add: Let_def t s)
    1.37    from evaldjf_bound0[OF th] show ?thesis
    1.38      by (simp add: msubstneq_def)
    1.39 @@ -2821,7 +2821,7 @@
    1.40  qed
    1.41  
    1.42  definition "msubstlt c t d s a r =
    1.43 -  evaldjf (split conj)
    1.44 +  evaldjf (case_prod conj)
    1.45    [(let cd = c *\<^sub>p d
    1.46      in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
    1.47     (let cd = c *\<^sub>p d
    1.48 @@ -2847,7 +2847,7 @@
    1.49     (conj (lt (CP c)) (Eq (CP d)), Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
    1.50     (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)), Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
    1.51     (conj (lt (CP d)) (Eq (CP c)), Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
    1.52 -   (conj (Eq (CP c)) (Eq (CP d)), Lt r)]. bound0 (split conj x)"
    1.53 +   (conj (Eq (CP c)) (Eq (CP d)), Lt r)]. bound0 (case_prod conj x)"
    1.54      using lp by (simp add: Let_def t s lt_nb)
    1.55    from evaldjf_bound0[OF th] show ?thesis
    1.56      by (simp add: msubstlt_def)
    1.57 @@ -3027,7 +3027,7 @@
    1.58  qed
    1.59  
    1.60  definition "msubstle c t d s a r =
    1.61 -  evaldjf (split conj)
    1.62 +  evaldjf (case_prod conj)
    1.63     [(let cd = c *\<^sub>p d
    1.64       in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
    1.65      (let cd = c *\<^sub>p d
    1.66 @@ -3053,7 +3053,7 @@
    1.67      (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
    1.68      (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
    1.69      (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
    1.70 -    (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (split conj x)"
    1.71 +    (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (case_prod conj x)"
    1.72      using lp by (simp add: Let_def t s lt_nb)
    1.73    from evaldjf_bound0[OF th] show ?thesis
    1.74      by (simp add: msubstle_def)