Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
(* Title: ZF/ind_syntax.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Abstract Syntax functions for Inductive Definitions.
*)
(*The structure protects these items from redeclaration (somewhat!). The
datatype definitions in theory files refer to these items by name!
*)
structure Ind_Syntax =
struct
(*Print tracing messages during processing of "inductive" theory sections*)
val trace = ref false;
fun traceIt msg thy t =
if !trace then (tracing (msg ^ Sign.string_of_term thy t); t)
else t;
(** Abstract syntax definitions for ZF **)
val iT = Type("i",[]);
val mem_const = @{term mem};
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
fun mk_all_imp (A,P) =
FOLogic.all_const iT $
Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $
Term.betapply(P, Bound 0));
val Part_const = Const("Part", [iT,iT-->iT]--->iT);
val apply_const = @{term apply};
val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT);
val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
(*simple error-checking in the premises of an inductive definition*)
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
error"Premises may not be conjuctive"
| chk_prem rec_hd (Const(@{const_name mem},_) $ t $ X) =
(Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
| chk_prem rec_hd t =
(Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
(*Return the conclusion of a rule, of the form t:X*)
fun rule_concl rl =
let val Const("Trueprop",_) $ (Const(@{const_name mem},_) $ t $ X) =
Logic.strip_imp_concl rl
in (t,X) end;
(*As above, but return error message if bad*)
fun rule_concl_msg sign rl = rule_concl rl
handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
Sign.string_of_term sign rl);
(*For deriving cases rules. CollectD2 discards the domain, which is redundant;
read_instantiate replaces a propositional variable by a formula variable*)
val equals_CollectD =
read_instantiate [("W","?Q")]
(make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
(** For datatype definitions **)
(*Constructor name, type, mixfix info;
internal name from mixfix, datatype sets, full premises*)
type constructor_spec =
((string * typ * mixfix) * string * term list * term list);
fun dest_mem (Const(@{const_name mem},_) $ x $ A) = (x,A)
| dest_mem _ = error "Constructor specifications must have the form x:A";
(*read a constructor specification*)
fun read_construct sign (id, sprems, syn) =
let val prems = map (Sign.simple_read_term sign FOLogic.oT) sprems
val args = map (#1 o dest_mem) prems
val T = (map (#2 o dest_Free) args) ---> iT
handle TERM _ => error
"Bad variable in constructor specification"
val name = Syntax.const_name id syn (*handle infix constructors*)
in ((id,T,syn), name, args, prems) end;
val read_constructs = map o map o read_construct;
(*convert constructor specifications into introduction rules*)
fun mk_intr_tms sg (rec_tm, constructs) =
let
fun mk_intr ((id,T,syn), name, args, prems) =
Logic.list_implies
(map FOLogic.mk_Trueprop prems,
FOLogic.mk_Trueprop
(mem_const $ list_comb (Const (Sign.full_name sg name, T), args)
$ rec_tm))
in map mk_intr constructs end;
fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
fun mk_Un (t1, t2) = Const(@{const_name Un}, [iT,iT]--->iT) $ t1 $ t2;
val empty = Const("0", iT)
and univ = Const("Univ.univ", iT-->iT)
and quniv = Const("QUniv.quniv", iT-->iT);
(*Make a datatype's domain: form the union of its set parameters*)
fun union_params (rec_tm, cs) =
let val (_,args) = strip_comb rec_tm
fun is_ind arg = (type_of arg = iT)
in case List.filter is_ind (args @ cs) of
[] => empty
| u_args => BalancedTree.make mk_Un u_args
end;
(*univ or quniv constitutes the sum domain for mutual recursion;
it is applied to the datatype parameters and to Consts occurring in the
definition other than Nat.nat and the datatype sets themselves.
FIXME: could insert all constant set expressions, e.g. nat->nat.*)
fun data_domain co (rec_tms, con_ty_lists) =
let val rec_hds = map head_of rec_tms
val dummy = assert_all is_Const rec_hds
(fn t => "Datatype set not previously declared as constant: " ^
Sign.string_of_term @{theory IFOL} t);
val rec_names = (*nat doesn't have to be added*)
@{const_name "nat"} :: map (#1 o dest_Const) rec_hds
val u = if co then quniv else univ
val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
(fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
| _ => I)) con_ty_lists [];
in u $ union_params (hd rec_tms, cs) end;
(*Could go to FOL, but it's hardly general*)
val def_swap_iff = prove_goal (the_context ()) "a==b ==> a=c <-> c=b"
(fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
val def_trans = prove_goal (the_context ()) "[| f==g; g(a)=b |] ==> f(a)=b"
(fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
(*Delete needless equality assumptions*)
val refl_thin = prove_goal (the_context ()) "!!P. [| a=a; P |] ==> P"
(fn _ => [assume_tac 1]);
(*Includes rules for succ and Pair since they are common constructions*)
val elim_rls = [asm_rl, FalseE, thm "succ_neq_0", sym RS thm "succ_neq_0",
thm "Pair_neq_0", sym RS thm "Pair_neq_0", thm "Pair_inject",
make_elim (thm "succ_inject"),
refl_thin, conjE, exE, disjE];
(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
| tryres (th, []) = raise THM("tryres", 0, [th]);
fun gen_make_elim elim_rls rl =
standard (tryres (rl, elim_rls @ [revcut_rl]));
(*Turns iff rules into safe elimination rules*)
fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
end;
(*For convenient access by the user*)
val trace_induct = Ind_Syntax.trace;