--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/README Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,6 @@
+How to build TFL and run the Unify example.
+
+1. Invoke the current version of Isabelle-HOL.
+2. use "sys.sml";
+3. cd examples/Subst
+4. use "ROOT.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/WF1.ML Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,232 @@
+(* Title: HOL/WF.ML
+ ID: $Id$
+ Author: Konrad Slind
+ Copyright 1996 TU Munich
+
+For WF1.thy.
+*)
+
+open WF1;
+
+(* TFL variants *)
+goal WF.thy
+ "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
+by (strip_tac 1);
+by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1);
+by (assume_tac 1);
+by (fast_tac HOL_cs 1);
+qed"tfl_wf_induct";
+
+goal WF.thy "!f R. (x,a):R --> (cut f R a)(x) = f(x)";
+by (strip_tac 1);
+by (rtac cut_apply 1);
+by (assume_tac 1);
+qed"tfl_cut_apply";
+
+goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)";
+by (strip_tac 1);
+by (res_inst_tac [("r","R"), ("H","M"),
+ ("a","x"), ("f","f")] (eq_reflection RS def_wfrec) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "tfl_wfrec";
+
+(*----------------------------------------------------------------------------
+ * Proof that the inverse image into a wellfounded relation is wellfounded.
+ * The proof is relatively sloppy - I map to another version of
+ * wellfoundedness (every n.e. set has an R-minimal element) and transport
+ * the proof for that formulation over. I also didn't remember the existence
+ * of "set_cs" so no doubt the proof can be dramatically shortened!
+ *---------------------------------------------------------------------------*)
+goal HOL.thy "(~(!x. P x)) = (? x. ~(P x))";
+by (fast_tac HOL_cs 1);
+val th1 = result();
+
+goal HOL.thy "(~(? x. P x)) = (!x. ~(P x))";
+by (fast_tac HOL_cs 1);
+val th2 = result();
+
+goal HOL.thy "(~(x-->y)) = (x & (~ y))";
+by (fast_tac HOL_cs 1);
+val th3 = result();
+
+goal HOL.thy "((~ x) | y) = (x --> y)";
+by (fast_tac HOL_cs 1);
+val th4 = result();
+
+goal HOL.thy "(~(x & y)) = ((~ x) | (~ y))";
+by (fast_tac HOL_cs 1);
+val th5 = result();
+
+goal HOL.thy "(~(x | y)) = ((~ x) & (~ y))";
+by (fast_tac HOL_cs 1);
+val th6 = result();
+
+goal HOL.thy "(~(~x)) = x";
+by (fast_tac HOL_cs 1);
+val th7 = result();
+
+(* Using [th1,th2,th3,th4,th5,th6,th7] as rewrites drives negation inwards. *)
+val NNF_rews = map (fn th => th RS eq_reflection)[th1,th2,th3,th4,th5,th6,th7];
+
+(* The name "contrapos" is already taken. *)
+goal HOL.thy "(P --> Q) = ((~ Q) --> (~ P))";
+by (fast_tac HOL_cs 1);
+val ol_contrapos = result();
+
+(* Maps to another version of wellfoundedness *)
+val [p1] = goalw WF.thy [wf_def]
+"wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))";
+by (rtac allI 1);
+by (rtac (ol_contrapos RS ssubst) 1);
+by (rewrite_tac NNF_rews);
+by (rtac impI 1);
+by (rtac ((p1 RS spec) RS mp) 1);
+by (fast_tac HOL_cs 1);
+val wf_minimal = result();
+
+goalw WF.thy [wf_def]
+"(!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b)))) --> wf R";
+by (rtac impI 1);
+by (rtac allI 1);
+by (rtac (ol_contrapos RS ssubst) 1);
+by (rewrite_tac NNF_rews);
+by (rtac impI 1);
+by (etac allE 1);
+by (dtac mp 1);
+by (assume_tac 1);
+by (fast_tac HOL_cs 1);
+val minimal_wf = result();
+
+val wf_eq_minimal =
+ standard ((wf_minimal COMP ((minimal_wf RS mp) COMP iffI)) RS sym);
+
+goalw WF1.thy [inv_image_def,wf_eq_minimal RS eq_reflection]
+"wf(R) --> wf(inv_image R (f::'a=>'b))";
+by (strip_tac 1);
+by (etac exE 1);
+by (subgoal_tac "? (w::'b). ? (x::'a). Q x & (f x = w)" 1);
+by (rtac exI 2);
+by (rtac exI 2);
+by (rtac conjI 2);
+by (assume_tac 2);
+by (rtac refl 2);
+
+by (etac allE 1);
+by (dtac mp 1);
+by (assume_tac 1);
+by (eres_inst_tac [("P","? min. (? x. Q x & f x = min) & \
+ \ (! b. (b, min) : R --> ~ (? x. Q x & f x = b))")] rev_mp 1);
+by (etac thin_rl 1);
+by (etac thin_rl 1);
+by (rewrite_tac NNF_rews);
+by (rtac impI 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (etac exE 1);
+by (rtac exI 1);
+by (etac conjE 1);
+by (rtac conjI 1);
+by (assume_tac 1);
+by (hyp_subst_tac 1);
+by (rtac allI 1);
+by (rtac impI 1);
+by (etac CollectE 1);
+by (etac allE 1);
+by (dtac mp 1);
+by (rewrite_tac[fst_conv RS eq_reflection,snd_conv RS eq_reflection]);
+by (assume_tac 1);
+by (fast_tac HOL_cs 1);
+val wf_inv_image = result() RS mp;
+
+(* from Nat.ML *)
+goalw WF1.thy [wf_def] "wf(pred_nat)";
+by (strip_tac 1);
+by (nat_ind_tac "x" 1);
+by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject,
+ make_elim Suc_inject]) 2);
+by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
+val wf_pred_nat = result();
+
+goalw WF1.thy [wf_def,pred_list_def] "wf(pred_list)";
+by (strip_tac 1);
+by (List.list.induct_tac "x" 1);
+by (etac allE 1);
+by (etac impE 1);
+by (assume_tac 2);
+by (strip_tac 1);
+by (etac CollectE 1);
+by (asm_full_simp_tac (!simpset) 1);
+
+by (etac allE 1);
+by (etac impE 1);
+by (assume_tac 2);
+by (strip_tac 1);
+by (etac CollectE 1);
+by (etac exE 1);
+by (asm_full_simp_tac (!simpset) 1);
+by (etac conjE 1);
+by (hyp_subst_tac 1);
+by (assume_tac 1);
+qed "wf_pred_list";
+
+(*----------------------------------------------------------------------------
+ * All measures are wellfounded.
+ *---------------------------------------------------------------------------*)
+
+goalw WF1.thy [measure_def] "wf (measure f)";
+by (rtac wf_inv_image 1);
+by (rtac wf_trancl 1);
+by (rtac wf_pred_nat 1);
+qed "wf_measure";
+
+(*----------------------------------------------------------------------------
+ * Wellfoundedness of lexicographic combinations
+ *---------------------------------------------------------------------------*)
+
+val prems = goal Prod.thy "!a b. P((a,b)) ==> !p. P(p)";
+by (cut_facts_tac prems 1);
+by (rtac allI 1);
+by (rtac (surjective_pairing RS ssubst) 1);
+by (fast_tac HOL_cs 1);
+qed "split_all_pair";
+
+val [wfa,wfb] = goalw WF1.thy [wf_def,lex_prod_def]
+ "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
+by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
+by (rtac (wfa RS spec RS mp) 1);
+by (EVERY1 [rtac allI,rtac impI]);
+by (rtac (wfb RS spec RS mp) 1);
+by (fast_tac (set_cs addSEs [Pair_inject]) 1);
+qed "wf_lex_prod";
+
+(*----------------------------------------------------------------------------
+ * Wellfoundedness of relational product
+ *---------------------------------------------------------------------------*)
+val [wfa,wfb] = goalw WF1.thy [wf_def,rprod_def]
+ "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)";
+by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
+by (rtac (wfa RS spec RS mp) 1);
+by (EVERY1 [rtac allI,rtac impI]);
+by (rtac (wfb RS spec RS mp) 1);
+by (fast_tac (set_cs addSEs [Pair_inject]) 1);
+qed "wf_rel_prod";
+
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of subsets
+ *---------------------------------------------------------------------------*)
+
+goalw WF1.thy [wf_eq_minimal RS eq_reflection]
+ "wf(r) --> (!x y. (x,y):p --> (x,y):r) --> wf(p)";
+by (fast_tac set_cs 1);
+qed "wf_subset";
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of the empty relation.
+ *---------------------------------------------------------------------------*)
+
+goalw WF1.thy [wf_eq_minimal RS eq_reflection,emptyr_def]
+ "wf(emptyr)";
+by (fast_tac set_cs 1);
+qed "wf_emptyr";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/WF1.thy Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,27 @@
+(* Derived wellfounded relations, plus customized-for-TFL theorems from WF *)
+
+WF1 = List +
+consts
+ inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
+ measure :: "('a => nat) => ('a * 'a)set"
+ "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
+ rprod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
+ emptyr :: "('a * 'b) set"
+ pred_list :: "('a list * 'a list) set"
+
+defs
+ inv_image_def "inv_image R f == {p. (f(fst p), f(snd p)) : R}"
+
+ measure_def "measure == inv_image (trancl pred_nat)"
+
+ lex_prod_def "ra**rb == {p. ? a a' b b'.
+ p = ((a,b),(a',b')) &
+ ((a,a') : ra | a=a' & (b,b') : rb)}"
+
+ rprod_def "rprod ra rb == {p. ? a a' b b'.
+ p = ((a,b),(a',b')) &
+ ((a,a') : ra & (b,b') : rb)}"
+
+ emptyr_def "emptyr == {}"
+ pred_list_def "pred_list == {p. ? h. snd p = h#(fst p)}"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/dcterm.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,271 @@
+(*---------------------------------------------------------------------------
+ * Derived efficient cterm destructors.
+ *---------------------------------------------------------------------------*)
+
+structure Dcterm :
+sig
+ val caconv : cterm -> cterm -> bool
+ val mk_eq : cterm * cterm -> cterm
+ val mk_imp : cterm * cterm -> cterm
+ val mk_conj : cterm * cterm -> cterm
+ val mk_disj : cterm * cterm -> cterm
+ val mk_select : cterm * cterm -> cterm
+ val mk_forall : cterm * cterm -> cterm
+ val mk_exists : cterm * cterm -> cterm
+
+ val dest_conj : cterm -> cterm * cterm
+ val dest_const : cterm -> {Name:string, Ty:typ}
+ val dest_disj : cterm -> cterm * cterm
+ val dest_eq : cterm -> cterm * cterm
+ val dest_exists : cterm -> cterm * cterm
+ val dest_forall : cterm -> cterm * cterm
+ val dest_imp : cterm -> cterm * cterm
+ val dest_let : cterm -> cterm * cterm
+ val dest_neg : cterm -> cterm
+ val dest_pair : cterm -> cterm * cterm
+ val dest_select : cterm -> cterm * cterm
+ val dest_var : cterm -> {Name:string, Ty:typ}
+ val is_abs : cterm -> bool
+ val is_comb : cterm -> bool
+ val is_conj : cterm -> bool
+ val is_cons : cterm -> bool
+ val is_const : cterm -> bool
+ val is_disj : cterm -> bool
+ val is_eq : cterm -> bool
+ val is_exists : cterm -> bool
+ val is_forall : cterm -> bool
+ val is_imp : cterm -> bool
+ val is_let : cterm -> bool
+ val is_neg : cterm -> bool
+ val is_pair : cterm -> bool
+ val is_select : cterm -> bool
+ val is_var : cterm -> bool
+ val list_mk_comb : cterm * cterm list -> cterm
+ val list_mk_abs : cterm list -> cterm -> cterm
+ val list_mk_imp : cterm list * cterm -> cterm
+ val list_mk_exists : cterm list * cterm -> cterm
+ val list_mk_forall : cterm list * cterm -> cterm
+ val list_mk_conj : cterm list -> cterm
+ val list_mk_disj : cterm list -> cterm
+ val strip_abs : cterm -> cterm list * cterm
+ val strip_comb : cterm -> cterm * cterm list
+ val strip_conj : cterm -> cterm list
+ val strip_disj : cterm -> cterm list
+ val strip_exists : cterm -> cterm list * cterm
+ val strip_forall : cterm -> cterm list * cterm
+ val strip_imp : cterm -> cterm list * cterm
+ val strip_pair : cterm -> cterm list
+ val drop_prop : cterm -> cterm
+ val mk_prop : cterm -> cterm
+ end =
+struct
+
+fun ERR func mesg = Utils.ERR{module = "Dcterm", func = func, mesg = mesg};
+
+(*---------------------------------------------------------------------------
+ * General support routines
+ *---------------------------------------------------------------------------*)
+val can = Utils.can;
+val quote = Utils.quote;
+fun swap (x,y) = (y,x);
+val bool = Type("bool",[]);
+
+fun itlist f L base_value =
+ let fun it [] = base_value
+ | it (a::rst) = f a (it rst)
+ in it L
+ end;
+
+fun end_itlist f =
+let fun endit [] = raise ERR"end_itlist" "list too short"
+ | endit alist =
+ let val (base::ralist) = rev alist
+ in itlist f (rev ralist) base end
+in endit
+end;
+
+fun rev_itlist f =
+ let fun rev_it [] base = base
+ | rev_it (a::rst) base = rev_it rst (f a base)
+ in rev_it
+ end;
+
+(*---------------------------------------------------------------------------
+ * Alpha conversion.
+ *---------------------------------------------------------------------------*)
+fun caconv ctm1 ctm2 = Term.aconv(#t(rep_cterm ctm1),#t(rep_cterm ctm2));
+
+
+(*---------------------------------------------------------------------------
+ * Some simple constructor functions.
+ *---------------------------------------------------------------------------*)
+
+fun mk_const sign pr = cterm_of sign (Const pr);
+val mk_hol_const = mk_const (sign_of HOL.thy);
+
+fun list_mk_comb (h,[]) = h
+ | list_mk_comb (h,L) = rev_itlist (fn t1 => fn t2 => capply t2 t1) L h;
+
+
+fun mk_eq(lhs,rhs) =
+ let val ty = #T(rep_cterm lhs)
+ val c = mk_hol_const("op =", ty --> ty --> bool)
+ in list_mk_comb(c,[lhs,rhs])
+ end;
+
+local val c = mk_hol_const("op -->", bool --> bool --> bool)
+in fun mk_imp(ant,conseq) = list_mk_comb(c,[ant,conseq])
+end;
+
+fun mk_select (r as (Bvar,Body)) =
+ let val ty = #T(rep_cterm Bvar)
+ val c = mk_hol_const("Eps", (ty --> bool) --> ty)
+ in capply c (uncurry cabs r)
+ end;
+
+fun mk_forall (r as (Bvar,Body)) =
+ let val ty = #T(rep_cterm Bvar)
+ val c = mk_hol_const("All", (ty --> bool) --> bool)
+ in capply c (uncurry cabs r)
+ end;
+
+fun mk_exists (r as (Bvar,Body)) =
+ let val ty = #T(rep_cterm Bvar)
+ val c = mk_hol_const("Ex", (ty --> bool) --> bool)
+ in capply c (uncurry cabs r)
+ end;
+
+
+local val c = mk_hol_const("op &", bool --> bool --> bool)
+in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
+end;
+
+local val c = mk_hol_const("op |", bool --> bool --> bool)
+in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
+end;
+
+
+(*---------------------------------------------------------------------------
+ * The primitives.
+ *---------------------------------------------------------------------------*)
+fun dest_const ctm =
+ (case #t(rep_cterm ctm)
+ of Const(s,ty) => {Name = s, Ty = ty}
+ | _ => raise ERR "dest_const" "not a constant");
+
+fun dest_var ctm =
+ (case #t(rep_cterm ctm)
+ of Var((s,i),ty) => {Name=s, Ty=ty}
+ | Free(s,ty) => {Name=s, Ty=ty}
+ | _ => raise ERR "dest_var" "not a variable");
+
+
+(*---------------------------------------------------------------------------
+ * Derived destructor operations.
+ *---------------------------------------------------------------------------*)
+
+fun dest_monop expected tm =
+ let exception Fail
+ val (c,N) = dest_comb tm
+ in if (#Name(dest_const c) = expected) then N else raise Fail
+ end handle e => raise ERR "dest_monop" ("Not a(n) "^quote expected);
+
+fun dest_binop expected tm =
+ let val (M,N) = dest_comb tm
+ in (dest_monop expected M, N)
+ end handle e => raise ERR "dest_binop" ("Not a(n) "^quote expected);
+
+(* For "if-then-else"
+fun dest_triop expected tm =
+ let val (MN,P) = dest_comb tm
+ val (M,N) = dest_binop expected MN
+ in (M,N,P)
+ end handle e => raise ERR "dest_triop" ("Not a(n) "^quote expected);
+*)
+
+fun dest_binder expected tm =
+ dest_abs(dest_monop expected tm)
+ handle e => raise ERR "dest_binder" ("Not a(n) "^quote expected);
+
+
+val dest_neg = dest_monop "not"
+val dest_pair = dest_binop "Pair";
+val dest_eq = dest_binop "op ="
+val dest_imp = dest_binop "op -->"
+val dest_conj = dest_binop "op &"
+val dest_disj = dest_binop "op |"
+val dest_cons = dest_binop "op #"
+val dest_let = swap o dest_binop "Let";
+(* val dest_cond = dest_triop "if" *)
+val dest_select = dest_binder "Eps"
+val dest_exists = dest_binder "Ex"
+val dest_forall = dest_binder "All"
+
+(* Query routines *)
+
+val is_var = can dest_var
+val is_const = can dest_const
+val is_comb = can dest_comb
+val is_abs = can dest_abs
+val is_eq = can dest_eq
+val is_imp = can dest_imp
+val is_select = can dest_select
+val is_forall = can dest_forall
+val is_exists = can dest_exists
+val is_neg = can dest_neg
+val is_conj = can dest_conj
+val is_disj = can dest_disj
+(* val is_cond = can dest_cond *)
+val is_pair = can dest_pair
+val is_let = can dest_let
+val is_cons = can dest_cons
+
+
+(*---------------------------------------------------------------------------
+ * Iterated creation.
+ *---------------------------------------------------------------------------*)
+val list_mk_abs = itlist cabs;
+
+fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp(a,tm)) A c;
+fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t;
+fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall(v, b)) V t;
+val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj(c1, tm))
+val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
+
+(*---------------------------------------------------------------------------
+ * Iterated destruction. (To the "right" in a term.)
+ *---------------------------------------------------------------------------*)
+fun strip break tm =
+ let fun dest (p as (ctm,accum)) =
+ let val (M,N) = break ctm
+ in dest (N, M::accum)
+ end handle _ => p
+ in dest (tm,[])
+ end;
+
+fun rev2swap (x,l) = (rev l, x);
+
+val strip_comb = strip (swap o dest_comb) (* Goes to the "left" *)
+val strip_imp = rev2swap o strip dest_imp
+val strip_abs = rev2swap o strip dest_abs
+val strip_forall = rev2swap o strip dest_forall
+val strip_exists = rev2swap o strip dest_exists
+
+val strip_conj = rev o (op::) o strip dest_conj
+val strip_disj = rev o (op::) o strip dest_disj
+val strip_pair = rev o (op::) o strip dest_pair;
+
+
+(*---------------------------------------------------------------------------
+ * Going into and out of prop
+ *---------------------------------------------------------------------------*)
+local val prop = cterm_of (sign_of HOL.thy) (read"Trueprop")
+in fun mk_prop ctm =
+ case (#t(rep_cterm ctm))
+ of (Const("Trueprop",_)$_) => ctm
+ | _ => capply prop ctm
+end;
+
+fun drop_prop ctm = dest_monop "Trueprop" ctm handle _ => ctm;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/mask.sig Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,8 @@
+signature Mask_sig =
+sig
+ datatype 'a binding = |-> of ('a * 'a) (* infix 7 |->; *)
+
+ type mask
+ val ERR : mask
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/mask.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,16 @@
+(*---------------------------------------------------------------------------
+ * This structure is intended to shield TFL from any constructors already
+ * declared in the environment. In the Isabelle port, for example, there
+ * was already a datatype with "|->" being a constructor. In TFL we were
+ * trying to define a function "|->", but it failed in PolyML (which conforms
+ * better to the Standard) while the definition was accepted in NJ/SML
+ * (which doesn't always conform so well to the standard).
+ *---------------------------------------------------------------------------*)
+
+structure Mask : Mask_sig =
+struct
+
+ datatype 'a binding = |-> of ('a * 'a) (* infix 7 |->; *)
+
+ datatype mask = ERR
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/post.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,193 @@
+structure Tfl
+ :sig
+ structure Prim : TFL_sig
+
+ val tgoalw : theory -> thm list -> thm -> thm list
+ val tgoal: theory -> thm -> thm list
+
+ val WF_TAC : thm list -> tactic
+
+ val simplifier : thm -> thm
+ val std_postprocessor : theory
+ -> {induction:thm, rules:thm, TCs:term list list}
+ -> {induction:thm, rules:thm, nested_tcs:thm list}
+
+ val rfunction : theory
+ -> (thm list -> thm -> thm)
+ -> term -> term
+ -> {induction:thm, rules:thm,
+ tcs:term list, theory:theory}
+
+ val Rfunction : theory -> term -> term
+ -> {induction:thm, rules:thm,
+ theory:theory, tcs:term list}
+
+ val function : theory -> term -> {theory:theory, eq_ind : thm}
+ val lazyR_def : theory -> term -> {theory:theory, eqns : thm}
+
+ val tflcongs : theory -> thm list
+
+ end =
+struct
+ structure Prim = Prim
+
+ fun tgoalw thy defs thm =
+ let val L = Prim.termination_goals thm
+ open USyntax
+ val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L))
+ in goalw_cterm defs g
+ end;
+
+ val tgoal = Utils.C tgoalw [];
+
+ fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
+ val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod,
+ wf_pred_nat, wf_pred_list, wf_trancl];
+
+ val terminator = simp_tac(HOL_ss addsimps[pred_nat_def,pred_list_def,
+ fst_conv,snd_conv,
+ mem_Collect_eq,lessI]) 1
+ THEN TRY(fast_tac set_cs 1);
+
+ val simpls = [less_eq RS eq_reflection,
+ lex_prod_def, measure_def, inv_image_def,
+ fst_conv RS eq_reflection, snd_conv RS eq_reflection,
+ mem_Collect_eq RS eq_reflection(*, length_Cons RS eq_reflection*)];
+
+ val std_postprocessor = Prim.postprocess{WFtac = WFtac,
+ terminator = terminator,
+ simplifier = Prim.Rules.simpl_conv simpls};
+
+ val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @
+ [pred_nat_def,pred_list_def]);
+ fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
+
+
+local structure S = Prim.USyntax
+in
+fun func_of_cond_eqn tm =
+ #1(S.strip_comb(#lhs(S.dest_eq(#2(S.strip_forall(#2(S.strip_imp tm)))))))
+end;
+
+
+val concl = #2 o Prim.Rules.dest_thm;
+
+(*---------------------------------------------------------------------------
+ * Defining a function with an associated termination relation. Lots of
+ * postprocessing takes place.
+ *---------------------------------------------------------------------------*)
+local
+structure S = Prim.USyntax
+structure R = Prim.Rules
+structure U = Utils
+
+val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl
+
+fun id_thm th =
+ let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th))))
+ in S.aconv lhs rhs
+ end handle _ => false
+
+fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
+val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
+val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
+fun mk_meta_eq r = case concl_of r of
+ Const("==",_)$_$_ => r
+ | _$(Const("op =",_)$_$_) => r RS eq_reflection
+ | _ => r RS P_imp_P_eq_True
+fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L))
+
+fun join_assums th =
+ let val {sign,...} = rep_thm th
+ val tych = cterm_of sign
+ val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
+ val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *)
+ val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *)
+ val cntxt = U.union S.aconv cntxtl cntxtr
+ in
+ R.GEN_ALL
+ (R.DISCH_ALL
+ (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
+ end
+ val gen_all = S.gen_all
+in
+fun rfunction theory reducer R eqs =
+ let val _ = output(std_out, "Making definition.. ")
+ val _ = flush_out std_out
+ val {rules,theory, full_pats_TCs,
+ TCs,...} = Prim.gen_wfrec_definition theory {R=R,eqs=eqs}
+ val f = func_of_cond_eqn(concl(R.CONJUNCT1 rules handle _ => rules))
+ val _ = output(std_out, "Definition made.\n")
+ val _ = output(std_out, "Proving induction theorem.. ")
+ val _ = flush_out std_out
+ val ind = Prim.mk_induction theory f R full_pats_TCs
+ val _ = output(std_out, "Proved induction theorem.\n")
+ val pp = std_postprocessor theory
+ val _ = output(std_out, "Postprocessing.. ")
+ val _ = flush_out std_out
+ val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
+ val normal_tcs = Prim.termination_goals rules
+ in
+ case nested_tcs
+ of [] => (output(std_out, "Postprocessing done.\n");
+ {theory=theory, induction=induction, rules=rules,tcs=normal_tcs})
+ | L => let val _ = output(std_out, "Simplifying nested TCs.. ")
+ val (solved,simplified,stubborn) =
+ U.itlist (fn th => fn (So,Si,St) =>
+ if (id_thm th) then (So, Si, th::St) else
+ if (solved th) then (th::So, Si, St)
+ else (So, th::Si, St)) nested_tcs ([],[],[])
+ val simplified' = map join_assums simplified
+ val induction' = reducer (solved@simplified') induction
+ val rules' = reducer (solved@simplified') rules
+ val _ = output(std_out, "Postprocessing done.\n")
+ in
+ {induction = induction',
+ rules = rules',
+ tcs = normal_tcs @
+ map (gen_all o S.rhs o #2 o S.strip_forall o concl)
+ (simplified@stubborn),
+ theory = theory}
+ end
+ end
+ handle (e as Utils.ERR _) => Utils.Raise e
+ | e => print_exn e
+
+
+fun Rfunction thry =
+ rfunction thry
+ (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss)));
+
+
+end;
+
+
+local structure R = Prim.Rules
+in
+fun function theory eqs =
+ let val _ = output(std_out, "Making definition.. ")
+ val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs
+ val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
+ val _ = output(std_out, "Definition made.\n")
+ val _ = output(std_out, "Proving induction theorem.. ")
+ val induction = Prim.mk_induction theory f R full_pats_TCs
+ val _ = output(std_out, "Induction theorem proved.\n")
+ in {theory = theory,
+ eq_ind = standard (induction RS (rules RS conjI))}
+ end
+ handle (e as Utils.ERR _) => Utils.Raise e
+ | e => print_exn e
+end;
+
+
+fun lazyR_def theory eqs =
+ let val {rules,theory, ...} = Prim.lazyR_def theory eqs
+ in {eqns=rules, theory=theory}
+ end
+ handle (e as Utils.ERR _) => Utils.Raise e
+ | e => print_exn e;
+
+
+ val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG];
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/rules.new.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,825 @@
+structure FastRules : Rules_sig =
+struct
+
+open Utils;
+open Mask;
+infix 7 |->;
+
+structure USyntax = USyntax;
+structure S = USyntax;
+structure U = Utils;
+structure D = Dcterm;
+
+type Type = USyntax.Type
+type Preterm = USyntax.Preterm
+type Term = USyntax.Term
+type Thm = Thm.thm
+type Tactic = tactic;
+
+fun RULES_ERR{func,mesg} = Utils.ERR{module = "FastRules",func=func,mesg=mesg};
+
+nonfix ##; val ## = Utils.##; infix 4 ##;
+
+fun cconcl thm = D.drop_prop(#prop(crep_thm thm));
+fun chyps thm = map D.drop_prop(#hyps(crep_thm thm));
+
+fun dest_thm thm =
+ let val drop = S.drop_Trueprop
+ val {prop,hyps,...} = rep_thm thm
+ in (map drop hyps, drop prop)
+ end;
+
+
+
+(* Inference rules *)
+
+(*---------------------------------------------------------------------------
+ * Equality (one step)
+ *---------------------------------------------------------------------------*)
+fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq;
+fun SYM thm = thm RS sym;
+
+fun ALPHA thm ctm1 =
+ let val ctm2 = cprop_of thm
+ val ctm2_eq = reflexive ctm2
+ val ctm1_eq = reflexive ctm1
+ in equal_elim (transitive ctm2_eq ctm1_eq) thm
+ end;
+
+val BETA_RULE = Utils.I;
+
+
+(*----------------------------------------------------------------------------
+ * Type instantiation
+ *---------------------------------------------------------------------------*)
+fun INST_TYPE blist thm =
+ let val {sign,...} = rep_thm thm
+ val blist' = map (fn (TVar(idx,_) |-> B) => (idx, ctyp_of sign B)) blist
+ in Thm.instantiate (blist',[]) thm
+ end
+ handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""};
+
+
+(*----------------------------------------------------------------------------
+ * Implication and the assumption list
+ *
+ * Assumptions get stuck on the meta-language assumption list. Implications
+ * are in the object language, so discharging an assumption "A" from theorem
+ * "B" results in something that looks like "A --> B".
+ *---------------------------------------------------------------------------*)
+fun ASSUME ctm = Thm.assume (D.mk_prop ctm);
+
+
+(*---------------------------------------------------------------------------
+ * Implication in TFL is -->. Meta-language implication (==>) is only used
+ * in the implementation of some of the inference rules below.
+ *---------------------------------------------------------------------------*)
+fun MP th1 th2 = th2 RS (th1 RS mp);
+
+fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI;
+
+fun DISCH_ALL thm = Utils.itlist DISCH (#hyps (crep_thm thm)) thm;
+
+
+fun FILTER_DISCH_ALL P thm =
+ let fun check tm = U.holds P (S.drop_Trueprop (#t(rep_cterm tm)))
+ in U.itlist (fn tm => fn th => if (check tm) then DISCH tm th else th)
+ (chyps thm) thm
+ end;
+
+(* freezeT expensive! *)
+fun UNDISCH thm =
+ let val tm = D.mk_prop(#1(D.dest_imp(cconcl (freezeT thm))))
+ in implies_elim (thm RS mp) (ASSUME tm)
+ end
+ handle _ => raise RULES_ERR{func = "UNDISCH", mesg = ""};
+
+fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
+
+local val [p1,p2] = goal HOL.thy "(A-->B) ==> (B --> C) ==> (A-->C)"
+ val _ = by (rtac impI 1)
+ val _ = by (rtac (p2 RS mp) 1)
+ val _ = by (rtac (p1 RS mp) 1)
+ val _ = by (assume_tac 1)
+ val imp_trans = result()
+in
+fun IMP_TRANS th1 th2 = th2 RS (th1 RS imp_trans)
+end;
+
+(*----------------------------------------------------------------------------
+ * Conjunction
+ *---------------------------------------------------------------------------*)
+fun CONJUNCT1 thm = (thm RS conjunct1)
+fun CONJUNCT2 thm = (thm RS conjunct2);
+fun CONJUNCTS th = (CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th))
+ handle _ => [th];
+
+fun LIST_CONJ [] = raise RULES_ERR{func = "LIST_CONJ", mesg = "empty list"}
+ | LIST_CONJ [th] = th
+ | LIST_CONJ (th::rst) = MP(MP(conjI COMP (impI RS impI)) th) (LIST_CONJ rst);
+
+
+(*----------------------------------------------------------------------------
+ * Disjunction
+ *---------------------------------------------------------------------------*)
+local val {prop,sign,...} = rep_thm disjI1
+ val [P,Q] = term_vars prop
+ val disj1 = forall_intr (cterm_of sign Q) disjI1
+in
+fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
+end;
+
+local val {prop,sign,...} = rep_thm disjI2
+ val [P,Q] = term_vars prop
+ val disj2 = forall_intr (cterm_of sign P) disjI2
+in
+fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
+end;
+
+
+(*----------------------------------------------------------------------------
+ *
+ * A1 |- M1, ..., An |- Mn
+ * ---------------------------------------------------
+ * [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
+ *
+ *---------------------------------------------------------------------------*)
+
+
+fun EVEN_ORS thms =
+ let fun blue ldisjs [] _ = []
+ | blue ldisjs (th::rst) rdisjs =
+ let val tail = tl rdisjs
+ val rdisj_tl = D.list_mk_disj tail
+ in itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)
+ :: blue (ldisjs@[cconcl th]) rst tail
+ end handle _ => [itlist DISJ2 ldisjs th]
+ in
+ blue [] thms (map cconcl thms)
+ end;
+
+
+(*----------------------------------------------------------------------------
+ *
+ * A |- P \/ Q B,P |- R C,Q |- R
+ * ---------------------------------------------------
+ * A U B U C |- R
+ *
+ *---------------------------------------------------------------------------*)
+local val [p1,p2,p3] = goal HOL.thy "(P | Q) ==> (P --> R) ==> (Q --> R) ==> R"
+ val _ = by (rtac (p1 RS disjE) 1)
+ val _ = by (rtac (p2 RS mp) 1)
+ val _ = by (assume_tac 1)
+ val _ = by (rtac (p3 RS mp) 1)
+ val _ = by (assume_tac 1)
+ val tfl_exE = result()
+in
+fun DISJ_CASES th1 th2 th3 =
+ let val c = D.drop_prop(cconcl th1)
+ val (disj1,disj2) = D.dest_disj c
+ val th2' = DISCH disj1 th2
+ val th3' = DISCH disj2 th3
+ in
+ th3' RS (th2' RS (th1 RS tfl_exE))
+ end
+end;
+
+
+(*-----------------------------------------------------------------------------
+ *
+ * |- A1 \/ ... \/ An [A1 |- M, ..., An |- M]
+ * ---------------------------------------------------
+ * |- M
+ *
+ * Note. The list of theorems may be all jumbled up, so we have to
+ * first organize it to align with the first argument (the disjunctive
+ * theorem).
+ *---------------------------------------------------------------------------*)
+
+fun organize eq = (* a bit slow - analogous to insertion sort *)
+ let fun extract a alist =
+ let fun ex (_,[]) = raise RULES_ERR{func = "organize",
+ mesg = "not a permutation.1"}
+ | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
+ in ex ([],alist)
+ end
+ fun place [] [] = []
+ | place (a::rst) alist =
+ let val (item,next) = extract a alist
+ in item::place rst next
+ end
+ | place _ _ = raise RULES_ERR{func = "organize",
+ mesg = "not a permutation.2"}
+ in place
+ end;
+(* freezeT expensive! *)
+fun DISJ_CASESL disjth thl =
+ let val c = cconcl disjth
+ fun eq th atm = exists (D.caconv atm) (chyps th)
+ val tml = D.strip_disj c
+ fun DL th [] = raise RULES_ERR{func="DISJ_CASESL",mesg="no cases"}
+ | DL th [th1] = PROVE_HYP th th1
+ | DL th [th1,th2] = DISJ_CASES th th1 th2
+ | DL th (th1::rst) =
+ let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
+ in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
+ in DL (freezeT disjth) (organize eq tml thl)
+ end;
+
+
+(*----------------------------------------------------------------------------
+ * Universals
+ *---------------------------------------------------------------------------*)
+local (* this is fragile *)
+ val {prop,sign,...} = rep_thm spec
+ val x = hd (tl (term_vars prop))
+ val (TVar (indx,_)) = type_of x
+ val gspec = forall_intr (cterm_of sign x) spec
+in
+fun SPEC tm thm =
+ let val {sign,T,...} = rep_cterm tm
+ val gspec' = instantiate([(indx,ctyp_of sign T)],[]) gspec
+ in thm RS (forall_elim tm gspec')
+ end
+end;
+
+fun SPEC_ALL thm = rev_itlist SPEC (#1(D.strip_forall(cconcl thm))) thm;
+
+val ISPEC = SPEC
+val ISPECL = rev_itlist ISPEC;
+
+(* Not optimized! Too complicated. *)
+local val {prop,sign,...} = rep_thm allI
+ val [P] = add_term_vars (prop, [])
+ fun cty_theta s = map (fn (i,ty) => (i, ctyp_of s ty))
+ fun ctm_theta s = map (fn (i,tm2) =>
+ let val ctm2 = cterm_of s tm2
+ in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2)
+ end)
+ fun certify s (ty_theta,tm_theta) = (cty_theta s ty_theta,
+ ctm_theta s tm_theta)
+in
+fun GEN v th =
+ let val gth = forall_intr v th
+ val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
+ val P' = Abs(x,ty, S.drop_Trueprop rst) (* get rid of trueprop *)
+ val tsig = #tsig(Sign.rep_sg sign)
+ val theta = Pattern.match tsig (P,P')
+ val allI2 = instantiate (certify sign theta) allI
+ val thm = implies_elim allI2 gth
+ val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
+ val prop' = tp $ (A $ Abs(x,ty,M))
+ in ALPHA thm (cterm_of sign prop')
+ end
+end;
+
+val GENL = itlist GEN;
+
+fun GEN_ALL thm =
+ let val {prop,sign,...} = rep_thm thm
+ val tycheck = cterm_of sign
+ val vlist = map tycheck (add_term_vars (prop, []))
+ in GENL vlist thm
+ end;
+
+
+local fun string_of(s,_) = s
+in
+fun freeze th =
+ let val fth = freezeT th
+ val {prop,sign,...} = rep_thm fth
+ fun mk_inst (Var(v,T)) =
+ (cterm_of sign (Var(v,T)),
+ cterm_of sign (Free(string_of v, T)))
+ val insts = map mk_inst (term_vars prop)
+ in instantiate ([],insts) fth
+ end
+end;
+
+fun MATCH_MP th1 th2 =
+ if (D.is_forall (D.drop_prop(cconcl th1)))
+ then MATCH_MP (th1 RS spec) th2
+ else MP th1 th2;
+
+
+(*----------------------------------------------------------------------------
+ * Existentials
+ *---------------------------------------------------------------------------*)
+
+
+
+(*---------------------------------------------------------------------------
+ * Existential elimination
+ *
+ * A1 |- ?x.t[x] , A2, "t[v]" |- t'
+ * ------------------------------------ (variable v occurs nowhere)
+ * A1 u A2 |- t'
+ *
+ *---------------------------------------------------------------------------*)
+
+local val [p1,p2] = goal HOL.thy "(? x. P x) ==> (!x. P x --> Q) ==> Q"
+ val _ = by (rtac (p1 RS exE) 1)
+ val _ = by (rtac ((p2 RS allE) RS mp) 1)
+ val _ = by (assume_tac 2)
+ val _ = by (assume_tac 1)
+ val choose_thm = result()
+in
+fun CHOOSE(fvar,exth) fact =
+ let val lam = #2(dest_comb(D.drop_prop(cconcl exth)))
+ val redex = capply lam fvar
+ val {sign,t,...} = rep_cterm redex
+ val residue = cterm_of sign (S.beta_conv t)
+ in GEN fvar (DISCH residue fact) RS (exth RS choose_thm)
+ end
+end;
+
+
+local val {prop,sign,...} = rep_thm exI
+ val [P,x] = term_vars prop
+in
+fun EXISTS (template,witness) thm =
+ let val {prop,sign,...} = rep_thm thm
+ val P' = cterm_of sign P
+ val x' = cterm_of sign x
+ val abstr = #2(dest_comb template)
+ in
+ thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
+ end
+end;
+
+(*----------------------------------------------------------------------------
+ *
+ * A |- M
+ * ------------------- [v_1,...,v_n]
+ * A |- ?v1...v_n. M
+ *
+ *---------------------------------------------------------------------------*)
+
+fun EXISTL vlist th =
+ U.itlist (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
+ vlist th;
+
+
+(*----------------------------------------------------------------------------
+ *
+ * A |- M[x_1,...,x_n]
+ * ---------------------------- [(x |-> y)_1,...,(x |-> y)_n]
+ * A |- ?y_1...y_n. M
+ *
+ *---------------------------------------------------------------------------*)
+(* Could be improved, but needs "subst" for certified terms *)
+
+fun IT_EXISTS blist th =
+ let val {sign,...} = rep_thm th
+ val tych = cterm_of sign
+ val detype = #t o rep_cterm
+ val blist' = map (fn (x|->y) => (detype x |-> detype y)) blist
+ fun ?v M = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
+
+ in
+ U.itlist (fn (b as (r1 |-> r2)) => fn thm =>
+ EXISTS(?r2(S.subst[b] (S.drop_Trueprop(#prop(rep_thm thm)))), tych r1)
+ thm)
+ blist' th
+ end;
+
+(*---------------------------------------------------------------------------
+ * Faster version, that fails for some as yet unknown reason
+ * fun IT_EXISTS blist th =
+ * let val {sign,...} = rep_thm th
+ * val tych = cterm_of sign
+ * fun detype (x |-> y) = ((#t o rep_cterm) x |-> (#t o rep_cterm) y)
+ * in
+ * fold (fn (b as (r1|->r2), thm) =>
+ * EXISTS(D.mk_exists(r2, tych(S.subst[detype b](#t(rep_cterm(cconcl thm))))),
+ * r1) thm) blist th
+ * end;
+ *---------------------------------------------------------------------------*)
+
+(*----------------------------------------------------------------------------
+ * Rewriting
+ *---------------------------------------------------------------------------*)
+
+fun SUBS thl =
+ rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl);
+
+val simplify = rewrite_rule;
+
+local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
+in
+fun simpl_conv thl ctm =
+ rew_conv (Thm.mss_of (#simps(rep_ss HOL_ss)@thl)) ctm
+ RS meta_eq_to_obj_eq
+end;
+
+local fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1])
+in
+val RIGHT_ASSOC = rewrite_rule [prover"((a|b)|c) = (a|(b|c))" RS eq_reflection]
+val ASM = refl RS iffD1
+end;
+
+
+
+
+(*---------------------------------------------------------------------------
+ * TERMINATION CONDITION EXTRACTION
+ *---------------------------------------------------------------------------*)
+
+
+
+val bool = S.bool
+val prop = Type("prop",[]);
+
+(* Object language quantifier, i.e., "!" *)
+fun Forall v M = S.mk_forall{Bvar=v, Body=M};
+
+
+(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
+fun is_cong thm =
+ let val {prop, ...} = rep_thm thm
+ in case prop
+ of (Const("==>",_)$(Const("Trueprop",_)$ _) $
+ (Const("==",_) $ (Const ("cut",_) $ f $ R $ a $ x) $ _)) => false
+ | _ => true
+ end;
+
+
+
+fun dest_equal(Const ("==",_) $
+ (Const ("Trueprop",_) $ lhs)
+ $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
+ | dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
+ | dest_equal tm = S.dest_eq tm;
+
+
+fun get_rhs tm = #rhs(dest_equal (S.drop_Trueprop tm));
+fun get_lhs tm = #lhs(dest_equal (S.drop_Trueprop tm));
+
+fun variants FV vlist =
+ rev(#1(U.rev_itlist (fn v => fn (V,W) =>
+ let val v' = S.variant W v
+ in (v'::V, v'::W) end)
+ vlist ([],FV)));
+
+
+fun dest_all(Const("all",_) $ (a as Abs _)) = S.dest_abs a
+ | dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};
+
+val is_all = Utils.can dest_all;
+
+fun strip_all fm =
+ if (is_all fm)
+ then let val {Bvar,Body} = dest_all fm
+ val (bvs,core) = strip_all Body
+ in ((Bvar::bvs), core)
+ end
+ else ([],fm);
+
+fun break_all(Const("all",_) $ Abs (_,_,body)) = body
+ | break_all _ = raise RULES_ERR{func = "break_all", mesg = "not a !!"};
+
+fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =
+ let val (L,core) = list_break_all body
+ in ((s,ty)::L, core)
+ end
+ | list_break_all tm = ([],tm);
+
+(*---------------------------------------------------------------------------
+ * Rename a term of the form
+ *
+ * !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
+ * ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
+ * to one of
+ *
+ * !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
+ * ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
+ *
+ * This prevents name problems in extraction, and helps the result to read
+ * better. There is a problem with varstructs, since they can introduce more
+ * than n variables, and some extra reasoning needs to be done.
+ *---------------------------------------------------------------------------*)
+
+fun get ([],_,L) = rev L
+ | get (ant::rst,n,L) =
+ case (list_break_all ant)
+ of ([],_) => get (rst, n+1,L)
+ | (vlist,body) =>
+ let val eq = Logic.strip_imp_concl body
+ val (f,args) = S.strip_comb (get_lhs eq)
+ val (vstrl,_) = S.strip_abs f
+ val names = map (#Name o S.dest_var)
+ (variants (S.free_vars body) vstrl)
+ in get (rst, n+1, (names,n)::L)
+ end handle _ => get (rst, n+1, L);
+
+(* Note: rename_params_rule counts from 1, not 0 *)
+fun rename thm =
+ let val {prop,sign,...} = rep_thm thm
+ val tych = cterm_of sign
+ val ants = Logic.strip_imp_prems prop
+ val news = get (ants,1,[])
+ in
+ U.rev_itlist rename_params_rule news thm
+ end;
+
+
+(*---------------------------------------------------------------------------
+ * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
+ *---------------------------------------------------------------------------*)
+
+fun list_beta_conv tm =
+ let fun rbeta th = transitive th (beta_conversion(#2(D.dest_eq(cconcl th))))
+ fun iter [] = reflexive tm
+ | iter (v::rst) = rbeta (combination(iter rst) (reflexive v))
+ in iter end;
+
+
+(*---------------------------------------------------------------------------
+ * Trace information for the rewriter
+ *---------------------------------------------------------------------------*)
+val term_ref = ref[] : term list ref
+val mss_ref = ref [] : meta_simpset list ref;
+val thm_ref = ref [] : thm list ref;
+val tracing = ref false;
+
+fun say s = if !tracing then (output(std_out,s); flush_out std_out) else ();
+
+fun print_thms s L =
+ (say s;
+ map (fn th => say (string_of_thm th ^"\n")) L;
+ say"\n");
+
+fun print_cterms s L =
+ (say s;
+ map (fn th => say (string_of_cterm th ^"\n")) L;
+ say"\n");
+
+(*---------------------------------------------------------------------------
+ * General abstraction handlers, should probably go in USyntax.
+ *---------------------------------------------------------------------------*)
+fun mk_aabs(vstr,body) = S.mk_abs{Bvar=vstr,Body=body}
+ handle _ => S.mk_pabs{varstruct = vstr, body = body};
+
+fun list_mk_aabs (vstrl,tm) =
+ U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
+
+fun dest_aabs tm =
+ let val {Bvar,Body} = S.dest_abs tm
+ in (Bvar,Body)
+ end handle _ => let val {varstruct,body} = S.dest_pabs tm
+ in (varstruct,body)
+ end;
+
+fun strip_aabs tm =
+ let val (vstr,body) = dest_aabs tm
+ val (bvs, core) = strip_aabs body
+ in (vstr::bvs, core)
+ end
+ handle _ => ([],tm);
+
+fun dest_combn tm 0 = (tm,[])
+ | dest_combn tm n =
+ let val {Rator,Rand} = S.dest_comb tm
+ val (f,rands) = dest_combn Rator (n-1)
+ in (f,Rand::rands)
+ end;
+
+
+
+
+local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
+ fun mk_fst tm =
+ let val ty = S.type_of tm
+ val {Tyop="*",Args=[fty,sty]} = S.dest_type ty
+ val fst = S.mk_const{Name="fst",Ty = ty --> fty}
+ in S.mk_comb{Rator=fst, Rand=tm}
+ end
+ fun mk_snd tm =
+ let val ty = S.type_of tm
+ val {Tyop="*",Args=[fty,sty]} = S.dest_type ty
+ val snd = S.mk_const{Name="snd",Ty = ty --> sty}
+ in S.mk_comb{Rator=snd, Rand=tm}
+ end
+in
+fun XFILL tych x vstruct =
+ let fun traverse p xocc L =
+ if (S.is_var p)
+ then tych xocc::L
+ else let val (p1,p2) = dest_pair p
+ in traverse p1 (mk_fst xocc) (traverse p2 (mk_snd xocc) L)
+ end
+ in
+ traverse vstruct x []
+end end;
+
+(*---------------------------------------------------------------------------
+ * Replace a free tuple (vstr) by a universally quantified variable (a).
+ * Note that the notion of "freeness" for a tuple is different than for a
+ * variable: if variables in the tuple also occur in any other place than
+ * an occurrences of the tuple, they aren't "free" (which is thus probably
+ * the wrong word to use).
+ *---------------------------------------------------------------------------*)
+
+fun VSTRUCT_ELIM tych a vstr th =
+ let val L = S.free_vars_lr vstr
+ val bind1 = tych (S.mk_prop (S.mk_eq{lhs=a, rhs=vstr}))
+ val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)
+ val thm2 = forall_intr_list (map tych L) thm1
+ val thm3 = forall_elim_list (XFILL tych a vstr) thm2
+ in refl RS
+ rewrite_rule[symmetric (surjective_pairing RS eq_reflection)] thm3
+ end;
+
+fun PGEN tych a vstr th =
+ let val a1 = tych a
+ val vstr1 = tych vstr
+ in
+ forall_intr a1
+ (if (S.is_var vstr)
+ then cterm_instantiate [(vstr1,a1)] th
+ else VSTRUCT_ELIM tych a vstr th)
+ end;
+
+
+(*---------------------------------------------------------------------------
+ * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
+ *
+ * (([x,y],N),vstr)
+ *---------------------------------------------------------------------------*)
+fun dest_pbeta_redex M n =
+ let val (f,args) = dest_combn M n
+ val _ = dest_aabs f
+ in (strip_aabs f,args)
+ end;
+
+fun pbeta_redex M n = U.can (U.C dest_pbeta_redex n) M;
+
+fun dest_impl tm =
+ let val ants = Logic.strip_imp_prems tm
+ val eq = Logic.strip_imp_concl tm
+ in (ants,get_lhs eq)
+ end;
+
+val pbeta_reduce = simpl_conv [split RS eq_reflection];
+val restricted = U.can(S.find_term
+ (U.holds(fn c => (#Name(S.dest_const c)="cut"))))
+
+fun CONTEXT_REWRITE_RULE(func,R){thms=[cut_lemma],congs,th} =
+ let val tc_list = ref[]: term list ref
+ val _ = term_ref := []
+ val _ = thm_ref := []
+ val _ = mss_ref := []
+ val cut_lemma' = (cut_lemma RS mp) RS eq_reflection
+ fun prover mss thm =
+ let fun cong_prover mss thm =
+ let val _ = say "cong_prover:\n"
+ val cntxt = prems_of_mss mss
+ val _ = print_thms "cntxt:\n" cntxt
+ val _ = say "cong rule:\n"
+ val _ = say (string_of_thm thm^"\n")
+ val _ = thm_ref := (thm :: !thm_ref)
+ val _ = mss_ref := (mss :: !mss_ref)
+ (* Unquantified eliminate *)
+ fun uq_eliminate (thm,imp,sign) =
+ let val tych = cterm_of sign
+ val _ = print_cterms "To eliminate:\n" [tych imp]
+ val ants = map tych (Logic.strip_imp_prems imp)
+ val eq = Logic.strip_imp_concl imp
+ val lhs = tych(get_lhs eq)
+ val mss' = add_prems(mss, map ASSUME ants)
+ val lhs_eq_lhs1 = rewrite_cterm(false,true)mss' prover lhs
+ handle _ => reflexive lhs
+ val _ = print_thms "proven:\n" [lhs_eq_lhs1]
+ val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
+ val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
+ in
+ lhs_eeq_lhs2 COMP thm
+ end
+ fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
+ let val ((vstrl,_),args) = dest_pbeta_redex lhs_eq(length vlist)
+ val true = forall (fn (tm1,tm2) => S.aconv tm1 tm2)
+ (Utils.zip vlist args)
+(* val fbvs1 = variants (S.free_vars imp) fbvs *)
+ val imp_body1 = S.subst (map (op|->) (U.zip args vstrl))
+ imp_body
+ val tych = cterm_of sign
+ val ants1 = map tych (Logic.strip_imp_prems imp_body1)
+ val eq1 = Logic.strip_imp_concl imp_body1
+ val Q = get_lhs eq1
+ val QeqQ1 = pbeta_reduce (tych Q)
+ val Q1 = #2(D.dest_eq(cconcl QeqQ1))
+ val mss' = add_prems(mss, map ASSUME ants1)
+ val Q1eeqQ2 = rewrite_cterm (false,true) mss' prover Q1
+ handle _ => reflexive Q1
+ val Q2 = get_rhs(S.drop_Trueprop(#prop(rep_thm Q1eeqQ2)))
+ val Q3 = tych(S.list_mk_comb(list_mk_aabs(vstrl,Q2),vstrl))
+ val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection)
+ val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
+ val QeeqQ3 = transitive thA Q2eeqQ3 handle _ =>
+ ((Q2eeqQ3 RS meta_eq_to_obj_eq)
+ RS ((thA RS meta_eq_to_obj_eq) RS trans))
+ RS eq_reflection
+ val impth = implies_intr_list ants1 QeeqQ3
+ val impth1 = impth RS meta_eq_to_obj_eq
+ (* Need to abstract *)
+ val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
+ in ant_th COMP thm
+ end
+ fun q_eliminate (thm,imp,sign) =
+ let val (vlist,imp_body) = strip_all imp
+ val (ants,Q) = dest_impl imp_body
+ in if (pbeta_redex Q) (length vlist)
+ then pq_eliminate (thm,sign,vlist,imp_body,Q)
+ else
+ let val tych = cterm_of sign
+ val ants1 = map tych ants
+ val mss' = add_prems(mss, map ASSUME ants1)
+ val Q_eeq_Q1 = rewrite_cterm(false,true) mss'
+ prover (tych Q)
+ handle _ => reflexive (tych Q)
+ val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
+ val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
+ val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
+ in
+ ant_th COMP thm
+ end end
+
+ fun eliminate thm =
+ case (rep_thm thm)
+ of {prop = (Const("==>",_) $ imp $ _), sign, ...} =>
+ eliminate
+ (if not(is_all imp)
+ then uq_eliminate (thm,imp,sign)
+ else q_eliminate (thm,imp,sign))
+ (* Assume that the leading constant is ==, *)
+ | _ => thm (* if it is not a ==> *)
+ in Some(eliminate (rename thm))
+ end handle _ => None
+
+ fun restrict_prover mss thm =
+ let val _ = say "restrict_prover:\n"
+ val cntxt = rev(prems_of_mss mss)
+ val _ = print_thms "cntxt:\n" cntxt
+ val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
+ sign,...} = rep_thm thm
+ fun genl tm = let val vlist = U.set_diff (U.curry(op aconv))
+ (add_term_frees(tm,[])) [func,R]
+ in U.itlist Forall vlist tm
+ end
+ (*--------------------------------------------------------------
+ * This actually isn't quite right, since it will think that
+ * not-fully applied occs. of "f" in the context mean that the
+ * current call is nested. The real solution is to pass in a
+ * term "f v1..vn" which is a pattern that any full application
+ * of "f" will match.
+ *-------------------------------------------------------------*)
+ val func_name = #Name(S.dest_const func handle _ =>
+ S.dest_var func)
+ fun is_func tm = (#Name(S.dest_const tm handle _ =>
+ S.dest_var tm) = func_name)
+ handle _ => false
+ val nested = U.can(S.find_term is_func)
+ val rcontext = rev cntxt
+ val cncl = S.drop_Trueprop o #prop o rep_thm
+ val antl = case rcontext of [] => []
+ | _ => [S.list_mk_conj(map cncl rcontext)]
+ val TC = genl(S.list_mk_imp(antl, A))
+ val _ = print_cterms "func:\n" [cterm_of sign func]
+ val _ = print_cterms "TC:\n" [cterm_of sign (S.mk_prop TC)]
+ val _ = tc_list := (TC :: !tc_list)
+ val nestedp = nested TC
+ val _ = if nestedp then say "nested\n" else say "not_nested\n"
+ val _ = term_ref := ([func,TC]@(!term_ref))
+ val th' = if nestedp then raise RULES_ERR{func = "solver",
+ mesg = "nested function"}
+ else let val cTC = cterm_of sign (S.mk_prop TC)
+ in case rcontext of
+ [] => SPEC_ALL(ASSUME cTC)
+ | _ => MP (SPEC_ALL (ASSUME cTC))
+ (LIST_CONJ rcontext)
+ end
+ val th'' = th' RS thm
+ in Some (th'')
+ end handle _ => None
+ in
+ (if (is_cong thm) then cong_prover else restrict_prover) mss thm
+ end
+ val ctm = cprop_of th
+ val th1 = rewrite_cterm(false,true) (add_congs(mss_of [cut_lemma'], congs))
+ prover ctm
+ val th2 = equal_elim th1 th
+ in
+ (th2, U.filter (not o restricted) (!tc_list))
+ end;
+
+
+
+fun prove (tm,tac) =
+ let val {t,sign,...} = rep_cterm tm
+ val ptm = cterm_of sign(S.mk_prop t)
+ in
+ freeze(prove_goalw_cterm [] ptm (fn _ => [tac]))
+ end;
+
+
+end; (* Rules *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/rules.sig Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,65 @@
+signature Rules_sig =
+sig
+(* structure USyntax : USyntax_sig *)
+ type Type
+ type Preterm
+ type Term
+ type Thm
+ type Tactic
+ type 'a binding
+
+ val dest_thm : Thm -> Preterm list * Preterm
+
+ (* Inference rules *)
+ val REFL :Term -> Thm
+ val ASSUME :Term -> Thm
+ val MP :Thm -> Thm -> Thm
+ val MATCH_MP :Thm -> Thm -> Thm
+ val CONJUNCT1 :Thm -> Thm
+ val CONJUNCT2 :Thm -> Thm
+ val CONJUNCTS :Thm -> Thm list
+ val DISCH :Term -> Thm -> Thm
+ val UNDISCH :Thm -> Thm
+ val INST_TYPE :Type binding list -> Thm -> Thm
+ val SPEC :Term -> Thm -> Thm
+ val ISPEC :Term -> Thm -> Thm
+ val ISPECL :Term list -> Thm -> Thm
+ val GEN :Term -> Thm -> Thm
+ val GENL :Term list -> Thm -> Thm
+ val BETA_RULE :Thm -> Thm
+ val LIST_CONJ :Thm list -> Thm
+
+ val SYM : Thm -> Thm
+ val DISCH_ALL : Thm -> Thm
+ val FILTER_DISCH_ALL : (Preterm -> bool) -> Thm -> Thm
+ val SPEC_ALL : Thm -> Thm
+ val GEN_ALL : Thm -> Thm
+ val IMP_TRANS : Thm -> Thm -> Thm
+ val PROVE_HYP : Thm -> Thm -> Thm
+
+ val CHOOSE : Term * Thm -> Thm -> Thm
+ val EXISTS : Term * Term -> Thm -> Thm
+ val EXISTL : Term list -> Thm -> Thm
+ val IT_EXISTS : Term binding list -> Thm -> Thm
+
+ val EVEN_ORS : Thm list -> Thm list
+ val DISJ_CASESL : Thm -> Thm list -> Thm
+
+ val SUBS : Thm list -> Thm -> Thm
+ val simplify : Thm list -> Thm -> Thm
+ val simpl_conv : Thm list -> Term -> Thm
+
+(* For debugging my isabelle solver in the conditional rewriter *)
+(*
+ val term_ref : Preterm list ref
+ val thm_ref : Thm list ref
+ val mss_ref : meta_simpset list ref
+ val tracing :bool ref
+*)
+ val CONTEXT_REWRITE_RULE : Preterm * Preterm
+ -> {thms:Thm list,congs: Thm list, th:Thm}
+ -> Thm * Preterm list
+ val RIGHT_ASSOC : Thm -> Thm
+
+ val prove : Term * Tactic -> Thm
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/sys.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,48 @@
+(* Compile the TFL system *)
+
+(* Portability stuff *)
+nonfix prefix;
+use"mask.sig";
+use"mask.sml";
+
+(* Establish a base of common and/or helpful functions. *)
+use "utils.sig";
+use "utils.sml";
+
+(* Get the specifications - these are independent of any system *)
+use "usyntax.sig";
+use "rules.sig";
+use "thry.sig";
+use "thms.sig";
+use "tfl.sig";
+
+(*----------------------------------------------------------------------------
+ * Load the TFL functor - this is defined totally in terms of the
+ * above interfaces.
+ *---------------------------------------------------------------------------*)
+
+use "tfl.sml";
+
+structure Utils = UTILS(val int_to_string = string_of_int);
+
+(*----------------------------------------------------------------------------
+ * Supply implementations
+ *---------------------------------------------------------------------------*)
+
+val _ = use_thy"WF1"; (* Wellfoundedness theory *)
+
+use "usyntax.sml";
+use "thms.sml";
+use"dcterm.sml"; use"rules.new.sml";
+use "thry.sml";
+
+
+(*----------------------------------------------------------------------------
+ * Link system and specialize for Isabelle
+ *---------------------------------------------------------------------------*)
+structure Prim = TFL(structure Rules = FastRules
+ structure Thms = Thms
+ structure Thry = Thry);
+
+use"post.sml";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/test.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,301 @@
+fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
+fun read thy = term_of o cread thy;
+fun Term s = read WF1.thy s;
+
+fun Rfunc thy R eqs =
+ let val {induction,rules,theory,tcs} =
+ timeit(fn () => Tfl.Rfunction thy (read thy R) (read thy eqs))
+ in {induction=induction, rules=rules, theory=theory,
+ tcs = map (cterm_of (sign_of theory)) tcs}
+ end;
+
+val Rfunction = Rfunc WF1.thy;
+
+fun function tm = timeit (fn () => Tfl.function WF1.thy (Term tm));
+
+
+(*---------------------------------------------------------------------------
+ * Factorial. Notice how functions without pattern matching are often harder
+ * to deal with than those with! Unfortunately, not all functions can be
+ * described purely by pattern matching, e.g., "variant" as below.
+ *---------------------------------------------------------------------------*)
+function "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))";
+
+Rfunction"pred_nat"
+ "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))";
+
+function "(Fact 0 = (Suc 0)) & \
+ \ (Fact (Suc x) = (Fact x * Suc x))";
+
+Rfunction "pred_nat"
+ "(Fact 0 = (Suc 0)) & \
+ \ (Fact (Suc x) = (Fact x * Suc x))";
+
+(*---------------------------------------------------------------------------
+ * Fibonacci.
+ *---------------------------------------------------------------------------*)
+function "(Fib 0 = (Suc 0)) & \
+ \ (Fib (Suc 0) = (Suc 0)) & \
+ \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
+
+(* "<" doesn't currently work smoothly *)
+Rfunction"{p::(nat*nat). fst p < snd p}"
+ "(Fib 0 = (Suc 0)) & \
+ \ (Fib (Suc 0) = (Suc 0)) & \
+ \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
+
+
+(* "trancl pred" means "<" and works better *)
+Rfunction"trancl pred_nat"
+ "(Fib 0 = (Suc 0)) & \
+ \ (Fib (Suc 0) = (Suc 0)) & \
+ \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
+
+(*---------------------------------------------------------------------------
+ * Ackermann.
+ *---------------------------------------------------------------------------*)
+Rfunction"pred_nat ** pred_nat"
+ "(Ack (0,n) = (n + Suc 0)) & \
+ \ (Ack (Suc m,0) = (Ack (m, Suc 0))) & \
+ \ (Ack (Suc m, Suc n) = Ack (m, Ack (Suc m, n)))";
+
+(*---------------------------------------------------------------------------
+ * Almost primitive recursion.
+ *---------------------------------------------------------------------------*)
+function"(map2(f, [], L) = []) & \
+ \ (map2(f, h#t, []) = []) & \
+ \ (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))";
+
+(* Swap arguments *)
+function"(map2(([],L), f) = []) & \
+ \ (map2((h#t, []), f) = []) & \
+ \ (map2((h1#t1, h2#t2), f) = f h1 h2 # map2((t1,t2),f))";
+
+Rfunction
+ "measure((length o fst o snd)::('a=>'b=>'c)*'a list*'b list => nat)"
+ "(map2((f::'a=>'b=>'c), ([]::'a list), (L::'b list)) = []) & \
+\ (map2(f, h#t, []) = []) & \
+\ (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))";
+
+(*---------------------------------------------------------------------------
+ * Relation "R" holds stepwise in a list
+ *---------------------------------------------------------------------------*)
+function"(finiteRchain ((R::'a=>'a=>bool), ([]::'a list)) = True) & \
+ \ (finiteRchain (R, [x]) = True) & \
+ \ (finiteRchain (R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))";
+
+
+Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
+ "(finiteRchain((R::'a=>'a=>bool), ([]::'a list)) = True) & \
+ \ (finiteRchain(R, [x]) = True) & \
+ \ (finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))";
+
+(*---------------------------------------------------------------------------
+ * Quicksort.
+ *---------------------------------------------------------------------------*)
+function"(qsort(ord, []) = []) & \
+ \ (qsort(ord, x#rst) = \
+ \ qsort(ord,filter(not o ord x) rst) \
+ \ @[x]@ \
+ \ qsort(ord,filter(ord x) rst))";
+
+Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
+ "(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
+ \ (qsort(ord, x#rst) = \
+ \ qsort(ord,filter(not o ord x) rst) \
+ \ @[x]@ \
+ \ qsort(ord,filter(ord x) rst))";
+
+(*---------------------------------------------------------------------------
+ * Variant.
+ *---------------------------------------------------------------------------*)
+function"variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)";
+
+Rfunction
+ "measure(%(p::nat*nat list). length(filter(%y. fst(p) <= y) (snd p)))"
+ "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)";
+
+(*---------------------------------------------------------------------------
+ * Euclid's algorithm
+ *---------------------------------------------------------------------------*)
+function"(gcd ((0::nat),(y::nat)) = y) & \
+ \ (gcd (Suc x, 0) = Suc x) & \
+ \ (gcd (Suc x, Suc y) = \
+ \ (if (y <= x) then gcd(x - y, Suc y) \
+ \ else gcd(Suc x, y - x)))";
+
+
+(*---------------------------------------------------------------------------
+ * Wrong answer because Isabelle rewriter (going bottom-up) attempts to
+ * apply congruence rule for split to "split" but can't because split is only
+ * partly applied. It then fails, instead of just not doing the rewrite.
+ * Tobias has said he'll fix it.
+ *
+ * ... July 96 ... seems to have been fixed.
+ *---------------------------------------------------------------------------*)
+
+Rfunction"measure (split (op+) ::nat*nat=>nat)"
+ "(gcd ((0::nat),(y::nat)) = y) & \
+ \ (gcd (Suc x, 0) = Suc x) & \
+ \ (gcd (Suc x, Suc y) = \
+ \ (if (y <= x) then gcd(x - y, Suc y) \
+ \ else gcd(Suc x, y - x)))";
+
+(*---------------------------------------------------------------------------
+ * A simple nested function.
+ *---------------------------------------------------------------------------*)
+Rfunction"trancl pred_nat"
+ "(g 0 = 0) & \
+ \ (g(Suc x) = g(g x))";
+
+(*---------------------------------------------------------------------------
+ * A clever division algorithm. Primitive recursive.
+ *---------------------------------------------------------------------------*)
+function"(Div(0,x) = (0,0)) & \
+ \ (Div(Suc x, y) = \
+ \ (let (q,r) = Div(x,y) \
+ \ in if (y <= Suc r) then (Suc q,0) else (q, Suc r)))";
+
+Rfunction"inv_image pred_nat (fst::nat*nat=>nat)"
+ "(Div(0,x) = (0,0)) & \
+ \ (Div(Suc x, y) = \
+ \ (let q = fst(Div(x,y)); \
+ \ r = snd(Div(x,y)) \
+ \ in \
+ \ if (y <= Suc r) then (Suc q,0) else (q, Suc r)))";
+
+(*---------------------------------------------------------------------------
+ * Testing nested contexts.
+ *---------------------------------------------------------------------------*)
+function"(f(0,x) = (0,0)) & \
+ \ (f(Suc x, y) = \
+ \ (let z = x \
+ \ in \
+ \ if (0<y) then (0,0) else f(z,y)))";
+
+
+function"(f(0,x) = (0,0)) & \
+ \ (f(Suc x, y) = \
+ \ (if y = x \
+ \ then (if (0<y) then (0,0) else f(x,y)) \
+ \ else (x,y)))";
+
+
+(*---------------------------------------------------------------------------
+ * Naming trickery in lets.
+ *---------------------------------------------------------------------------*)
+
+(* No trick *)
+function "(test(x, []) = x) & \
+ \ (test(x,h#t) = (let y = Suc x in test(y,t)))";
+
+(* Trick *)
+function"(test(x, []) = x) & \
+ \ (test(x,h#t) = \
+ \ (let x = Suc x \
+ \ in \
+ \ test(x,t)))";
+
+(* Tricky naming, plus nested contexts *)
+function "vary(x, L) = \
+ \ (if (x mem L) \
+ \ then (let x = Suc x \
+ \ in vary(x,L)) \
+ \ else x)";
+
+
+(*---------------------------------------------------------------------------
+ * Handling paired lets of various kinds
+ *---------------------------------------------------------------------------*)
+function
+ "(Fib(0) = Suc 0) & \
+ \ (Fib (Suc 0) = Suc 0) & \
+ \ (Fib (Suc (Suc n)) = \
+ \ (let (x,y) = (Fib (Suc n), Fib n) in x+y))";
+
+
+function
+ "(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
+ \ (qsort(ord, x#rst) = \
+ \ (let (L1,L2) = (filter(not o ord x) rst, \
+ \ filter (ord x) rst) \
+ \ in \
+ \ qsort(ord,L1)@[x]@qsort(ord,L2)))";
+
+function"(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
+ \ (qsort(ord, x#rst) = \
+ \ (let (L1,L2,P) = (filter(not o ord x) rst, \
+ \ filter (ord x) rst, x) \
+ \ in \
+ \ qsort(ord,L1)@[x]@qsort(ord,L2)))";
+
+function"(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
+ \ (qsort(ord, x#rst) = \
+ \ (let (L1,L2) = (filter(not o ord x) rst, \
+ \ filter (ord x) rst); \
+ \ (p,q) = (x,rst) \
+ \ in \
+ \ qsort(ord,L1)@[x]@qsort(ord,L2)))";
+
+
+(*---------------------------------------------------------------------------
+ * A biggish function
+ *---------------------------------------------------------------------------*)
+
+function"(acc1(A,[],s,xss,zs,xs) = \
+\ (if xs=[] then (xss, zs) \
+\ else acc1(A, zs,s,(xss @ [xs]),[],[]))) & \
+\ (acc1(A,(y#ys), s, xss, zs, xs) = \
+\ (let s' = s; \
+\ zs' = (if fst A s' then [] else zs@[y]); \
+\ xs' = (if fst A s' then xs@zs@[y] else xs) \
+\ in \
+\ acc1(A, ys, s', xss, zs', xs')))";
+
+
+(*---------------------------------------------------------------------------
+ * Nested, with context.
+ *---------------------------------------------------------------------------*)
+Rfunction"pred_nat"
+ "(k 0 = 0) & \
+\ (k (Suc n) = (let x = k (Suc 0) \
+\ in if (0=Suc 0) then k (Suc(Suc 0)) else n))";
+
+
+(*---------------------------------------------------------------------------
+ * A function that partitions a list into two around a predicate "P".
+ *---------------------------------------------------------------------------*)
+val {theory,induction,rules,tcs} =
+ Rfunction
+ "inv_image pred_list \
+ \ ((fst o snd)::('a=>bool)*'a list*'a list*'a list => 'a list)"
+
+ "(part(P::'a=>bool, [], l1,l2) = (l1,l2)) & \
+\ (part(P, h#rst, l1,l2) = \
+\ (if P h then part(P,rst, h#l1, l2) \
+\ else part(P,rst, l1, h#l2)))";
+
+
+(*---------------------------------------------------------------------------
+ * Another quicksort.
+ *---------------------------------------------------------------------------*)
+Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
+ "(fqsort(ord,[]) = []) & \
+\ (fqsort(ord, x#rst) = \
+ \ (let less = fst(part((%y. ord y x), rst,([],[]))); \
+ \ more = snd(part((%y. ord y x), rst,([],[]))) \
+ \ in \
+ \ fqsort(ord,less)@[x]@fqsort(ord,more)))";
+
+Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
+ "(fqsort(ord,[]) = []) & \
+\ (fqsort(ord, x#rst) = \
+ \ (let (less,more) = part((%y. ord y x), rst,([],[])) \
+ \ in \
+ \ fqsort(ord,less)@[x]@fqsort(ord,more)))";
+
+
+(* Should fail on repeated variables. *)
+function"(And(x,[]) = x) & \
+ \ (And(y, y#t) = And(y, t))";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/test1.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,83 @@
+(*---------------------------------------------------------------------------
+ * Pattern matching extensions.
+ *---------------------------------------------------------------------------*)
+
+fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
+fun read thy = term_of o cread thy;
+fun Term s = read WF1.thy s;
+
+fun Rfunc thy R eqs =
+ let val {induction,rules,theory,tcs} =
+ timeit(fn () => Tfl.Rfunction thy (read thy R) (read thy eqs))
+ in {induction=induction, rules=rules, theory=theory,
+ tcs = map (cterm_of (sign_of theory)) tcs}
+ end;
+
+fun def tm = timeit (fn () => Tfl.function WF1.thy (Term tm));
+
+
+
+
+(*---------------------------------------------------------------------------
+ * Normal patterns
+ *---------------------------------------------------------------------------*)
+def "(f(x,y) = x+y)";
+
+def "(f1 0 = 1) & (f1 (Suc n) = 2)";
+
+(*---------------------------------------------------------------------------
+ * Omitted patterns
+ *---------------------------------------------------------------------------*)
+def "(f2 0 = 1)";
+
+def "(f3 (h#t) = h)";
+
+def "(f4 [a,b] = a) & (f4 [b] = b)";
+
+def "(f5 (0,0) = 0)";
+
+def "(f6 (0,0) = 0) & (f6 (0,Suc x) = x) & (f6 (Suc x, y) = y+x)";
+
+def "(f7 (Suc 0, h#t) = 1) & (f7 (Suc(Suc n),h1#h2#t) = h1)";
+
+def "(f8 (Suc(Suc n),h1#h2#t) = h1)";
+
+
+(*---------------------------------------------------------------------------
+ * Overlapping patterns
+ *---------------------------------------------------------------------------*)
+def "(f9 (h1#h2#t) = t) & (f9 x = x)";
+
+def "(g (x,0) = 1) & (g (0,x) = 2)";
+
+def "(g1 (0,x) = x) & (g1 (x,0) = x)";
+
+def "(g2 ([], a#b#x) = 1) & (g2 (a#b#x, y) = 2) & (g2 (z, a#y) = a)";
+
+def "(g3 (x,y,0) = 1) & (g3 (x,0,y) = 2) & (g3 (0,x,y) = x)";
+
+def "(g4 (0,y,z) = 1) & (g4 (x,0,z) = 2) & (g4 (x,y,0) = x)";
+
+def "(g5(0,x,y,z) = 1) & (g5(w,0,y,z) = 2) & (g5(w,x,0,z) = z) & \
+ \ (g5(w,x,y,0) = y)";
+
+def "(g6 (0,w,x,y,z) = 1) & (g6 (v,0,x,y,z) = 2) & (g6 (v,w,0,y,z) = z) & \
+ \ (g6 (v,w,x,0,z) = z) & (g6 (v,w,x,y,0) = 0)";
+
+def "(g7 [x, 0] = x) & (g7 [Suc v] = 1) & (g7 z = 2)";
+
+def "(g8 (h1#h2#h3#h4#h5#h6) = [h1,h2,h3,h4,h5]# g8 h6) & (g8 x = [x])";
+
+(* Normal *)
+def "(g9 (Suc(Suc x)) = 1) & (g9 (Suc x) = 2) & (g9 0 = 0)";
+
+(*---------------------------------------------------------------------------
+ * Inaccessible patterns
+ *---------------------------------------------------------------------------*)
+def "(h x = 1) & (h x = 2)";
+
+def "(h1 (x,0) = 1) & (h1 (x,Suc y) = 2) & \
+ \ (h1 (x,y) = x) & (h1 (x,y) = y)";
+
+def "(h2 (x,0) = 1) & (h2 (0,x) = 2) & \
+ \ (h2 (0,0) = 0) & (h2 (x,y) = x)";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/tfl.sig Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,65 @@
+signature TFL_sig =
+sig
+ structure Rules: Rules_sig
+ structure Thms : Thms_sig
+ structure Thry : Thry_sig
+ structure USyntax : USyntax_sig
+
+ type Preterm
+ type Term
+ type Thm
+ type Thry
+ type Tactic
+
+ datatype pattern = GIVEN of Preterm * int
+ | OMITTED of Preterm * int
+
+ val mk_functional : Thry -> Preterm
+ -> {functional:Preterm,
+ pats: pattern list}
+
+ val prim_wfrec_definition : Thry
+ -> {R:Preterm, functional:Preterm}
+ -> {def:Thm, corollary:Thm, theory:Thry}
+
+ val wfrec_eqns : Thry -> Preterm
+ -> {WFR : Preterm,
+ proto_def : Preterm,
+ extracta :(Thm * Preterm list) list,
+ pats : pattern list}
+
+
+ val gen_wfrec_definition : Thry
+ -> {R:Preterm, eqs:Preterm}
+ -> {theory:Thry,
+ rules :Thm,
+ TCs : Preterm list list,
+ full_pats_TCs :(Preterm * Preterm list) list,
+ patterns : pattern list}
+
+ val lazyR_def : Thry
+ -> Preterm
+ -> {theory:Thry,
+ rules :Thm,
+ R :Preterm,
+ full_pats_TCs :(Preterm * Preterm list) list,
+ patterns: pattern list}
+
+ val mk_induction : Thry
+ -> Preterm -> Preterm
+ -> (Preterm * Preterm list) list
+ -> Thm
+
+ val postprocess: {WFtac:Tactic, terminator:Tactic, simplifier:Term -> Thm}
+ -> Thry
+ -> {rules:Thm, induction:Thm, TCs:Preterm list list}
+ -> {rules:Thm, induction:Thm, nested_tcs:Thm list}
+
+ val termination_goals : Thm -> Preterm list
+
+ structure Context
+ : sig
+ val read : unit -> Thm list
+ val write : Thm list -> unit
+ end
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/tfl.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,922 @@
+functor TFL(structure Rules : Rules_sig
+ structure Thry : Thry_sig
+ structure Thms : Thms_sig
+ sharing type Rules.binding = Thry.binding =
+ Thry.USyntax.binding = Mask.binding
+ sharing type Rules.Type = Thry.Type = Thry.USyntax.Type
+ sharing type Rules.Preterm = Thry.Preterm = Thry.USyntax.Preterm
+ sharing type Rules.Term = Thry.Term = Thry.USyntax.Term
+ sharing type Thms.Thm = Rules.Thm = Thry.Thm) : TFL_sig =
+struct
+
+(* Declarations *)
+structure Thms = Thms;
+structure Rules = Rules;
+structure Thry = Thry;
+structure USyntax = Thry.USyntax;
+
+type Preterm = Thry.USyntax.Preterm;
+type Term = Thry.USyntax.Term;
+type Thm = Thms.Thm;
+type Thry = Thry.Thry;
+type Tactic = Rules.Tactic;
+
+
+(* Abbreviations *)
+structure R = Rules;
+structure S = USyntax;
+structure U = S.Utils;
+
+(* Declares 'a binding datatype *)
+open Mask;
+
+nonfix mem --> |-> ##;
+val --> = S.-->;
+val ## = U.##;
+
+infixr 3 -->;
+infixr 7 |->;
+infix 4 ##;
+
+val concl = #2 o R.dest_thm;
+val hyp = #1 o R.dest_thm;
+
+val list_mk_type = U.end_itlist (U.curry(op -->));
+
+fun flatten [] = []
+ | flatten (h::t) = h@flatten t;
+
+
+fun gtake f =
+ let fun grab(0,rst) = ([],rst)
+ | grab(n, x::rst) =
+ let val (taken,left) = grab(n-1,rst)
+ in (f x::taken, left) end
+ in grab
+ end;
+
+fun enumerate L =
+ rev(#1(U.rev_itlist (fn x => fn (alist,i) => ((x,i)::alist, i+1)) L ([],0)));
+
+fun stringize [] = ""
+ | stringize [i] = U.int_to_string i
+ | stringize (h::t) = (U.int_to_string h^", "^stringize t);
+
+
+fun TFL_ERR{func,mesg} = U.ERR{module = "Tfl", func = func, mesg = mesg};
+
+
+(*---------------------------------------------------------------------------
+ * The next function is common to pattern-match translation and
+ * proof of completeness of cases for the induction theorem.
+ *
+ * "gvvariant" make variables that are guaranteed not to be in vlist and
+ * furthermore, are guaranteed not to be equal to each other. The names of
+ * the variables will start with "v" and end in a number.
+ *---------------------------------------------------------------------------*)
+local val counter = ref 0
+in
+fun gvvariant vlist =
+ let val slist = ref (map (#Name o S.dest_var) vlist)
+ val mem = U.mem (U.curry (op=))
+ val _ = counter := 0
+ fun pass str =
+ if (mem str (!slist))
+ then ( counter := !counter + 1;
+ pass (U.concat"v" (U.int_to_string(!counter))))
+ else (slist := str :: !slist; str)
+ in
+ fn ty => S.mk_var{Name=pass "v", Ty=ty}
+ end
+end;
+
+
+(*---------------------------------------------------------------------------
+ * Used in induction theorem production. This is the simple case of
+ * partitioning up pattern rows by the leading constructor.
+ *---------------------------------------------------------------------------*)
+fun ipartition gv (constructors,rows) =
+ let fun pfail s = raise TFL_ERR{func = "partition.part", mesg = s}
+ fun part {constrs = [], rows = [], A} = rev A
+ | part {constrs = [], rows = _::_, A} = pfail"extra cases in defn"
+ | part {constrs = _::_, rows = [], A} = pfail"cases missing in defn"
+ | part {constrs = c::crst, rows, A} =
+ let val {Name,Ty} = S.dest_const c
+ val (L,_) = S.strip_type Ty
+ val (in_group, not_in_group) =
+ U.itlist (fn (row as (p::rst, rhs)) =>
+ fn (in_group,not_in_group) =>
+ let val (pc,args) = S.strip_comb p
+ in if (#Name(S.dest_const pc) = Name)
+ then ((args@rst, rhs)::in_group, not_in_group)
+ else (in_group, row::not_in_group)
+ end) rows ([],[])
+ val col_types = U.take S.type_of (length L, #1(hd in_group))
+ in
+ part{constrs = crst, rows = not_in_group,
+ A = {constructor = c,
+ new_formals = map gv col_types,
+ group = in_group}::A}
+ end
+ in part{constrs = constructors, rows = rows, A = []}
+ end;
+
+
+
+(*---------------------------------------------------------------------------
+ * This datatype carries some information about the origin of a
+ * clause in a function definition.
+ *---------------------------------------------------------------------------*)
+datatype pattern = GIVEN of S.Preterm * int
+ | OMITTED of S.Preterm * int
+
+fun psubst theta (GIVEN (tm,i)) = GIVEN(S.subst theta tm, i)
+ | psubst theta (OMITTED (tm,i)) = OMITTED(S.subst theta tm, i);
+
+fun dest_pattern (GIVEN (tm,i)) = ((GIVEN,i),tm)
+ | dest_pattern (OMITTED (tm,i)) = ((OMITTED,i),tm);
+
+val pat_of = #2 o dest_pattern;
+val row_of_pat = #2 o #1 o dest_pattern;
+
+(*---------------------------------------------------------------------------
+ * Produce an instance of a constructor, plus genvars for its arguments.
+ *---------------------------------------------------------------------------*)
+fun fresh_constr ty_match colty gv c =
+ let val {Ty,...} = S.dest_const c
+ val (L,ty) = S.strip_type Ty
+ val ty_theta = ty_match ty colty
+ val c' = S.inst ty_theta c
+ val gvars = map (S.inst ty_theta o gv) L
+ in (c', gvars)
+ end;
+
+
+(*---------------------------------------------------------------------------
+ * Goes through a list of rows and picks out the ones beginning with a
+ * pattern with constructor = Name.
+ *---------------------------------------------------------------------------*)
+fun mk_group Name rows =
+ U.itlist (fn (row as ((prefix, p::rst), rhs)) =>
+ fn (in_group,not_in_group) =>
+ let val (pc,args) = S.strip_comb p
+ in if ((#Name(S.dest_const pc) = Name) handle _ => false)
+ then (((prefix,args@rst), rhs)::in_group, not_in_group)
+ else (in_group, row::not_in_group) end)
+ rows ([],[]);
+
+(*---------------------------------------------------------------------------
+ * Partition the rows. Not efficient: we should use hashing.
+ *---------------------------------------------------------------------------*)
+fun partition _ _ (_,_,_,[]) = raise TFL_ERR{func="partition", mesg="no rows"}
+ | partition gv ty_match
+ (constructors, colty, res_ty, rows as (((prefix,_),_)::_)) =
+let val fresh = fresh_constr ty_match colty gv
+ fun part {constrs = [], rows, A} = rev A
+ | part {constrs = c::crst, rows, A} =
+ let val (c',gvars) = fresh c
+ val {Name,Ty} = S.dest_const c'
+ val (in_group, not_in_group) = mk_group Name rows
+ val in_group' =
+ if (null in_group) (* Constructor not given *)
+ then [((prefix, #2(fresh c)), OMITTED (S.ARB res_ty, ~1))]
+ else in_group
+ in
+ part{constrs = crst,
+ rows = not_in_group,
+ A = {constructor = c',
+ new_formals = gvars,
+ group = in_group'}::A}
+ end
+in part{constrs=constructors, rows=rows, A=[]}
+end;
+
+(*---------------------------------------------------------------------------
+ * Misc. routines used in mk_case
+ *---------------------------------------------------------------------------*)
+
+fun mk_pat c =
+ let val L = length(#1(S.strip_type(S.type_of c)))
+ fun build (prefix,tag,plist) =
+ let val (args,plist') = gtake U.I (L, plist)
+ in (prefix,tag,S.list_mk_comb(c,args)::plist') end
+ in map build
+ end;
+
+fun v_to_prefix (prefix, v::pats) = (v::prefix,pats)
+ | v_to_prefix _ = raise TFL_ERR{func="mk_case", mesg="v_to_prefix"};
+
+fun v_to_pats (v::prefix,tag, pats) = (prefix, tag, v::pats)
+ | v_to_pats _ = raise TFL_ERR{func="mk_case", mesg="v_to_pats"};
+
+
+(*----------------------------------------------------------------------------
+ * Translation of pattern terms into nested case expressions.
+ *
+ * This performs the translation and also builds the full set of patterns.
+ * Thus it supports the construction of induction theorems even when an
+ * incomplete set of patterns is given.
+ *---------------------------------------------------------------------------*)
+
+fun mk_case ty_info ty_match FV range_ty =
+ let
+ fun mk_case_fail s = raise TFL_ERR{func = "mk_case", mesg = s}
+ val fresh_var = gvvariant FV
+ val divide = partition fresh_var ty_match
+ fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
+ | expand constructors ty (row as ((prefix, p::rst), rhs)) =
+ if (S.is_var p)
+ then let val fresh = fresh_constr ty_match ty fresh_var
+ fun expnd (c,gvs) =
+ let val capp = S.list_mk_comb(c,gvs)
+ in ((prefix, capp::rst), psubst[p |-> capp] rhs)
+ end
+ in map expnd (map fresh constructors) end
+ else [row]
+ fun mk{rows=[],...} = mk_case_fail"no rows"
+ | mk{path=[], rows = ((prefix, []), rhs)::_} = (* Done *)
+ let val (tag,tm) = dest_pattern rhs
+ in ([(prefix,tag,[])], tm)
+ end
+ | mk{path=[], rows = _::_} = mk_case_fail"blunder"
+ | mk{path as u::rstp, rows as ((prefix, []), rhs)::rst} =
+ mk{path = path,
+ rows = ((prefix, [fresh_var(S.type_of u)]), rhs)::rst}
+ | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
+ let val (pat_rectangle,rights) = U.unzip rows
+ val col0 = map(hd o #2) pat_rectangle
+ in
+ if (U.all S.is_var col0)
+ then let val rights' = map(fn(v,e) => psubst[v|->u] e) (U.zip col0 rights)
+ val pat_rectangle' = map v_to_prefix pat_rectangle
+ val (pref_patl,tm) = mk{path = rstp,
+ rows = U.zip pat_rectangle' rights'}
+ in (map v_to_pats pref_patl, tm)
+ end
+ else
+ let val pty = S.type_of p
+ val ty_name = (#Tyop o S.dest_type) pty
+ in
+ case (ty_info ty_name)
+ of U.NONE => mk_case_fail("Not a known datatype: "^ty_name)
+ | U.SOME{case_const,constructors} =>
+ let val case_const_name = #Name(S.dest_const case_const)
+ val nrows = flatten (map (expand constructors pty) rows)
+ val subproblems = divide(constructors, pty, range_ty, nrows)
+ val groups = map #group subproblems
+ and new_formals = map #new_formals subproblems
+ and constructors' = map #constructor subproblems
+ val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
+ (U.zip new_formals groups)
+ val rec_calls = map mk news
+ val (pat_rect,dtrees) = U.unzip rec_calls
+ val case_functions = map S.list_mk_abs(U.zip new_formals dtrees)
+ val types = map S.type_of (case_functions@[u]) @ [range_ty]
+ val case_const' = S.mk_const{Name = case_const_name,
+ Ty = list_mk_type types}
+ val tree = S.list_mk_comb(case_const', case_functions@[u])
+ val pat_rect1 = flatten(U.map2 mk_pat constructors' pat_rect)
+ in (pat_rect1,tree)
+ end
+ end end
+ in mk
+ end;
+
+
+(* Repeated variable occurrences in a pattern are not allowed. *)
+fun FV_multiset tm =
+ case (S.dest_term tm)
+ of S.VAR v => [S.mk_var v]
+ | S.CONST _ => []
+ | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
+ | S.LAMB _ => raise TFL_ERR{func = "FV_multiset", mesg = "lambda"};
+
+fun no_repeat_vars thy pat =
+ let fun check [] = true
+ | check (v::rst) =
+ if (U.mem S.aconv v rst)
+ then raise TFL_ERR{func = "no_repeat_vars",
+ mesg = U.concat(U.quote(#Name(S.dest_var v)))
+ (U.concat" occurs repeatedly in the pattern "
+ (U.quote(S.Term_to_string (Thry.typecheck thy pat))))}
+ else check rst
+ in check (FV_multiset pat)
+ end;
+
+local fun paired1{lhs,rhs} = (lhs,rhs)
+ and paired2{Rator,Rand} = (Rator,Rand)
+ fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
+in
+fun mk_functional thy eqs =
+ let val clauses = S.strip_conj eqs
+ val (L,R) = U.unzip (map (paired1 o S.dest_eq o U.snd o S.strip_forall)
+ clauses)
+ val (funcs,pats) = U.unzip(map (paired2 o S.dest_comb) L)
+ val [f] = U.mk_set (S.aconv) funcs
+ handle _ => mk_functional_err "function name not unique"
+ val _ = map (no_repeat_vars thy) pats
+ val rows = U.zip (map (fn x => ([],[x])) pats) (map GIVEN (enumerate R))
+ val fvs = S.free_varsl R
+ val a = S.variant fvs (S.mk_var{Name="a", Ty = S.type_of(hd pats)})
+ val FV = a::fvs
+ val ty_info = Thry.match_info thy
+ val ty_match = Thry.match_type thy
+ val range_ty = S.type_of (hd R)
+ val (patts, case_tm) = mk_case ty_info ty_match FV range_ty
+ {path=[a], rows=rows}
+ val patts1 = map (fn (_,(tag,i),[pat]) => tag (pat,i)) patts handle _
+ => mk_functional_err "error in pattern-match translation"
+ val patts2 = U.sort(fn p1=>fn p2=> row_of_pat p1 < row_of_pat p2) patts1
+ val finals = map row_of_pat patts2
+ val originals = map (row_of_pat o #2) rows
+ fun int_eq i1 (i2:int) = (i1=i2)
+ val _ = case (U.set_diff int_eq originals finals)
+ of [] => ()
+ | L => mk_functional_err("The following rows (counting from zero)\
+ \ are inaccessible: "^stringize L)
+ in {functional = S.list_mk_abs ([f,a], case_tm),
+ pats = patts2}
+end end;
+
+
+(*----------------------------------------------------------------------------
+ *
+ * PRINCIPLES OF DEFINITION
+ *
+ *---------------------------------------------------------------------------*)
+
+
+(*----------------------------------------------------------------------------
+ * This basic principle of definition takes a functional M and a relation R
+ * and specializes the following theorem
+ *
+ * |- !M R f. (f = WFREC R M) ==> WF R ==> !x. f x = M (f%R,x) x
+ *
+ * to them (getting "th1", say). Then we make the definition "f = WFREC R M"
+ * and instantiate "th1" to the constant "f" (getting th2). Then we use the
+ * definition to delete the first antecedent to th2. Hence the result in
+ * the "corollary" field is
+ *
+ * |- WF R ==> !x. f x = M (f%R,x) x
+ *
+ *---------------------------------------------------------------------------*)
+
+fun prim_wfrec_definition thy {R, functional} =
+ let val tych = Thry.typecheck thy
+ val {Bvar,...} = S.dest_abs functional
+ val {Name,...} = S.dest_var Bvar (* Intended name of definition *)
+ val cor1 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
+ val cor2 = R.ISPEC (tych R) cor1
+ val f_eq_WFREC_R_M = (#ant o S.dest_imp o #Body
+ o S.dest_forall o concl) cor2
+ val {lhs,rhs} = S.dest_eq f_eq_WFREC_R_M
+ val {Ty, ...} = S.dest_var lhs
+ val def_term = S.mk_eq{lhs = S.mk_var{Name=Name,Ty=Ty}, rhs=rhs}
+ val (def_thm,thy1) = Thry.make_definition thy
+ (U.concat Name "_def") def_term
+ val (_,[f,_]) = (S.strip_comb o concl) def_thm
+ val cor3 = R.ISPEC (Thry.typecheck thy1 f) cor2
+ in
+ {theory = thy1, def=def_thm, corollary=R.MP cor3 def_thm}
+ end;
+
+
+(*---------------------------------------------------------------------------
+ * This structure keeps track of congruence rules that aren't derived
+ * from a datatype definition.
+ *---------------------------------------------------------------------------*)
+structure Context =
+struct
+ val non_datatype_context = ref []:Rules.Thm list ref
+ fun read() = !non_datatype_context
+ fun write L = (non_datatype_context := L)
+end;
+
+fun extraction_thms thy =
+ let val {case_rewrites,case_congs} = Thry.extract_info thy
+ in (case_rewrites, case_congs@Context.read())
+ end;
+
+
+(*---------------------------------------------------------------------------
+ * Pair patterns with termination conditions. The full list of patterns for
+ * a definition is merged with the TCs arising from the user-given clauses.
+ * There can be fewer clauses than the full list, if the user omitted some
+ * cases. This routine is used to prepare input for mk_induction.
+ *---------------------------------------------------------------------------*)
+fun merge full_pats TCs =
+let fun insert (p,TCs) =
+ let fun insrt ((x as (h,[]))::rst) =
+ if (S.aconv p h) then (p,TCs)::rst else x::insrt rst
+ | insrt (x::rst) = x::insrt rst
+ | insrt[] = raise TFL_ERR{func="merge.insert",mesg="pat not found"}
+ in insrt end
+ fun pass ([],ptcl_final) = ptcl_final
+ | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl)
+in
+ pass (TCs, map (fn p => (p,[])) full_pats)
+end;
+
+fun not_omitted (GIVEN(tm,_)) = tm
+ | not_omitted (OMITTED _) = raise TFL_ERR{func="not_omitted",mesg=""}
+val givens = U.mapfilter not_omitted;
+
+
+(*--------------------------------------------------------------------------
+ * This is a wrapper for "prim_wfrec_definition": it builds a functional,
+ * calls "prim_wfrec_definition", then specializes the result. This gives a
+ * list of rewrite rules where the right hand sides are quite ugly, so we
+ * simplify to get rid of the case statements. In essence, this function
+ * performs pre- and post-processing for patterns. As well, after
+ * simplification, termination conditions are extracted.
+ *-------------------------------------------------------------------------*)
+
+fun gen_wfrec_definition thy {R, eqs} =
+ let val {functional,pats} = mk_functional thy eqs
+ val given_pats = givens pats
+ val {def,corollary,theory} = prim_wfrec_definition thy
+ {R=R, functional=functional}
+ val tych = Thry.typecheck theory
+ val {lhs=f,...} = S.dest_eq(concl def)
+ val WFR = #ant(S.dest_imp(concl corollary))
+ val corollary' = R.UNDISCH corollary (* put WF R on assums *)
+ val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
+ val (case_rewrites,context_congs) = extraction_thms thy
+ val corollaries' = map(R.simplify case_rewrites) corollaries
+ fun xtract th = R.CONTEXT_REWRITE_RULE(f,R)
+ {thms = [(R.ISPECL o map tych)[f,R] Thms.CUT_LEMMA],
+ congs = context_congs,
+ th = th}
+ val (rules, TCs) = U.unzip (map xtract corollaries')
+ val rules0 = map (R.simplify [Thms.CUT_DEF]) rules
+ val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR)
+ val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
+ in
+ {theory = theory, (* holds def, if it's needed *)
+ rules = rules1,
+ full_pats_TCs = merge (map pat_of pats) (U.zip given_pats TCs),
+ TCs = TCs,
+ patterns = pats}
+ end;
+
+
+(*---------------------------------------------------------------------------
+ * Perform the extraction without making the definition. Definition and
+ * extraction commute for the non-nested case. For hol90 users, this
+ * function can be invoked without being in draft mode.
+ *---------------------------------------------------------------------------*)
+fun wfrec_eqns thy eqns =
+ let val {functional,pats} = mk_functional thy eqns
+ val given_pats = givens pats
+ val {Bvar = f, Body} = S.dest_abs functional
+ val {Bvar = x, ...} = S.dest_abs Body
+ val {Name,Ty = fty} = S.dest_var f
+ val {Tyop="fun", Args = [f_dty, f_rty]} = S.dest_type fty
+ val (case_rewrites,context_congs) = extraction_thms thy
+ val tych = Thry.typecheck thy
+ val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
+ val R = S.variant(S.free_vars eqns)
+ (#Bvar(S.dest_forall(concl WFREC_THM0)))
+ val WFREC_THM = R.ISPECL [tych R, tych f] WFREC_THM0
+ val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
+ val R1 = S.rand WFR
+ val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
+ val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
+ val corollaries' = map (R.simplify case_rewrites) corollaries
+ fun extract th = R.CONTEXT_REWRITE_RULE(f,R1)
+ {thms = [(R.ISPECL o map tych)[f,R1] Thms.CUT_LEMMA],
+ congs = context_congs,
+ th = th}
+ in {proto_def=proto_def,
+ WFR=WFR,
+ pats=pats,
+ extracta = map extract corollaries'}
+ end;
+
+
+(*---------------------------------------------------------------------------
+ * Define the constant after extracting the termination conditions. The
+ * wellfounded relation used in the definition is computed by using the
+ * choice operator on the extracted conditions (plus the condition that
+ * such a relation must be wellfounded).
+ *---------------------------------------------------------------------------*)
+fun lazyR_def thy eqns =
+ let val {proto_def,WFR,pats,extracta} = wfrec_eqns thy eqns
+ val R1 = S.rand WFR
+ val f = S.lhs proto_def
+ val {Name,...} = S.dest_var f
+ val (extractants,TCl) = U.unzip extracta
+ val TCs = U.Union S.aconv TCl
+ val full_rqt = WFR::TCs
+ val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
+ val R'abs = S.rand R'
+ val (def,theory) = Thry.make_definition thy (U.concat Name "_def")
+ (S.subst[R1 |-> R'] proto_def)
+ val fconst = #lhs(S.dest_eq(concl def))
+ val tych = Thry.typecheck theory
+ val baz = R.DISCH (tych proto_def)
+ (U.itlist (R.DISCH o tych) full_rqt (R.LIST_CONJ extractants))
+ val def' = R.MP (R.SPEC (tych fconst)
+ (R.SPEC (tych R') (R.GENL[tych R1, tych f] baz)))
+ def
+ val body_th = R.LIST_CONJ (map (R.ASSUME o tych) full_rqt)
+ val bar = R.MP (R.BETA_RULE(R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX))
+ body_th
+ in {theory = theory, R=R1,
+ rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def',
+ full_pats_TCs = merge (map pat_of pats) (U.zip (givens pats) TCl),
+ patterns = pats}
+ end;
+
+
+
+(*----------------------------------------------------------------------------
+ *
+ * INDUCTION THEOREM
+ *
+ *---------------------------------------------------------------------------*)
+
+
+(*------------------------ Miscellaneous function --------------------------
+ *
+ * [x_1,...,x_n] ?v_1...v_n. M[v_1,...,v_n]
+ * -----------------------------------------------------------
+ * ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]),
+ * ...
+ * (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] )
+ *
+ * This function is totally ad hoc. Used in the production of the induction
+ * theorem. The nchotomy theorem can have clauses that look like
+ *
+ * ?v1..vn. z = C vn..v1
+ *
+ * in which the order of quantification is not the order of occurrence of the
+ * quantified variables as arguments to C. Since we have no control over this
+ * aspect of the nchotomy theorem, we make the correspondence explicit by
+ * pairing the incoming new variable with the term it gets beta-reduced into.
+ *---------------------------------------------------------------------------*)
+
+fun alpha_ex_unroll xlist tm =
+ let val (qvars,body) = S.strip_exists tm
+ val vlist = #2(S.strip_comb (S.rhs body))
+ val plist = U.zip vlist xlist
+ val args = map (U.C (U.assoc1 (U.uncurry S.aconv)) plist) qvars
+ val args' = map (fn U.SOME(_,v) => v
+ | U.NONE => raise TFL_ERR{func = "alpha_ex_unroll",
+ mesg = "no correspondence"}) args
+ fun build ex [] = []
+ | build ex (v::rst) =
+ let val ex1 = S.beta_conv(S.mk_comb{Rator=S.rand ex, Rand=v})
+ in ex1::build ex1 rst
+ end
+ val (nex::exl) = rev (tm::build tm args')
+ in
+ (nex, U.zip args' (rev exl))
+ end;
+
+
+
+(*----------------------------------------------------------------------------
+ *
+ * PROVING COMPLETENESS OF PATTERNS
+ *
+ *---------------------------------------------------------------------------*)
+
+fun mk_case ty_info FV thy =
+ let
+ val divide = ipartition (gvvariant FV)
+ val tych = Thry.typecheck thy
+ fun tych_binding(x|->y) = (tych x |-> tych y)
+ fun fail s = raise TFL_ERR{func = "mk_case", mesg = s}
+ fun mk{rows=[],...} = fail"no rows"
+ | mk{path=[], rows = [([], (thm, bindings))]} =
+ R.IT_EXISTS (map tych_binding bindings) thm
+ | mk{path = u::rstp, rows as (p::_, _)::_} =
+ let val (pat_rectangle,rights) = U.unzip rows
+ val col0 = map hd pat_rectangle
+ val pat_rectangle' = map tl pat_rectangle
+ in
+ if (U.all S.is_var col0) (* column 0 is all variables *)
+ then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[u|->v]))
+ (U.zip rights col0)
+ in mk{path = rstp, rows = U.zip pat_rectangle' rights'}
+ end
+ else (* column 0 is all constructors *)
+ let val ty_name = (#Tyop o S.dest_type o S.type_of) p
+ in
+ case (ty_info ty_name)
+ of U.NONE => fail("Not a known datatype: "^ty_name)
+ | U.SOME{constructors,nchotomy} =>
+ let val thm' = R.ISPEC (tych u) nchotomy
+ val disjuncts = S.strip_disj (concl thm')
+ val subproblems = divide(constructors, rows)
+ val groups = map #group subproblems
+ and new_formals = map #new_formals subproblems
+ val existentials = U.map2 alpha_ex_unroll new_formals disjuncts
+ val constraints = map #1 existentials
+ val vexl = map #2 existentials
+ fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b))
+ val news = map (fn (nf,rows,c) => {path = nf@rstp,
+ rows = map (expnd c) rows})
+ (U.zip3 new_formals groups constraints)
+ val recursive_thms = map mk news
+ val build_exists = U.itlist(R.CHOOSE o (tych##(R.ASSUME o tych)))
+ val thms' = U.map2 build_exists vexl recursive_thms
+ val same_concls = R.EVEN_ORS thms'
+ in R.DISJ_CASESL thm' same_concls
+ end
+ end end
+ in mk
+ end;
+
+
+fun complete_cases thy =
+ let val tych = Thry.typecheck thy
+ fun pmk_var n ty = S.mk_var{Name = n,Ty = ty}
+ val ty_info = Thry.induct_info thy
+ in fn pats =>
+ let val FV0 = S.free_varsl pats
+ val a = S.variant FV0 (pmk_var "a" (S.type_of(hd pats)))
+ val v = S.variant (a::FV0) (pmk_var "v" (S.type_of a))
+ val FV = a::v::FV0
+ val a_eq_v = S.mk_eq{lhs = a, rhs = v}
+ val ex_th0 = R.EXISTS ((tych##tych) (S.mk_exists{Bvar=v,Body=a_eq_v},a))
+ (R.REFL (tych a))
+ val th0 = R.ASSUME (tych a_eq_v)
+ val rows = map (fn x => ([x], (th0,[]))) pats
+ in
+ R.GEN (tych a)
+ (R.RIGHT_ASSOC
+ (R.CHOOSE(tych v, ex_th0)
+ (mk_case ty_info FV thy {path=[v], rows=rows})))
+ end end;
+
+
+(*---------------------------------------------------------------------------
+ * Constructing induction hypotheses: one for each recursive call.
+ *
+ * Note. R will never occur as a variable in the ind_clause, because
+ * to do so, it would have to be from a nested definition, and we don't
+ * allow nested defns to have R variable.
+ *
+ * Note. When the context is empty, there can be no local variables.
+ *---------------------------------------------------------------------------*)
+
+local nonfix ^ ; infix 9 ^ ; infix 5 ==>
+ fun (tm1 ^ tm2) = S.mk_comb{Rator = tm1, Rand = tm2}
+ fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
+in
+fun build_ih f P (pat,TCs) =
+ let val globals = S.free_vars_lr pat
+ fun nested tm = U.can(S.find_term (S.aconv f)) tm handle _ => false
+ fun dest_TC tm =
+ let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
+ val (R,y,_) = S.dest_relation R_y_pat
+ val P_y = if (nested tm) then R_y_pat ==> P^y else P^y
+ in case cntxt
+ of [] => (P_y, (tm,[]))
+ | _ => let
+ val imp = S.list_mk_conj cntxt ==> P_y
+ val lvs = U.set_diff S.aconv (S.free_vars_lr imp) globals
+ val locals = #2(U.pluck (S.aconv P) lvs) handle _ => lvs
+ in (S.list_mk_forall(locals,imp), (tm,locals)) end
+ end
+ in case TCs
+ of [] => (S.list_mk_forall(globals, P^pat), [])
+ | _ => let val (ihs, TCs_locals) = U.unzip(map dest_TC TCs)
+ val ind_clause = S.list_mk_conj ihs ==> P^pat
+ in (S.list_mk_forall(globals,ind_clause), TCs_locals)
+ end
+ end
+end;
+
+
+
+(*---------------------------------------------------------------------------
+ * This function makes good on the promise made in "build_ih: we prove
+ * <something>.
+ *
+ * Input is tm = "(!y. R y pat ==> P y) ==> P pat",
+ * TCs = TC_1[pat] ... TC_n[pat]
+ * thm = ih1 /\ ... /\ ih_n |- ih[pat]
+ *---------------------------------------------------------------------------*)
+fun prove_case f thy (tm,TCs_locals,thm) =
+ let val tych = Thry.typecheck thy
+ val antc = tych(#ant(S.dest_imp tm))
+ val thm' = R.SPEC_ALL thm
+ fun nested tm = U.can(S.find_term (S.aconv f)) tm handle _ => false
+ fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
+ fun mk_ih ((TC,locals),th2,nested) =
+ R.GENL (map tych locals)
+ (if nested
+ then R.DISCH (get_cntxt TC) th2 handle _ => th2
+ else if S.is_imp(concl TC)
+ then R.IMP_TRANS TC th2
+ else R.MP th2 TC)
+ in
+ R.DISCH antc
+ (if S.is_imp(concl thm') (* recursive calls in this clause *)
+ then let val th1 = R.ASSUME antc
+ val TCs = map #1 TCs_locals
+ val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o
+ #2 o S.strip_forall) TCs
+ val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs))
+ TCs_locals
+ val th2list = map (U.C R.SPEC th1 o tych) ylist
+ val nlist = map nested TCs
+ val triples = U.zip3 TClist th2list nlist
+ val Pylist = map mk_ih triples
+ in R.MP thm' (R.LIST_CONJ Pylist) end
+ else thm')
+ end;
+
+
+(*---------------------------------------------------------------------------
+ *
+ * x = (v1,...,vn) |- M[x]
+ * ---------------------------------------------
+ * ?v1 ... vn. x = (v1,...,vn) |- M[x]
+ *
+ *---------------------------------------------------------------------------*)
+fun LEFT_ABS_VSTRUCT tych thm =
+ let fun CHOOSER v (tm,thm) =
+ let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
+ in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
+ end
+ val [veq] = U.filter (U.can S.dest_eq) (#1 (R.dest_thm thm))
+ val {lhs,rhs} = S.dest_eq veq
+ val L = S.free_vars_lr rhs
+ in U.snd(U.itlist CHOOSER L (veq,thm))
+ end;
+
+
+fun combize M N = S.mk_comb{Rator=M,Rand=N};
+fun eq v tm = S.mk_eq{lhs=v,rhs=tm};
+
+
+(*----------------------------------------------------------------------------
+ * Input : f, R, and [(pat1,TCs1),..., (patn,TCsn)]
+ *
+ * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove
+ * recursion induction (Rinduct) by proving the antecedent of Sinduct from
+ * the antecedent of Rinduct.
+ *---------------------------------------------------------------------------*)
+fun mk_induction thy f R pat_TCs_list =
+let val tych = Thry.typecheck thy
+ val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
+ val (pats,TCsl) = U.unzip pat_TCs_list
+ val case_thm = complete_cases thy pats
+ val domain = (S.type_of o hd) pats
+ val P = S.variant (S.all_varsl (pats@flatten TCsl))
+ (S.mk_var{Name="P", Ty=domain --> S.bool})
+ val Sinduct = R.SPEC (tych P) Sinduction
+ val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
+ val Rassums_TCl' = map (build_ih f P) pat_TCs_list
+ val (Rassums,TCl') = U.unzip Rassums_TCl'
+ val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
+ val cases = map (S.beta_conv o combize Sinduct_assumf) pats
+ val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
+ val proved_cases = map (prove_case f thy) tasks
+ val v = S.variant (S.free_varsl (map concl proved_cases))
+ (S.mk_var{Name="v", Ty=domain})
+ val vtyped = tych v
+ val substs = map (R.SYM o R.ASSUME o tych o eq v) pats
+ val proved_cases1 = U.map2 (fn th => R.SUBS[th]) substs proved_cases
+ val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
+ val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases)
+ val dc = R.MP Sinduct dant
+ val Parg_ty = S.type_of(#Bvar(S.dest_forall(concl dc)))
+ val vars = map (gvvariant[P]) (S.strip_prod_type Parg_ty)
+ val dc' = U.itlist (R.GEN o tych) vars
+ (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
+in
+ R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc')
+end
+handle _ => raise TFL_ERR{func = "mk_induction", mesg = "failed derivation"};
+
+
+
+(*---------------------------------------------------------------------------
+ *
+ * POST PROCESSING
+ *
+ *---------------------------------------------------------------------------*)
+
+
+fun simplify_induction thy hth ind =
+ let val tych = Thry.typecheck thy
+ val (asl,_) = R.dest_thm ind
+ val (_,tc_eq_tc') = R.dest_thm hth
+ val tc = S.lhs tc_eq_tc'
+ fun loop [] = ind
+ | loop (asm::rst) =
+ if (U.can (Thry.match_term thy asm) tc)
+ then R.UNDISCH
+ (R.MATCH_MP
+ (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind))
+ hth)
+ else loop rst
+ in loop asl
+end;
+
+
+(*---------------------------------------------------------------------------
+ * The termination condition is an antecedent to the rule, and an
+ * assumption to the theorem.
+ *---------------------------------------------------------------------------*)
+fun elim_tc tcthm (rule,induction) =
+ (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
+
+
+fun postprocess{WFtac, terminator, simplifier} theory {rules,induction,TCs} =
+let val tych = Thry.typecheck theory
+
+ (*---------------------------------------------------------------------
+ * Attempt to eliminate WF condition. It's the only assumption of rules
+ *---------------------------------------------------------------------*)
+ val (rules1,induction1) =
+ let val thm = R.prove(tych(hd(#1(R.dest_thm rules))),WFtac)
+ in (R.PROVE_HYP thm rules, R.PROVE_HYP thm induction)
+ end handle _ => (rules,induction)
+
+ (*----------------------------------------------------------------------
+ * The termination condition (tc) is simplified to |- tc = tc' (there
+ * might not be a change!) and then 3 attempts are made:
+ *
+ * 1. if |- tc = T, then eliminate it with eqT; otherwise,
+ * 2. apply the terminator to tc'. If |- tc' = T then eliminate; else
+ * 3. replace tc by tc' in both the rules and the induction theorem.
+ *---------------------------------------------------------------------*)
+ fun simplify_tc tc (r,ind) =
+ let val tc_eq = simplifier (tych tc)
+ in
+ elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
+ handle _ =>
+ (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
+ (R.prove(tych(S.rhs(concl tc_eq)),terminator)))
+ (r,ind)
+ handle _ =>
+ (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq),
+ simplify_induction theory tc_eq ind))
+ end
+
+ (*----------------------------------------------------------------------
+ * Nested termination conditions are harder to get at, since they are
+ * left embedded in the body of the function (and in induction
+ * theorem hypotheses). Our "solution" is to simplify them, and try to
+ * prove termination, but leave the application of the resulting theorem
+ * to a higher level. So things go much as in "simplify_tc": the
+ * termination condition (tc) is simplified to |- tc = tc' (there might
+ * not be a change) and then 2 attempts are made:
+ *
+ * 1. if |- tc = T, then return |- tc; otherwise,
+ * 2. apply the terminator to tc'. If |- tc' = T then return |- tc; else
+ * 3. return |- tc = tc'
+ *---------------------------------------------------------------------*)
+ fun simplify_nested_tc tc =
+ let val tc_eq = simplifier (tych (#2 (S.strip_forall tc)))
+ in
+ R.GEN_ALL
+ (R.MATCH_MP Thms.eqT tc_eq
+ handle _
+ => (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
+ (R.prove(tych(S.rhs(concl tc_eq)),terminator))
+ handle _ => tc_eq))
+ end
+
+ (*-------------------------------------------------------------------
+ * Attempt to simplify the termination conditions in each rule and
+ * in the induction theorem.
+ *-------------------------------------------------------------------*)
+ fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm
+ fun loop ([],extras,R,ind) = (rev R, ind, extras)
+ | loop ((r,ftcs)::rst, nthms, R, ind) =
+ let val tcs = #1(strip_imp (concl r))
+ val extra_tcs = U.set_diff S.aconv ftcs tcs
+ val extra_tc_thms = map simplify_nested_tc extra_tcs
+ val (r1,ind1) = U.rev_itlist simplify_tc tcs (r,ind)
+ val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
+ in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
+ end
+ val rules_tcs = U.zip (R.CONJUNCTS rules1) TCs
+ val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
+in
+ {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras}
+end;
+
+
+(*---------------------------------------------------------------------------
+ * Extract termination goals so that they can be put it into a goalstack, or
+ * have a tactic directly applied to them.
+ *--------------------------------------------------------------------------*)
+local exception IS_NEG
+ fun strip_imp tm = if S.is_neg tm then raise IS_NEG else S.strip_imp tm
+in
+fun termination_goals rules =
+ U.itlist (fn th => fn A =>
+ let val tcl = (#1 o S.strip_imp o #2 o S.strip_forall o concl) th
+ in tcl@A
+ end handle _ => A) (R.CONJUNCTS rules) (hyp rules)
+end;
+
+end; (* TFL *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/thms.sig Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,16 @@
+signature Thms_sig =
+sig
+ type Thm
+ val WF_INDUCTION_THM:Thm
+ val WFREC_COROLLARY :Thm
+ val CUT_DEF :Thm
+ val CUT_LEMMA :Thm
+ val SELECT_AX :Thm
+
+ val COND_CONG :Thm
+ val LET_CONG :Thm
+
+ val eqT :Thm
+ val rev_eq_mp :Thm
+ val simp_thm :Thm
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/thms.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,39 @@
+structure Thms : Thms_sig =
+struct
+ type Thm = Thm.thm
+
+ val WFREC_COROLLARY = get_thm WF1.thy "tfl_wfrec"
+ val WF_INDUCTION_THM = get_thm WF1.thy "tfl_wf_induct"
+ val CUT_LEMMA = get_thm WF1.thy "tfl_cut_apply"
+ val CUT_DEF = cut_def
+
+ local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
+ val _ = by (strip_tac 1)
+ val _ = by (rtac selectI 1)
+ val _ = by (assume_tac 1)
+ in val SELECT_AX = result()
+ end;
+
+ (*-------------------------------------------------------------------------
+ * A useful congruence rule
+ *-------------------------------------------------------------------------*)
+ local val [p1,p2] = goal HOL.thy "(M = N) ==> \
+ \ (!!x. ((x = N) ==> (f x = g x))) ==> \
+ \ (Let M f = Let N g)";
+ val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
+ val _ = by (rtac p2 1);
+ val _ = by (rtac refl 1);
+ in val LET_CONG = result() RS eq_reflection
+ end;
+
+ val COND_CONG = if_cong RS eq_reflection;
+
+ fun C f x y = f y x;
+ fun prover thl = [fast_tac HOL_cs 1];
+ val P = C (prove_goal HOL.thy) prover;
+
+ val eqT = P"(x = True) --> x"
+ val rev_eq_mp = P"(x = y) --> y --> x"
+ val simp_thm = P"(x-->y) --> (x = x') --> (x' --> y)"
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/thry.sig Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,31 @@
+signature Thry_sig =
+sig
+ type Type
+ type Preterm
+ type Term
+ type Thm
+ type Thry
+ type 'a binding
+
+ structure USyntax : USyntax_sig
+ val match_term : Thry -> Preterm -> Preterm
+ -> Preterm binding list * Type binding list
+
+ val match_type : Thry -> Type -> Type -> Type binding list
+
+ val typecheck : Thry -> Preterm -> Term
+
+ val make_definition: Thry -> string -> Preterm -> Thm * Thry
+
+ (* Datatype facts of various flavours *)
+ val match_info: Thry -> string -> {constructors:Preterm list,
+ case_const:Preterm} USyntax.Utils.option
+
+ val induct_info: Thry -> string -> {constructors:Preterm list,
+ nchotomy:Thm} USyntax.Utils.option
+
+ val extract_info: Thry -> {case_congs:Thm list, case_rewrites:Thm list}
+
+end;
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/thry.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,139 @@
+structure Thry : Thry_sig (* LThry_sig *) =
+struct
+
+structure USyntax = USyntax;
+type Type = USyntax.Type
+type Preterm = USyntax.Preterm
+type Term = USyntax.Term
+type Thm = Thm.thm
+type Thry = theory;
+
+open Mask;
+structure S = USyntax;
+
+
+fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
+
+(*---------------------------------------------------------------------------
+ * Matching
+ *---------------------------------------------------------------------------*)
+
+local open Utils
+ infix 3 |->
+ fun tybind (x,y) = TVar (x,["term"]) |-> y
+ fun tmbind (x,y) = Var (x,type_of y) |-> y
+in
+ fun match_term thry pat ob =
+ let val tsig = #tsig(Sign.rep_sg(sign_of thry))
+ val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
+ in (map tmbind tm_theta, map tybind ty_theta)
+ end
+
+ fun match_type thry pat ob =
+ map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob)))
+end;
+
+
+(*---------------------------------------------------------------------------
+ * Typing
+ *---------------------------------------------------------------------------*)
+
+fun typecheck thry = cterm_of (sign_of thry);
+
+
+
+(*----------------------------------------------------------------------------
+ * Making a definition. The argument "tm" looks like "f = WFREC R M". This
+ * entrypoint is specialized for interactive use, since it closes the theory
+ * after making the definition. This allows later interactive definitions to
+ * refer to previous ones. The name for the new theory is automatically
+ * generated from the name of the argument theory.
+ *---------------------------------------------------------------------------*)
+local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))
+ val Const(eeq_name, ty) = eeq
+ val prop = #2 (S.strip_type ty)
+in
+fun make_definition parent s tm =
+ let val {lhs,rhs} = S.dest_eq tm
+ val {Name,Ty} = S.dest_var lhs
+ val lhs1 = S.mk_const{Name = Name, Ty = Ty}
+ val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
+ val dtm = S.list_mk_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *)
+ val thry1 = add_consts_i [(Name,Ty,NoSyn)] parent
+ val thry2 = add_defs_i [(s,dtm)] thry1
+ val parent_names = map ! (stamps_of_thy parent)
+ val newthy_name = variant parent_names (hd parent_names)
+ val new_thy = add_thyname newthy_name thry2
+ in
+ ((get_axiom new_thy s) RS meta_eq_to_obj_eq, new_thy)
+ end
+end;
+
+
+(*---------------------------------------------------------------------------
+ * Utility routine. Insert into list ordered by the key (a string). If two
+ * keys are equal, the new element replaces the old. A more efficient option
+ * for the future is needed. In fact, having the list of datatype facts be
+ * ordered is useless, since the lookup should never fail!
+ *---------------------------------------------------------------------------*)
+fun insert (el as (x:string, _)) =
+ let fun canfind[] = [el]
+ | canfind(alist as ((y as (k,_))::rst)) =
+ if (x<k) then el::alist
+ else if (x=k) then el::rst
+ else y::canfind rst
+ in canfind
+ end;
+
+
+(*---------------------------------------------------------------------------
+ * A collection of facts about datatypes
+ *---------------------------------------------------------------------------*)
+val nat_record = Dtype.build_record (Nat.thy, ("nat",["0","Suc"]), nat_ind_tac)
+val prod_record =
+ let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split]
+ (fn s => res_inst_tac [("p",s)] PairE_lemma)
+ fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s))
+ in ("*",
+ {constructors = [const "Pair"],
+ case_const = const "split",
+ case_rewrites = [split RS eq_reflection],
+ case_cong = #case_cong prod_case_thms,
+ nchotomy = #nchotomy prod_case_thms})
+ end;
+
+(*---------------------------------------------------------------------------
+ * Hacks to make interactive mode work. Referring to "datatypes" directly
+ * is temporary, I hope!
+ *---------------------------------------------------------------------------*)
+val match_info = fn thy =>
+ fn "*" => Utils.SOME({case_const = #case_const (#2 prod_record),
+ constructors = #constructors (#2 prod_record)})
+ | "nat" => Utils.SOME({case_const = #case_const (#2 nat_record),
+ constructors = #constructors (#2 nat_record)})
+ | ty => case assoc(!datatypes,ty)
+ of None => Utils.NONE
+ | Some{case_const,constructors, ...} =>
+ Utils.SOME{case_const=case_const, constructors=constructors}
+
+val induct_info = fn thy =>
+ fn "*" => Utils.SOME({nchotomy = #nchotomy (#2 prod_record),
+ constructors = #constructors (#2 prod_record)})
+ | "nat" => Utils.SOME({nchotomy = #nchotomy (#2 nat_record),
+ constructors = #constructors (#2 nat_record)})
+ | ty => case assoc(!datatypes,ty)
+ of None => Utils.NONE
+ | Some{nchotomy,constructors, ...} =>
+ Utils.SOME{nchotomy=nchotomy, constructors=constructors}
+
+val extract_info = fn thy =>
+ let val case_congs = map (#case_cong o #2) (!datatypes)
+ val case_rewrites = flat(map (#case_rewrites o #2) (!datatypes))
+ in {case_congs = #case_cong (#2 prod_record)::
+ #case_cong (#2 nat_record)::case_congs,
+ case_rewrites = #case_rewrites(#2 prod_record)@
+ #case_rewrites(#2 nat_record)@case_rewrites}
+ end;
+
+
+end; (* Thry *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/usyntax.sig Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,134 @@
+signature USyntax_sig =
+sig
+ structure Utils : Utils_sig
+
+ type Type
+ type Term
+ type Preterm
+ type 'a binding
+
+ datatype lambda = VAR of {Name : string, Ty : Type}
+ | CONST of {Name : string, Ty : Type}
+ | COMB of {Rator: Preterm, Rand : Preterm}
+ | LAMB of {Bvar : Preterm, Body : Preterm}
+
+ val alpha : Type
+ val bool : Type
+ val mk_preterm : Term -> Preterm
+ val drop_Trueprop : Preterm -> Preterm
+
+ (* Types *)
+ val type_vars : Type -> Type list
+ val type_varsl : Type list -> Type list
+ val mk_type : {Tyop: string, Args:Type list} -> Type
+ val dest_type : Type -> {Tyop : string, Args : Type list}
+ val mk_vartype : string -> Type
+ val is_vartype : Type -> bool
+ val --> : Type * Type -> Type
+ val strip_type : Type -> Type list * Type
+ val strip_prod_type : Type -> Type list
+ val match_type: Type -> Type -> Type binding list
+
+ (* Terms *)
+ val free_vars : Preterm -> Preterm list
+ val free_varsl : Preterm list -> Preterm list
+ val free_vars_lr : Preterm -> Preterm list
+ val all_vars : Preterm -> Preterm list
+ val all_varsl : Preterm list -> Preterm list
+ val variant : Preterm list -> Preterm -> Preterm
+ val type_of : Preterm -> Type
+ val type_vars_in_term : Preterm -> Type list
+ val dest_term : Preterm -> lambda
+
+ (* Prelogic *)
+ val aconv : Preterm -> Preterm -> bool
+ val subst : Preterm binding list -> Preterm -> Preterm
+ val inst : Type binding list -> Preterm -> Preterm
+ val beta_conv : Preterm -> Preterm
+
+ (* Construction routines *)
+ val mk_prop :Preterm -> Preterm
+ val mk_var :{Name : string, Ty : Type} -> Preterm
+ val mk_const :{Name : string, Ty : Type} -> Preterm
+ val mk_comb :{Rator : Preterm, Rand : Preterm} -> Preterm
+ val mk_abs :{Bvar : Preterm, Body : Preterm} -> Preterm
+
+ val mk_eq :{lhs : Preterm, rhs : Preterm} -> Preterm
+ val mk_imp :{ant : Preterm, conseq : Preterm} -> Preterm
+ val mk_select :{Bvar : Preterm, Body : Preterm} -> Preterm
+ val mk_forall :{Bvar : Preterm, Body : Preterm} -> Preterm
+ val mk_exists :{Bvar : Preterm, Body : Preterm} -> Preterm
+ val mk_conj :{conj1 : Preterm, conj2 : Preterm} -> Preterm
+ val mk_disj :{disj1 : Preterm, disj2 : Preterm} -> Preterm
+ val mk_pabs :{varstruct : Preterm, body : Preterm} -> Preterm
+
+ (* Destruction routines *)
+ val dest_var : Preterm -> {Name : string, Ty : Type}
+ val dest_const: Preterm -> {Name : string, Ty : Type}
+ val dest_comb : Preterm -> {Rator : Preterm, Rand : Preterm}
+ val dest_abs : Preterm -> {Bvar : Preterm, Body : Preterm}
+ val dest_eq : Preterm -> {lhs : Preterm, rhs : Preterm}
+ val dest_imp : Preterm -> {ant : Preterm, conseq : Preterm}
+ val dest_select : Preterm -> {Bvar : Preterm, Body : Preterm}
+ val dest_forall : Preterm -> {Bvar : Preterm, Body : Preterm}
+ val dest_exists : Preterm -> {Bvar : Preterm, Body : Preterm}
+ val dest_neg : Preterm -> Preterm
+ val dest_conj : Preterm -> {conj1 : Preterm, conj2 : Preterm}
+ val dest_disj : Preterm -> {disj1 : Preterm, disj2 : Preterm}
+ val dest_pair : Preterm -> {fst : Preterm, snd : Preterm}
+ val dest_pabs : Preterm -> {varstruct : Preterm, body : Preterm}
+
+ val lhs : Preterm -> Preterm
+ val rhs : Preterm -> Preterm
+ val rator : Preterm -> Preterm
+ val rand : Preterm -> Preterm
+ val bvar : Preterm -> Preterm
+ val body : Preterm -> Preterm
+
+
+ (* Query routines *)
+ val is_var : Preterm -> bool
+ val is_const: Preterm -> bool
+ val is_comb : Preterm -> bool
+ val is_abs : Preterm -> bool
+ val is_eq : Preterm -> bool
+ val is_imp : Preterm -> bool
+ val is_forall : Preterm -> bool
+ val is_exists : Preterm -> bool
+ val is_neg : Preterm -> bool
+ val is_conj : Preterm -> bool
+ val is_disj : Preterm -> bool
+ val is_pair : Preterm -> bool
+ val is_pabs : Preterm -> bool
+
+ (* Construction of a Preterm from a list of Preterms *)
+ val list_mk_comb : (Preterm * Preterm list) -> Preterm
+ val list_mk_abs : (Preterm list * Preterm) -> Preterm
+ val list_mk_imp : (Preterm list * Preterm) -> Preterm
+ val list_mk_forall : (Preterm list * Preterm) -> Preterm
+ val list_mk_exists : (Preterm list * Preterm) -> Preterm
+ val list_mk_conj : Preterm list -> Preterm
+ val list_mk_disj : Preterm list -> Preterm
+
+ (* Destructing a Preterm to a list of Preterms *)
+ val strip_comb : Preterm -> (Preterm * Preterm list)
+ val strip_abs : Preterm -> (Preterm list * Preterm)
+ val strip_imp : Preterm -> (Preterm list * Preterm)
+ val strip_forall : Preterm -> (Preterm list * Preterm)
+ val strip_exists : Preterm -> (Preterm list * Preterm)
+ val strip_conj : Preterm -> Preterm list
+ val strip_disj : Preterm -> Preterm list
+ val strip_pair : Preterm -> Preterm list
+
+ (* Miscellaneous *)
+ val mk_vstruct : Type -> Preterm list -> Preterm
+ val gen_all : Preterm -> Preterm
+ val find_term : (Preterm -> bool) -> Preterm -> Preterm
+ val find_terms : (Preterm -> bool) -> Preterm -> Preterm list
+ val dest_relation : Preterm -> Preterm * Preterm * Preterm
+ val is_WFR : Preterm -> bool
+ val ARB : Type -> Preterm
+
+ (* Prettyprinting *)
+ val Term_to_string : Term -> string
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/usyntax.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,482 @@
+structure USyntax : USyntax_sig =
+struct
+
+structure Utils = Utils;
+open Utils;
+open Mask;
+
+infix 7 |->;
+infix 4 ##;
+
+fun ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg};
+
+type Type = typ
+type Term = cterm
+type Preterm = term
+
+
+(*---------------------------------------------------------------------------
+ *
+ * Types
+ *
+ *---------------------------------------------------------------------------*)
+fun mk_type{Tyop, Args} = Type(Tyop,Args);
+val mk_prim_vartype = TVar;
+fun mk_vartype s = mk_prim_vartype((s,0),["term"]);
+
+fun dest_type(Type(ty,args)) = {Tyop = ty, Args = args}
+ | dest_type _ = raise ERR{func = "dest_type", mesg = "Not a compound type"};
+
+
+(* But internally, it's useful *)
+fun dest_vtype (TVar x) = x
+ | dest_vtype _ = raise ERR{func = "dest_vtype",
+ mesg = "not a flexible type variable"};
+
+val is_vartype = Utils.can dest_vtype;
+
+val type_vars = map mk_prim_vartype o typ_tvars
+fun type_varsl L = Utils.mk_set (Utils.curry op=)
+ (Utils.rev_itlist (Utils.curry op @ o type_vars) L []);
+
+val alpha = mk_vartype "'a"
+val beta = mk_vartype "'b"
+
+val bool = Type("bool",[]);
+
+fun match_type ty1 ty2 = raise ERR{func="match_type",mesg="not implemented"};
+
+
+(* What nonsense *)
+nonfix -->;
+val --> = -->;
+infixr 3 -->;
+
+(* hol_type -> hol_type list * hol_type *)
+fun strip_type ty =
+ let val {Tyop = "fun", Args = [ty1,ty2]} = dest_type ty
+ val (D,r) = strip_type ty2
+ in (ty1::D, r)
+ end
+ handle _ => ([],ty);
+
+(* hol_type -> hol_type list *)
+fun strip_prod_type ty =
+ let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty
+ in strip_prod_type ty1 @ strip_prod_type ty2
+ end handle _ => [ty];
+
+
+
+(*---------------------------------------------------------------------------
+ *
+ * Terms
+ *
+ *---------------------------------------------------------------------------*)
+nonfix aconv;
+val aconv = Utils.curry (op aconv);
+
+fun free_vars tm = add_term_frees(tm,[]);
+
+
+(* Free variables, in order of occurrence, from left to right in the
+ * syntax tree. *)
+fun free_vars_lr tm =
+ let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
+ fun add (t, frees) = case t of
+ Free _ => if (memb t frees) then frees else t::frees
+ | Abs (_,_,body) => add(body,frees)
+ | f$t => add(t, add(f, frees))
+ | _ => frees
+ in rev(add(tm,[]))
+ end;
+
+
+
+fun free_varsl L = Utils.mk_set aconv
+ (Utils.rev_itlist (Utils.curry op @ o free_vars) L []);
+
+val type_of = type_of;
+val type_vars_in_term = map mk_prim_vartype o term_tvars;
+
+(* Can't really be very exact in Isabelle *)
+fun all_vars tm =
+ let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
+ fun add (t, A) = case t of
+ Free _ => if (memb t A) then A else t::A
+ | Abs (s,ty,body) => add(body, add(Free(s,ty),A))
+ | f$t => add(t, add(f, A))
+ | _ => A
+ in rev(add(tm,[]))
+ end;
+fun all_varsl L = Utils.mk_set aconv
+ (Utils.rev_itlist (Utils.curry op @ o all_vars) L []);
+
+
+(* Prelogic *)
+val subst = subst_free o map (fn (a |-> b) => (a,b));
+
+fun dest_tybinding (v |-> ty) = (#1(dest_vtype v),ty)
+fun inst theta = subst_vars (map dest_tybinding theta,[])
+
+fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2)
+ | beta_conv _ = raise ERR{func = "beta_conv", mesg = "Not a beta-redex"};
+
+
+(* Construction routines *)
+(* fun mk_var{Name,Ty} = Var((Name,0),Ty); *)
+fun mk_var{Name,Ty} = Free(Name,Ty);
+val mk_prim_var = Var;
+
+val string_variant = variant;
+
+local fun var_name(Var((Name,_),_)) = Name
+ | var_name(Free(s,_)) = s
+ | var_name _ = raise ERR{func = "variant",
+ mesg = "list elem. is not a variable"}
+in
+fun variant [] v = v
+ | variant vlist (Var((Name,i),ty)) =
+ Var((string_variant (map var_name vlist) Name,i),ty)
+ | variant vlist (Free(Name,ty)) =
+ Free(string_variant (map var_name vlist) Name,ty)
+ | variant _ _ = raise ERR{func = "variant",
+ mesg = "2nd arg. should be a variable"}
+end;
+
+fun mk_const{Name,Ty} = Const(Name,Ty)
+fun mk_comb{Rator,Rand} = Rator $ Rand;
+
+fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body))
+ | mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body))
+ | mk_abs _ = raise ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
+
+fun list_mk_comb (h,[]) = h
+ | list_mk_comb (h,L) =
+ rev_itlist (fn t1 => fn t2 => mk_comb{Rator = t2, Rand = t1}) L h;
+
+
+fun mk_eq{lhs,rhs} =
+ let val ty = type_of lhs
+ val c = mk_const{Name = "op =", Ty = ty --> ty --> bool}
+ in list_mk_comb(c,[lhs,rhs])
+ end
+
+fun mk_imp{ant,conseq} =
+ let val c = mk_const{Name = "op -->", Ty = bool --> bool --> bool}
+ in list_mk_comb(c,[ant,conseq])
+ end;
+
+fun mk_select (r as {Bvar,Body}) =
+ let val ty = type_of Bvar
+ val c = mk_const{Name = "Eps", Ty = (ty --> bool) --> ty}
+ in list_mk_comb(c,[mk_abs r])
+ end;
+
+fun mk_forall (r as {Bvar,Body}) =
+ let val ty = type_of Bvar
+ val c = mk_const{Name = "All", Ty = (ty --> bool) --> bool}
+ in list_mk_comb(c,[mk_abs r])
+ end;
+
+fun mk_exists (r as {Bvar,Body}) =
+ let val ty = type_of Bvar
+ val c = mk_const{Name = "Ex", Ty = (ty --> bool) --> bool}
+ in list_mk_comb(c,[mk_abs r])
+ end;
+
+
+fun mk_conj{conj1,conj2} =
+ let val c = mk_const{Name = "op &", Ty = bool --> bool --> bool}
+ in list_mk_comb(c,[conj1,conj2])
+ end;
+
+fun mk_disj{disj1,disj2} =
+ let val c = mk_const{Name = "op |", Ty = bool --> bool --> bool}
+ in list_mk_comb(c,[disj1,disj2])
+ end;
+
+fun prod_ty ty1 ty2 = mk_type{Tyop = "*", Args = [ty1,ty2]};
+
+local
+fun mk_uncurry(xt,yt,zt) =
+ mk_const{Name = "split", Ty = (xt --> yt --> zt) --> prod_ty xt yt --> zt}
+fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
+ | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"}
+fun is_var(Var(_)) = true | is_var (Free _) = true | is_var _ = false
+in
+fun mk_pabs{varstruct,body} =
+ let fun mpa(varstruct,body) =
+ if (is_var varstruct)
+ then mk_abs{Bvar = varstruct, Body = body}
+ else let val {fst,snd} = dest_pair varstruct
+ in mk_comb{Rator= mk_uncurry(type_of fst,type_of snd,type_of body),
+ Rand = mpa(fst,mpa(snd,body))}
+ end
+ in mpa(varstruct,body)
+ end
+ handle _ => raise ERR{func = "mk_pabs", mesg = ""};
+end;
+
+(* Destruction routines *)
+
+datatype lambda = VAR of {Name : string, Ty : Type}
+ | CONST of {Name : string, Ty : Type}
+ | COMB of {Rator: Preterm, Rand : Preterm}
+ | LAMB of {Bvar : Preterm, Body : Preterm};
+
+
+fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty}
+ | dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty}
+ | dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty}
+ | dest_term(M$N) = COMB{Rator=M,Rand=N}
+ | dest_term(Abs(s,ty,M)) = let val v = mk_var{Name = s, Ty = ty}
+ in LAMB{Bvar = v, Body = betapply (M,v)}
+ end
+ | dest_term(Bound _) = raise ERR{func = "dest_term",mesg = "Bound"};
+
+fun dest_var(Var((s,i),ty)) = {Name = s, Ty = ty}
+ | dest_var(Free(s,ty)) = {Name = s, Ty = ty}
+ | dest_var _ = raise ERR{func = "dest_var", mesg = "not a variable"};
+
+fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
+ | dest_const _ = raise ERR{func = "dest_const", mesg = "not a constant"};
+
+fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
+ | dest_comb _ = raise ERR{func = "dest_comb", mesg = "not a comb"};
+
+fun dest_abs(a as Abs(s,ty,M)) =
+ let val v = mk_var{Name = s, Ty = ty}
+ in {Bvar = v, Body = betapply (a,v)}
+ end
+ | dest_abs _ = raise ERR{func = "dest_abs", mesg = "not an abstraction"};
+
+fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
+ | dest_eq _ = raise ERR{func = "dest_eq", mesg = "not an equality"};
+
+fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
+ | dest_imp _ = raise ERR{func = "dest_imp", mesg = "not an implication"};
+
+fun dest_select(Const("Eps",_) $ (a as Abs _)) = dest_abs a
+ | dest_select _ = raise ERR{func = "dest_select", mesg = "not a select"};
+
+fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a
+ | dest_forall _ = raise ERR{func = "dest_forall", mesg = "not a forall"};
+
+fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a
+ | dest_exists _ = raise ERR{func = "dest_exists", mesg="not an existential"};
+
+fun dest_neg(Const("not",_) $ M) = M
+ | dest_neg _ = raise ERR{func = "dest_neg", mesg = "not a negation"};
+
+fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
+ | dest_conj _ = raise ERR{func = "dest_conj", mesg = "not a conjunction"};
+
+fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
+ | dest_disj _ = raise ERR{func = "dest_disj", mesg = "not a disjunction"};
+
+fun mk_pair{fst,snd} =
+ let val ty1 = type_of fst
+ val ty2 = type_of snd
+ val c = mk_const{Name = "Pair", Ty = ty1 --> ty2 --> prod_ty ty1 ty2}
+ in list_mk_comb(c,[fst,snd])
+ end;
+
+fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
+ | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"};
+
+
+local val ucheck = Utils.assert (curry (op =) "split" o #Name o dest_const)
+in
+fun dest_pabs tm =
+ let val {Bvar,Body} = dest_abs tm
+ in {varstruct = Bvar, body = Body}
+ end handle _
+ => let val {Rator,Rand} = dest_comb tm
+ val _ = ucheck Rator
+ val {varstruct = lv,body} = dest_pabs Rand
+ val {varstruct = rv,body} = dest_pabs body
+ in {varstruct = mk_pair{fst = lv, snd = rv}, body = body}
+ end
+end;
+
+
+(* Garbage - ought to be dropped *)
+val lhs = #lhs o dest_eq
+val rhs = #rhs o dest_eq
+val rator = #Rator o dest_comb
+val rand = #Rand o dest_comb
+val bvar = #Bvar o dest_abs
+val body = #Body o dest_abs
+
+
+(* Query routines *)
+val is_var = can dest_var
+val is_const = can dest_const
+val is_comb = can dest_comb
+val is_abs = can dest_abs
+val is_eq = can dest_eq
+val is_imp = can dest_imp
+val is_forall = can dest_forall
+val is_exists = can dest_exists
+val is_neg = can dest_neg
+val is_conj = can dest_conj
+val is_disj = can dest_disj
+val is_pair = can dest_pair
+val is_pabs = can dest_pabs
+
+
+(* Construction of a Term from a list of Terms *)
+
+fun list_mk_abs(L,tm) = itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
+
+(* These others are almost never used *)
+fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
+fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists{Bvar=v, Body=b})V t;
+fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
+val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
+val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj{disj1=d1, disj2=tm})
+
+
+(* Need to reverse? *)
+fun gen_all tm = list_mk_forall(free_vars tm, tm);
+
+(* Destructing a Term to a list of Terms *)
+fun strip_comb tm =
+ let fun dest(M$N, A) = dest(M, N::A)
+ | dest x = x
+ in dest(tm,[])
+ end;
+
+fun strip_abs(tm as Abs _) =
+ let val {Bvar,Body} = dest_abs tm
+ val (bvs, core) = strip_abs Body
+ in (Bvar::bvs, core)
+ end
+ | strip_abs M = ([],M);
+
+
+fun strip_imp fm =
+ if (is_imp fm)
+ then let val {ant,conseq} = dest_imp fm
+ val (was,wb) = strip_imp conseq
+ in ((ant::was), wb)
+ end
+ else ([],fm);
+
+fun strip_forall fm =
+ if (is_forall fm)
+ then let val {Bvar,Body} = dest_forall fm
+ val (bvs,core) = strip_forall Body
+ in ((Bvar::bvs), core)
+ end
+ else ([],fm);
+
+
+fun strip_exists fm =
+ if (is_exists fm)
+ then let val {Bvar, Body} = dest_exists fm
+ val (bvs,core) = strip_exists Body
+ in (Bvar::bvs, core)
+ end
+ else ([],fm);
+
+fun strip_conj w =
+ if (is_conj w)
+ then let val {conj1,conj2} = dest_conj w
+ in (strip_conj conj1@strip_conj conj2)
+ end
+ else [w];
+
+fun strip_disj w =
+ if (is_disj w)
+ then let val {disj1,disj2} = dest_disj w
+ in (strip_disj disj1@strip_disj disj2)
+ end
+ else [w];
+
+fun strip_pair tm =
+ if (is_pair tm)
+ then let val {fst,snd} = dest_pair tm
+ fun dtuple t =
+ if (is_pair t)
+ then let val{fst,snd} = dest_pair t
+ in (fst :: dtuple snd)
+ end
+ else [t]
+ in fst::dtuple snd
+ end
+ else [tm];
+
+
+fun mk_preterm tm = #t(rep_cterm tm);
+
+fun mk_prop (tm as Const("Trueprop",_) $ _) = tm
+ | mk_prop tm = mk_comb{Rator=mk_const{Name = "Trueprop",
+ Ty = bool --> mk_type{Tyop = "prop",Args=[]}},
+ Rand = tm};
+
+fun drop_Trueprop (Const("Trueprop",_) $ X) = X
+ | drop_Trueprop X = X;
+
+(* Miscellaneous *)
+
+fun mk_vstruct ty V =
+ let fun follow_prod_type ty vs =
+ let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty
+ val (ltm,vs1) = follow_prod_type ty1 vs
+ val (rtm,vs2) = follow_prod_type ty2 vs1
+ in (mk_pair{fst=ltm, snd=rtm}, vs2)
+ end handle _ => (hd vs, tl vs)
+ in fst(follow_prod_type ty V)
+ end;
+
+
+(* Search a term for a sub-term satisfying the predicate p. *)
+fun find_term p =
+ let fun find tm =
+ if (p tm)
+ then tm
+ else if (is_abs tm)
+ then find (#Body(dest_abs tm))
+ else let val {Rator,Rand} = dest_comb tm
+ in find Rator handle _ => find Rand
+ end handle _ => raise ERR{func = "find_term",mesg = ""}
+ in find
+ end;
+
+(*******************************************************************
+ * find_terms: (term -> bool) -> term -> term list
+ *
+ * Find all subterms in a term that satisfy a given predicate p.
+ *
+ *******************************************************************)
+fun find_terms p =
+ let fun accum tl tm =
+ let val tl' = if (p tm) then (tm::tl) else tl
+ in if (is_abs tm)
+ then accum tl' (#Body(dest_abs tm))
+ else let val {Rator,Rand} = dest_comb tm
+ in accum (accum tl' Rator) Rand
+ end handle _ => tl'
+ end
+ in accum []
+ end;
+
+
+val Term_to_string = string_of_cterm;
+
+fun dest_relation tm =
+ if (type_of tm = bool)
+ then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
+ in (R,y,x)
+ end handle _ => raise ERR{func="dest_relation",
+ mesg="unexpected term structure"}
+ else raise ERR{func="dest_relation",mesg="not a boolean term"};
+
+fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false;
+
+fun ARB ty = mk_select{Bvar=mk_var{Name="v",Ty=ty},
+ Body=mk_const{Name="True",Ty=bool}};
+
+end; (* Syntax *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/utils.sig Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,55 @@
+signature Utils_sig =
+sig
+ (* General error format and reporting mechanism *)
+ exception ERR of {module:string,func:string, mesg:string}
+ val Raise : exn -> 'a
+
+ (* infix 3 ## *)
+ val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd
+ val can : ('a -> 'b) -> 'a -> bool
+ val holds : ('a -> bool) -> 'a -> bool
+ val assert: ('a -> bool) -> 'a -> 'a
+ val W : ('a -> 'a -> 'b) -> 'a -> 'b
+ val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
+ val I : 'a -> 'a
+ val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
+ val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
+ val fst : 'a * 'b -> 'a
+ val snd : 'a * 'b -> 'b
+
+ (* option type *)
+ datatype 'a option = SOME of 'a | NONE
+
+ (* Set operations *)
+ val mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool
+ val union : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
+ val Union : ('a -> 'a -> bool) -> 'a list list -> 'a list
+ val intersect : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
+ val set_diff : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list
+ val mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list
+ val set_eq : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
+
+ val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+ val itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+ val rev_itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+ val end_itlist : ('a -> 'a -> 'a) -> 'a list -> 'a
+ val itlist2 :('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+ val filter : ('a -> bool) -> 'a list -> 'a list
+ val mapfilter : ('a -> 'b) -> 'a list -> 'b list
+ val pluck : ('a -> bool) -> 'a list -> 'a * 'a list
+ val assoc1 : ('a*'a->bool) -> 'a -> ('a * 'b) list -> ('a * 'b) option
+ val front_back : 'a list -> 'a list * 'a
+ val all : ('a -> bool) -> 'a list -> bool
+ val exists : ('a -> bool) -> 'a list -> bool
+ val zip : 'a list -> 'b list -> ('a*'b) list
+ val zip3 : 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
+ val unzip : ('a*'b) list -> ('a list * 'b list)
+ val take : ('a -> 'b) -> int * 'a list -> 'b list
+ val sort : ('a -> 'a -> bool) -> 'a list -> 'a list
+
+ val int_to_string : int -> string
+ val concat : string -> string -> string
+ val quote : string -> string
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/utils.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,197 @@
+(*---------------------------------------------------------------------------
+ * Some common utilities. This strucuture is parameterized over
+ * "int_to_string" because there is a difference between the string
+ * operations of SML/NJ versions 93 and 109.
+ *---------------------------------------------------------------------------*)
+
+functor UTILS (val int_to_string : int -> string) :Utils_sig =
+struct
+
+(* Standard exception for TFL. *)
+exception ERR of {module:string,func:string, mesg:string};
+fun UTILS_ERR{func,mesg} = ERR{module = "Utils",func=func,mesg=mesg};
+
+local
+fun info_string s {module,func,mesg} =
+ (s^" at "^module^"."^func^":\n"^mesg^"\n")
+in
+val ERR_string = info_string "Exception raised"
+val MESG_string = info_string "Message"
+end;
+
+fun Raise (e as ERR sss) = (output(std_out, ERR_string sss); raise e)
+ | Raise e = raise e;
+
+
+(* option type *)
+datatype 'a option = SOME of 'a | NONE
+
+
+(* Simple combinators *)
+
+infix 3 ##
+fun f ## g = (fn (x,y) => (f x, g y))
+
+fun W f x = f x x
+fun C f x y = f y x
+fun I x = x
+
+fun curry f x y = f(x,y)
+fun uncurry f (x,y) = f x y
+
+fun fst(x,y) = x
+fun snd(x,y) = y;
+
+val concat = curry (op ^)
+fun quote s = "\""^s^"\"";
+
+fun map2 f L1 L2 =
+ let fun mp2 [] [] L = rev L
+ | mp2 (a1::rst1) (a2::rst2) L = mp2 rst1 rst2 (f a1 a2::L)
+ | mp2 _ _ _ = raise UTILS_ERR{func="map2",mesg="different length lists"}
+ in mp2 L1 L2 []
+ end;
+
+
+fun itlist f L base_value =
+ let fun it [] = base_value
+ | it (a::rst) = f a (it rst)
+ in it L
+ end;
+
+fun rev_itlist f =
+ let fun rev_it [] base = base
+ | rev_it (a::rst) base = rev_it rst (f a base)
+ in rev_it
+ end;
+
+fun end_itlist f =
+ let fun endit [] = raise UTILS_ERR{func="end_itlist", mesg="list too short"}
+ | endit alist =
+ let val (base::ralist) = rev alist
+ in itlist f (rev ralist) base
+ end
+ in endit
+ end;
+
+fun itlist2 f L1 L2 base_value =
+ let fun it ([],[]) = base_value
+ | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
+ | it _ = raise UTILS_ERR{func="itlist2",mesg="different length lists"}
+ in it (L1,L2)
+ end;
+
+fun filter p L = itlist (fn x => fn y => if (p x) then x::y else y) L []
+
+fun mapfilter f alist = itlist (fn i=>fn L=> (f i::L) handle _ => L) alist [];
+
+fun pluck p =
+ let fun remv ([],_) = raise UTILS_ERR{func="pluck",mesg = "item not found"}
+ | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A)
+ in fn L => remv(L,[])
+ end;
+
+fun front_back [] = raise UTILS_ERR{func="front_back",mesg="empty list"}
+ | front_back [x] = ([],x)
+ | front_back (h::t) =
+ let val (L,b) = front_back t
+ in (h::L,b)
+ end;
+
+fun take f =
+ let fun grab(0,L) = []
+ | grab(n, x::rst) = f x::grab(n-1,rst)
+ in grab
+ end;
+
+fun all p =
+ let fun every [] = true
+ | every (a::rst) = (p a) andalso every rst
+ in every
+ end;
+
+fun exists p =
+ let fun ex [] = false
+ | ex (a::rst) = (p a) orelse ex rst
+ in ex
+ end;
+
+fun zip [] [] = []
+ | zip (a::b) (c::d) = (a,c)::(zip b d)
+ | zip _ _ = raise UTILS_ERR{func = "zip",mesg = "different length lists"};
+
+fun unzip L = itlist (fn (x,y) => fn (l1,l2) =>((x::l1),(y::l2))) L ([],[]);
+
+fun zip3 [][][] = []
+ | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
+ | zip3 _ _ _ = raise UTILS_ERR{func="zip3",mesg="different lengths"};
+
+
+fun can f x = (f x ; true) handle _ => false;
+fun holds P x = P x handle _ => false;
+
+
+fun assert p x =
+ if (p x) then x else raise UTILS_ERR{func="assert", mesg="predicate not true"}
+
+fun assoc1 eq item =
+ let fun assc ((entry as (key,_))::rst) =
+ if eq(item,key) then SOME entry else assc rst
+ | assc [] = NONE
+ in assc
+ end;
+
+(* Set ops *)
+nonfix mem union; (* Gag Barf Choke *)
+fun mem eq_func i =
+ let val eqi = eq_func i
+ fun mm [] = false
+ | mm (a::rst) = eqi a orelse mm rst
+ in mm
+ end;
+
+fun union eq_func =
+ let val mem = mem eq_func
+ fun un S1 [] = S1
+ | un [] S1 = S1
+ | un (a::rst) S2 = if (mem a S2) then (un rst S2) else (a::un rst S2)
+ in un
+ end;
+
+fun mk_set eq_func =
+ let val mem = mem eq_func
+ fun mk [] = []
+ | mk (a::rst) = if (mem a rst) then mk rst else a::(mk rst)
+ in mk
+ end;
+
+(* Union of a family of sets *)
+fun Union eq_func set_o_sets = itlist (union eq_func) set_o_sets [];
+
+fun intersect eq_func S1 S2 = mk_set eq_func (filter (C (mem eq_func) S2) S1);
+
+(* All the elements in the first set that are not also in the second set. *)
+fun set_diff eq_func S1 S2 = filter (fn x => not (mem eq_func x S2)) S1
+
+fun set_eq eq_func S1 S2 =
+ null(set_diff eq_func S1 S2) andalso null(set_diff eq_func S2 S1);
+
+
+fun sort R =
+let fun part (m, []) = ([],[])
+ | part (m, h::rst) =
+ let val (l1,l2) = part (m,rst)
+ in if (R h m) then (h::l1, l2)
+ else (l1, h::l2) end
+ fun qsort [] = []
+ | qsort (h::rst) =
+ let val (l1,l2) = part(h,rst)
+ in qsort l1@ [h] @qsort l2
+ end
+in qsort
+end;
+
+
+val int_to_string = int_to_string;
+
+end; (* Utils *)