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.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 +
```