--- a/src/FOLP/simp.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/FOLP/simp.ML Fri Oct 20 17:07:26 2006 +0200
@@ -64,7 +64,7 @@
(*** Indexing and filtering of theorems ***)
-fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop (th1,th2);
+fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Drule.eq_thm_prop (th1, th2);
(*insert a thm in a discrimination net by its lhs*)
fun lhs_insert_thm (th,net) =
@@ -155,25 +155,25 @@
(*ccs contains the names of the constants possessing congruence rules*)
fun add_hidden_vars ccs =
- let fun add_hvars(tm,hvars) = case tm of
+ let fun add_hvars tm hvars = case tm of
Abs(_,_,body) => add_term_vars(body,hvars)
| _$_ => let val (f,args) = strip_comb tm
in case f of
Const(c,T) =>
- if c mem ccs
- then foldr add_hvars hvars args
- else add_term_vars(tm,hvars)
- | _ => add_term_vars(tm,hvars)
+ if member (op =) ccs c
+ then fold_rev add_hvars args hvars
+ else add_term_vars (tm, hvars)
+ | _ => add_term_vars (tm, hvars)
end
| _ => hvars;
in add_hvars end;
fun add_new_asm_vars new_asms =
- let fun itf((tm,at),vars) =
+ let fun itf (tm, at) vars =
if at then vars else add_term_vars(tm,vars)
fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
in if length(tml)=length(al)
- then foldr itf vars (tml~~al)
+ then fold_rev itf (tml ~~ al) vars
else vars
end
fun add_vars (tm,vars) = case tm of
@@ -194,12 +194,12 @@
val lhs = rhs_of_eq 1 thm'
val rhs = lhs_of_eq nops thm'
val asms = tl(rev(tl(prems_of thm')))
- val hvars = foldr (add_hidden_vars ccs) [] (lhs::rhs::asms)
+ val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) []
val hvars = add_new_asm_vars new_asms (rhs,hvars)
- fun it_asms (asm,hvars) =
+ fun it_asms asm hvars =
if atomic asm then add_new_asm_vars new_asms (asm,hvars)
else add_term_frees(asm,hvars)
- val hvars = foldr it_asms hvars asms
+ val hvars = fold_rev it_asms asms hvars
val hvs = map (#1 o dest_Var) hvars
val refl1_tac = refl_tac 1
fun norm_step_tac st = st |>
@@ -247,18 +247,18 @@
(** Insertion of congruences and rewrites **)
(*insert a thm in a thm net*)
-fun insert_thm_warn (th,net) =
+fun insert_thm_warn th net =
Net.insert_term Drule.eq_thm_prop (concl_of th, th) net
handle Net.INSERT =>
(writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
net);
-val insert_thms = foldr insert_thm_warn;
+val insert_thms = fold_rev insert_thm_warn;
fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
let val thms = mk_simps thm
in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
- simps = (thm,thms)::simps, simp_net = insert_thms simp_net thms}
+ simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net}
end;
val op addrews = Library.foldl addrew;
@@ -266,25 +266,25 @@
fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
let val congs' = thms @ congs;
in SS{auto_tac=auto_tac, congs= congs',
- cong_net= insert_thms cong_net (map mk_trans thms),
+ cong_net= insert_thms (map mk_trans thms) cong_net,
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
end;
(** Deletion of congruences and rewrites **)
(*delete a thm from a thm net*)
-fun delete_thm_warn (th,net) =
+fun delete_thm_warn th net =
Net.delete_term Drule.eq_thm_prop (concl_of th, th) net
handle Net.DELETE =>
(writeln"\nNo such rewrite or congruence rule:"; print_thm th;
net);
-val delete_thms = foldr delete_thm_warn;
+val delete_thms = fold_rev delete_thm_warn;
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
let val congs' = fold (remove Drule.eq_thm_prop) thms congs
in SS{auto_tac=auto_tac, congs= congs',
- cong_net= delete_thms cong_net (map mk_trans thms),
+ cong_net= delete_thms (map mk_trans thms) cong_net,
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
end;
@@ -296,7 +296,7 @@
([],simps'))
val (thms,simps') = find(simps,[])
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
- simps = simps', simp_net = delete_thms simp_net thms}
+ simps = simps', simp_net = delete_thms thms simp_net }
end;
val op delrews = Library.foldl delrew;
--- a/src/HOL/Import/replay.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Import/replay.ML Fri Oct 20 17:07:26 2006 +0200
@@ -27,12 +27,12 @@
end
| rp (PSubst(prfs,ctxt,prf)) thy =
let
- val (thy',ths) = foldr (fn (p,(thy,ths)) =>
+ val (thy',ths) = fold_rev (fn p => fn (thy, ths) =>
let
val (thy',th) = rp' p thy
in
(thy',th::ths)
- end) (thy,[]) prfs
+ end) prfs (thy,[])
val (thy'',th) = rp' prf thy'
in
P.SUBST ths ctxt th thy''
--- a/src/HOL/Import/shuffler.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Import/shuffler.ML Fri Oct 20 17:07:26 2006 +0200
@@ -83,7 +83,7 @@
val copy = I
val extend = I
fun merge _ = Library.gen_union Thm.eq_thm
-fun print sg thms =
+fun print _ thms =
Pretty.writeln (Pretty.big_list "Shuffle theorems:"
(map Display.pretty_thm thms))
end
@@ -92,7 +92,7 @@
val weaken =
let
- val cert = cterm_of (sign_of ProtoPure.thy)
+ val cert = cterm_of ProtoPure.thy
val P = Free("P",propT)
val Q = Free("Q",propT)
val PQ = Logic.mk_implies(P,Q)
@@ -111,7 +111,7 @@
val imp_comm =
let
- val cert = cterm_of (sign_of ProtoPure.thy)
+ val cert = cterm_of ProtoPure.thy
val P = Free("P",propT)
val Q = Free("Q",propT)
val R = Free("R",propT)
@@ -131,7 +131,7 @@
val def_norm =
let
- val cert = cterm_of (sign_of ProtoPure.thy)
+ val cert = cterm_of ProtoPure.thy
val aT = TFree("'a",[])
val bT = TFree("'b",[])
val v = Free("v",aT)
@@ -158,7 +158,7 @@
val all_comm =
let
- val cert = cterm_of (sign_of ProtoPure.thy)
+ val cert = cterm_of ProtoPure.thy
val xT = TFree("'a",[])
val yT = TFree("'b",[])
val P = Free("P",xT-->yT-->propT)
@@ -182,7 +182,7 @@
val equiv_comm =
let
- val cert = cterm_of (sign_of ProtoPure.thy)
+ val cert = cterm_of ProtoPure.thy
val T = TFree("'a",[])
val t = Free("t",T)
val u = Free("u",T)
@@ -216,28 +216,28 @@
| swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t)
| swap_bound n t = t
-fun rew_th sg (xv as (x,xT)) (yv as (y,yT)) t =
+fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
let
val lhs = list_all ([xv,yv],t)
val rhs = list_all ([yv,xv],swap_bound 0 t)
val rew = Logic.mk_equals (lhs,rhs)
- val init = trivial (cterm_of sg rew)
+ val init = trivial (cterm_of thy rew)
in
(all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
end
-fun quant_rewrite sg assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
+fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
let
val res = (find_bound 0 body;2) handle RESULT i => i
in
case res of
- 0 => SOME (rew_th sg (x,xT) (y,yT) body)
+ 0 => SOME (rew_th thy (x,xT) (y,yT) body)
| 1 => if string_ord(y,x) = LESS
then
let
val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
- val t_th = reflexive (cterm_of sg t)
- val newt_th = reflexive (cterm_of sg newt)
+ val t_th = reflexive (cterm_of thy t)
+ val newt_th = reflexive (cterm_of thy newt)
in
SOME (transitive t_th newt_th)
end
@@ -264,10 +264,10 @@
| _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
end
-fun inst_tfrees sg [] thm = thm
- | inst_tfrees sg ((name,U)::rest) thm =
+fun inst_tfrees thy [] thm = thm
+ | inst_tfrees thy ((name,U)::rest) thm =
let
- val cU = ctyp_of sg U
+ val cU = ctyp_of thy U
val tfrees = add_term_tfrees (prop_of thm,[])
val (rens, thm') = Thm.varifyT'
(remove (op = o apsnd fst) name tfrees) thm
@@ -275,10 +275,10 @@
case rens of
[] => thm'
| [((_, S), idx)] => instantiate
- ([(ctyp_of sg (TVar (idx, S)), cU)], []) thm'
+ ([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
| _ => error "Shuffler.inst_tfrees internal error"
in
- inst_tfrees sg rest mid
+ inst_tfrees thy rest mid
end
fun is_Abs (Abs _) = true
@@ -295,11 +295,11 @@
end
| eta_redex _ = false
-fun eta_contract sg assumes origt =
+fun eta_contract thy assumes origt =
let
val (typet,Tinst) = freeze_thaw_term origt
- val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet))
- val final = inst_tfrees sg Tinst o thaw
+ val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
+ val final = inst_tfrees thy Tinst o thaw
val t = #1 (Logic.dest_equals (prop_of init))
val _ =
let
@@ -307,11 +307,11 @@
in
if not (lhs aconv origt)
then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
- writeln (string_of_cterm (cterm_of sg origt));
- writeln (string_of_cterm (cterm_of sg lhs));
- writeln (string_of_cterm (cterm_of sg typet));
- writeln (string_of_cterm (cterm_of sg t));
- app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst;
+ writeln (string_of_cterm (cterm_of thy origt));
+ writeln (string_of_cterm (cterm_of thy lhs));
+ writeln (string_of_cterm (cterm_of thy typet));
+ writeln (string_of_cterm (cterm_of thy t));
+ app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
writeln "done")
else ()
end
@@ -321,7 +321,7 @@
((if eta_redex P andalso eta_redex Q
then
let
- val cert = cterm_of sg
+ val cert = cterm_of thy
val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
val cv = cert v
val ct = cert t
@@ -347,21 +347,21 @@
| _ => NONE
end
-fun beta_fun sg assume t =
- SOME (beta_conversion true (cterm_of sg t))
+fun beta_fun thy assume t =
+ SOME (beta_conversion true (cterm_of thy t))
val meta_sym_rew = thm "refl"
-fun equals_fun sg assume t =
+fun equals_fun thy assume t =
case t of
Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
| _ => NONE
-fun eta_expand sg assumes origt =
+fun eta_expand thy assumes origt =
let
val (typet,Tinst) = freeze_thaw_term origt
- val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet))
- val final = inst_tfrees sg Tinst o thaw
+ val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
+ val final = inst_tfrees thy Tinst o thaw
val t = #1 (Logic.dest_equals (prop_of init))
val _ =
let
@@ -369,11 +369,11 @@
in
if not (lhs aconv origt)
then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
- writeln (string_of_cterm (cterm_of sg origt));
- writeln (string_of_cterm (cterm_of sg lhs));
- writeln (string_of_cterm (cterm_of sg typet));
- writeln (string_of_cterm (cterm_of sg t));
- app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst;
+ writeln (string_of_cterm (cterm_of thy origt));
+ writeln (string_of_cterm (cterm_of thy lhs));
+ writeln (string_of_cterm (cterm_of thy typet));
+ writeln (string_of_cterm (cterm_of thy t));
+ app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
writeln "done")
else ()
end
@@ -384,7 +384,7 @@
then (case domain_type T of
Type("fun",[aT,bT]) =>
let
- val cert = cterm_of sg
+ val cert = cterm_of thy
val vname = Name.variant (add_term_free_names(t,[])) "v"
val v = Free(vname,aT)
val cv = cert v
@@ -409,7 +409,7 @@
end
| _ => NONE)
else NONE
- | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
+ | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
end
handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
@@ -423,30 +423,30 @@
val S = mk_free "S" xT
val S' = mk_free "S'" xT
in
-fun beta_simproc sg = Simplifier.simproc_i
- sg
+fun beta_simproc thy = Simplifier.simproc_i
+ thy
"Beta-contraction"
[Abs("x",xT,Q) $ S]
beta_fun
-fun equals_simproc sg = Simplifier.simproc_i
- sg
+fun equals_simproc thy = Simplifier.simproc_i
+ thy
"Ordered rewriting of meta equalities"
[Const("op ==",xT) $ S $ S']
equals_fun
-fun quant_simproc sg = Simplifier.simproc_i
- sg
+fun quant_simproc thy = Simplifier.simproc_i
+ thy
"Ordered rewriting of nested quantifiers"
[all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
quant_rewrite
-fun eta_expand_simproc sg = Simplifier.simproc_i
- sg
+fun eta_expand_simproc thy = Simplifier.simproc_i
+ thy
"Smart eta-expansion by equivalences"
[Logic.mk_equals(Q,R)]
eta_expand
-fun eta_contract_simproc sg = Simplifier.simproc_i
- sg
+fun eta_contract_simproc thy = Simplifier.simproc_i
+ thy
"Smart handling of eta-contractions"
[all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
eta_contract
@@ -455,7 +455,7 @@
(* Disambiguates the names of bound variables in a term, returning t
== t' where all the names of bound variables in t' are unique *)
-fun disamb_bound sg t =
+fun disamb_bound thy t =
let
fun F (t $ u,idx) =
@@ -474,8 +474,8 @@
end
| F arg = arg
val (t',_) = F (t,0)
- val ct = cterm_of sg t
- val ct' = cterm_of sg t'
+ val ct = cterm_of thy t
+ val ct' = cterm_of thy t'
val res = transitive (reflexive ct) (reflexive ct')
val _ = message ("disamb_term: " ^ (string_of_thm res))
in
@@ -488,12 +488,11 @@
fun norm_term thy t =
let
- val sg = sign_of thy
val norms = ShuffleData.get thy
val ss = Simplifier.theory_context thy empty_ss
setmksimps single
- addsimps (map (Thm.transfer sg) norms)
- addsimprocs [quant_simproc sg, eta_expand_simproc sg,eta_contract_simproc sg]
+ addsimps (map (Thm.transfer thy) norms)
+ addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
fun chain f th =
let
val rhs = snd (dest_equals (cprop_of th))
@@ -501,7 +500,7 @@
transitive th (f rhs)
end
val th =
- t |> disamb_bound sg
+ t |> disamb_bound thy
|> chain (Simplifier.full_rewrite ss)
|> chain eta_conversion
|> strip_shyps
@@ -509,7 +508,7 @@
in
th
end
- handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)
+ handle e => (writeln "norm_term internal error"; print_sign_exn thy e)
(* Closes a theorem with respect to free and schematic variables (does
@@ -517,11 +516,11 @@
fun close_thm th =
let
- val sg = sign_of_thm th
+ val thy = sign_of_thm th
val c = prop_of th
val vars = add_term_frees (c,add_term_vars(c,[]))
in
- Drule.forall_intr_list (map (cterm_of sg) vars) th
+ Drule.forall_intr_list (map (cterm_of thy) vars) th
end
handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
@@ -534,14 +533,14 @@
equal_elim (norm_term thy c) th
end
-(* make_equal sg t u tries to construct the theorem t == u under the
-signature sg. If it succeeds, SOME (t == u) is returned, otherwise
+(* make_equal thy t u tries to construct the theorem t == u under the
+signature thy. If it succeeds, SOME (t == u) is returned, otherwise
NONE is returned. *)
-fun make_equal sg t u =
+fun make_equal thy t u =
let
- val t_is_t' = norm_term sg t
- val u_is_u' = norm_term sg u
+ val t_is_t' = norm_term thy t
+ val u_is_u' = norm_term thy u
val th = transitive t_is_t' (symmetric u_is_u')
val _ = message ("make_equal: SOME " ^ (string_of_thm th))
in
@@ -569,7 +568,7 @@
end
val collect_ignored =
- foldr (fn (thm,cs) =>
+ fold_rev (fn thm => fn cs =>
let
val (lhs,rhs) = Logic.dest_equals (prop_of thm)
val ignore_lhs = term_consts lhs \\ term_consts rhs
@@ -584,10 +583,9 @@
fun set_prop thy t =
let
- val sg = sign_of thy
val vars = add_term_frees (t,add_term_vars (t,[]))
- val closed_t = foldr (fn (v,body) => let val vT = type_of v
- in all vT $ (Abs("x",vT,abstract_over(v,body))) end) t vars
+ val closed_t = Library.foldr (fn (v, body) =>
+ let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
val rew_th = norm_term thy closed_t
val rhs = snd (dest_equals (cprop_of rew_th))
@@ -595,7 +593,7 @@
fun process [] = NONE
| process ((name,th)::thms) =
let
- val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer sg th)))
+ val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
val triv_th = trivial rhs
val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
@@ -608,7 +606,7 @@
val closed_th = equal_elim (symmetric rew_th) mod_th
in
message ("Shuffler.set_prop succeeded by " ^ name);
- SOME (name,forall_elim_list (map (cterm_of sg) vars) closed_th)
+ SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
end
| NONE => process thms
end
@@ -626,7 +624,7 @@
fun find_potential thy t =
let
val shuffles = ShuffleData.get thy
- val ignored = collect_ignored [] shuffles
+ val ignored = collect_ignored shuffles []
val rel_consts = term_consts t \\ ignored
val pot_thms = PureThy.thms_containing_consts thy rel_consts
in
--- a/src/HOL/Integ/cooper_dec.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Fri Oct 20 17:07:26 2006 +0200
@@ -443,7 +443,7 @@
val ts = coeffs_of t
in case ts of
[] => raise DVD_UNKNOWN
- |_ => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
+ |_ => fold_rev (fn k => fn r => r andalso (k mod dn = 0)) ts true
end;
@@ -736,7 +736,7 @@
in (rw,HOLogic.mk_disj(F',rf))
end)
val f = if b then linear_add else linear_sub
- val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (myupto 1 d)
+ val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_numeral i)) st)) (myupto 1 d) []
in h p_elements
end;
--- a/src/HOL/Nominal/nominal_permeq.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Fri Oct 20 17:07:26 2006 +0200
@@ -268,9 +268,9 @@
val ps = Logic.strip_params (term_of goal);
val Ts = rev (map snd ps);
val vs = collect_vars 0 x [];
- val s = foldr (fn (v, s) =>
+ val s = Library.foldr (fn (v, s) =>
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
- HOLogic.unit vs;
+ (vs, HOLogic.unit);
val s' = list_abs (ps,
Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
val supports_rule' = Thm.lift_rule goal supports_rule;
@@ -305,9 +305,9 @@
val ps = Logic.strip_params (term_of goal);
val Ts = rev (map snd ps);
val vs = collect_vars 0 t [];
- val s = foldr (fn (v, s) =>
+ val s = Library.foldr (fn (v, s) =>
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
- HOLogic.unit vs;
+ (vs, HOLogic.unit);
val s' = list_abs (ps,
Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
--- a/src/HOL/Real/ferrante_rackoff.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Real/ferrante_rackoff.ML Fri Oct 20 17:07:26 2006 +0200
@@ -5,94 +5,85 @@
Ferrante and Rackoff Algorithm.
*)
-structure Ferrante_Rackoff:
+signature FERRANTE_RACKOFF =
sig
- val trace : bool ref
- val ferrack_tac : bool -> int -> tactic
- val setup : theory -> theory
-end =
+ val ferrack_tac: bool -> int -> tactic
+ val setup: theory -> theory
+ val trace: bool ref
+end;
+
+structure Ferrante_Rackoff : FERRANTE_RACKOFF =
struct
val trace = ref false;
fun trace_msg s = if !trace then tracing s else ();
-val context_ss = simpset_of (the_context ());
-
-val nT = HOLogic.natT;
-val binarith = map thm
- ["Pls_0_eq", "Min_1_eq",
- "pred_Pls","pred_Min","pred_1","pred_0",
+val binarith = map thm ["Pls_0_eq", "Min_1_eq", "pred_Pls", "pred_Min","pred_1","pred_0",
"succ_Pls", "succ_Min", "succ_1", "succ_0",
- "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
- "add_BIT_11", "minus_Pls", "minus_Min", "minus_1",
- "minus_0", "mult_Pls", "mult_Min", "mult_1", "mult_0",
+ "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10", "add_BIT_11",
+ "minus_Pls", "minus_Min", "minus_1", "minus_0",
+ "mult_Pls", "mult_Min", "mult_1", "mult_0",
"add_Pls_right", "add_Min_right"];
- val intarithrel =
- (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT",
- "int_le_number_of_eq","int_iszero_number_of_0",
- "int_less_number_of_eq_neg"]) @
- (map (fn s => thm s RS thm "lift_bool")
- ["int_iszero_number_of_Pls","int_iszero_number_of_1",
- "int_neg_number_of_Min"])@
- (map (fn s => thm s RS thm "nlift_bool")
- ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
-
+
+val intarithrel =
+ map thm ["int_eq_number_of_eq", "int_neg_number_of_BIT", "int_le_number_of_eq",
+ "int_iszero_number_of_0", "int_less_number_of_eq_neg"]
+ @ map (fn s => thm s RS thm "lift_bool") ["int_iszero_number_of_Pls",
+ "int_iszero_number_of_1", "int_neg_number_of_Min"]
+ @ map (fn s => thm s RS thm "nlift_bool") ["int_nonzero_number_of_Min",
+ "int_not_neg_number_of_Pls"];
+
val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
- "int_number_of_diff_sym", "int_number_of_mult_sym"];
+ "int_number_of_diff_sym", "int_number_of_mult_sym"];
+
val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
- "mult_nat_number_of", "eq_nat_number_of",
- "less_nat_number_of"]
-val powerarith =
- (map thm ["nat_number_of", "zpower_number_of_even",
- "zpower_Pls", "zpower_Min"]) @
- [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
- thm "one_eq_Numeral1_nring"]
- (thm "zpower_number_of_odd"))]
+ "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"];
+
+val powerarith =
+ map thm ["nat_number_of", "zpower_number_of_even",
+ "zpower_Pls", "zpower_Min"]
+ @ [Tactic.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
+ (thm "zpower_number_of_odd")]
val comp_arith = binarith @ intarith @ intarithrel @ natarith
- @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
+ @ powerarith @ [thm "not_false_eq_true", thm "not_true_eq_false"];
-fun prepare_for_linr sg q fm =
+fun prepare_for_linr q fm =
let
val ps = Logic.strip_params fm
val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
- fun mk_all ((s, T), (P,n)) =
+ fun mk_all ((s, T), (P, n)) =
if 0 mem loose_bnos P then
(HOLogic.all_const T $ Abs (s, T, P), n)
else (incr_boundvars ~1 P, n-1)
fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
- val rhs = hs
-(* val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
- val np = length ps
- val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
- (foldr HOLogic.mk_imp c rhs, np) ps
- val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
+ val rhs = hs;
+ val np = length ps;
+ val (fm', np) = Library.foldr mk_all (ps, (Library.foldr HOLogic.mk_imp (rhs, c), np));
+ val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
(term_frees fm' @ term_vars fm');
- val fm2 = foldr mk_all2 fm' vs
+ val fm2 = Library.foldr mk_all2 (vs, fm');
in (fm2, np + length vs, length rhs) end;
-(*Object quantifier to meta --*)
-fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
-
-(* object implication to meta---*)
-fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
-
+fun spec_step n th = if n = 0 then th else spec_step (n - 1) th RS spec ;
+fun mp_step n th = if n = 0 then th else mp_step (n - 1) th RS mp;
-fun ferrack_tac q i =
- (ObjectLogic.atomize_tac i)
- THEN (REPEAT_DETERM (split_tac [split_min, split_max,abs_split] i))
- THEN (fn st =>
+local
+ val context_ss = simpset_of (the_context ())
+in fun ferrack_tac q i = ObjectLogic.atomize_tac i
+ THEN REPEAT_DETERM (split_tac [split_min, split_max,abs_split] i)
+ THEN (fn st =>
let
- val g = List.nth (prems_of st, i - 1)
- val sg = sign_of_thm st
+ val g = nth (prems_of st) (i - 1)
+ val thy = sign_of_thm st
(* Transform the term*)
- val (t,np,nh) = prepare_for_linr sg q g
+ val (t,np,nh) = prepare_for_linr q g
(* Some simpsets for dealing with mod div abs and nat*)
val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [split_min, split_max]
(* simp rules for elimination of abs *)
val simpset3 = HOL_basic_ss addsplits [abs_split]
- val ct = cterm_of sg (HOLogic.mk_Trueprop t)
+ val ct = cterm_of thy (HOLogic.mk_Trueprop t)
(* Theorem for the nat --> int transformation *)
val pre_thm = Seq.hd (EVERY
[simp_tac simpset0 1, TRY (simp_tac context_ss 1)]
@@ -101,10 +92,10 @@
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
- let val pth = Ferrante_Rackoff_Proof.qelim (cterm_of sg (Pattern.eta_long [] t1))
+ let val pth = Ferrante_Rackoff_Proof.qelim (cterm_of thy (Pattern.eta_long [] t1))
in
(trace_msg ("calling procedure with term:\n" ^
- Sign.string_of_term sg t1);
+ Sign.string_of_term thy t1);
((pth RS iffD2) RS pre_thm,
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
end
@@ -112,10 +103,11 @@
in (rtac (((mp_step nh) o (spec_step np)) th) i
THEN tac) st
end handle Subscript => no_tac st | Ferrante_Rackoff_Proof.FAILURE _ => no_tac st);
+end; (*local*)
fun ferrack_args meth =
- let val parse_flag =
- Args.$$$ "no_quantify" >> (K (K false));
+ let
+ val parse_flag = Args.$$$ "no_quantify" >> (K (K false));
in
Method.simple_args
(Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Fri Oct 20 17:07:26 2006 +0200
@@ -443,7 +443,7 @@
val ts = coeffs_of t
in case ts of
[] => raise DVD_UNKNOWN
- |_ => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
+ |_ => fold_rev (fn k => fn r => r andalso (k mod dn = 0)) ts true
end;
@@ -736,7 +736,7 @@
in (rw,HOLogic.mk_disj(F',rf))
end)
val f = if b then linear_add else linear_sub
- val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (myupto 1 d)
+ val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_numeral i)) st)) (myupto 1 d) []
in h p_elements
end;
--- a/src/HOL/Tools/datatype_prop.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Fri Oct 20 17:07:26 2006 +0200
@@ -64,24 +64,23 @@
fun make_injs descr sorts =
let
- val descr' = List.concat descr;
-
- fun make_inj T ((cname, cargs), injs) =
- if null cargs then injs else
+ val descr' = flat descr;
+ fun make_inj T (cname, cargs) =
+ if null cargs then I else
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
val constr_t = Const (cname, Ts ---> T);
val tnames = make_tnames Ts;
val frees = map Free (tnames ~~ Ts);
val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
- in (HOLogic.mk_Trueprop (HOLogic.mk_eq
+ in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
(HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
foldr1 (HOLogic.mk_binop "op &")
- (map HOLogic.mk_eq (frees ~~ frees')))))::injs
+ (map HOLogic.mk_eq (frees ~~ frees')))))
end;
-
- in map (fn (d, T) => foldr (make_inj T) [] (#3 (snd d)))
- ((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
+ in
+ map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
+ (hd descr) (Library.take (length (hd descr), get_rec_types descr' sorts))
end;
(********************************* induction **********************************)
--- a/src/HOL/Tools/recdef_package.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Tools/recdef_package.ML Fri Oct 20 17:07:26 2006 +0200
@@ -80,8 +80,6 @@
val (del, rest) = List.partition (Library.equal c o fst) congs;
in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
-val add_congs = foldr (uncurry add_cong);
-
end;
--- a/src/HOL/Tools/record_package.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Tools/record_package.ML Fri Oct 20 17:07:26 2006 +0200
@@ -491,7 +491,7 @@
fun record_update_tr [t, u] =
- foldr (op $) t (rev (gen_fields_tr "_updates" "_update" updateN u))
+ Library.foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
| record_update_tr ts = raise TERM ("record_update_tr", ts);
fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
@@ -1547,8 +1547,8 @@
(* mk_recordT builds up the record type from the current extension tpye extT and a list
* of parent extensions, starting with the root of the record hierarchy
*)
-fun mk_recordT extT parent_exts =
- foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) extT parent_exts;
+fun mk_recordT extT =
+ fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
@@ -1646,12 +1646,12 @@
val extension_id = Library.foldl (op ^) ("",extension_names);
- fun rec_schemeT n = mk_recordT extT (map #extension (prune n parents));
+ fun rec_schemeT n = mk_recordT (map #extension (prune n parents)) extT;
val rec_schemeT0 = rec_schemeT 0;
fun recT n =
let val (c,Ts) = extension
- in mk_recordT (Type (c,subst_last HOLogic.unitT Ts))(map #extension (prune n parents))
+ in mk_recordT (map #extension (prune n parents)) (Type (c,subst_last HOLogic.unitT Ts))
end;
val recT0 = recT 0;
--- a/src/HOL/Tools/refute.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Tools/refute.ML Fri Oct 20 17:07:26 2006 +0200
@@ -421,8 +421,8 @@
(* (string * Term.term) list *)
val axioms = Theory.all_axioms_of thy;
(* string list *)
- val rec_names = Symtab.fold (fn (_, info) => fn acc =>
- #rec_names info @ acc) (DatatypePackage.get_datatypes thy) []
+ val rec_names = Symtab.fold (append o #rec_names o snd)
+ (DatatypePackage.get_datatypes thy) [];
(* string list *)
val const_of_class_names = map Logic.const_of_class (Sign.classes thy)
(* given a constant 's' of type 'T', which is a subterm of 't', where *)
@@ -677,7 +677,7 @@
fun is_IDT_recursor () =
(* I'm not quite sure if checking the name 's' is sufficient, *)
(* or if we should also check the type 'T' *)
- s mem rec_names
+ member (op =) rec_names s
in
if is_const_of_class () then
(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" and *)
--- a/src/HOL/ex/reflection.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/ex/reflection.ML Fri Oct 20 17:07:26 2006 +0200
@@ -184,8 +184,8 @@
val tml = Vartab.dest tmenv
val SOME (_,t') = AList.lookup (op =) tml (xn,0)
val cvs =
- cert (foldr (fn (x,xs) => Const("List.list.Cons", ntT --> ntlT --> ntlT)$x$xs)
- (Free(vsn,ntlT)) bsT)
+ cert (fold_rev (fn x => fn xs => Const("List.list.Cons", ntT --> ntlT --> ntlT)$x$xs)
+ bsT (Free (vsn, ntlT)))
val cts = map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t))
(AList.delete (op =) (xn,0) tml)
val th = (instantiate
@@ -232,12 +232,12 @@
fun mk_congs ctxt raw_eqs =
let
- val fs = foldr (fn (eq,fns) =>
+ val fs = fold_rev (fn eq =>
insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop
|> HOLogic.dest_eq |> fst |> strip_comb
- |> fst) fns) [] raw_eqs
- val tys = foldr (fn (f,ts) => (f |> fastype_of |> binder_types |> split_last |> fst)
- union ts) [] fs
+ |> fst)) raw_eqs []
+ val tys = fold_rev (fn f => fn ts => (f |> fastype_of |> binder_types |> split_last |> fst)
+ union ts) fs []
val _ = bds := AList.make (fn _ => ([],[])) tys
val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt
val thy = ProofContext.theory_of ctxt'
--- a/src/HOL/ex/svc_funcs.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/ex/svc_funcs.ML Fri Oct 20 17:07:26 2006 +0200
@@ -119,7 +119,7 @@
in #1 o tag end;
(*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
- fun add_nat_var (a, e) =
+ fun add_nat_var a e =
Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
e]);
@@ -240,7 +240,7 @@
val body_e = mt pos body (*evaluate now to assign into !nat_vars*)
in
- foldr add_nat_var body_e (!nat_vars)
+ fold_rev add_nat_var (!nat_vars) body_e
end;
--- a/src/HOL/hologic.ML Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/hologic.ML Fri Oct 20 17:07:26 2006 +0200
@@ -165,7 +165,7 @@
fun all_const T = Const ("All", [T --> boolT] ---> boolT);
fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
-fun list_all (vs,x) = foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)) x vs;
+fun list_all (vs,x) = Library.foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)) (vs, x);
fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);