--- a/src/HOL/Complex/ex/MIR.thy Thu Jul 19 21:47:44 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Thu Jul 19 21:47:45 2007 +0200
@@ -5,7 +5,7 @@
header {* Quatifier elimination for R(0,1,+,floor,<) *}
theory MIR
- imports Real GCD
+ imports Real GCD Pretty_Int
uses ("mireif.ML") ("mirtac.ML")
begin
@@ -106,8 +106,10 @@
qed
(* The Divisibility relation between reals *)
-consts rdvd:: "real \<Rightarrow> real \<Rightarrow> bool" (infixl 50)
-defs rdvd_def: "x rdvd y \<equiv> \<exists> (k::int). y=x*(real k)"
+definition
+ rdvd:: "real \<Rightarrow> real \<Rightarrow> bool" (infixl "rdvd" 50)
+where
+ rdvd_def: "x rdvd y \<longleftrightarrow> (\<exists>k\<Colon>int. y = x * real k)"
lemma int_rdvd_real:
shows "real (i::int) rdvd x = (i dvd (floor x) \<and> real (floor x) = x)" (is "?l = ?r")
@@ -637,10 +639,8 @@
"lex_bnd t s \<equiv> lex_ns (bnds t, bnds s)"
consts
- numgcd :: "num \<Rightarrow> int"
numgcdh:: "num \<Rightarrow> int \<Rightarrow> int"
reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num"
- reducecoeff :: "num \<Rightarrow> num"
dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
consts maxcoeff:: "num \<Rightarrow> int"
recdef maxcoeff "measure size"
@@ -658,7 +658,11 @@
"numgcdh (CN n c t) = (\<lambda>g. igcd c (numgcdh t g))"
"numgcdh (CF c s t) = (\<lambda>g. igcd c (numgcdh t g))"
"numgcdh t = (\<lambda>g. 1)"
-defs numgcd_def: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
+
+definition
+ numgcd :: "num \<Rightarrow> int"
+where
+ numgcd_def: "numgcd t = numgcdh t (maxcoeff t)"
recdef reducecoeffh "measure size"
"reducecoeffh (C i) = (\<lambda> g. C (i div g))"
@@ -666,7 +670,10 @@
"reducecoeffh (CF c s t) = (\<lambda> g. CF (c div g) s (reducecoeffh t g))"
"reducecoeffh t = (\<lambda>g. t)"
-defs reducecoeff_def: "reducecoeff t \<equiv>
+definition
+ reducecoeff :: "num \<Rightarrow> num"
+where
+ reducecoeff_def: "reducecoeff t =
(let g = numgcd t in
if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)"
@@ -832,7 +839,6 @@
simpnum:: "num \<Rightarrow> num"
numadd:: "num \<times> num \<Rightarrow> num"
nummul:: "num \<Rightarrow> int \<Rightarrow> num"
- numfloor:: "num \<Rightarrow> num"
recdef numadd "measure (\<lambda> (t,s). size t + size s)"
"numadd (CN n1 c1 r1,CN n2 c2 r2) =
@@ -939,7 +945,10 @@
lemma split_int_nb: "numbound0 t \<Longrightarrow> numbound0 (fst (split_int t)) \<and> numbound0 (snd (split_int t)) "
by (induct t rule: split_int.induct, auto simp add: Let_def split_def)
-defs numfloor_def: "numfloor t \<equiv> (let (tv,ti) = split_int t in
+definition
+ numfloor:: "num \<Rightarrow> num"
+where
+ numfloor_def: "numfloor t = (let (tv,ti) = split_int t in
(case tv of C i \<Rightarrow> numadd (tv,ti)
| _ \<Rightarrow> numadd(CF 1 tv (C 0),ti)))"
@@ -3884,25 +3893,40 @@
with rsplit_ex fnsS fx show "?I x (rsplit f a)" by auto
qed
-consts
+definition
lt :: "int \<Rightarrow> num \<Rightarrow> fm"
- le :: "int \<Rightarrow> num \<Rightarrow> fm"
- gt :: "int \<Rightarrow> num \<Rightarrow> fm"
- ge :: "int \<Rightarrow> num \<Rightarrow> fm"
- eq :: "int \<Rightarrow> num \<Rightarrow> fm"
- neq :: "int \<Rightarrow> num \<Rightarrow> fm"
-
-defs lt_def: "lt c t \<equiv> (if c = 0 then (Lt t) else if c > 0 then (Lt (CN 0 c t))
+where
+ lt_def: "lt c t = (if c = 0 then (Lt t) else if c > 0 then (Lt (CN 0 c t))
else (Gt (CN 0 (-c) (Neg t))))"
-defs le_def: "le c t \<equiv> (if c = 0 then (Le t) else if c > 0 then (Le (CN 0 c t))
+
+definition
+ le :: "int \<Rightarrow> num \<Rightarrow> fm"
+where
+ le_def: "le c t = (if c = 0 then (Le t) else if c > 0 then (Le (CN 0 c t))
else (Ge (CN 0 (-c) (Neg t))))"
-defs gt_def: "gt c t \<equiv> (if c = 0 then (Gt t) else if c > 0 then (Gt (CN 0 c t))
+
+definition
+ gt :: "int \<Rightarrow> num \<Rightarrow> fm"
+where
+ gt_def: "gt c t = (if c = 0 then (Gt t) else if c > 0 then (Gt (CN 0 c t))
else (Lt (CN 0 (-c) (Neg t))))"
-defs ge_def: "ge c t \<equiv> (if c = 0 then (Ge t) else if c > 0 then (Ge (CN 0 c t))
+
+definition
+ ge :: "int \<Rightarrow> num \<Rightarrow> fm"
+where
+ ge_def: "ge c t = (if c = 0 then (Ge t) else if c > 0 then (Ge (CN 0 c t))
else (Le (CN 0 (-c) (Neg t))))"
-defs eq_def: "eq c t \<equiv> (if c = 0 then (Eq t) else if c > 0 then (Eq (CN 0 c t))
+
+definition
+ eq :: "int \<Rightarrow> num \<Rightarrow> fm"
+where
+ eq_def: "eq c t = (if c = 0 then (Eq t) else if c > 0 then (Eq (CN 0 c t))
else (Eq (CN 0 (-c) (Neg t))))"
-defs neq_def: "neq c t \<equiv> (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t))
+
+definition
+ neq :: "int \<Rightarrow> num \<Rightarrow> fm"
+where
+ neq_def: "neq c t = (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t))
else (NEq (CN 0 (-c) (Neg t))))"
lemma lt_mono: "\<forall> a n s. Inum (x#bs) a = Inum (x#bs) (CN 0 n s) \<and> numbound0 s \<longrightarrow> Ifm (x#bs) (lt n s) = Ifm (x#bs) (Lt a)"
@@ -3973,12 +3997,6 @@
by (rule rsplit_l[where f="neq" and a="a"], auto simp add: neq_def)
(case_tac s, simp_all, case_tac"nat", simp_all)
-consts
- DVD :: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm"
- DVDJ:: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm"
- NDVD :: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm"
- NDVDJ:: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm"
-
lemma small_le:
assumes u0:"0 \<le> u" and u1: "u < 1"
shows "(-u \<le> real (n::int)) = (0 \<le> n)"
@@ -4017,8 +4035,15 @@
finally show ?thesis .
qed
-defs DVDJ_def: "DVDJ i n s \<equiv> (foldr disj (map (\<lambda> j. conj (Eq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) F)"
-defs NDVDJ_def: "NDVDJ i n s \<equiv> (foldr conj (map (\<lambda> j. disj (NEq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) T)"
+definition
+ DVDJ:: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm"
+where
+ DVDJ_def: "DVDJ i n s = (foldr disj (map (\<lambda> j. conj (Eq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) F)"
+
+definition
+ NDVDJ:: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm"
+where
+ NDVDJ_def: "NDVDJ i n s = (foldr conj (map (\<lambda> j. disj (NEq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) T)"
lemma DVDJ_DVD:
assumes xp:"x\<ge> 0" and x1: "x < 1" and np:"real n > 0"
@@ -4077,10 +4102,17 @@
from NDVDJ_def foldr_And_map_rlfm2[OF th] show ?thesis by auto
qed
-defs DVD_def: "DVD i c t \<equiv>
+definition
+ DVD :: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm"
+where
+ DVD_def: "DVD i c t =
(if i=0 then eq c t else
if c = 0 then (Dvd i t) else if c >0 then DVDJ (abs i) c t else DVDJ (abs i) (-c) (Neg t))"
-defs NDVD_def: "NDVD i c t \<equiv>
+
+definition
+ NDVD :: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm"
+where
+ "NDVD i c t =
(if i=0 then neq c t else
if c = 0 then (NDvd i t) else if c >0 then NDVDJ (abs i) c t else NDVDJ (abs i) (-c) (Neg t))"
@@ -5750,32 +5782,42 @@
declare zdvd_iff_zmod_eq_0 [code]
declare max_def [code unfold]
-code_module Mir
-file "mir.ML"
-contains
- mircfrqe = "mircfrqe"
- mirlfrqe = "mirlfrqe"
- test = "%x . mircfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))"
- test2 = "%x . mircfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))"
- test' = "%x . mirlfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))"
- test2' = "%x . mirlfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))"
-test3 = "%x .mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
-
-ML {* use "mir.ML" *}
+definition
+ "test1 (u\<Colon>unit) = mircfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))"
+
+definition
+ "test2 (u\<Colon>unit) = mircfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))"
+
+definition
+ "test3 (u\<Colon>unit) = mirlfrqe (A (And (Le (Sub (Floor (Bound 0)) (Bound 0))) (Le (Add (Bound 0) (Floor (Neg (Bound 0)))))))"
+
+definition
+ "test4 (u\<Colon>unit) = mirlfrqe (A (Iff (Eq (Add (Floor (Bound 0)) (Floor (Neg (Bound 0))))) (Eq (Sub (Floor (Bound 0)) (Bound 0)))))"
+
+definition
+ "test5 (u\<Colon>unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
+
+code_gen mircfrqe mirlfrqe test1 test2 test3 test4 test5
+ in SML to Mir
+
+code_gen mircfrqe mirlfrqe in SML to Mir file "raw_mir.ML"
+
ML "set Toplevel.timing"
-ML "Mir.test ()"
+ML "Mir.test1 ()"
ML "Mir.test2 ()"
-ML "Mir.test' ()"
-ML "Mir.test2' ()"
ML "Mir.test3 ()"
+ML "Mir.test4 ()"
+ML "Mir.test5 ()"
+ML "reset Toplevel.timing"
use "mireif.ML"
oracle mircfr_oracle ("term") = ReflectedMir.mircfr_oracle
oracle mirlfr_oracle ("term") = ReflectedMir.mirlfr_oracle
-use"mirtac.ML"
+use "mirtac.ML"
setup "MirTac.setup"
ML "set Toplevel.timing"
+
lemma "ALL (x::real). (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))"
apply mir
done
@@ -5788,10 +5830,10 @@
apply mir
done
-
lemma "ALL (x::real). \<exists>y \<le> x. (\<lfloor>x\<rfloor> = \<lceil>y\<rceil>)"
apply mir
done
+
ML "reset Toplevel.timing"
end
--- a/src/HOL/Complex/ex/mireif.ML Thu Jul 19 21:47:44 2007 +0200
+++ b/src/HOL/Complex/ex/mireif.ML Thu Jul 19 21:47:45 2007 +0200
@@ -1,6 +1,9 @@
-(*
- The oracle for Mixed Real-Integer auantifier elimination
- based on the verified Code in ~/work/MIR/MIR.thy
+(* Title: HOL/Complex/ex/mireif.ML
+ ID: $Id$
+ Author: Amine Chaieb, TU Muenchen
+
+Oracle for Mixed Real-Integer auantifier elimination
+based on the verified code in HOL/Complex/ex/MIR.thy.
*)
structure ReflectedMir =
@@ -10,20 +13,11 @@
exception MIR;
-(* pseudo reification : term -> intterm *)
-val iT = HOLogic.intT;
-val rT = Type ("RealDef.real",[]);
-val bT = HOLogic.boolT;
-val realC = @{term "real :: int => _"};
-val floorC = @{term "floor"};
-val ceilC = @{term "ceiling"};
-val rzero = @{term "0::real"};
-
fun num_of_term vs t =
case t of
- Free(xn,xT) => (case AList.lookup (op =) vs t of
- NONE => error "Variable not found in the list!!"
- | SOME n => Bound n)
+ Free(xn,xT) => (case AList.lookup (op =) vs t of
+ NONE => error "Variable not found in the list!"
+ | SOME n => Bound n)
| Const("RealDef.real",_)$ @{term "0::int"} => C 0
| Const("RealDef.real",_)$ @{term "1::int"} => C 1
| @{term "0::real"} => C 0
@@ -33,99 +27,99 @@
| Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
| Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
| Const (@{const_name "HOL.times"},_)$t1$t2 =>
- (case (num_of_term vs t1) of C i =>
- Mul (i,num_of_term vs t2)
- | _ => error "num_of_term: unsupported Multiplication")
+ (case (num_of_term vs t1) of C i =>
+ Mul (i,num_of_term vs t2)
+ | _ => error "num_of_term: unsupported Multiplication")
| Const("RealDef.real",_)$ (Const (@{const_name "RComplete.floor"},_)$ t') => Floor (num_of_term vs t')
| Const("RealDef.real",_)$ (Const (@{const_name "RComplete.ceiling"},_)$ t') => Neg(Floor (Neg (num_of_term vs t')))
| Const("RealDef.real",_) $ Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
| Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
| _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t));
-
+
(* pseudo reification : term -> fm *)
fun fm_of_term vs t =
case t of
- Const("True",_) => T
+ Const("True",_) => T
| Const("False",_) => F
- | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2))
- | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2))
- | Const (@{const_name "MIR.op rdvd"},_)$(Const("RealDef.real",_)$(Const(@{const_name "Numeral.number_of"},_)$t1))$t2 =>
- Dvd(HOLogic.dest_numeral t1,num_of_term vs t2)
+ | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
+ | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
+ | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 =>
+ Dvda (HOLogic.dest_numeral t1, num_of_term vs t2)
| Const("op =",eqT)$t1$t2 =>
- if (domain_type eqT = rT)
- then Eq (Sub (num_of_term vs t1,num_of_term vs t2))
- else Iff(fm_of_term vs t1,fm_of_term vs t2)
- | Const("op &",_)$t1$t2 => And(fm_of_term vs t1,fm_of_term vs t2)
- | Const("op |",_)$t1$t2 => Or(fm_of_term vs t1,fm_of_term vs t2)
- | Const("op -->",_)$t1$t2 => Imp(fm_of_term vs t1,fm_of_term vs t2)
- | Const("Not",_)$t' => NOT(fm_of_term vs t')
+ if (domain_type eqT = @{typ real})
+ then Eqa (Sub (num_of_term vs t1, num_of_term vs t2))
+ else Iffa (fm_of_term vs t1, fm_of_term vs t2)
+ | Const("op &",_)$t1$t2 => And (fm_of_term vs t1, fm_of_term vs t2)
+ | Const("op |",_)$t1$t2 => Or (fm_of_term vs t1, fm_of_term vs t2)
+ | Const("op -->",_)$t1$t2 => Impa (fm_of_term vs t1, fm_of_term vs t2)
+ | Const("Not",_)$t' => Nota (fm_of_term vs t')
| Const("Ex",_)$Abs(xn,xT,p) =>
- E(fm_of_term (map (fn(v,n) => (v,Suc n)) vs) p)
+ E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
| Const("All",_)$Abs(xn,xT,p) =>
- A(fm_of_term (map (fn(v,n) => (v,Suc n)) vs) p)
- | _ => error ("fm_of_term : unknown term!" ^ (Display.raw_string_of_term t));
-
-fun zip [] [] = []
- | zip (x::xs) (y::ys) = (x,y)::(zip xs ys);
-
+ A (fm_of_term (map (fn(v, n) => (v, Suc n)) vs) p)
+ | _ => error ("fm_of_term : unknown term!" ^ Display.raw_string_of_term t);
fun start_vs t =
let val fs = term_frees t
- in zip fs (map nat (0 upto (length fs - 1)))
+ in fs ~~ map nat (0 upto (length fs - 1))
end ;
(* transform num and fm back to terms *)
fun myassoc2 l v =
case l of
- [] => NONE
+ [] => NONE
| (x,v')::xs => if v = v' then SOME x
- else myassoc2 xs v;
+ else myassoc2 xs v;
+
+val realC = @{term "real :: int => _"};
+val rzero = @{term "0::real"};
fun term_of_num vs t =
case t of
- C i => realC $ (HOLogic.mk_number HOLogic.intT i)
+ C i => realC $ (HOLogic.mk_number HOLogic.intT i)
| Bound n => valOf (myassoc2 vs n)
- | Neg (Floor (Neg t')) => realC $ (ceilC $ (term_of_num vs t'))
+ | Neg (Floor (Neg t')) => realC $ (@{term "ceiling"} $ term_of_num vs t')
| Neg t' => @{term "uminus:: real => _"} $ term_of_num vs t'
| Add(t1,t2) => @{term "op +:: real => _"} $ term_of_num vs t1 $ term_of_num vs t2
| Sub(t1,t2) => @{term "op -:: real => _"} $ term_of_num vs t1 $ term_of_num vs t2
| Mul(i,t2) => @{term "op -:: real => _"} $ term_of_num vs (C i) $ term_of_num vs t2
- | Floor t => realC $ (floorC $ (term_of_num vs t))
- | CN(n,i,t) => term_of_num vs (Add(Mul(i,Bound n),t))
- | CF(c,t,s) => term_of_num vs (Add(Mul(c,Floor t),s));
+ | Floor t => realC $ (@{term "floor"} $ term_of_num vs t)
+ | Cn(n,i,t) => term_of_num vs (Add(Mul(i,Bound n),t))
+ | Cf(c,t,s) => term_of_num vs (Add(Mul(c,Floor t),s));
fun term_of_fm vs t =
case t of
- T => HOLogic.true_const
+ T => HOLogic.true_const
| F => HOLogic.false_const
- | Lt t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero
- | Le t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero
- | Gt t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t
- | Ge t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t
- | Eq t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero
- | NEq t => term_of_fm vs (NOT (Eq t))
- | NDvd (i,t) => term_of_fm vs (NOT (Dvd (i,t)))
- | Dvd (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t
- | NOT t' => HOLogic.Not$(term_of_fm vs t')
+ | Lta t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero
+ | Lea t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero
+ | Gta t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t
+ | Gea t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t
+ | Eqa t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero
+ | NEq t => term_of_fm vs (Nota (Eqa t))
+ | NDvd (i,t) => term_of_fm vs (Nota (Dvda (i,t)))
+ | Dvda (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t
+ | Nota t' => HOLogic.Not$(term_of_fm vs t')
| And(t1,t2) => HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
| Or(t1,t2) => HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
- | Imp(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
- | Iff(t1,t2) => HOLogic.eq_const bT $ term_of_fm vs t1 $ term_of_fm vs t2
+ | Impa(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
+ | Iffa(t1,t2) => HOLogic.mk_eq (term_of_fm vs t1, term_of_fm vs t2)
| _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
(* The oracle *)
fun mircfr_oracle thy t =
let
- val vs = start_vs t
+ val vs = start_vs t
in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm vs (mircfrqe (fm_of_term vs t))))
end;
fun mirlfr_oracle thy t =
let
- val vs = start_vs t
+ val vs = start_vs t
in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm vs (mirlfrqe (fm_of_term vs t))))
end;
+
end;