(*
ID: $Id$
Author: Amine Chaieb, TU Muenchen
LCF proof synthesis for Ferrante and Rackoff.
*)
structure Ferrante_Rackoff_Proof:
sig
val qelim: cterm -> thm
exception FAILURE of string
end =
struct
(* Some certified types *)
val cbT = @{ctyp bool};
val rT = @{typ RealDef.real};
val crT = @{ctyp RealDef.real};
(* Normalization*)
(* Computation of uset *)
fun uset x fm =
case fm of
Const("op &",_)$p$q => fold (insert (op =)) (uset x p) (uset x q)
| Const("op |",_)$p$q => fold (insert (op =)) (uset x p) (uset x q)
| Const(@{const_name Orderings.less},_)$s$t => if s=x then [t]
else if t = x then [s]
else []
| Const(@{const_name Orderings.less_eq},_)$s$t => if s=x then [t]
else if t = x then [s]
else []
| Const("op =",_)$s$t => if s=x then [t]
else []
| Const("Not",_)$ (Const("op =",_)$s$t) => if s=x then [t]
else []
| _ => [];
val rsT = @{typ "RealDef.real set"};
fun holrealset [] = @{term "{} :: RealDef.real set"}
| holrealset (x::xs) = @{term "insert :: RealDef.real => RealDef.real set => RealDef.real set"}
$ x $ holrealset xs;
fun prove_bysimp thy ss t = Goal.prove (ProofContext.init thy) [] []
(HOLogic.mk_Trueprop t) (fn _ => simp_tac ss 1);
fun inusetthms sg x fm =
let val U = uset x fm
val hU = holrealset U
fun inC T = Const("op :",[T,Type("set",[T])] ---> HOLogic.boolT);
val ss = simpset_of sg
fun proveinU t = prove_bysimp sg ss ((inC rT)$t$hU)
val uf = prove_bysimp sg ss (Const ("Finite_Set.finite", rsT --> HOLogic.boolT) $ hU)
in (U,cterm_of sg hU,map proveinU U,uf)
end;
(* Theorems for minus/plusinfinity *)
val [minf_lt,minf_gt,minf_le,minf_ge,minf_eq,minf_neq,minf_fm,minf_conj,minf_disj] = thms"minf";
val [pinf_lt,pinf_gt,pinf_le,pinf_ge,pinf_eq,pinf_neq,pinf_fm,pinf_conj,pinf_disj] = thms"pinf";
(* Theorems for boundedness from below/above *)
val [nmilbnd_lt,nmilbnd_gt,nmilbnd_le,nmilbnd_ge,nmilbnd_eq,nmilbnd_neq,nmilbnd_fm,nmilbnd_conj,nmilbnd_disj] = thms"nmilbnd";
val [npiubnd_lt,npiubnd_gt,npiubnd_le,npiubnd_ge,npiubnd_eq,npiubnd_neq,npiubnd_fm,npiubnd_conj,npiubnd_disj] = thms"npiubnd";
(* Theorems for no changes over smallest intervals in U *)
val lin_dense_lt = thm "lin_dense_lt";
val lin_dense_le = thm "lin_dense_le";
val lin_dense_gt = thm "lin_dense_gt";
val lin_dense_ge = thm "lin_dense_ge";
val lin_dense_eq = thm "lin_dense_eq";
val lin_dense_neq = thm "lin_dense_neq";
val lin_dense_conj = thm "lin_dense_conj";
val lin_dense_disj = thm "lin_dense_disj";
val lin_dense_fm = thm "lin_dense_fm";
val fr_eq = thm "fr_eq";
val fr_simps = thms "fr_simps";
fun dest5 [] = ([],[],[],[],[])
| dest5 ((x,y,z,w,v)::xs) =
let val (x',y',z',w',v') = dest5 xs
in (x::x',y::y',z::z',w::w',v::v') end ;
fun dest2 [] = ([],[])
| dest2 ((x,y)::xs) = let val (x',y') = dest2 xs
in (x::x',y::y') end ;
fun myfwd (th1,th2,th3,th4,th5) xs =
let val (ths1,ths2,ths3,ths4,ths5) = dest5 xs
in (ths1 MRS th1,ths2 MRS th2,ths3 MRS th3,ths4 MRS th4, ths5 MRS th5)
end;
fun myfwd2 (th1,th2) xs =
let val (ths1,ths2) = dest2 xs
in (ths1 MRS th1,ths2 MRS th2)
end;
fun decomp_mpinf sg x (U,CU,uths) fm =
let val cx = cterm_of sg x in
(case fm of
Const("op &",_)$p$q =>
([p,q],myfwd (minf_conj,pinf_conj, nmilbnd_conj, npiubnd_conj,lin_dense_conj))
| Const("op |",_)$p$q =>
([p,q],myfwd (minf_disj,pinf_disj, nmilbnd_disj,npiubnd_disj,lin_dense_disj))
| Const(@{const_name Orderings.less},_)$s$t =>
if s= x then
let val ct = cterm_of sg t
val tinU = nth uths (find_index (fn a => a=t) U)
val mith = instantiate' [] [SOME ct] minf_lt
val pith = instantiate' [] [SOME ct] pinf_lt
val nmilth = tinU RS nmilbnd_lt
val npiuth = tinU RS npiubnd_lt
val lindth = tinU RS lin_dense_lt
in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
end
else if t = x then
let val ct = cterm_of sg s
val tinU = nth uths (find_index (fn a => a=s) U)
val mith = instantiate' [] [SOME ct] minf_gt
val pith = instantiate' [] [SOME ct] pinf_gt
val nmilth = tinU RS nmilbnd_gt
val npiuth = tinU RS npiubnd_gt
val lindth = tinU RS lin_dense_gt
in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
end
else
let val cfm = cterm_of sg fm
val mith = instantiate' [] [SOME cfm] minf_fm
val pith = instantiate' [] [SOME cfm] pinf_fm
val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
end
| Const(@{const_name Orderings.less_eq},_)$s$t =>
if s= x then
let val ct = cterm_of sg t
val tinU = nth uths (find_index (fn a => a=t) U)
val mith = instantiate' [] [SOME ct] minf_le
val pith = instantiate' [] [SOME ct] pinf_le
val nmilth = tinU RS nmilbnd_le
val npiuth = tinU RS npiubnd_le
val lindth = tinU RS lin_dense_le
in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
end
else if t = x then
let val ct = cterm_of sg s
val tinU = nth uths (find_index (fn a => a=s) U)
val mith = instantiate' [] [SOME ct] minf_ge
val pith = instantiate' [] [SOME ct] pinf_ge
val nmilth = tinU RS nmilbnd_ge
val npiuth = tinU RS npiubnd_ge
val lindth = tinU RS lin_dense_ge
in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
end
else
let val cfm = cterm_of sg fm
val mith = instantiate' [] [SOME cfm] minf_fm
val pith = instantiate' [] [SOME cfm] pinf_fm
val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
end
| Const("op =",_)$s$t =>
if s= x then
let val ct = cterm_of sg t
val tinU = nth uths (find_index (fn a => a=t) U)
val mith = instantiate' [] [SOME ct] minf_eq
val pith = instantiate' [] [SOME ct] pinf_eq
val nmilth = tinU RS nmilbnd_eq
val npiuth = tinU RS npiubnd_eq
val lindth = tinU RS lin_dense_eq
in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
end
else
let val cfm = cterm_of sg fm
val mith = instantiate' [] [SOME cfm] minf_fm
val pith = instantiate' [] [SOME cfm] pinf_fm
val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
end
| Const("Not",_)$(Const("op =",_)$s$t) =>
if s= x then
let val ct = cterm_of sg t
val tinU = nth uths (find_index (fn a => a=t) U)
val mith = instantiate' [] [SOME ct] minf_neq
val pith = instantiate' [] [SOME ct] pinf_neq
val nmilth = tinU RS nmilbnd_neq
val npiuth = tinU RS npiubnd_neq
val lindth = tinU RS lin_dense_neq
in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
end
else
let val cfm = cterm_of sg fm
val mith = instantiate' [] [SOME cfm] minf_fm
val pith = instantiate' [] [SOME cfm] pinf_fm
val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
end
| _ => let val cfm = cterm_of sg fm
val mith = instantiate' [] [SOME cfm] minf_fm
val pith = instantiate' [] [SOME cfm] pinf_fm
val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
end)
end;
fun ferrack_eq thy p =
case p of
Const("Ex",_)$Abs(x1,T,p1) =>
let val (xn,fm) = Syntax.variant_abs(x1,T,p1)
val x = Free(xn,T)
val (u,cu,uths,uf) = inusetthms thy x fm
val (mi,pi,nmi,npi,lind) = divide_and_conquer (decomp_mpinf thy x (u,cu,uths)) fm
val frth = [uf,lind,nmi,npi,mi,pi] MRS fr_eq
val (cTp,ceq) = Thm.dest_comb (cprop_of frth)
val qth = (Simplifier.rewrite (HOL_basic_ss addsimps fr_simps addsimps [refl])
(snd (Thm.dest_comb ceq))) RS meta_eq_to_obj_eq
in [frth,qth] MRS trans
end
| _ => instantiate' [SOME cbT] [SOME (cterm_of thy p)] refl;
(* Code for normalization of terms and Formulae *)
(* For NNF reuse the CooperProof methods*)
(*FIXME:: This is copied from cooper_proof.ML *)
val FWD = fn th => fn ths => ths MRS th;
val qe_Not = thm "qe_Not";
val qe_conjI = thm "qe_conjI";
val qe_disjI = thm "qe_disjI";
val qe_impI = thm "qe_impI";
val qe_eqI = thm "qe_eqI";
val qe_exI = thm "qe_exI";
val qe_ALLI = thm "qe_ALLI";
val nnf_nn = thm "nnf_nn";
val nnf_im = thm "nnf_im";
val nnf_eq = thm "nnf_eq";
val nnf_sdj = thm "nnf_sdj";
val nnf_ncj = thm "nnf_ncj";
val nnf_nim = thm "nnf_nim";
val nnf_neq = thm "nnf_neq";
val nnf_ndj = thm "nnf_ndj";
fun negate (Const ("Not",_) $ p) = p
|negate p = (HOLogic.Not $ p);
fun decomp_cnnf lfnp P =
case P of
Const ("op &",_) $ p $q => ([p,q] , FWD qe_conjI )
| Const ("op |",_) $ p $q => ([p,q] , FWD qe_disjI)
| Const ("Not",_) $ (Const("Not",_) $ p) => ([p], FWD nnf_nn)
| Const("Not",_) $ (Const(opn,T) $ p $ q) =>
if opn = "op |"
then
(case (p,q) of
(A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
if r1 = negate r
then ([r,HOLogic.Not$s,r1,HOLogic.Not$t],
fn [th1_1,th1_2,th2_1,th2_2] =>
[[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj)
else ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj)
| (_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj))
else (
case (opn,T) of
("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ncj )
| ("op -->",_) => ([p,HOLogic.Not $ q ], FWD nnf_nim )
| ("op =",Type ("fun",[Type ("bool", []),_])) =>
([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q],
FWD nnf_neq)
| (_,_) => ([], fn [] => lfnp P))
| (Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], FWD nnf_im)
| (Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) =>
([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], FWD nnf_eq )
| _ => ([], fn [] => lfnp P);
fun nnfp afnp vs p =
let val th = divide_and_conquer (decomp_cnnf (afnp vs)) p
val Pth = (Simplifier.rewrite
(HOL_basic_ss addsimps fr_simps addsimps [refl])
(snd(Thm.dest_comb(snd(Thm.dest_comb (cprop_of th))))))
RS meta_eq_to_obj_eq
in [th,Pth] MRS trans
end;
(* Normalization of arithmetical expressions *)
val rzero = HOLogic.mk_number rT 0;
val rone = HOLogic.mk_number rT 1;
fun mk_real i = HOLogic.mk_number rT i;
val dest_real = snd o HOLogic.dest_number;
(* Normal form for terms is:
(c0*x0 + ... + cn*xn + k) / c , where ci!=0 and x0<..<xn ordered according to vs*)
(* functions to prove trivial properties about numbers *)
fun proveq thy n m = prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq(mk_real n,mk_real m));
fun provenz thy n =
prove_bysimp thy (simpset_of thy) (HOLogic.Not$(HOLogic.mk_eq(mk_real n,rzero)));
fun proveprod thy m n =
prove_bysimp thy (simpset_of thy)
(HOLogic.mk_eq(HOLogic.mk_binop @{const_name HOL.times} (mk_real m,mk_real n),mk_real (m*n)));
fun proveadd thy m n =
prove_bysimp thy (simpset_of thy)
(HOLogic.mk_eq(HOLogic.mk_binop @{const_name HOL.plus} (mk_real m,mk_real n),mk_real (m+n)));
fun provediv thy m n =
let val g = Integer.gcd m n
val m' = m div g
val n'= n div g
in
(prove_bysimp thy (simpset_of thy)
(HOLogic.mk_eq(HOLogic.mk_binop @{const_name HOL.divide} (mk_real m,mk_real n),
HOLogic.mk_binop @{const_name HOL.divide}
(mk_real m',mk_real n'))),m')
end;
(* Multiplication of a normal term by a constant *)
val ncmul_congh = thm "ncmul_congh";
val ncmul_cong = thm "ncmul_cong";
fun decomp_ncmulh thy c t =
if c = 0 then ([],fn _ => instantiate' [SOME crT] [SOME (cterm_of thy t)] @{thm mult_zero_left}) else
case t of
Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c'$v)$b =>
([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)]
((proveprod thy c (dest_real c')) RS ncmul_congh)))
| _ => ([],fn _ => proveprod thy c (dest_real t));
fun prove_ncmulh thy c = divide_and_conquer (decomp_ncmulh thy c);
(* prove_ncmul thy n t n = a theorem : "c*(t/n) = (t'/n')*)
fun prove_ncmul thy c (t,m) =
let val (eq1,c') = provediv thy c m
val tt' = prove_ncmulh thy c' t
in [eq1,tt'] MRS ncmul_cong
end;
(* prove_nneg returns "-(t/n) = t'/n'" ; normally t'=t and n' = -n*)
val nneg_cong = thm "nneg_cong";
fun prove_nneg thy (t,m) = (prove_ncmul thy ~1 (t, m)) RS nneg_cong;
(* Addition of 2 expressions in normal form*)
val naddh_cong_same = thm "naddh_cong_same";
val naddh_cong_same0 = thm "naddh_cong_same0";
val naddh_cong_ts = thm "naddh_cong_ts";
val naddh_cong_st = thm "naddh_cong_st";
fun earlier [] x y = false
| earlier (h::t) x y =
if h = y then false
else if h = x then true
else earlier t x y ;
fun decomp_naddh thy vs (t,s) =
case (t,s) of
(Const(@{const_name HOL.plus},_)$(ctv as Const(@{const_name HOL.times},_)$tc$tv)$tr,
Const(@{const_name HOL.plus},_)$(csv as Const(@{const_name HOL.times},_)$sc$sv)$sr) =>
if tv = sv then
let val ntc = dest_real tc
val nsc = dest_real sc
val addth = proveadd thy ntc nsc
in if ntc + nsc = 0
then ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)]
(addth RS naddh_cong_same0)))
else ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)]
(addth RS naddh_cong_same)))
end
else if earlier vs tv sv
then ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
else ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
| (Const(@{const_name HOL.plus},_)$(ctv as Const(@{const_name HOL.times},_)$tc$tv)$tr,_) =>
([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
| (_,Const(@{const_name HOL.plus},_)$(csv as Const(@{const_name HOL.times},_)$sc$sv)$sr) =>
([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
| (_,_) => ([], fn _ => proveadd thy (dest_real t) (dest_real s));
(* prove_naddh returns "t + s = t'*)
fun prove_naddh thy vs = divide_and_conquer (decomp_naddh thy vs);
val nadd_cong_same = thm "nadd_cong_same";
val nadd_cong = thm "nadd_cong";
val plus_cong = thm "plus_cong";
(* prove_nadd resturns: "t/m + s/n = t'/m'"*)
fun prove_nadd thy vs (t,m) (s,n) =
if n=m then
let val nm = proveq thy n m
val ts = prove_naddh thy vs (t,s)
in [nm,ts] MRS nadd_cong_same
end
else let val l = Integer.lcm m n
val m' = l div m
val n' = l div n
val mml = proveprod thy m' m
val nnl = proveprod thy n' n
val mnz = provenz thy m
val nnz = provenz thy n
val lnz = provenz thy l
val mt = prove_ncmulh thy m' t
val ns = prove_ncmulh thy n' s
val _$(_$_$t') = prop_of mt
val _$(_$_$s') = prop_of ns
in [mml,nnl,mnz,nnz,lnz,[mt,ns,prove_naddh thy vs (t',s')] MRS plus_cong]
MRS nadd_cong
end;
(* prove_nsub returns: "t/m - s/n = t'/m'"*)
val nsub_cong = thm "nsub_cong";
fun prove_nsub thy vs (t,m) (s,n) =
let val nsm = prove_nneg thy (s,n)
val _$(_$_$(_$s'$n')) = prop_of nsm
val ts = prove_nadd thy vs (t,m) (s',dest_real n')
in [nsm,ts] MRS nsub_cong
end;
val ndivide_cong = thm "ndivide_cong";
fun prove_ndivide thy (t,m) n = instantiate' [] [SOME(cterm_of thy t)]
((proveprod thy m n) RS ndivide_cong);
exception FAILURE of string;
val divide_cong = thm"divide_cong";
val diff_cong = thm"diff_cong";
val uminus_cong = thm"uminus_cong";
val mult_cong = thm"mult_cong";
val mult_cong2 = thm"mult_cong2";
val normalizeh_var = thm "normalizeh_var";
val nrefl = thm "nrefl";
fun decomp_normalizeh thy vs t =
case t of
Free _ => ([], fn _ => instantiate' [] [SOME(cterm_of thy t)] normalizeh_var)
| Const(@{const_name HOL.uminus},_)$a =>
([a],
fn [tha] => let val _$(_$_$(_$a'$n')) = prop_of tha
in [tha,prove_nneg thy (a',dest_real n')]
MRS uminus_cong
end )
| Const(@{const_name HOL.plus},_)$a$b =>
([a,b],
fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
val _$(_$_$(_$b'$m')) = prop_of thb
in [tha,thb,prove_nadd thy vs (a',dest_real n') (b',dest_real m')]
MRS plus_cong
end )
| Const(@{const_name HOL.minus},_)$a$b =>
([a,b],
fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
val _$(_$_$(_$b'$m')) = prop_of thb
in [tha,thb,prove_nsub thy vs (a',dest_real n') (b',dest_real m')]
MRS diff_cong
end )
| Const(@{const_name HOL.times},_)$a$b =>
if can dest_real a
then ([b], fn [thb] =>
let val _$(_$_$(_$b'$m')) = prop_of thb
in [thb, prove_ncmul thy (dest_real a) (b',dest_real m')] MRS mult_cong
end )
else if can dest_real b
then ([a], fn [tha] =>
let val _$(_$_$(_$a'$m')) = prop_of tha
in [tha, prove_ncmul thy (dest_real b) (a',dest_real m')] MRS mult_cong2
end )
else raise FAILURE "decomp_normalizeh: non linear term"
| Const(@{const_name HOL.divide},_)$a$b =>
if can dest_real b
then ([a], fn [tha] =>
let val _$(_$_$(_$a'$m')) = prop_of tha
in [tha, prove_ndivide thy (a',dest_real m') (dest_real b)] MRS divide_cong
end )
else raise FAILURE "decomp_normalizeh: non linear term"
| _ => ([], fn _ => instantiate' [] [SOME (cterm_of thy t)] nrefl);
fun prove_normalizeh thy vs = divide_and_conquer (decomp_normalizeh thy vs);
fun dest_xth vs th =
let val _$(_$_$(_$t$n)) = prop_of th
in (case t of
Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$r =>
if vs = [] then (0,t,dest_real n)
else if hd vs = y then (dest_real c, r,dest_real n)
else (0,t,dest_real n)
| _ => (0,t,dest_real n))
end;
fun prove_strictsign thy n =
prove_bysimp thy (simpset_of thy)
(HOLogic.mk_binrel @{const_name Orderings.less}
(if n > 0 then (rzero, mk_real n) else (mk_real n, rzero)));
fun prove_fracsign thy (m,n) =
let val mn = HOLogic.mk_binop @{const_name HOL.divide} (mk_real m, mk_real n)
in prove_bysimp thy (simpset_of thy)
(HOLogic.mk_binrel @{const_name Orderings.less}
(if m*n > 0 then (rzero, mn) else (mn, rzero)))
end;
fun holbool_of true = HOLogic.true_const
| holbool_of false = HOLogic.false_const;
fun prove_fracsign_eq thy s (m,n) =
let fun f s = the (AList.lookup (op =) [(@{const_name Orderings.less}, op <),(@{const_name Orderings.less_eq}, op <=),("op =", op =)] s)
in
prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq
(HOLogic.mk_binrel s
(HOLogic.mk_binop @{const_name HOL.divide} (mk_real m, mk_real n),rzero),
holbool_of (f s (m*n,0))))
end;
fun proveq_eq thy n m =
prove_bysimp thy (simpset_of thy)
(HOLogic.mk_eq
(HOLogic.mk_eq(mk_real n, mk_real m),holbool_of (n = m)));
val sum_of_same_denoms = thm "sum_of_same_denoms";
val sum_of_opposite_denoms = thm "sum_of_opposite_denoms";
val trivial_sum_of_opposites = thm "trivial_sum_of_opposites";
val normalize_ltground_cong = thm "normalize_ltground_cong";
val normalize_ltnoxpos_cong = thm "normalize_ltnoxpos_cong";
val normalize_ltnoxneg_cong = thm "normalize_ltnoxneg_cong";
val normalize_ltxpos_cong = thm "normalize_ltxpos_cong";
val normalize_ltxneg_cong = thm "normalize_ltxneg_cong";
val normalize_leground_cong = thm "normalize_leground_cong";
val normalize_lenoxpos_cong = thm "normalize_lenoxpos_cong";
val normalize_lenoxneg_cong = thm "normalize_lenoxneg_cong";
val normalize_lexpos_cong = thm "normalize_lexpos_cong";
val normalize_lexneg_cong = thm "normalize_lexneg_cong";
val normalize_eqground_cong = thm "normalize_eqground_cong";
val normalize_eqnox_cong = thm "normalize_eqnox_cong";
val normalize_eqxpos_cong = thm "normalize_eqxpos_cong";
val normalize_eqxneg_cong = thm "normalize_eqxneg_cong";
val normalize_not_lt = thm "normalize_not_lt";
val normalize_not_le = thm "normalize_not_le";
val normalize_not_eq = thm "normalize_not_eq";
fun prove_normalize thy vs at =
case at of
Const(@{const_name Orderings.less},_)$s$t =>
let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop @{const_name HOL.minus} (s,t))
val (cx,r,n) = dest_xth vs smtth
in if cx = 0 then if can dest_real r
then [smtth, prove_fracsign_eq thy @{const_name Orderings.less} (dest_real r, n)]
MRS normalize_ltground_cong
else [smtth, prove_strictsign thy n]
MRS (if n > 0 then normalize_ltnoxpos_cong
else normalize_ltnoxneg_cong)
else let val srn = prove_fracsign thy (n,cx)
val rr' = if cx < 0
then instantiate' [] [SOME (cterm_of thy r)]
((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
else instantiate' [] [SOME (cterm_of thy (mk_real cx))]
(((prove_ncmulh thy ~1 r) RS nneg_cong)
RS sum_of_same_denoms)
in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_ltxneg_cong
else normalize_ltxpos_cong)
end
end
| Const(@{const_name Orderings.less_eq},_)$s$t =>
let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop @{const_name HOL.minus} (s,t))
val (cx,r,n) = dest_xth vs smtth
in if cx = 0 then if can dest_real r
then [smtth, prove_fracsign_eq thy @{const_name Orderings.less_eq} (dest_real r, n)]
MRS normalize_leground_cong
else [smtth, prove_strictsign thy n]
MRS (if n > 0 then normalize_lenoxpos_cong
else normalize_lenoxneg_cong)
else let val srn = prove_fracsign thy (n,cx)
val rr' = if cx < 0
then instantiate' [] [SOME (cterm_of thy r)]
((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
else instantiate' [] [SOME (cterm_of thy (mk_real cx))]
(((prove_ncmulh thy ~1 r) RS nneg_cong)
RS sum_of_same_denoms)
in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_lexneg_cong
else normalize_lexpos_cong)
end
end
| Const("op =",_)$s$t =>
let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop @{const_name HOL.minus} (s,t))
val (cx,r,n) = dest_xth vs smtth
in if cx = 0 then if can dest_real r
then [smtth, provenz thy n,
proveq_eq thy (dest_real r) 0]
MRS normalize_eqground_cong
else [smtth, provenz thy n]
MRS normalize_eqnox_cong
else let val scx = prove_strictsign thy cx
val nnz = provenz thy n
val rr' = if cx < 0
then proveadd thy cx (~cx)
else ((prove_ncmulh thy ~1 r) RS nneg_cong)
RS trivial_sum_of_opposites
in [smtth,scx,nnz,rr'] MRS (if cx < 0 then normalize_eqxneg_cong
else normalize_eqxpos_cong)
end
end
| Const("Not",_)$(Const(@{const_name Orderings.less},T)$s$t) =>
(prove_normalize thy vs (Const(@{const_name Orderings.less_eq},T)$t$s)) RS normalize_not_lt
| Const("Not",_)$(Const(@{const_name Orderings.less_eq},T)$s$t) =>
(prove_normalize thy vs (Const(@{const_name Orderings.less},T)$t$s)) RS normalize_not_le
| (nt as Const("Not",_))$(Const("op =",T)$s$t) =>
(prove_normalize thy vs (Const("op =",T)$s$t)) RS qe_Not
| _ => instantiate' [SOME cbT] [SOME (cterm_of thy at)] refl;
(* Generic quantifier elimination *)
val qe_ex_conj = thm "qe_ex_conj";
val qe_ex_nconj = thm "qe_ex_nconj";
val qe_ALL = thm "qe_ALL";
val ex_eq_cong = thm "ex_eq_cong";
fun get_terms th =
let
val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) =
prop_of th
in (A,B) end;
fun decomp_genqelim thy afnp nfnp qfnp (P,vs) =
case P of
(Const("op &",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_conjI)
| (Const("op |",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_disjI)
| (Const("op -->",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_impI)
| (Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) =>
([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_eqI)
| (Const("Not",_)$p) => ([(p,vs)],fn [th] => th RS qe_Not)
| (Const("Ex",_)$Abs(xn,xT,p)) =>
let val (xn1,p1) = Syntax.variant_abs(xn,xT,p)
val x= Free(xn1,xT)
in ([(p1,x::vs)],
fn [th1_1] =>
let val th2 = [th1_1,nfnp (x::vs) (snd (get_terms th1_1))] MRS trans
val eth1 = (forall_intr (cterm_of thy (Free(xn1,xT))) th2) COMP ex_eq_cong
val th3 = qfnp (snd(get_terms eth1))
in [eth1,th3] MRS trans
end )
end
| (Const("All",_)$Abs(xn,xT,p)) =>
([((HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p),vs)], fn [th] => th RS qe_ALL)
| _ => ([], fn [] => afnp vs P);
val fr_prepqelim = thms "fr_prepqelim";
val prepare_qelim_ss = HOL_basic_ss
addsimps simp_thms
addsimps (List.take(ex_simps,4))
addsimps fr_prepqelim
addsimps [not_all,ex_disj_distrib];
fun prove_genqelim thy afnp nfnp qfnp P =
let val thP = (Simplifier.rewrite prepare_qelim_ss P) RS meta_eq_to_obj_eq
val _$(_$_$P') = prop_of thP
val vs = term_frees P'
val qeth = divide_and_conquer (decomp_genqelim thy afnp nfnp qfnp) (Pattern.eta_long [] P',vs)
val _$(_$_$p'') = prop_of qeth
val thp' = nfnp vs p''
in [[thP, qeth] MRS trans, thp'] MRS trans
end;
fun qelim P =
let val {thy, ...} = Thm.rep_cterm P
in prove_genqelim thy (prove_normalize thy) (nnfp (prove_normalize thy)) (ferrack_eq thy) P end;
(* Just for testing!! *)
(*
val thy = the_context();
fun parseb s = term_of (read_cterm thy (s,HOLogic.boolT));
fun parser s = term_of (read_cterm thy (s,rT));
val fm = parseb "(x::real) < y + t & (y - 5 < x | 34 < y + t) & (x = s + 3*y) | (x ~= y - s)";
provediv thy 4 2;
provediv thy ~4 2;
provediv thy 4 ~2;
provediv thy 44 32;
provediv thy ~34 20000;
provediv thy ~4000000 ~27676;
val vs = [Free("x",rT),Free("y",rT),Free("z",rT)] ;
prove_nsub thy vs
(parser "4*(x::real) + (3*y + 5)" ,54) (parser "3*(y::real) + (4*z + 5)",9);
prove_ndivide thy (parser "4*(x::real) + (3*y + 5)" ,5) 4;
prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)]
(parser "4*(x::real) + 3* ((3*y + 5) + x)");
prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)]
(parser "4*(x::real) - 3* ((3*y + 5)*9 + x)");
prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)]
(parser "- x");
prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)]
(parser "4*(x::real) +3* ((3*y + 5) / 3 - (- x))");
fun test xn s = ferrack_eq thy (parseb ("EX (" ^ xn ^ "::real)." ^ s));
test "x" "(x::real) < y + t & (y - 5 < x | 34 < y + t) & (x = s + 3*y) | (x ~= y - s) & (x::real) <= y + t & (y - 5 <= x)";
test "x" "(x::real) < y + t & y - 5 < x & (x ~= y - s)";
test "x" "(x::real) < y + t";
test "x" "(x::real) > y + t";
test "x" "(x::real) = y + t";
test "x" "(x::real) ~= y + t";
test "x" "34 < y + (t::real)";
test "x" "(x::real) ~= y + t & 34 < y + (t::real)";
test "x" "(x::real) ~= y + t & (x::real) < y + t";
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= 3*x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= (-1)*x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= x + 3 + 4* (y - 15*z) / 3 ");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < 3*x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < (-1)*x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < x + 3 + 4* (y - 15*z) / 3 ");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = 3*x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = (-1)*x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = x + 3 + 4* (y - 15*z) / 3 ");
prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= x + y)");
prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= 3*x + y)");
prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= (-1)*x + y)");
prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= x + 3 + 4* (y - 15*z) / 3 )");
prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < x + y)");
prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < 3*x + y)");
prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < (-1)*x + y)");
prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < x + 3 + 4* (y - 15*z) / 3 )");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= 3*x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= (-1)*x + y");
prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= x + 3 + 4* (y - 15*z) / 3 ");
nnfp (prove_normalize thy) vs
(parseb "~((x::real) + 4* (y - 15*z) / 3 ~= x + 3 + 4* (y - 15*z) / 3 | (~ (~((x::real) + 4* (y - 15*z) / 3 < x + 3 + 4* (y - 15*z) / 3 ) & (x::real) + 4* (y - 15*z) / 3 <= x + y)))");
nnfp (prove_normalize thy) vs
(parseb "~ ~((x::real) + 4* (y - 15*z) / 3 ~= x + 3 + 4* (y - 15*z) / 3 | (~ (~((x::real) + 4* (y - 15*z) / 3 < x + 3 + 4* (y - 15*z) / 3 ) & (x::real) + 4* (y - 15*z) / 3 <= x + y)))");
fun frtest s = frqelim thy (read_cterm thy (s,HOLogic.boolT));
frtest "~ (ALL (x::real) y. x < y --> 10*x < 11*y)";
frtest "ALL (x::real) y. x < y --> (10*(x + 5*y + -1) < 60*y)";
frtest "EX (x::real) y. x ~= y --> x < y";
frtest "EX (x::real) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y";
frtest "ALL (x::real) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y";
*)
(* 1 Alternations *)
(*
frtest "ALL (x::real). (EX (y::real). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)";
frtest "ALL (x::real) < 0. (EX (y::real) > 0. 7*x + y > 0 & x - y <= 9)";
frtest "EX (x::real). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)";
frtest "EX (x::real). 0 < x & x < 1 & (ALL y. (1 < y & y < 2) --> (1 < 2*(y - x) & 2*(y - x) <3))";
frtest "ALL (x::real). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)";
*)
(* Formulae with 3 quantifiers *)
(* 0 Alternations *)
(*
frtest "ALL (x::real) y z. x + y < z --> y >= z --> x < 0";
frtest "EX (x::real) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0";
frtest "ALL (x::real) y z. abs (x + y) <= z --> (abs z = z)";
frtest "EX (x::real) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0";
frtest "ALL (x::real) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))";
*)
(* 1 Alternations *)
(*
frtest "ALL (x::real) y. x < y --> (EX z>0. x+z = y)";
frtest "ALL (x::real) y. (EX z>0. abs (x - y) <= z )";
frtest "EX (x::real) y. (ALL z>0. (z < x --> z <= 5) & (z > y --> z >= x))";
frtest "EX (x::real) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))";
frtest "EX (x::real) y. (ALL z>0. abs (3*x - 7*y) >= 5 & abs (3*x+7*y) <= 2*z + 1)";
*)
(* 2 Alternations *)
(*
frtest "EX (x::real)>0. (ALL y >0. (EX z>7. 5*x - 3*y <= 7*z))";
frtest "EX (x::real). abs x < 4 & (ALL y > 0. (EX z. 5*x - 3*y <= 7*z))";
frtest "ALL (x::real). (EX y > x. (ALL z < y. x+z < 2*y))" ;
frtest "ALL (x::real). (EX y<(3*x - 1). (ALL z >= (3*x - 1). x - y + z > x ))" ;
frtest "EX (x::real). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))";
*)
(* Formulae with 4 quantifiers *)
(* 0 Alternations *)
(*
frtest "ALL (x::real) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y";
frtest "ALL (x::real) y. ALL z >x. ALL w > y. abs (z-x) + abs (y-w + x) <= z - x + w-y+abs x";
frtest "EX (x::real) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89";
frtest "EX (x::real) y z w. abs (5*x + 3*z - 17*w) + 7* abs (y - 8*x + z) <= max y (7*z - x + w)";
frtest "EX (x::real) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)";
*)
(* 1 Alternations *)
(*
frtest "ALL (x::real) y z. (EX w >= abs (x+y+z). w <= abs x + abs y + abs z)";
frtest "ALL (x::real). (EX y z w. x< y & x < z & x> w & 3*x < w + y)";
frtest "ALL (x::real) y. (EX z w. abs (x-y) = abs (z-w) & z < x & w ~= y)";
frtest "ALL (x::real). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))";
frtest "EX (x::real) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)";
*)
(* 2 Alternations *)
(*
frtest "EX z. (ALL (x::real) y. (EX w >= abs (x+y+z). w <= abs x + abs y + abs z))";
frtest "EX z. (ALL (x::real) < z. (EX y w. x< y & x < z & x> w & 3*x < w + y))";
frtest "ALL (x::real) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))";
frtest "EX y. (ALL (x::real). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))";
frtest "EX (x::real) z. (ALL w >= abs (x+z). (EX y. w >= abs x + abs y + abs z))";
*)
(* 3 Alternations *)
(*
frtest "EX (x::real). (ALL y < x. (EX z > (x+y). (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))";
frtest "EX (x::real). (ALL y < 3*x. (EX z > max x y.
(ALL w . abs w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))";
frtest "ALL (x::real). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))";
frtest "ALL (x::real). (EX y. (ALL z>19. abs (y) <= abs (x + z) & (EX w. abs (x + z) < w - y)))";
frtest "ALL (x::real). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))";
*)
end