--- a/TFL/dcterm.sml Thu Jan 04 18:13:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,193 +0,0 @@
-(* Title: TFL/dcterm.sml
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-*)
-
-(*---------------------------------------------------------------------------
- * Derived efficient cterm destructors.
- *---------------------------------------------------------------------------*)
-
-structure Dcterm :
-sig
- val mk_conj : cterm * cterm -> cterm
- val mk_disj : 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_var : cterm -> {Name:string, Ty:typ}
- val is_conj : cterm -> bool
- val is_cons : 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 list_mk_disj : cterm list -> cterm
- val strip_abs : cterm -> cterm list * cterm
- val strip_comb : cterm -> 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 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;
-fun swap (x,y) = (y,x);
-
-
-(*---------------------------------------------------------------------------
- * Some simple constructor functions.
- *---------------------------------------------------------------------------*)
-
-fun mk_const sign pr = cterm_of sign (Const pr);
-val mk_hol_const = mk_const (Theory.sign_of HOL.thy);
-
-fun mk_exists (r as (Bvar,Body)) =
- let val ty = #T(rep_cterm Bvar)
- val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
- in capply c (uncurry cabs r)
- end;
-
-
-local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
-in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
-end;
-
-local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
-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 None (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 "Cons"
-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_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_disj = Utils.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 (* FIXME do not handle _ !!! *)
- 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 None)
-val strip_forall = rev2swap o strip dest_forall
-val strip_exists = rev2swap o strip dest_exists
-
-val strip_disj = rev o (op::) o strip dest_disj
-
-
-(*---------------------------------------------------------------------------
- * Going into and out of prop
- *---------------------------------------------------------------------------*)
-local val prop = cterm_of (Theory.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; (* FIXME do not handle _ !!! *)
-
-end;
--- a/TFL/post.sml Thu Jan 04 18:13:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,231 +0,0 @@
-(* Title: TFL/post.sml
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-Second part of main module (postprocessing of TFL definitions).
-*)
-
-signature TFL =
-sig
- val trace: bool ref
- val quiet_mode: bool ref
- val message: string -> unit
- val tgoalw: theory -> thm list -> thm list -> thm list
- val tgoal: theory -> thm list -> thm list
- val std_postprocessor: claset -> simpset -> thm list -> theory ->
- {induction: thm, rules: thm, TCs: term list list} ->
- {induction: thm, rules: thm, nested_tcs: thm list}
- val define_i: theory -> claset -> simpset -> thm list -> thm list -> xstring ->
- term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
- val define: theory -> claset -> simpset -> thm list -> thm list -> xstring ->
- string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
- val defer_i: theory -> thm list -> xstring -> term list -> theory * thm
- val defer: theory -> thm list -> xstring -> string list -> theory * thm
-end;
-
-structure Tfl: TFL =
-struct
-
-structure S = USyntax
-
-
-(* messages *)
-
-val trace = Prim.trace
-
-val quiet_mode = ref false;
-fun message s = if ! quiet_mode then () else writeln s;
-
-
-(* misc *)
-
-fun read_term thy = Sign.simple_read_term (Theory.sign_of thy) HOLogic.termT;
-
-
-(*---------------------------------------------------------------------------
- * Extract termination goals so that they can be put it into a goalstack, or
- * have a tactic directly applied to them.
- *--------------------------------------------------------------------------*)
-fun termination_goals rules =
- map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
- (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
-
-(*---------------------------------------------------------------------------
- * Finds the termination conditions in (highly massaged) definition and
- * puts them into a goalstack.
- *--------------------------------------------------------------------------*)
-fun tgoalw thy defs rules =
- case termination_goals rules of
- [] => error "tgoalw: no termination conditions to prove"
- | L => goalw_cterm defs
- (Thm.cterm_of (Theory.sign_of thy)
- (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
-
-fun tgoal thy = tgoalw thy [];
-
-(*---------------------------------------------------------------------------
- * Three postprocessors are applied to the definition. It
- * attempts to prove wellfoundedness of the given relation, simplifies the
- * non-proved termination conditions, and finally attempts to prove the
- * simplified termination conditions.
- *--------------------------------------------------------------------------*)
-fun std_postprocessor cs ss wfs =
- Prim.postprocess
- {wf_tac = REPEAT (ares_tac wfs 1),
- terminator = asm_simp_tac ss 1
- THEN TRY (fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
- simplifier = Rules.simpl_conv ss []};
-
-
-
-val concl = #2 o Rules.dest_thm;
-
-(*---------------------------------------------------------------------------
- * Postprocess a definition made by "define". This is a separate stage of
- * processing from the definition stage.
- *---------------------------------------------------------------------------*)
-local
-structure R = Rules
-structure U = Utils
-
-(* The rest of these local definitions are for the tricky nested case *)
-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 lhs aconv rhs
- end handle _ => false (* FIXME do not handle _ !!! *)
-
-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
-
-(*Is this the best way to invoke the simplifier??*)
-fun rewrite L = rewrite_rule (map mk_meta_eq (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 = gen_union (op 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 proof_stage cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
- let
- val _ = message "Proving induction theorem ..."
- val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
- val _ = message "Postprocessing ...";
- val {rules, induction, nested_tcs} =
- std_postprocessor cs ss wfs theory {rules=rules, induction=ind, TCs=TCs}
- in
- case nested_tcs
- of [] => {induction=induction, rules=rules,tcs=[]}
- | L => let val dummy = message "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 rewr = full_simplify (ss addsimps (solved @ simplified'));
- val induction' = rewr induction
- and rules' = rewr rules
- in
- {induction = induction',
- rules = rules',
- tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
- (simplified@stubborn)}
- end
- end;
-
-
-(*lcp: curry the predicate of the induction rule*)
-fun curry_rule rl = split_rule_var
- (head_of (HOLogic.dest_Trueprop (concl_of rl)),
- rl);
-
-(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
-val meta_outer =
- curry_rule o standard o
- rule_by_tactic (REPEAT
- (FIRSTGOAL (resolve_tac [allI, impI, conjI]
- ORELSE' etac conjE)));
-
-(*Strip off the outer !P*)
-val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
-
-fun simplify_defn thy cs ss congs wfs id pats def0 =
- let val def = freezeT def0 RS meta_eq_to_obj_eq
- val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats))
- val {lhs=f,rhs} = S.dest_eq (concl def)
- val (_,[R,_]) = S.strip_comb rhs
- val {induction, rules, tcs} =
- proof_stage cs ss wfs theory
- {f = f, R = R, rules = rules,
- full_pats_TCs = full_pats_TCs,
- TCs = TCs}
- val rules' = map (standard o Rulify.rulify_no_asm) (R.CONJUNCTS rules)
- in {induct = meta_outer (Rulify.rulify_no_asm (induction RS spec')),
- rules = ListPair.zip(rules', rows),
- tcs = (termination_goals rules') @ tcs}
- end
- handle Utils.ERR {mesg,func,module} =>
- error (mesg ^
- "\n (In TFL function " ^ module ^ "." ^ func ^ ")");
-
-(*---------------------------------------------------------------------------
- * Defining a function with an associated termination relation.
- *---------------------------------------------------------------------------*)
-fun define_i thy cs ss congs wfs fid R eqs =
- let val {functional,pats} = Prim.mk_functional thy eqs
- val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
- in (thy, simplify_defn thy cs ss congs wfs fid pats def) end;
-
-fun define thy cs ss congs wfs fid R seqs =
- define_i thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)
- handle Utils.ERR {mesg,...} => error mesg;
-
-
-(*---------------------------------------------------------------------------
- *
- * Definitions with synthesized termination relation
- *
- *---------------------------------------------------------------------------*)
-
-local open USyntax
-in
-fun func_of_cond_eqn tm =
- #1(strip_comb(#lhs(dest_eq(#2 (strip_forall(#2(strip_imp tm)))))))
-end;
-
-fun defer_i thy congs fid eqs =
- let val {rules,R,theory,full_pats_TCs,SV,...} =
- Prim.lazyR_def thy (Sign.base_name fid) congs eqs
- val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) (* FIXME do not handle _ !!! *)
- val dummy = message "Proving induction theorem ...";
- val induction = Prim.mk_induction theory
- {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
- in (theory,
- (*return the conjoined induction rule and recursion equations,
- with assumptions remaining to discharge*)
- standard (induction RS (rules RS conjI)))
- end
-
-fun defer thy congs fid seqs =
- defer_i thy congs fid (map (read_term thy) seqs)
- handle Utils.ERR {mesg,...} => error mesg;
-end;
-
-end;
--- a/TFL/rules.sml Thu Jan 04 18:13:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,847 +0,0 @@
-(* Title: TFL/rules.sml
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-Emulation of HOL inference rules for TFL
-*)
-
-signature Rules_sig =
-sig
- val dest_thm : thm -> term list * term
-
- (* Inference rules *)
- val REFL :cterm -> thm
- val ASSUME :cterm -> 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 :cterm -> thm -> thm
- val UNDISCH :thm -> thm
- val INST_TYPE :(typ*typ)list -> thm -> thm
- val SPEC :cterm -> thm -> thm
- val ISPEC :cterm -> thm -> thm
- val ISPECL :cterm list -> thm -> thm
- val GEN :cterm -> thm -> thm
- val GENL :cterm list -> thm -> thm
- val LIST_CONJ :thm list -> thm
-
- val SYM : thm -> thm
- val DISCH_ALL : thm -> thm
- val FILTER_DISCH_ALL : (term -> 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 : cterm * thm -> thm -> thm
- val EXISTS : cterm * cterm -> thm -> thm
- val EXISTL : cterm list -> thm -> thm
- val IT_EXISTS : (cterm*cterm) list -> thm -> thm
-
- val EVEN_ORS : thm list -> thm list
- val DISJ_CASESL : thm -> thm list -> thm
-
- val list_beta_conv : cterm -> cterm list -> thm
- val SUBS : thm list -> thm -> thm
- val simpl_conv : simpset -> thm list -> cterm -> thm
-
- val rbeta : thm -> thm
-(* For debugging my isabelle solver in the conditional rewriter *)
- val term_ref : term list ref
- val thm_ref : thm list ref
- val mss_ref : meta_simpset list ref
- val tracing : bool ref
- val CONTEXT_REWRITE_RULE : term * term list * thm * thm list
- -> thm -> thm * term list
- val RIGHT_ASSOC : thm -> thm
-
- val prove : cterm * tactic -> thm
-end;
-
-
-structure Rules : Rules_sig =
-struct
-
-open Utils;
-
-structure USyntax = USyntax;
-structure S = USyntax;
-structure U = Utils;
-structure D = Dcterm;
-
-
-fun RULES_ERR{func,mesg} = Utils.ERR{module = "Rules",func=func,mesg=mesg};
-
-
-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 {prop,hyps,...} = rep_thm thm
- in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop 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;
-
-fun rbeta th =
- case Dcterm.strip_comb (cconcl th)
- of (eeq,[l,r]) => transitive th (beta_conversion false r)
- | _ => raise RULES_ERR{func="rbeta", mesg =""};
-
-(*----------------------------------------------------------------------------
- * typ 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 = ""}; (* FIXME do not handle _ !!! *)
-
-
-(*----------------------------------------------------------------------------
- * 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);
-
-(*forces the first argument to be a proposition if necessary*)
-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 (#t(rep_cterm tm))
- in foldr (fn (tm,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 = ""}; (* FIXME do not handle _ !!! *)
-
-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 dummy = by (rtac impI 1)
- val dummy = by (rtac (p2 RS mp) 1)
- val dummy = by (rtac (p1 RS mp) 1)
- val dummy = 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]; (* FIXME do not handle _ !!! *)
-
-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] (* FIXME do not handle _ !!! *)
- 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 dummy = by (rtac (p1 RS disjE) 1)
- val dummy = by (rtac (p2 RS mp) 1)
- val dummy = by (assume_tac 1)
- val dummy = by (rtac (p3 RS mp) 1)
- val dummy = 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 (fn t => HOLogic.dest_Trueprop t
- aconv term_of atm)
- (#hyps(rep_thm 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, HOLogic.dest_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;
-
-
-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 dummy = by (rtac (p1 RS exE) 1)
- val dummy = by (rtac ((p2 RS allE) RS mp) 1)
- val dummy = by (assume_tac 2)
- val dummy = 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 = t$u,...} = rep_cterm redex
- val residue = cterm_of sign (betapply(t,u))
- 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_free" 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(subst_free[b]
- (HOLogic.dest_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(subst_free[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); (* FIXME do not handle _ !!! *)
-
-local fun rew_conv mss = MetaSimplifier.rewrite_cterm (true,false,false) (K(K None)) mss
-in
-fun simpl_conv ss thl ctm =
- rew_conv (MetaSimplifier.mss_of (#simps (MetaSimplifier.dest_mss (#mss (rep_ss 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
- *---------------------------------------------------------------------------*)
-
-
-(* 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 ("Wellfounded_Recursion.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_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
-
-fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a
- | dest_all _ _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};
-
-val is_all = Utils.can (dest_all []);
-
-fun strip_all used fm =
- if (is_all fm)
- then let val ({Bvar, Body}, used') = dest_all used fm
- val (bvs, core, used'') = strip_all used' Body
- in ((Bvar::bvs), core, used'')
- end
- else ([], fm, used);
-
-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 = variantlist (map (#1 o dest_Free) vstrl,
- add_term_names(body, []))
- in get (rst, n+1, (names,n)::L)
- end handle _ => get (rst, n+1, L); (* FIXME do not handle _ !!! *)
-
-(* 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 false (#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 writeln s else ();
-
-fun print_thms s L =
- say (cat_lines (s :: map string_of_thm L));
-
-fun print_cterms s L =
- say (cat_lines (s :: map string_of_cterm L));
-
-
-(*---------------------------------------------------------------------------
- * 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}; (* FIXME do not handle _ !!! *)
-
-fun list_mk_aabs (vstrl,tm) =
- U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
-
-fun dest_aabs used tm =
- let val ({Bvar,Body}, used') = S.dest_abs used tm
- in (Bvar, Body, used') end handle _ => (* FIXME do not handle _ !!! *)
- let val {varstruct, body, used} = S.dest_pabs used tm
- in (varstruct, body, used) end;
-
-fun strip_aabs used tm =
- let val (vstr, body, used') = dest_aabs used tm
- val (bvs, core, used'') = strip_aabs used' body
- in (vstr::bvs, core, used'')
- end
- handle _ => ([], tm, used); (* FIXME do not handle _ !!! *)
-
-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 as Type("*", [fty,sty]) = type_of tm
- in Const ("fst", ty --> fty) $ tm end
- fun mk_snd tm =
- let val ty as Type("*", [fty,sty]) = type_of tm
- in Const ("snd", ty --> sty) $ tm end
-in
-fun XFILL tych x vstruct =
- let fun traverse p xocc L =
- if (is_Free 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 (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,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 (is_Free 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 used M n =
- let val (f,args) = dest_combn M n
- val dummy = dest_aabs used f
- in (strip_aabs used 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;
-
-fun restricted t = is_some (S.find_term
- (fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false)
- t)
-
-fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
- let val globals = func::G
- val pbeta_reduce = simpl_conv empty_ss [split RS eq_reflection];
- val tc_list = ref[]: term list ref
- val dummy = term_ref := []
- val dummy = thm_ref := []
- val dummy = mss_ref := []
- val cut_lemma' = cut_lemma RS eq_reflection
- fun prover used mss thm =
- let fun cong_prover mss thm =
- let val dummy = say "cong_prover:"
- val cntxt = prems_of_mss mss
- val dummy = print_thms "cntxt:" cntxt
- val dummy = say "cong rule:"
- val dummy = say (string_of_thm thm)
- val dummy = thm_ref := (thm :: !thm_ref)
- val dummy = mss_ref := (mss :: !mss_ref)
- (* Unquantified eliminate *)
- fun uq_eliminate (thm,imp,sign) =
- let val tych = cterm_of sign
- val dummy = print_cterms "To eliminate:" [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 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) mss' lhs
- handle _ => reflexive lhs (* FIXME do not handle _ !!! *)
- val dummy = print_thms "proven:" [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, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
- val dummy = assert (forall (op aconv)
- (ListPair.zip (vlist, args)))
- "assertion failed in CONTEXT_REWRITE_RULE"
- val imp_body1 = subst_free (ListPair.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 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') mss' Q1
- handle _ => reflexive Q1 (* FIXME do not handle _ !!! *)
- val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
- val Q3 = tych(list_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 _ => (* FIXME do not 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, used') = strip_all used 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 = MetaSimplifier.rewrite_cterm
- (false,true,false) (prover used') mss' (tych Q)
- handle _ => reflexive (tych Q) (* FIXME do not handle _ !!! *)
- 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 (* FIXME do not handle _ !!! *)
-
- fun restrict_prover mss thm =
- let val dummy = say "restrict_prover:"
- val cntxt = rev(prems_of_mss mss)
- val dummy = print_thms "cntxt:" cntxt
- val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
- sign,...} = rep_thm thm
- fun genl tm = let val vlist = gen_rems (op aconv)
- (add_term_frees(tm,[]), globals)
- 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 = #1(dest_Const func)
- fun is_func (Const (name,_)) = (name = func_name)
- | is_func _ = false
- val rcontext = rev cntxt
- val cncl = HOLogic.dest_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 dummy = print_cterms "func:" [cterm_of sign func]
- val dummy = print_cterms "TC:"
- [cterm_of sign (HOLogic.mk_Trueprop TC)]
- val dummy = tc_list := (TC :: !tc_list)
- val nestedp = is_some (S.find_term is_func TC)
- val dummy = if nestedp then say "nested" else say "not_nested"
- val dummy = 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
- (HOLogic.mk_Trueprop 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 (* FIXME do not handle _ !!! *)
- in
- (if (is_cong thm) then cong_prover else restrict_prover) mss thm
- end
- val ctm = cprop_of th
- val names = add_term_names (term_of ctm, [])
- val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
- (prover names) (add_congs(mss_of [cut_lemma'], congs)) ctm
- val th2 = equal_elim th1 th
- in
- (th2, filter (not o restricted) (!tc_list))
- end;
-
-
-
-fun prove (ptm,tac) =
- #1 (freeze_thaw (prove_goalw_cterm [] ptm (fn _ => [tac])));
-
-
-end; (* Rules *)
--- a/TFL/tfl.sml Thu Jan 04 18:13:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1006 +0,0 @@
-(* Title: TFL/tfl.sml
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-First part of main module.
-*)
-
-signature TFL_sig =
-sig
- val trace: bool ref
- type pattern
- val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
- val wfrec_definition0: theory -> string -> term -> term -> theory * thm
- val post_definition: thm list -> theory * (thm * pattern list) ->
- {theory: theory,
- rules: thm,
- rows: int list,
- TCs: term list list,
- full_pats_TCs: (term * term list) list}
- val wfrec_eqns: theory -> xstring -> thm list -> term list ->
- {WFR: term,
- SV: term list,
- proto_def: term,
- extracta: (thm * term list) list,
- pats: pattern list}
- val lazyR_def: theory -> xstring -> thm list -> term list ->
- {theory: theory,
- rules: thm,
- R: term,
- SV: term list,
- full_pats_TCs: (term * term list) list,
- patterns : pattern list}
- val mk_induction: theory ->
- {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
- val postprocess: {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} -> theory ->
- {rules: thm, induction: thm, TCs: term list list} ->
- {rules: thm, induction: thm, nested_tcs: thm list}
-end;
-
-
-structure Prim: TFL_sig =
-struct
-
-val trace = ref false;
-
-open BasisLibrary;
-
-structure R = Rules;
-structure S = USyntax;
-structure U = Utils;
-
-
-fun TFL_ERR {func, mesg} = U.ERR {module = "Tfl", func = func, mesg = mesg};
-
-val concl = #2 o R.dest_thm;
-val hyp = #1 o R.dest_thm;
-
-val list_mk_type = U.end_itlist (curry (op -->));
-
-fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1));
-
-fun front_last [] = raise TFL_ERR {func="front_last", mesg="empty list"}
- | front_last [x] = ([],x)
- | front_last (h::t) =
- let val (pref,x) = front_last t
- in
- (h::pref,x)
- end;
-
-
-(*---------------------------------------------------------------------------
- * The next function is common to pattern-match translation and
- * proof of completeness of cases for the induction theorem.
- *
- * The curried function "gvvariant" returns a function to generate distinct
- * variables that are guaranteed not to be in names. The names of
- * the variables go u, v, ..., z, aa, ..., az, ... The returned
- * function contains embedded refs!
- *---------------------------------------------------------------------------*)
-fun gvvariant names =
- let val slist = ref names
- val vname = ref "u"
- fun new() =
- if !vname mem_string (!slist)
- then (vname := bump_string (!vname); new())
- else (slist := !vname :: !slist; !vname)
- in
- fn ty => Free(new(), ty)
- 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) = dest_Const c
- val L = binder_types 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 (#1(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 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;
-
-
-
-(*---------------------------------------------------------------------------
- * Each pattern carries with it a tag (i,b) where
- * i is the clause it came from and
- * b=true indicates that clause was given by the user
- * (or is an instantiation of a user supplied pattern)
- * b=false --> i = ~1
- *---------------------------------------------------------------------------*)
-
-type pattern = term * (int * bool)
-
-fun pattern_map f (tm,x) = (f tm, x);
-
-fun pattern_subst theta = pattern_map (subst_free theta);
-
-val pat_of = fst;
-fun row_of_pat x = fst (snd x);
-fun given x = snd (snd x);
-
-(*---------------------------------------------------------------------------
- * Produce an instance of a constructor, plus genvars for its arguments.
- *---------------------------------------------------------------------------*)
-fun fresh_constr ty_match colty gv c =
- let val (_,Ty) = dest_Const c
- val L = binder_types Ty
- and ty = body_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 ((prfx, p::rst), rhs)) =>
- fn (in_group,not_in_group) =>
- let val (pc,args) = S.strip_comb p
- in if ((#1(dest_Const pc) = Name) handle _ => false) (* FIXME do not handle _ !!! *)
- then (((prfx,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 (((prfx,_),_)::_)) =
-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) = dest_Const c'
- val (in_group, not_in_group) = mk_group Name rows
- val in_group' =
- if (null in_group) (* Constructor not given *)
- then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))]
- 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,l) =
- let val L = length (binder_types (type_of c))
- fun build (prfx,tag,plist) =
- let val args = take (L,plist)
- and plist' = drop(L,plist)
- in (prfx,tag,list_comb(c,args)::plist') end
- in map build l end;
-
-fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
- | v_to_prfx _ = raise TFL_ERR{func="mk_case", mesg="v_to_prfx"};
-
-fun v_to_pats (v::prfx,tag, pats) = (prfx, 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 usednames range_ty =
- let
- fun mk_case_fail s = raise TFL_ERR{func = "mk_case", mesg = s}
- val fresh_var = gvvariant usednames
- val divide = partition fresh_var ty_match
- fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
- | expand constructors ty (row as ((prfx, p::rst), rhs)) =
- if (is_Free p)
- then let val fresh = fresh_constr ty_match ty fresh_var
- fun expnd (c,gvs) =
- let val capp = list_comb(c,gvs)
- in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs)
- end
- in map expnd (map fresh constructors) end
- else [row]
- fun mk{rows=[],...} = mk_case_fail"no rows"
- | mk{path=[], rows = ((prfx, []), (tm,tag))::_} = (* Done *)
- ([(prfx,tag,[])], tm)
- | mk{path=[], rows = _::_} = mk_case_fail"blunder"
- | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} =
- mk{path = path,
- rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst}
- | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
- let val (pat_rectangle,rights) = ListPair.unzip rows
- val col0 = map(hd o #2) pat_rectangle
- in
- if (forall is_Free col0)
- then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e)
- (ListPair.zip (col0, rights))
- val pat_rectangle' = map v_to_prfx pat_rectangle
- val (pref_patl,tm) = mk{path = rstp,
- rows = ListPair.zip (pat_rectangle',
- rights')}
- in (map v_to_pats pref_patl, tm)
- end
- else
- let val pty as Type (ty_name,_) = type_of p
- in
- case (ty_info ty_name)
- of None => mk_case_fail("Not a known datatype: "^ty_name)
- | Some{case_const,constructors} =>
- let
- val case_const_name = #1(dest_Const case_const)
- val nrows = List.concat (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})
- (ListPair.zip (new_formals, groups))
- val rec_calls = map mk news
- val (pat_rect,dtrees) = ListPair.unzip rec_calls
- val case_functions = map S.list_mk_abs
- (ListPair.zip (new_formals, dtrees))
- val types = map type_of (case_functions@[u]) @ [range_ty]
- val case_const' = Const(case_const_name, list_mk_type types)
- val tree = list_comb(case_const', case_functions@[u])
- val pat_rect1 = List.concat
- (ListPair.map 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{Name,Ty} => [Free(Name,Ty)]
- | 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 mem_term (v,rst) then
- raise TFL_ERR{func = "no_repeat_vars",
- mesg = quote(#1(dest_Free v)) ^
- " occurs repeatedly in the pattern " ^
- quote (string_of_cterm (Thry.typecheck thy pat))}
- else check rst
- in check (FV_multiset pat)
- end;
-
-fun dest_atom (Free p) = p
- | dest_atom (Const p) = p
- | dest_atom _ = raise TFL_ERR {func="dest_atom",
- mesg="function name not an identifier"};
-
-fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q);
-
-local fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
- fun single [_$_] =
- mk_functional_err "recdef does not allow currying"
- | single [f] = f
- | single fs =
- (*multiple function names?*)
- if length (gen_distinct same_name fs) < length fs
- then mk_functional_err
- "The function being declared appears with multiple types"
- else mk_functional_err
- (Int.toString (length fs) ^
- " distinct function names being declared")
-in
-fun mk_functional thy clauses =
- let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses)
- handle _ => raise TFL_ERR (* FIXME do not handle _ !!! *)
- {func = "mk_functional",
- mesg = "recursion equations must use the = relation"}
- val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
- val atom = single (gen_distinct (op aconv) funcs)
- val (fname,ftype) = dest_atom atom
- val dummy = map (no_repeat_vars thy) pats
- val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
- map (fn (t,i) => (t,(i,true))) (enumerate R))
- val names = foldr add_term_names (R,[])
- val atype = type_of(hd pats)
- and aname = variant names "a"
- val a = Free(aname,atype)
- val ty_info = Thry.match_info thy
- val ty_match = Thry.match_type thy
- val range_ty = type_of (hd R)
- val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty
- {path=[a], rows=rows}
- val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
- handle _ => mk_functional_err "error in pattern-match translation" (* FIXME do not handle _ !!! *)
- 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
- val dummy = case (originals\\finals)
- of [] => ()
- | L => mk_functional_err
- ("The following clauses are redundant (covered by preceding clauses): " ^
- commas (map (fn i => Int.toString (i + 1)) L))
- in {functional = Abs(Sign.base_name fname, ftype,
- abstract_over (atom,
- absfree(aname,atype, case_tm))),
- pats = patts2}
-end end;
-
-
-(*----------------------------------------------------------------------------
- *
- * PRINCIPLES OF DEFINITION
- *
- *---------------------------------------------------------------------------*)
-
-
-(*For Isabelle, the lhs of a definition must be a constant.*)
-fun mk_const_def sign (Name, Ty, rhs) =
- Sign.infer_types sign (K None) (K None) [] false
- ([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT)
- |> #1;
-
-(*Make all TVars available for instantiation by adding a ? to the front*)
-fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
- | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
- | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
-
-local val f_eq_wfrec_R_M =
- #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY))))
- val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M
- val (fname,_) = dest_Free f
- val (wfrec,_) = S.strip_comb rhs
-in
-fun wfrec_definition0 thy fid R (functional as Abs(Name, Ty, _)) =
- let val def_name = if Name<>fid then
- raise TFL_ERR{func = "wfrec_definition0",
- mesg = "Expected a definition of " ^
- quote fid ^ " but found one of " ^
- quote Name}
- else Name ^ "_def"
- val wfrec_R_M = map_term_types poly_tvars
- (wfrec $ map_term_types poly_tvars R)
- $ functional
- val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M)
- val (thy', [def]) = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
- in (thy', def) end;
-end;
-
-
-
-(*---------------------------------------------------------------------------
- * This structure keeps track of congruence rules that aren't derived
- * from a datatype definition.
- *---------------------------------------------------------------------------*)
-fun extraction_thms thy =
- let val {case_rewrites,case_congs} = Thry.extract_info thy
- in (case_rewrites, case_congs)
- 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 (p aconv h) then (p,TCs)::rst else x::insrt rst
- | insrt (x::rst) = x::insrt rst
- | insrt[] = raise TFL_ERR{func="merge.insert",
- mesg="pattern 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 givens pats = map pat_of (filter given pats);
-
-fun post_definition meta_tflCongs (theory, (def, pats)) =
- let val tych = Thry.typecheck theory
- val f = #lhs(S.dest_eq(concl def))
- val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
- val pats' = filter given pats
- val given_pats = map pat_of pats'
- val rows = map row_of_pat pats'
- val WFR = #ant(S.dest_imp(concl corollary))
- val R = #Rand(S.dest_comb WFR)
- val corollary' = R.UNDISCH corollary (* put WF R on assums *)
- val corollaries = map (fn pat => R.SPEC (tych pat) corollary')
- given_pats
- val (case_rewrites,context_congs) = extraction_thms theory
- val corollaries' = map(rewrite_rule case_rewrites) corollaries
- val extract = R.CONTEXT_REWRITE_RULE
- (f, [R], cut_apply, meta_tflCongs@context_congs)
- val (rules, TCs) = ListPair.unzip (map extract corollaries')
- val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
- val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
- val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
- in
- {theory = theory, (* holds def, if it's needed *)
- rules = rules1,
- rows = rows,
- full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
- TCs = TCs}
- end;
-
-
-(*---------------------------------------------------------------------------
- * Perform the extraction without making the definition. Definition and
- * extraction commute for the non-nested case. (Deferred recdefs)
- *
- * The purpose of wfrec_eqns is merely to instantiate the recursion theorem
- * and extract termination conditions: no definition is made.
- *---------------------------------------------------------------------------*)
-
-fun wfrec_eqns thy fid tflCongs eqns =
- let val {lhs,rhs} = S.dest_eq (hd eqns)
- val (f,args) = S.strip_comb lhs
- val (fname,fty) = dest_atom f
- val (SV,a) = front_last args (* SV = schematic variables *)
- val g = list_comb(f,SV)
- val h = Free(fname,type_of g)
- val eqns1 = map (subst_free[(g,h)]) eqns
- val {functional as Abs(Name, Ty, _), pats} = mk_functional thy eqns1
- val given_pats = givens pats
- (* val f = Free(Name,Ty) *)
- val Type("fun", [f_dty, f_rty]) = Ty
- val dummy = if Name<>fid then
- raise TFL_ERR{func = "wfrec_eqns",
- mesg = "Expected a definition of " ^
- quote fid ^ " but found one of " ^
- quote Name}
- else ()
- val (case_rewrites,context_congs) = extraction_thms thy
- val tych = Thry.typecheck thy
- val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
- val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
- val R = Free (variant (foldr add_term_names (eqns,[])) Rname,
- Rtype)
- val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
- val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
- val dummy =
- if !trace then
- writeln ("ORIGINAL PROTO_DEF: " ^
- Sign.string_of_term (Theory.sign_of thy) proto_def)
- else ()
- val R1 = S.rand WFR
- val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
- val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
- val corollaries' = map (rewrite_rule case_rewrites) corollaries
- fun extract X = R.CONTEXT_REWRITE_RULE
- (f, R1::SV, cut_apply, tflCongs@context_congs) X
- in {proto_def = proto_def,
- SV=SV,
- 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 fid tflCongs eqns =
- let val {proto_def,WFR,pats,extracta,SV} =
- wfrec_eqns thy fid tflCongs eqns
- val R1 = S.rand WFR
- val f = #lhs(S.dest_eq proto_def)
- val (extractants,TCl) = ListPair.unzip extracta
- val dummy = if !trace
- then (writeln "Extractants = ";
- prths extractants;
- ())
- else ()
- val TCs = foldr (gen_union (op 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 proto_def' = subst_free[(R1,R')] proto_def
- val dummy = if !trace then writeln ("proto_def' = " ^
- Sign.string_of_term
- (Theory.sign_of thy) proto_def')
- else ()
- val {lhs,rhs} = S.dest_eq proto_def'
- val (c,args) = S.strip_comb lhs
- val (Name,Ty) = dest_atom c
- val defn = mk_const_def (Theory.sign_of thy)
- (Name, Ty, S.list_mk_abs (args,rhs))
- val (theory, [def0]) =
- thy
- |> PureThy.add_defs_i false
- [Thm.no_attributes (fid ^ "_def", defn)]
- val def = freezeT def0;
- val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
- else ()
- (* val fconst = #lhs(S.dest_eq(concl def)) *)
- val tych = Thry.typecheck theory
- val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
- (*lcp: a lot of object-logic inference to remove*)
- val baz = R.DISCH_ALL
- (U.itlist R.DISCH full_rqt_prop
- (R.LIST_CONJ extractants))
- val dum = if !trace then writeln ("baz = " ^ string_of_thm baz)
- else ()
- val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
- val SV' = map tych SV;
- val SVrefls = map reflexive SV'
- val def0 = (U.rev_itlist (fn x => fn th => R.rbeta(combination th x))
- SVrefls def)
- RS meta_eq_to_obj_eq
- val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
- val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
- val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX)
- body_th
- in {theory = theory, R=R1, SV=SV,
- rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def',
- full_pats_TCs = merge (map pat_of pats) (ListPair.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 = ListPair.zip (vlist, xlist)
- val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars
- handle OPTION => error
- "TFL fault [alpha_ex_unroll]: no correspondence"
- fun build ex [] = []
- | build (_$rex) (v::rst) =
- let val ex1 = betapply(rex, v)
- in ex1 :: build ex1 rst
- end
- val (nex::exl) = rev (tm::build tm args)
- in
- (nex, ListPair.zip (args, rev exl))
- end;
-
-
-
-(*----------------------------------------------------------------------------
- *
- * PROVING COMPLETENESS OF PATTERNS
- *
- *---------------------------------------------------------------------------*)
-
-fun mk_case ty_info usednames thy =
- let
- val divide = ipartition (gvvariant usednames)
- 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) = ListPair.unzip rows
- val col0 = map hd pat_rectangle
- val pat_rectangle' = map tl pat_rectangle
- in
- if (forall is_Free col0) (* column 0 is all variables *)
- then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
- (ListPair.zip (rights, col0))
- in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
- end
- else (* column 0 is all constructors *)
- let val Type (ty_name,_) = type_of p
- in
- case (ty_info ty_name)
- of None => fail("Not a known datatype: "^ty_name)
- | 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 = ListPair.map 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 = foldr
- (fn((x,t), th) =>
- R.CHOOSE (tych x, R.ASSUME (tych t)) th)
- val thms' = ListPair.map 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
- val ty_info = Thry.induct_info thy
- in fn pats =>
- let val names = foldr add_term_names (pats,[])
- val T = type_of (hd pats)
- val aname = Term.variant names "a"
- val vname = Term.variant (aname::names) "v"
- val a = Free (aname, T)
- val v = Free (vname, T)
- val a_eq_v = HOLogic.mk_eq(a,v)
- val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych 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 (vname::aname::names)
- 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 infix 5 ==>
- 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 = is_some (S.find_term (curry (op aconv) f) tm)
- 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 = gen_rems (op aconv) (S.free_vars_lr imp, globals)
- val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs (* FIXME do not handle _ !!! *)
- 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) = ListPair.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;
-*)
-
-local infix 5 ==>
- fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
-in
-fun build_ih f (P,SV) (pat,TCs) =
- let val pat_vars = S.free_vars_lr pat
- val globals = pat_vars@SV
- fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
- 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 = gen_rems (op aconv) (S.free_vars_lr imp, globals)
- val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs (* FIXME do not handle _ !!! *)
- in (S.list_mk_forall(locals,imp), (tm,locals)) end
- end
- in case TCs
- of [] => (S.list_mk_forall(pat_vars, P$pat), [])
- | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
- val ind_clause = S.list_mk_conj ihs ==> P$pat
- in (S.list_mk_forall(pat_vars,ind_clause), TCs_locals)
- end
- end
-end;
-
-(*---------------------------------------------------------------------------
- * This function makes good on the promise made in "build_ih".
- *
- * 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 = is_some (S.find_term (curry (op aconv) f) tm)
- 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 (* FIXME do not handle _ !!! *)
- 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] = 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 #2 (U.itlist CHOOSER L (veq,thm)) end;
-
-
-(*----------------------------------------------------------------------------
- * 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 {fconst, R, SV, pat_TCs_list} =
-let val tych = Thry.typecheck thy
- val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
- val (pats,TCsl) = ListPair.unzip pat_TCs_list
- val case_thm = complete_cases thy pats
- val domain = (type_of o hd) pats
- val Pname = Term.variant (foldr (foldr add_term_names)
- (pats::TCsl, [])) "P"
- val P = Free(Pname, domain --> HOLogic.boolT)
- 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 fconst (P,SV)) pat_TCs_list
- val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
- val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
- val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats
- val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
- val proved_cases = map (prove_case fconst thy) tasks
- val v = Free (variant (foldr add_term_names (map concl proved_cases, []))
- "v",
- domain)
- val vtyped = tych v
- val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
- val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]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 = type_of(#Bvar(S.dest_forall(concl dc)))
- val vars = map (gvvariant[Pname]) (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"}; (* FIXME do not handle _ !!! *)
-
-
-
-
-(*---------------------------------------------------------------------------
- *
- * 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{wf_tac, 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(HOLogic.mk_Trueprop
- (hd(#1(R.dest_thm rules)))),
- wf_tac)
- in (R.PROVE_HYP thm rules, R.PROVE_HYP thm induction)
- end handle _ => (rules,induction) (* FIXME do not handle _ !!! *)
-
- (*----------------------------------------------------------------------
- * 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 print_thms s L =
- if !trace then writeln (cat_lines (s :: map string_of_thm L))
- else ();
-
- fun print_cterms s L =
- if !trace then writeln (cat_lines (s :: map string_of_cterm L))
- else ();;
-
- fun simplify_tc tc (r,ind) =
- let val tc1 = tych tc
- val _ = print_cterms "TC before simplification: " [tc1]
- val tc_eq = simplifier tc1
- val _ = print_thms "result: " [tc_eq]
- in
- elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
- handle _ => (* FIXME do not handle _ !!! *)
- (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
- (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
- terminator)))
- (r,ind)
- handle _ => (* FIXME do not 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 _ (* FIXME do not handle _ !!! *)
- => (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
- (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
- terminator))
- handle _ => tc_eq)) (* FIXME do not handle _ !!! *)
- 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 = gen_rems (op 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 = ListPair.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;
-
-end;
--- a/TFL/thms.sml Thu Jan 04 18:13:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: TFL/thms.sml
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-*)
-
-signature Thms_sig =
-sig
- val WF_INDUCTION_THM: thm
- val WFREC_COROLLARY: thm
- val CUT_DEF: thm
- val SELECT_AX: thm
- val eqT: thm
- val rev_eq_mp: thm
- val simp_thm: thm
-end;
-
-structure Thms: Thms_sig =
-struct
- val WFREC_COROLLARY = get_thm Wellfounded_Recursion.thy "tfl_wfrec";
- val WF_INDUCTION_THM = get_thm Wellfounded_Recursion.thy "tfl_wf_induct";
- val CUT_DEF = get_thm Wellfounded_Recursion.thy "cut_def";
-
- val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
- (fn _ => [strip_tac 1, rtac someI 1, assume_tac 1]);
-
- fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
-
- val eqT = prove"(x = True) --> x";
- val rev_eq_mp = prove"(x = y) --> y --> x";
- val simp_thm = prove"(x-->y) --> (x = x') --> (x' --> y)";
-end;
--- a/TFL/thry.sml Thu Jan 04 18:13:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-(* Title: TFL/thry.sml
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-*)
-
-signature Thry_sig =
-sig
- val match_term : theory -> term -> term
- -> (term*term)list * (typ*typ)list
-
- val match_type : theory -> typ -> typ -> (typ*typ)list
-
- val typecheck : theory -> term -> cterm
-
- (* Datatype facts of various flavours *)
- val match_info: theory -> string -> {constructors:term list,
- case_const:term} option
-
- val induct_info: theory -> string -> {constructors:term list,
- nchotomy:thm} option
-
- val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list}
-
-end;
-
-
-structure Thry : Thry_sig (* LThry_sig *) =
-struct
-
-structure S = USyntax;
-
-fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
-
-(*---------------------------------------------------------------------------
- * Matching
- *---------------------------------------------------------------------------*)
-
-local 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(Theory.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 (Vartab.dest
- (Type.typ_match (#tsig(Sign.rep_sg(Theory.sign_of thry))) (Vartab.empty, (pat,ob))))
-end;
-
-
-(*---------------------------------------------------------------------------
- * Typing
- *---------------------------------------------------------------------------*)
-
-fun typecheck thry = Thm.cterm_of (Theory.sign_of thry);
-
-
-(*---------------------------------------------------------------------------
- * Get information about datatypes
- *---------------------------------------------------------------------------*)
-
-fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty);
-
-fun match_info thy tname =
- case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
- (Some case_const, Some constructors) =>
- Some {case_const = case_const, constructors = constructors}
- | _ => None;
-
-fun induct_info thy tname = case get_info thy tname of
- None => None
- | Some {nchotomy, ...} =>
- Some {nchotomy = nchotomy,
- constructors = the (DatatypePackage.constrs_of thy tname)};
-
-fun extract_info thy =
- let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
- in {case_congs = map (mk_meta_eq o #case_cong) infos,
- case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)}
- end;
-
-end; (* Thry *)
--- a/TFL/usyntax.sml Thu Jan 04 18:13:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,416 +0,0 @@
-(* Title: TFL/usyntax.sml
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-Emulation of HOL's abstract syntax functions.
-*)
-
-signature USyntax_sig =
-sig
- datatype lambda = VAR of {Name : string, Ty : typ}
- | CONST of {Name : string, Ty : typ}
- | COMB of {Rator: term, Rand : term}
- | LAMB of {Bvar : term, Body : term}
-
- val alpha : typ
-
- (* Types *)
- val type_vars : typ -> typ list
- val type_varsl : typ list -> typ list
- val mk_vartype : string -> typ
- val is_vartype : typ -> bool
- val strip_prod_type : typ -> typ list
-
- (* Terms *)
- val free_vars_lr : term -> term list
- val type_vars_in_term : term -> typ list
- val dest_term : term -> lambda
-
- (* Prelogic *)
- val inst : (typ*typ) list -> term -> term
-
- (* Construction routines *)
- val mk_abs :{Bvar : term, Body : term} -> term
-
- val mk_imp :{ant : term, conseq : term} -> term
- val mk_select :{Bvar : term, Body : term} -> term
- val mk_forall :{Bvar : term, Body : term} -> term
- val mk_exists :{Bvar : term, Body : term} -> term
- val mk_conj :{conj1 : term, conj2 : term} -> term
- val mk_disj :{disj1 : term, disj2 : term} -> term
- val mk_pabs :{varstruct : term, body : term} -> term
-
- (* Destruction routines *)
- val dest_const: term -> {Name : string, Ty : typ}
- val dest_comb : term -> {Rator : term, Rand : term}
- val dest_abs : string list -> term -> {Bvar : term, Body : term} * string list
- val dest_eq : term -> {lhs : term, rhs : term}
- val dest_imp : term -> {ant : term, conseq : term}
- val dest_forall : term -> {Bvar : term, Body : term}
- val dest_exists : term -> {Bvar : term, Body : term}
- val dest_neg : term -> term
- val dest_conj : term -> {conj1 : term, conj2 : term}
- val dest_disj : term -> {disj1 : term, disj2 : term}
- val dest_pair : term -> {fst : term, snd : term}
- val dest_pabs : string list -> term -> {varstruct : term, body : term, used : string list}
-
- val lhs : term -> term
- val rhs : term -> term
- val rand : term -> term
-
- (* Query routines *)
- val is_imp : term -> bool
- val is_forall : term -> bool
- val is_exists : term -> bool
- val is_neg : term -> bool
- val is_conj : term -> bool
- val is_disj : term -> bool
- val is_pair : term -> bool
- val is_pabs : term -> bool
-
- (* Construction of a term from a list of Preterms *)
- val list_mk_abs : (term list * term) -> term
- val list_mk_imp : (term list * term) -> term
- val list_mk_forall : (term list * term) -> term
- val list_mk_conj : term list -> term
-
- (* Destructing a term to a list of Preterms *)
- val strip_comb : term -> (term * term list)
- val strip_abs : term -> (term list * term)
- val strip_imp : term -> (term list * term)
- val strip_forall : term -> (term list * term)
- val strip_exists : term -> (term list * term)
- val strip_disj : term -> term list
-
- (* Miscellaneous *)
- val mk_vstruct : typ -> term list -> term
- val gen_all : term -> term
- val find_term : (term -> bool) -> term -> term option
- val dest_relation : term -> term * term * term
- val is_WFR : term -> bool
- val ARB : typ -> term
-end;
-
-
-structure USyntax : USyntax_sig =
-struct
-
-open Utils;
-
-infix 4 ##;
-
-fun USYN_ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg};
-
-
-(*---------------------------------------------------------------------------
- *
- * Types
- *
- *---------------------------------------------------------------------------*)
-val mk_prim_vartype = TVar;
-fun mk_vartype s = mk_prim_vartype((s,0),["term"]);
-
-(* But internally, it's useful *)
-fun dest_vtype (TVar x) = x
- | dest_vtype _ = raise USYN_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 = distinct (Utils.rev_itlist (curry op @ o type_vars) L []);
-
-val alpha = mk_vartype "'a"
-val beta = mk_vartype "'b"
-
-val strip_prod_type = HOLogic.prodT_factors;
-
-
-
-(*---------------------------------------------------------------------------
- *
- * Terms
- *
- *---------------------------------------------------------------------------*)
-
-(* 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;
-
-
-
-val type_vars_in_term = map mk_prim_vartype o term_tvars;
-
-
-
-(* Prelogic *)
-fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
-fun inst theta = subst_vars (map dest_tybinding theta,[])
-
-
-(* Construction routines *)
-
-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 USYN_ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
-
-
-fun mk_imp{ant,conseq} =
- let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
- in list_comb(c,[ant,conseq])
- end;
-
-fun mk_select (r as {Bvar,Body}) =
- let val ty = type_of Bvar
- val c = Const("Eps",(ty --> HOLogic.boolT) --> ty)
- in list_comb(c,[mk_abs r])
- end;
-
-fun mk_forall (r as {Bvar,Body}) =
- let val ty = type_of Bvar
- val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT)
- in list_comb(c,[mk_abs r])
- end;
-
-fun mk_exists (r as {Bvar,Body}) =
- let val ty = type_of Bvar
- val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT)
- in list_comb(c,[mk_abs r])
- end;
-
-
-fun mk_conj{conj1,conj2} =
- let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
- in list_comb(c,[conj1,conj2])
- end;
-
-fun mk_disj{disj1,disj2} =
- let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
- in list_comb(c,[disj1,disj2])
- end;
-
-fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
-
-local
-fun mk_uncurry(xt,yt,zt) =
- Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt)
-fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
- | dest_pair _ = raise USYN_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_uncurry(type_of fst,type_of snd,type_of body) $
- mpa(fst,mpa(snd,body))
- end
- in mpa(varstruct,body)
- end
- handle _ => raise USYN_ERR{func = "mk_pabs", mesg = ""}; (* FIXME do not handle _ !!! *)
-end;
-
-(* Destruction routines *)
-
-datatype lambda = VAR of {Name : string, Ty : typ}
- | CONST of {Name : string, Ty : typ}
- | COMB of {Rator: term, Rand : term}
- | LAMB of {Bvar : term, Body : term};
-
-
-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 = Free(s,ty)
- in LAMB{Bvar = v, Body = betapply (M,v)}
- end
- | dest_term(Bound _) = raise USYN_ERR{func = "dest_term",mesg = "Bound"};
-
-fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
- | dest_const _ = raise USYN_ERR{func = "dest_const", mesg = "not a constant"};
-
-fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
- | dest_comb _ = raise USYN_ERR{func = "dest_comb", mesg = "not a comb"};
-
-fun dest_abs used (a as Abs(s, ty, M)) =
- let
- val s' = variant used s;
- val v = Free(s', ty);
- in ({Bvar = v, Body = betapply (a,v)}, s'::used)
- end
- | dest_abs _ _ = raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"};
-
-fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
- | dest_eq _ = raise USYN_ERR{func = "dest_eq", mesg = "not an equality"};
-
-fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
- | dest_imp _ = raise USYN_ERR{func = "dest_imp", mesg = "not an implication"};
-
-fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a)
- | dest_forall _ = raise USYN_ERR{func = "dest_forall", mesg = "not a forall"};
-
-fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a)
- | dest_exists _ = raise USYN_ERR{func = "dest_exists", mesg="not an existential"};
-
-fun dest_neg(Const("not",_) $ M) = M
- | dest_neg _ = raise USYN_ERR{func = "dest_neg", mesg = "not a negation"};
-
-fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
- | dest_conj _ = raise USYN_ERR{func = "dest_conj", mesg = "not a conjunction"};
-
-fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
- | dest_disj _ = raise USYN_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 = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2)
- in list_comb(c,[fst,snd])
- end;
-
-fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
- | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"};
-
-
-local fun ucheck t = (if #Name(dest_const t) = "split" then t
- else raise Match)
-in
-fun dest_pabs used tm =
- let val ({Bvar,Body}, used') = dest_abs used tm
- in {varstruct = Bvar, body = Body, used = used'}
- end
- handle (* FIXME do not handle _ !!! *)
- _ => let val {Rator,Rand} = dest_comb tm
- val _ = ucheck Rator
- val {varstruct = lv, body, used = used'} = dest_pabs used Rand
- val {varstruct = rv, body, used = used''} = dest_pabs used' body
- in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''}
- end
-end;
-
-
-val lhs = #lhs o dest_eq
-val rhs = #rhs o dest_eq
-val rand = #Rand o dest_comb
-
-
-(* Query routines *)
-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 cterm 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_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})
-
-
-(* Need to reverse? *)
-fun gen_all tm = list_mk_forall(term_frees tm, tm);
-
-(* Destructing a cterm 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_disj w =
- if (is_disj w)
- then let val {disj1,disj2} = dest_disj w
- in (strip_disj disj1@strip_disj disj2)
- end
- else [w];
-
-
-(* Miscellaneous *)
-
-fun mk_vstruct ty V =
- let fun follow_prod_type (Type("*",[ty1,ty2])) vs =
- let 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
- | follow_prod_type _ (v::vs) = (v,vs)
- in #1 (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 Some tm
- else case tm of
- Abs(_,_,body) => find body
- | (t$u) => (Some (the (find t)) handle _ => find u) (* FIXME do not handle _ !!! *)
- | _ => None
- in find
- end;
-
-fun dest_relation tm =
- if (type_of tm = HOLogic.boolT)
- then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
- in (R,y,x)
- end handle _ => raise USYN_ERR{func="dest_relation",
- mesg="unexpected term structure"} (* FIXME do not handle _ !!! *)
- else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
-
-fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true
- | is_WFR _ = false;
-
-fun ARB ty = mk_select{Bvar=Free("v",ty),
- Body=Const("True",HOLogic.boolT)};
-
-end; (* Syntax *)
--- a/TFL/utils.sml Thu Jan 04 18:13:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-(* Title: TFL/utils.sml
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-Basic utilities.
-*)
-
-signature Utils_sig =
-sig
- exception ERR of {module:string,func:string, mesg:string}
-
- val can : ('a -> 'b) -> 'a -> bool
- val holds : ('a -> bool) -> 'a -> bool
- val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
-
- 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 pluck : ('a -> bool) -> 'a list -> 'a * 'a list
- val zip3 : 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
- val take : ('a -> 'b) -> int * 'a list -> 'b list
- val sort : ('a -> 'a -> bool) -> 'a list -> 'a list
-
-end;
-
-
-structure Utils =
-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};
-
-
-(* Simple combinators *)
-
-fun C f x y = f y x
-
-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 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 take f =
- let fun grab(0,L) = []
- | grab(n, x::rst) = f x::grab(n-1,rst)
- in grab
- end;
-
-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; (* FIXME do not handle _ !!! *)
-fun holds P x = P x handle _ => false; (* FIXME do not handle _ !!! *)
-
-
-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;
-
-
-end;