# HG changeset patch # User paulson # Date 845635264 -7200 # Node ID 3902e9af752f931d73c62d2c92c59a7b89f72f8b # Parent 81c8d46edfa3e8aebb8b9610c4eefe9334d67c70 Konrad Slind's TFL diff -r 81c8d46edfa3 -r 3902e9af752f TFL/README --- /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"; diff -r 81c8d46edfa3 -r 3902e9af752f TFL/WF1.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"; diff -r 81c8d46edfa3 -r 3902e9af752f TFL/WF1.thy --- /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 diff -r 81c8d46edfa3 -r 3902e9af752f TFL/dcterm.sml --- /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; diff -r 81c8d46edfa3 -r 3902e9af752f TFL/mask.sig --- /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 diff -r 81c8d46edfa3 -r 3902e9af752f TFL/mask.sml --- /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; diff -r 81c8d46edfa3 -r 3902e9af752f TFL/post.sml --- /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; diff -r 81c8d46edfa3 -r 3902e9af752f TFL/rules.new.sml --- /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 *) diff -r 81c8d46edfa3 -r 3902e9af752f TFL/rules.sig --- /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; diff -r 81c8d46edfa3 -r 3902e9af752f TFL/sys.sml --- /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"; + diff -r 81c8d46edfa3 -r 3902e9af752f TFL/test.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'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))"; + diff -r 81c8d46edfa3 -r 3902e9af752f TFL/test1.sml --- /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)"; diff -r 81c8d46edfa3 -r 3902e9af752f TFL/tfl.sig --- /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; diff -r 81c8d46edfa3 -r 3902e9af752f TFL/tfl.sml --- /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 + * . + * + * 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 *) diff -r 81c8d46edfa3 -r 3902e9af752f TFL/thms.sig --- /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; diff -r 81c8d46edfa3 -r 3902e9af752f TFL/thms.sml --- /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; diff -r 81c8d46edfa3 -r 3902e9af752f TFL/thry.sig --- /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; + + diff -r 81c8d46edfa3 -r 3902e9af752f TFL/thry.sml --- /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 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 *) diff -r 81c8d46edfa3 -r 3902e9af752f TFL/usyntax.sig --- /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; diff -r 81c8d46edfa3 -r 3902e9af752f TFL/usyntax.sml --- /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 *) diff -r 81c8d46edfa3 -r 3902e9af752f TFL/utils.sig --- /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; + diff -r 81c8d46edfa3 -r 3902e9af752f TFL/utils.sml --- /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 *)