--- a/src/HOL/Real/ferrante_rackoff_proof.ML Sat Jul 08 12:54:36 2006 +0200
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML Sat Jul 08 12:54:37 2006 +0200
@@ -19,39 +19,39 @@
(* Normalization*)
- (* Computation of uset *)
+ (* Computation of uset *)
fun uset x fm =
case fm of
- Const("op &",_)$p$q => (uset x p) union (uset x q)
+ Const("op &",_)$p$q => (uset x p) union (uset x q)
| Const("op |",_)$p$q => (uset x p) union (uset x q)
| Const("Orderings.less",_)$s$t => if s=x then [t]
- else if t = x then [s]
- else []
+ else if t = x then [s]
+ else []
| Const("Orderings.less_eq",_)$s$t => if s=x then [t]
- else if t = x then [s]
- else []
+ else if t = x then [s]
+ else []
| Const("op =",_)$s$t => if s=x then [t]
- else []
+ else []
| Const("Not",_)$ (Const("op =",_)$s$t) => if s=x then [t]
- else []
+ else []
| _ => [];
val rsT = Type("set",[rT]);
fun holrealset [] = Const("{}",rsT)
| holrealset (x::xs) = Const("insert",[rT,rsT] ---> rsT)$x$(holrealset xs);
-fun prove_bysimp thy ss t = Goal.prove thy [] []
- (HOLogic.mk_Trueprop t) (fn _ => simp_tac ss 1);
+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 ((inC rsT)$hU$Const("Finite_Set.Finites",Type("set",[rsT])))
+ 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 ((inC rsT)$hU$Const("Finite_Set.Finites",Type("set",[rsT])))
in (U,cterm_of sg hU,map proveinU U,uf)
end;
- (* Theorems for minus/plusinfinity *)
+ (* 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 *)
@@ -78,7 +78,7 @@
fun dest2 [] = ([],[])
| dest2 ((x,y)::xs) = let val (x',y') = dest2 xs
- in (x::x',y::y') end ;
+ 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)
@@ -91,137 +91,137 @@
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("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
+ (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("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("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("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
+ 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)
+ | 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) = 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
+ Const("Ex",_)$Abs(x1,T,p1) =>
+ let val (xn,fm) = 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 *)
@@ -248,40 +248,40 @@
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_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 = CooperDec.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)
+ if opn = "op |"
+ then
+ (case (p,q) of
+ (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
+ if r1 = CooperDec.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 (
+ 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))
+ ("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 )
+ ([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
+ 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;
@@ -291,7 +291,7 @@
val rone = Const("1",rT);
fun mk_real i =
case i of
- 0 => rzero
+ 0 => rzero
| 1 => rone
| _ => (HOLogic.number_of_const rT)$(HOLogic.mk_binum i);
@@ -299,38 +299,38 @@
| dest_real (Const("1",_)) = 1
| dest_real (Const("Numeral.number_of",_)$b) = HOLogic.dest_binum b;
- (* 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 *)
+ (* 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 "HOL.times" (mk_real m,mk_real n),mk_real (m*n)));
+ (HOLogic.mk_eq(HOLogic.mk_binop "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 "HOL.plus" (mk_real m,mk_real n),mk_real (m+n)));
+ (HOLogic.mk_eq(HOLogic.mk_binop "HOL.plus" (mk_real m,mk_real n),mk_real (m+n)));
fun provediv thy m n =
let val g = gcd (m,n)
- val m' = m div g
- val n'= n div g
+ val m' = m div g
+ val n'= n div g
in
- (prove_bysimp thy (simpset_of thy)
- (HOLogic.mk_eq(HOLogic.mk_binop "HOL.divide" (mk_real m,mk_real n),
- HOLogic.mk_binop "HOL.divide"
- (mk_real m',mk_real n'))),m')
+ (prove_bysimp thy (simpset_of thy)
+ (HOLogic.mk_eq(HOLogic.mk_binop "HOL.divide" (mk_real m,mk_real n),
+ HOLogic.mk_binop "HOL.divide"
+ (mk_real m',mk_real n'))),m')
end;
- (* Multiplication of a normal term by a constant *)
+ (* 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)] mult_zero_left) else
case t of
- Const("HOL.plus",_)$(Const("HOL.times",_)$c'$v)$b =>
- ([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)]
- ((proveprod thy c (dest_real c')) RS ncmul_congh)))
+ Const("HOL.plus",_)$(Const("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);
@@ -338,7 +338,7 @@
(* 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
+ val tt' = prove_ncmulh thy c' t
in [eq1,tt'] MRS ncmul_cong
end;
@@ -360,25 +360,25 @@
fun decomp_naddh thy vs (t,s) =
case (t,s) of
- (Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr,
- Const("HOL.plus",_)$(csv as Const("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("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr,
+ Const("HOL.plus",_)$(csv as Const("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("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr,_) =>
- ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
+ ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
| (_,Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) =>
- ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
+ ([(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'*)
@@ -390,38 +390,38 @@
(* 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
+ 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 = 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;
+ 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')
+ 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);
+ ((proveprod thy m n) RS ndivide_cong);
exception FAILURE of string;
@@ -435,67 +435,67 @@
fun decomp_normalizeh thy vs t =
case t of
- Free _ => ([], fn _ => instantiate' [] [SOME(cterm_of thy t)] normalizeh_var)
+ Free _ => ([], fn _ => instantiate' [] [SOME(cterm_of thy t)] normalizeh_var)
| Const("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 )
+ ([a],
+ fn [tha] => let val _$(_$_$(_$a'$n')) = prop_of tha
+ in [tha,prove_nneg thy (a',dest_real n')]
+ MRS uminus_cong
+ end )
| Const("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 )
+ ([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("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 )
+ ([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("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"
+ 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("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"
+ 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("HOL.plus",_)$(Const("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))
+ Const("HOL.plus",_)$(Const("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 "Orderings.less"
- (if n > 0 then (rzero, mk_real n) else (mk_real n, rzero)));
+ (HOLogic.mk_binrel "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 "HOL.divide" (mk_real m, mk_real n)
in prove_bysimp thy (simpset_of thy)
- (HOLogic.mk_binrel "Orderings.less"
- (if m*n > 0 then (rzero, mn) else (mn, rzero)))
+ (HOLogic.mk_binrel "Orderings.less"
+ (if m*n > 0 then (rzero, mn) else (mn, rzero)))
end;
fun holbool_of true = HOLogic.true_const
@@ -505,15 +505,15 @@
let fun f s = the (AList.lookup (op =) [("Orderings.less", op <),("Orderings.less_eq", op <=),("op =", op =)] s)
in
prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq
- (HOLogic.mk_binrel s
- (HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n),rzero),
- holbool_of (f s (m*n,0))))
+ (HOLogic.mk_binrel s
+ (HOLogic.mk_binop "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)));
+ (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";
@@ -541,71 +541,71 @@
fun prove_normalize thy vs at =
case at of
- Const("Orderings.less",_)$s$t =>
- let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "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 "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("Orderings.less",_)$s$t =>
+ let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "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 "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("Orderings.less_eq",_)$s$t =>
- let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "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 "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
+ let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "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 "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 "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
+ let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "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("Orderings.less",T)$s$t) =>
- (prove_normalize thy vs (Const("Orderings.less_eq",T)$t$s)) RS normalize_not_lt
+ (prove_normalize thy vs (Const("Orderings.less_eq",T)$t$s)) RS normalize_not_lt
| Const("Not",_)$(Const("Orderings.less_eq",T)$s$t) =>
- (prove_normalize thy vs (Const("Orderings.less",T)$t$s)) RS normalize_not_le
+ (prove_normalize thy vs (Const("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
+ (prove_normalize thy vs (Const("op =",T)$s$t)) RS qe_Not
| _ => instantiate' [SOME cbT] [SOME (cterm_of thy at)] refl;
(* Generic quantifier elimination *)
@@ -618,41 +618,41 @@
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_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)
+ ([(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) = variant_abs(xn,xT,p)
- val x= Free(xn1,xT)
- in ([(p1,x::vs)],
+ let val (xn1,p1) = 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 (CooperProof.qe_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(CooperProof.qe_get_terms eth1))
+ val eth1 = (forall_intr (cterm_of thy (Free(xn1,xT))) th2) COMP ex_eq_cong
+ val th3 = qfnp (snd(CooperProof.qe_get_terms eth1))
in [eth1,th3] MRS trans
end )
- 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)
+ ([((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];
+ 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''
+ 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;
@@ -677,17 +677,17 @@
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);
+ (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)");
+ (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)");
+ (parser "4*(x::real) - 3* ((3*y + 5)*9 + x)");
prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)]
- (parser "- x");
+ (parser "- x");
prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)]
- (parser "4*(x::real) +3* ((3*y + 5) / 3 - (- x))");
+ (parser "4*(x::real) +3* ((3*y + 5) / 3 - (- x))");