(* 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
(*Make a definition lhs==rhs, checking that vars on lhs contain those of rhs*)
fun mk_defpair (lhs, rhs) =
let val Const(name, _) = head_of lhs
val dummy = assert (term_vars rhs subset term_vars lhs
andalso
term_frees rhs subset term_frees lhs
andalso
term_tvars rhs subset term_tvars lhs
andalso
term_tfrees rhs subset term_tfrees lhs)
("Extra variables on RHS in definition of " ^ name)
in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
fun get_def thy s = get_axiom thy (s^"_def");
fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
(*export to Pure/library? *)
fun assert_all pred l msg_fn =
let fun asl [] = ()
| asl (x::xs) = if pred x then asl xs
else error (msg_fn x)
in asl l end;
(** Abstract syntax definitions for FOL and ZF **)
val iT = Type("i",[])
and oT = Type("o",[]);
fun ap t u = t$u;
fun app t (u1,u2) = t $ u1 $ u2;
(*Given u expecting arguments of types [T1,...,Tn], create term of
type T1*...*Tn => i using split*)
fun ap_split split u [ ] = Abs("null", iT, u)
| ap_split split u [_] = u
| ap_split split u [_,_] = split $ u
| ap_split split u (T::Ts) =
split $ (Abs("v", T, ap_split split (u $ Bound(length Ts - 2)) Ts));
val conj = Const("op &", [oT,oT]--->oT)
and disj = Const("op |", [oT,oT]--->oT)
and imp = Const("op -->", [oT,oT]--->oT);
val eq_const = Const("op =", [iT,iT]--->oT);
val mem_const = Const("op :", [iT,iT]--->oT);
val exists_const = Const("Ex", [iT-->oT]--->oT);
fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P));
val all_const = Const("All", [iT-->oT]--->oT);
fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P));
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
fun mk_all_imp (A,P) =
all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
val Part_const = Const("Part", [iT,iT-->iT]--->iT);
val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
val Trueprop = Const("Trueprop",oT-->propT);
fun mk_tprop P = Trueprop $ P;
(*Prove a goal stated as a term, with exception handling*)
fun prove_term sign defs (P,tacsf) =
let val ct = cterm_of sign P
in prove_goalw_cterm defs ct tacsf
handle e => (writeln ("Exception in proof of\n" ^
string_of_cterm ct);
raise e)
end;
(*Read an assumption in the given theory*)
fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
fun readtm sign T a =
read_cterm sign (a,T) |> term_of
handle ERROR => error ("The error above occurred for " ^ a);
(*Skipping initial blanks, find the first identifier*)
fun scan_to_id s =
s |> explode |> take_prefix is_blank |> #2 |> Lexicon.scan_id |> #1
handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
fun is_backslash c = c = "\\";
(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
Does not handle the \ddd form; no error checking*)
fun escape [] = []
| escape cs = (case take_prefix (not o is_backslash) cs of
(front, []) => front
| (front, _::"n"::rest) => front @ ("\n" :: escape rest)
| (front, _::"t"::rest) => front @ ("\t" :: escape rest)
| (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
| (front, _::"\""::rest) => front @ ("\"" :: escape rest)
| (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
| (front, b::c::rest) =>
if is_blank c (*remove any further blanks and the following \ *)
then front @ escape (tl (snd (take_prefix is_blank rest)))
else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
(*Remove the first and last charaters -- presumed to be quotes*)
val trim = implode o escape o rev o tl o rev o tl o explode;
(*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("op :",_) $ t $ X) =
deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
| chk_prem rec_hd t =
deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
(*Inverse of varifyT. Move to Pure/type.ML?*)
fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
| unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
| unvarifyT T = T;
(*Inverse of varify. Move to Pure/logic.ML?*)
fun unvarify (Const(a,T)) = Const(a, unvarifyT T)
| unvarify (Var((a,0), T)) = Free(a, unvarifyT T)
| unvarify (Var(ixn,T)) = Var(ixn, unvarifyT T) (*non-zero index!*)
| unvarify (Abs (a,T,body)) = Abs (a, unvarifyT T, unvarify body)
| unvarify (f$t) = unvarify f $ unvarify t
| unvarify t = t;
(*Make distinct individual variables a1, a2, a3, ..., an. *)
fun mk_frees a [] = []
| mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
(*Return the conclusion of a rule, of the form t:X*)
fun rule_concl rl =
let val Const("Trueprop",_) $ (Const("op :",_) $ 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 (equalityD1 RS subsetD RS CollectD2));
(*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]));
(** For datatype definitions **)
fun dest_mem (Const("op :",_) $ 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 (readtm sign 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 = 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 (rec_tm, constructs) =
let fun mk_intr ((id,T,syn), name, args, prems) =
Logic.list_implies
(map mk_tprop prems,
mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm))
in map mk_intr constructs end;
val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
val Un = Const("op Un", [iT,iT]--->iT)
and empty = Const("0", iT)
and univ = Const("univ", iT-->iT)
and quniv = Const("quniv", iT-->iT);
(*Make a datatype's domain: form the union of its set parameters*)
fun union_params rec_tm =
let val (_,args) = strip_comb rec_tm
in case (filter (fn arg => type_of arg = iT) args) of
[] => empty
| iargs => fold_bal (app Un) iargs
end;
fun data_domain rec_tms =
replicate (length rec_tms) (univ $ union_params (hd rec_tms));
fun Codata_domain rec_tms =
replicate (length rec_tms) (quniv $ union_params (hd rec_tms));
(*Could go to FOL, but it's hardly general*)
val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
(fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
val def_trans = prove_goal IFOL.thy "[| 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 IFOL.thy "!!P. [| a=a; P |] ==> P"
(fn _ => [assume_tac 1]);
end;