src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 50045 2214bc566f88
parent 49962 a8cc904a6820
child 50282 fe4d4bb9f4c2
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Nov 09 19:21:47 2012 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Nov 11 19:24:01 2012 +0100
     1.3 @@ -1129,7 +1129,7 @@
     1.4  lemma list_conj: "Ifm vs bs (list_conj ps) = (\<forall>p\<in> set ps. Ifm vs bs p)"
     1.5    by (induct ps, auto simp add: list_conj_def)
     1.6  lemma list_conj_qf: " \<forall>p\<in> set ps. qfree p \<Longrightarrow> qfree (list_conj ps)"
     1.7 -  by (induct ps, auto simp add: list_conj_def conj_qf)
     1.8 +  by (induct ps, auto simp add: list_conj_def)
     1.9  lemma list_disj: "Ifm vs bs (list_disj ps) = (\<exists>p\<in> set ps. Ifm vs bs p)"
    1.10    by (induct ps, auto simp add: list_disj_def)
    1.11  
    1.12 @@ -1586,7 +1586,7 @@
    1.13    then obtain c s where csU: "(c,s) \<in> set (uset p)" and x: "(Ipoly vs c < 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s) \<or>  (Ipoly vs c > 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s)" by blast
    1.14    hence "x \<ge> (- Itm vs (x#bs) s) / Ipoly vs c"
    1.15      using divide_le_eq[of "- Itm vs (x#bs) s" "Ipoly vs c" x]
    1.16 -    by (auto simp add: mult_commute del: divide_minus_left)
    1.17 +      by (auto simp add: mult_commute)
    1.18    thus ?thesis using csU by auto
    1.19  qed
    1.20  
    1.21 @@ -2733,7 +2733,7 @@
    1.22     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.23    from subst0_nb[of "CP 0\<^sub>p" ?q] q_qf evaldjf_bound0[OF bnd1] evaldjf_bound0[OF bnd0] mp_nb pp_nb stupid
    1.24    have nb: "bound0 ?R "
    1.25 -    by (simp add: list_disj_def disj_nb0 simpfm_bound0)
    1.26 +    by (simp add: list_disj_def simpfm_bound0)
    1.27    let ?s = "\<lambda>((b,a),(d,c)). msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))"
    1.28  
    1.29    {fix b a d c assume baU: "(b,a) \<in> set ?U" and dcU: "(d,c) \<in> set ?U"
    1.30 @@ -2789,222 +2789,156 @@
    1.31  show ?thesis  unfolding frpar2_def by (auto simp add: prep)
    1.32  qed
    1.33  
    1.34 +oracle frpar_oracle = {*
    1.35 +let
    1.36 +
    1.37 +fun binopT T = T --> T --> T;
    1.38 +fun relT T = T --> T --> @{typ bool};
    1.39 +
    1.40 +val dest_num = snd o HOLogic.dest_number;
    1.41 +
    1.42 +fun try_dest_num t = SOME ((snd o HOLogic.dest_number) t)
    1.43 +  handle TERM _ => NONE;
    1.44 +
    1.45 +fun dest_nat (t as Const (@{const_name Suc}, _)) = HOLogic.dest_nat t
    1.46 +  | dest_nat t = dest_num t;
    1.47 +
    1.48 +fun the_index ts t =
    1.49 +  let
    1.50 +    val k = find_index (fn t' => t aconv t') ts;
    1.51 +  in if k < 0 then raise General.Subscript else k end;
    1.52 +
    1.53 +fun num_of_term ps (Const (@{const_name Groups.uminus}, _) $ t) = @{code poly.Neg} (num_of_term ps t)
    1.54 +  | num_of_term ps (Const (@{const_name Groups.plus}, _) $ a $ b) = @{code poly.Add} (num_of_term ps a, num_of_term ps b)
    1.55 +  | num_of_term ps (Const (@{const_name Groups.minus}, _) $ a $ b) = @{code poly.Sub} (num_of_term ps a, num_of_term ps b)
    1.56 +  | num_of_term ps (Const (@{const_name Groups.times}, _) $ a $ b) = @{code poly.Mul} (num_of_term ps a, num_of_term ps b)
    1.57 +  | num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) = @{code poly.Pw} (num_of_term ps a, dest_nat n)
    1.58 +  | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) = @{code poly.C} (dest_num a, dest_num b)
    1.59 +  | num_of_term ps t = (case try_dest_num t
    1.60 +     of SOME k => @{code poly.C} (k, 1)
    1.61 +      | NONE => @{code poly.Bound} (the_index ps t));
    1.62 +
    1.63 +fun tm_of_term fs ps (Const(@{const_name Groups.uminus}, _) $ t) = @{code Neg} (tm_of_term fs ps t)
    1.64 +  | tm_of_term fs ps (Const(@{const_name Groups.plus}, _) $ a $ b) = @{code Add} (tm_of_term fs ps a, tm_of_term fs ps b)
    1.65 +  | tm_of_term fs ps (Const(@{const_name Groups.minus}, _) $ a $ b) = @{code Sub} (tm_of_term fs ps a, tm_of_term fs ps b)
    1.66 +  | tm_of_term fs ps (Const(@{const_name Groups.times}, _) $ a $ b) = @{code Mul} (num_of_term ps a, tm_of_term fs ps b)
    1.67 +  | tm_of_term fs ps t = (@{code CP} (num_of_term ps t) 
    1.68 +      handle TERM _ => @{code Bound} (the_index fs t)
    1.69 +           | General.Subscript => @{code Bound} (the_index fs t));
    1.70 +
    1.71 +fun fm_of_term fs ps @{term True} = @{code T}
    1.72 +  | fm_of_term fs ps @{term False} = @{code F}
    1.73 +  | fm_of_term fs ps (Const (@{const_name Not}, _) $ p) = @{code NOT} (fm_of_term fs ps p)
    1.74 +  | fm_of_term fs ps (Const (@{const_name HOL.conj}, _) $ p $ q) = @{code And} (fm_of_term fs ps p, fm_of_term fs ps q)
    1.75 +  | fm_of_term fs ps (Const (@{const_name HOL.disj}, _) $ p $ q) = @{code Or} (fm_of_term fs ps p, fm_of_term fs ps q)
    1.76 +  | fm_of_term fs ps (Const (@{const_name HOL.implies}, _) $ p $ q) = @{code Imp} (fm_of_term fs ps p, fm_of_term fs ps q)
    1.77 +  | fm_of_term fs ps (@{term HOL.iff} $ p $ q) = @{code Iff} (fm_of_term fs ps p, fm_of_term fs ps q)
    1.78 +  | fm_of_term fs ps (Const (@{const_name HOL.eq}, T) $ p $ q) =
    1.79 +      @{code Eq} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
    1.80 +  | fm_of_term fs ps (Const (@{const_name Orderings.less}, _) $ p $ q) =
    1.81 +      @{code Lt} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
    1.82 +  | fm_of_term fs ps (Const (@{const_name Orderings.less_eq}, _) $ p $ q) =
    1.83 +      @{code Le} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
    1.84 +  | fm_of_term fs ps (Const (@{const_name Ex}, _) $ Abs (abs as (_, xT, _))) =
    1.85 +      let
    1.86 +        val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
    1.87 +      in @{code E} (fm_of_term (Free (xn', xT) :: fs) ps p') end
    1.88 +  | fm_of_term fs ps (Const (@{const_name All},_) $ Abs (abs as (_, xT, _))) =
    1.89 +      let
    1.90 +        val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
    1.91 +      in @{code A} (fm_of_term (Free (xn', xT) :: fs) ps p') end
    1.92 +  | fm_of_term fs ps _ = error "fm_of_term";
    1.93 +
    1.94 +fun term_of_num T ps (@{code poly.C} (a, b)) = 
    1.95 +    (if b = 1 then HOLogic.mk_number T a
    1.96 +     else if b = 0 then Const (@{const_name Groups.zero}, T)
    1.97 +     else Const (@{const_name Fields.divide}, binopT T) $ HOLogic.mk_number T a $ HOLogic.mk_number T b)
    1.98 +  | term_of_num T ps (@{code poly.Bound} i) = nth ps i
    1.99 +  | term_of_num T ps (@{code poly.Add} (a, b)) = Const (@{const_name Groups.plus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b
   1.100 +  | term_of_num T ps (@{code poly.Mul} (a, b)) = Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_num T ps b
   1.101 +  | term_of_num T ps (@{code poly.Sub} (a, b)) = Const (@{const_name Groups.minus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b
   1.102 +  | term_of_num T ps (@{code poly.Neg} a) = Const (@{const_name Groups.uminus}, T --> T) $ term_of_num T ps a
   1.103 +  | term_of_num T ps (@{code poly.Pw} (a, n)) =
   1.104 +      Const (@{const_name Power.power}, T --> @{typ nat} --> T) $ term_of_num T ps a $ HOLogic.mk_number HOLogic.natT n
   1.105 +  | term_of_num T ps (@{code poly.CN} (c, n, p)) =
   1.106 +      term_of_num T ps (@{code poly.Add} (c, @{code poly.Mul} (@{code poly.Bound} n, p)));
   1.107 +
   1.108 +fun term_of_tm T fs ps (@{code CP} p) = term_of_num T ps p
   1.109 +  | term_of_tm T fs ps (@{code Bound} i) = nth fs i
   1.110 +  | term_of_tm T fs ps (@{code Add} (a, b)) = Const (@{const_name Groups.plus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b
   1.111 +  | term_of_tm T fs ps (@{code Mul} (a, b)) = Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_tm T fs ps b
   1.112 +  | term_of_tm T fs ps (@{code Sub} (a, b)) = Const (@{const_name Groups.minus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b
   1.113 +  | term_of_tm T fs ps (@{code Neg} a) = Const (@{const_name Groups.uminus}, T --> T) $ term_of_tm T fs ps a
   1.114 +  | term_of_tm T fs ps (@{code CNP} (n, c, p)) = term_of_tm T fs ps
   1.115 +     (@{code Add} (@{code Mul} (c, @{code Bound} n), p));
   1.116 +
   1.117 +fun term_of_fm T fs ps @{code T} = @{term True}
   1.118 +  | term_of_fm T fs ps @{code F} = @{term False}
   1.119 +  | term_of_fm T fs ps (@{code NOT} p) = @{term Not} $ term_of_fm T fs ps p
   1.120 +  | term_of_fm T fs ps (@{code And} (p, q)) = @{term HOL.conj} $ term_of_fm T fs ps p $ term_of_fm T fs ps q
   1.121 +  | term_of_fm T fs ps (@{code Or} (p, q)) = @{term HOL.disj} $ term_of_fm T fs ps p $ term_of_fm T fs ps q
   1.122 +  | term_of_fm T fs ps (@{code Imp} (p, q)) = @{term HOL.implies} $ term_of_fm T fs ps p $ term_of_fm T fs ps q
   1.123 +  | term_of_fm T fs ps (@{code Iff} (p, q)) = @{term HOL.iff} $ term_of_fm T fs ps p $ term_of_fm T fs ps q
   1.124 +  | term_of_fm T fs ps (@{code Lt} p) = Const (@{const_name Orderings.less}, relT T) $ term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T)
   1.125 +  | term_of_fm T fs ps (@{code Le} p) = Const (@{const_name Orderings.less_eq}, relT T) $ term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T)
   1.126 +  | term_of_fm T fs ps (@{code Eq} p) = Const (@{const_name HOL.eq}, relT T) $ term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T)
   1.127 +  | term_of_fm T fs ps (@{code NEq} p) = @{term Not} $ (Const (@{const_name HOL.eq}, relT T) $ term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T))
   1.128 +  | term_of_fm T fs ps _ = error "term_of_fm: quantifiers";
   1.129 +
   1.130 +fun frpar_procedure alternative T ps fm =
   1.131 +  let 
   1.132 +    val frpar = if alternative then @{code frpar2} else @{code frpar};
   1.133 +    val fs = subtract (op aconv) (map Free (Term.add_frees fm [])) ps;
   1.134 +    val eval = term_of_fm T fs ps o frpar o fm_of_term fs ps;
   1.135 +    val t = HOLogic.dest_Trueprop fm;
   1.136 +  in
   1.137 +    (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, eval t)
   1.138 +  end;
   1.139 +
   1.140 +in
   1.141 +
   1.142 +  fn (ctxt, alternative, ty, ps, ct) => 
   1.143 +    cterm_of (Proof_Context.theory_of ctxt)
   1.144 +      (frpar_procedure alternative ty ps (term_of ct))
   1.145 +
   1.146 +end
   1.147 +*}
   1.148 +
   1.149  ML {* 
   1.150 -structure ReflectedFRPar = 
   1.151 +structure Parametric_Ferrante_Rackoff = 
   1.152  struct
   1.153  
   1.154 -val bT = HOLogic.boolT;
   1.155 -fun num rT x = HOLogic.mk_number rT x;
   1.156 -fun rrelT rT = [rT,rT] ---> rT;
   1.157 -fun rrT rT = [rT, rT] ---> bT;
   1.158 -fun divt rT = Const(@{const_name Fields.divide},rrelT rT);
   1.159 -fun timest rT = Const(@{const_name Groups.times},rrelT rT);
   1.160 -fun plust rT = Const(@{const_name Groups.plus},rrelT rT);
   1.161 -fun minust rT = Const(@{const_name Groups.minus},rrelT rT);
   1.162 -fun uminust rT = Const(@{const_name Groups.uminus}, rT --> rT);
   1.163 -fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
   1.164 -val brT = [bT, bT] ---> bT;
   1.165 -val nott = @{term "Not"};
   1.166 -val conjt = @{term HOL.conj};
   1.167 -val disjt = @{term HOL.disj};
   1.168 -val impt = @{term HOL.implies};
   1.169 -val ifft = @{term "op = :: bool => _"}
   1.170 -fun llt rT = Const(@{const_name Orderings.less},rrT rT);
   1.171 -fun lle rT = Const(@{const_name Orderings.less},rrT rT);
   1.172 -fun eqt rT = Const(@{const_name HOL.eq},rrT rT);
   1.173 -fun rz rT = Const(@{const_name Groups.zero},rT);
   1.174 -
   1.175 -fun dest_nat t = case t of
   1.176 -  Const (@{const_name Suc}, _) $ t' => 1 + dest_nat t'
   1.177 -| _ => (snd o HOLogic.dest_number) t;
   1.178 -
   1.179 -fun num_of_term m t = 
   1.180 - case t of
   1.181 -   Const(@{const_name Groups.uminus},_)$t => @{code poly.Neg} (num_of_term m t)
   1.182 - | Const(@{const_name Groups.plus},_)$a$b => @{code poly.Add} (num_of_term m a, num_of_term m b)
   1.183 - | Const(@{const_name Groups.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
   1.184 - | Const(@{const_name Groups.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
   1.185 - | Const(@{const_name Power.power},_)$a$n => @{code poly.Pw} (num_of_term m a, dest_nat n)
   1.186 - | Const(@{const_name Fields.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
   1.187 - | _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1) 
   1.188 -         handle TERM _ => @{code poly.Bound} (AList.lookup (op aconv) m t |> the));
   1.189 -
   1.190 -fun tm_of_term m m' t = 
   1.191 - case t of
   1.192 -   Const(@{const_name Groups.uminus},_)$t => @{code Neg} (tm_of_term m m' t)
   1.193 - | Const(@{const_name Groups.plus},_)$a$b => @{code Add} (tm_of_term m m' a, tm_of_term m m' b)
   1.194 - | Const(@{const_name Groups.minus},_)$a$b => @{code Sub} (tm_of_term m m' a, tm_of_term m m' b)
   1.195 - | Const(@{const_name Groups.times},_)$a$b => @{code Mul} (num_of_term m' a, tm_of_term m m' b)
   1.196 - | _ => (@{code CP} (num_of_term m' t) 
   1.197 -         handle TERM _ => @{code Bound} (AList.lookup (op aconv) m t |> the)
   1.198 -              | Option => @{code Bound} (AList.lookup (op aconv) m t |> the));
   1.199 -
   1.200 -fun term_of_num T m t = 
   1.201 - case t of
   1.202 -  @{code poly.C} (a,b) => (if b = 1 then num T a else if b=0 then (rz T) 
   1.203 -                                        else (divt T) $ num T a $ num T b)
   1.204 -| @{code poly.Bound} i => AList.lookup (op = : int*int -> bool) m i |> the
   1.205 -| @{code poly.Add} (a,b) => (plust T)$(term_of_num T m a)$(term_of_num T m b)
   1.206 -| @{code poly.Mul} (a,b) => (timest T)$(term_of_num T m a)$(term_of_num T m b)
   1.207 -| @{code poly.Sub} (a,b) => (minust T)$(term_of_num T m a)$(term_of_num T m b)
   1.208 -| @{code poly.Neg} a => (uminust T)$(term_of_num T m a)
   1.209 -| @{code poly.Pw} (a,n) => (powt T)$(term_of_num T m t)$(HOLogic.mk_number HOLogic.natT n)
   1.210 -| @{code poly.CN} (c,n,p) => term_of_num T m (@{code poly.Add} (c, @{code poly.Mul} (@{code poly.Bound} n, p)))
   1.211 -| _ => error "term_of_num: Unknown term";
   1.212 +fun tactic ctxt alternative T ps = 
   1.213 +  Object_Logic.full_atomize_tac
   1.214 +  THEN' CSUBGOAL (fn (g, i) =>
   1.215 +    let
   1.216 +      val th = frpar_oracle (ctxt, alternative, T, ps, g)
   1.217 +    in rtac (th RS iffD2) i end);
   1.218  
   1.219 -fun term_of_tm T m m' t = 
   1.220 - case t of
   1.221 -  @{code CP} p => term_of_num T m' p
   1.222 -| @{code Bound} i => AList.lookup (op = : int*int -> bool) m i |> the
   1.223 -| @{code Add} (a,b) => (plust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
   1.224 -| @{code Mul} (a,b) => (timest T)$(term_of_num T m' a)$(term_of_tm T m m' b)
   1.225 -| @{code Sub} (a,b) => (minust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
   1.226 -| @{code Neg} a => (uminust T)$(term_of_tm T m m' a)
   1.227 -| @{code CNP} (n,c,p) => term_of_tm T m m' (@{code Add}
   1.228 -     (@{code Mul} (c, @{code Bound} n), p))
   1.229 -| _ => error "term_of_tm: Unknown term";
   1.230 -
   1.231 -fun fm_of_term m m' fm = 
   1.232 - case fm of
   1.233 -    Const(@{const_name True},_) => @{code T}
   1.234 -  | Const(@{const_name False},_) => @{code F}
   1.235 -  | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
   1.236 -  | Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
   1.237 -  | Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
   1.238 -  | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
   1.239 -  | Const(@{const_name HOL.eq},ty)$p$q => 
   1.240 -       if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
   1.241 -       else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
   1.242 -  | Const(@{const_name Orderings.less},_)$p$q => 
   1.243 -        @{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
   1.244 -  | Const(@{const_name Orderings.less_eq},_)$p$q => 
   1.245 -        @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
   1.246 -  | Const(@{const_name Ex},_)$Abs(xn,xT,p) => 
   1.247 -     let val (xn', p') = Syntax_Trans.variant_abs (xn,xT,p)  (* FIXME !? *)
   1.248 -         val x = Free(xn',xT)
   1.249 -         fun incr i = i + 1
   1.250 -         val m0 = (x,0):: (map (apsnd incr) m)
   1.251 -      in @{code E} (fm_of_term m0 m' p') end
   1.252 -  | Const(@{const_name All},_)$Abs(xn,xT,p) => 
   1.253 -     let val (xn', p') = Syntax_Trans.variant_abs (xn,xT,p)  (* FIXME !? *)
   1.254 -         val x = Free(xn',xT)
   1.255 -         fun incr i = i + 1
   1.256 -         val m0 = (x,0):: (map (apsnd incr) m)
   1.257 -      in @{code A} (fm_of_term m0 m' p') end
   1.258 -  | _ => error "fm_of_term";
   1.259 -
   1.260 -
   1.261 -fun term_of_fm T m m' t = 
   1.262 -  case t of
   1.263 -    @{code T} => Const(@{const_name True},bT)
   1.264 -  | @{code F} => Const(@{const_name False},bT)
   1.265 -  | @{code NOT} p => nott $ (term_of_fm T m m' p)
   1.266 -  | @{code And} (p,q) => conjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.267 -  | @{code Or} (p,q) => disjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.268 -  | @{code Imp} (p,q) => impt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.269 -  | @{code Iff} (p,q) => ifft $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.270 -  | @{code Lt} p => (llt T) $ (term_of_tm T m m' p) $ (rz T)
   1.271 -  | @{code Le} p => (lle T) $ (term_of_tm T m m' p) $ (rz T)
   1.272 -  | @{code Eq} p => (eqt T) $ (term_of_tm T m m' p) $ (rz T)
   1.273 -  | @{code NEq} p => nott $ ((eqt T) $ (term_of_tm T m m' p) $ (rz T))
   1.274 -  | _ => error "term_of_fm: quantifiers!!!!???";
   1.275 -
   1.276 -fun frpar_oracle (T,m, m', fm) = 
   1.277 - let 
   1.278 -   val t = HOLogic.dest_Trueprop fm
   1.279 -   val im = 0 upto (length m - 1)
   1.280 -   val im' = 0 upto (length m' - 1)   
   1.281 - in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm T (im ~~ m) (im' ~~ m')  
   1.282 -                                                     (@{code frpar} (fm_of_term (m ~~ im) (m' ~~ im') t))))
   1.283 - end;
   1.284 -
   1.285 -fun frpar_oracle2 (T,m, m', fm) = 
   1.286 - let 
   1.287 -   val t = HOLogic.dest_Trueprop fm
   1.288 -   val im = 0 upto (length m - 1)
   1.289 -   val im' = 0 upto (length m' - 1)   
   1.290 - in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm T (im ~~ m) (im' ~~ m')  
   1.291 -                                                     (@{code frpar2} (fm_of_term (m ~~ im) (m' ~~ im') t))))
   1.292 - end;
   1.293 +fun method alternative =
   1.294 +  let
   1.295 +    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   1.296 +    val parsN = "pars"
   1.297 +    val typN = "type"
   1.298 +    val any_keyword = keyword parsN || keyword typN
   1.299 +    val terms = Scan.repeat (Scan.unless any_keyword Args.term)
   1.300 +    val typ = Scan.unless any_keyword Args.typ
   1.301 +  in
   1.302 +    (keyword typN |-- typ) -- (keyword parsN |-- terms) >>
   1.303 +      (fn (T, ps) => fn ctxt => SIMPLE_METHOD' (tactic ctxt alternative T ps))
   1.304 +  end
   1.305  
   1.306  end;
   1.307 -
   1.308 -
   1.309 -*}
   1.310 -
   1.311 -oracle frpar_oracle = {* fn (ty, ts, ts', ct) => 
   1.312 - let 
   1.313 -  val thy = Thm.theory_of_cterm ct
   1.314 - in cterm_of thy (ReflectedFRPar.frpar_oracle (ty,ts, ts', term_of ct))
   1.315 - end *}
   1.316 -
   1.317 -oracle frpar_oracle2 = {* fn (ty, ts, ts', ct) => 
   1.318 - let 
   1.319 -  val thy = Thm.theory_of_cterm ct
   1.320 - in cterm_of thy (ReflectedFRPar.frpar_oracle2 (ty,ts, ts', term_of ct))
   1.321 - end *}
   1.322 -
   1.323 -ML{* 
   1.324 -structure FRParTac = 
   1.325 -struct
   1.326 -
   1.327 -fun frpar_tac T ps ctxt = 
   1.328 - Object_Logic.full_atomize_tac
   1.329 - THEN' CSUBGOAL (fn (g, i) =>
   1.330 -  let
   1.331 -    val thy = Proof_Context.theory_of ctxt
   1.332 -    val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
   1.333 -    val th = frpar_oracle (T, fs, ps, (* Pattern.eta_long [] *) g)
   1.334 -  in rtac (th RS iffD2) i end);
   1.335 -
   1.336 -fun frpar2_tac T ps ctxt = 
   1.337 - Object_Logic.full_atomize_tac
   1.338 - THEN' CSUBGOAL (fn (g, i) =>
   1.339 -  let
   1.340 -    val thy = Proof_Context.theory_of ctxt
   1.341 -    val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
   1.342 -    val th = frpar_oracle2 (T, fs, ps, (* Pattern.eta_long [] *) g)
   1.343 -  in rtac (th RS iffD2) i end);
   1.344 -
   1.345 -end;
   1.346 -
   1.347  *}
   1.348  
   1.349  method_setup frpar = {*
   1.350 -let
   1.351 - fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   1.352 - fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
   1.353 - val parsN = "pars"
   1.354 - val typN = "type"
   1.355 - val any_keyword = keyword parsN || keyword typN
   1.356 - val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
   1.357 - val cterms = thms >> map Drule.dest_term;
   1.358 - val terms = Scan.repeat (Scan.unless any_keyword Args.term)
   1.359 - val typ = Scan.unless any_keyword Args.typ
   1.360 -in
   1.361 - (keyword typN |-- typ) -- (keyword parsN |-- terms) >>
   1.362 -  (fn (T,ps) => fn ctxt => SIMPLE_METHOD' (FRParTac.frpar_tac T ps ctxt))
   1.363 -end
   1.364 -*} "parametric QE for linear Arithmetic over fields, Version 1"
   1.365 +  Parametric_Ferrante_Rackoff.method false
   1.366 +*} "parametric QE for linear Arithmetic over fields"
   1.367  
   1.368  method_setup frpar2 = {*
   1.369 -let
   1.370 - fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   1.371 - fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
   1.372 - val parsN = "pars"
   1.373 - val typN = "type"
   1.374 - val any_keyword = keyword parsN || keyword typN
   1.375 - val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
   1.376 - val cterms = thms >> map Drule.dest_term;
   1.377 - val terms = Scan.repeat (Scan.unless any_keyword Args.term)
   1.378 - val typ = Scan.unless any_keyword Args.typ
   1.379 -in
   1.380 - (keyword typN |-- typ) -- (keyword parsN |-- terms) >>
   1.381 -  (fn (T,ps) => fn ctxt => SIMPLE_METHOD' (FRParTac.frpar2_tac T ps ctxt))
   1.382 -end
   1.383 +  Parametric_Ferrante_Rackoff.method true
   1.384  *} "parametric QE for linear Arithmetic over fields, Version 2"
   1.385  
   1.386 -
   1.387  lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   1.388    apply (frpar type: "'a::{linordered_field_inverse_zero}" pars: "y::'a::{linordered_field_inverse_zero}")
   1.389    apply (simp add: field_simps)
   1.390 @@ -3012,6 +2946,13 @@
   1.391    apply (frpar type: "'a::{linordered_field_inverse_zero}" pars: "z::'a::{linordered_field_inverse_zero}")
   1.392    by simp
   1.393  
   1.394 +lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   1.395 +  apply (frpar2 type: "'a::{linordered_field_inverse_zero}" pars: "y::'a::{linordered_field_inverse_zero}")
   1.396 +  apply (simp add: field_simps)
   1.397 +  apply (rule spec[where x=y])
   1.398 +  apply (frpar2 type: "'a::{linordered_field_inverse_zero}" pars: "z::'a::{linordered_field_inverse_zero}")
   1.399 +  by simp
   1.400 +
   1.401  text{* Collins/Jones Problem *}
   1.402  (*
   1.403  lemma "\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   1.404 @@ -3030,13 +2971,6 @@
   1.405  oops
   1.406  *)
   1.407  
   1.408 -lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   1.409 -  apply (frpar2 type: "'a::{linordered_field_inverse_zero}" pars: "y::'a::{linordered_field_inverse_zero}")
   1.410 -  apply (simp add: field_simps)
   1.411 -  apply (rule spec[where x=y])
   1.412 -  apply (frpar2 type: "'a::{linordered_field_inverse_zero}" pars: "z::'a::{linordered_field_inverse_zero}")
   1.413 -  by simp
   1.414 -
   1.415  text{* Collins/Jones Problem *}
   1.416  
   1.417  (*
   1.418 @@ -3058,3 +2992,4 @@
   1.419  oops
   1.420  *)
   1.421  end
   1.422 +