Now for recdefs that omit the WF relation;
removed the separation between draft and theory modes
--- a/TFL/post.sml Fri Apr 23 12:22:30 1999 +0200
+++ b/TFL/post.sml Fri Apr 23 12:23:21 1999 +0200
@@ -23,15 +23,18 @@
val define : theory -> xstring -> string -> string list
-> theory * Prim.pattern list
+ val function_i : theory -> xstring
+ -> thm list (* congruence rules *)
+ -> term list -> theory * thm
+
+ val function : theory -> xstring
+ -> thm list
+ -> string list -> theory * thm
+
val simplify_defn : simpset * thm list
-> theory * (string * Prim.pattern list)
-> {rules:thm list, induct:thm, tcs:term list}
- (*-------------------------------------------------------------------------
- val function : theory -> term -> {theory:theory, eq_ind : thm}
- val lazyR_def: theory -> term -> {theory:theory, eqns : thm}
- *-------------------------------------------------------------------------*)
-
end;
@@ -40,216 +43,217 @@
structure Prim = Prim
structure S = USyntax
-(*---------------------------------------------------------------------------
- * 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, []));
+ val trace = Prim.trace
+
+ (*---------------------------------------------------------------------------
+ * 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.
+ (*---------------------------------------------------------------------------
+ * 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 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 ss =
- Prim.postprocess
- {WFtac = REPEAT (ares_tac [wf_empty, wf_measure, wf_inv_image,
- wf_lex_prod, wf_less_than, wf_trancl] 1),
- terminator = asm_simp_tac ss 1
- THEN TRY(CLASET' (fn cs => best_tac
- (cs addSDs [not0_implies_Suc] addss ss)) 1),
- simplifier = Rules.simpl_conv ss []};
+ fun std_postprocessor ss =
+ Prim.postprocess
+ {WFtac = REPEAT (ares_tac [wf_empty, wf_pred_nat,
+ wf_measure, wf_inv_image,
+ wf_lex_prod, wf_less_than, wf_trancl] 1),
+ terminator = asm_simp_tac ss 1
+ THEN TRY(CLASET' (fn cs => best_tac
+ (cs addSDs [not0_implies_Suc] addss ss)) 1),
+ simplifier = Rules.simpl_conv ss []};
-val concl = #2 o Rules.dest_thm;
+ val concl = #2 o Rules.dest_thm;
-(*---------------------------------------------------------------------------
- * Defining a function with an associated termination relation.
- *---------------------------------------------------------------------------*)
-fun define_i thy fid R eqs =
- let val {functional,pats} = Prim.mk_functional thy eqs
- in (Prim.wfrec_definition0 thy (Sign.base_name fid) R functional, pats)
- end;
+ (*---------------------------------------------------------------------------
+ * Defining a function with an associated termination relation.
+ *---------------------------------------------------------------------------*)
+ fun define_i thy fid R eqs =
+ let val {functional,pats} = Prim.mk_functional thy eqs
+ in (Prim.wfrec_definition0 thy (Sign.base_name fid) R functional, pats)
+ end;
-(*lcp's version: takes strings; doesn't return "thm"
- (whose signature is a draft and therefore useless) *)
-fun define thy fid R eqs =
- let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[]))
- in define_i thy fid (read thy R) (map (read thy) eqs) end
- handle Utils.ERR {mesg,...} => error mesg;
+ fun define thy fid R eqs =
+ let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[]))
+ in define_i thy fid (read thy R) (map (read thy) eqs) end
+ handle Utils.ERR {mesg,...} => error mesg;
(*---------------------------------------------------------------------------
* Postprocess a definition made by "define". This is a separate stage of
* processing from the definition stage.
*---------------------------------------------------------------------------*)
-local
-structure R = Rules
-structure U = Utils
+ 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
+ (* 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
+ 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
-fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
-val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
-val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
-fun mk_meta_eq r = case concl_of r of
- Const("==",_)$_$_ => r
- | _$(Const("op =",_)$_$_) => r RS eq_reflection
- | _ => r RS P_imp_P_eq_True
+ fun 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))
+ (*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 ss theory {f, R, rules, full_pats_TCs, TCs} =
- let val dummy = writeln "Proving induction theorem.. "
- val ind = Prim.mk_induction theory f R full_pats_TCs
- val dummy = writeln "Proved induction theorem.\nPostprocessing.. "
- val {rules, induction, nested_tcs} =
- std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
- in
- case nested_tcs
- of [] => (writeln "Postprocessing done.";
- {induction=induction, rules=rules,tcs=[]})
- | L => let val dummy = writeln "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
- val dummy = writeln "Postprocessing done."
- in
- {induction = induction',
- rules = rules',
- tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
- (simplified@stubborn)}
- end
- end;
+ 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 ss theory {f, R, rules, full_pats_TCs, TCs} =
+ let val dummy = writeln "Proving induction theorem.. "
+ val ind = Prim.mk_induction theory
+ {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
+ val dummy = writeln "Proved induction theorem.\nPostprocessing.. "
+ val {rules, induction, nested_tcs} =
+ std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
+ in
+ case nested_tcs
+ of [] => (writeln "Postprocessing done.";
+ {induction=induction, rules=rules,tcs=[]})
+ | L => let val dummy = writeln "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
+ val dummy = writeln "Postprocessing done."
+ 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)));
+ (*lcp: curry the predicate of the induction rule*)
+ fun curry_rule rl = split_rule_var
+ (head_of (HOLogic.dest_Trueprop (concl_of rl)),
+ rl);
-(*Strip off the outer !P*)
-val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
-
-val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def];
+ (*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)));
-(*Convert conclusion from = to ==*)
-val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th);
+ (*Strip off the outer !P*)
+ val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
-(*---------------------------------------------------------------------------
- * Install the basic context notions. Others (for nat and list and prod)
- * have already been added in thry.sml
- *---------------------------------------------------------------------------*)
-val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong];
+ val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def];
+
+ (*Convert conclusion from = to ==*)
+ val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th);
-fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
- let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy)))
- ("Recursive definition " ^ id ^
- " would clash with the theory of the same name!")
- val def = freezeT(get_def thy id) RS meta_eq_to_obj_eq
- val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs)
- val {theory,rules,TCs,full_pats_TCs,patterns} =
- Prim.post_definition
- (ss', defaultTflCongs @ eq_reflect_list tflCongs)
- (thy, (def,pats))
- val {lhs=f,rhs} = S.dest_eq(concl def)
- val (_,[R,_]) = S.strip_comb rhs
- val {induction, rules, tcs} =
- proof_stage ss' theory
- {f = f, R = R, rules = rules,
- full_pats_TCs = full_pats_TCs,
- TCs = TCs}
- val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules)
- in {induct = meta_outer
- (normalize_thm [RSspec,RSmp] (induction RS spec')),
- rules = rules',
- tcs = (termination_goals rules') @ tcs}
- end
- handle Utils.ERR {mesg,func,module} =>
- error (mesg ^
- "\n (In TFL function " ^ module ^ "." ^ func ^ ")");
-end;
+ (*---------------------------------------------------------------------------
+ * Install the basic context notions. Others (for nat and list and prod)
+ * have already been added in thry.sml
+ *---------------------------------------------------------------------------*)
+ fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
+ let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy)))
+ ("Recursive definition " ^ id ^
+ " would clash with the theory of the same name!")
+ val def = freezeT(get_def thy id) RS meta_eq_to_obj_eq
+ val {theory,rules,TCs,full_pats_TCs,patterns} =
+ Prim.post_definition (Prim.congs tflCongs)
+ (thy, (def,pats))
+ val {lhs=f,rhs} = S.dest_eq(concl def)
+ val (_,[R,_]) = S.strip_comb rhs
+ val ss' = ss addsimps Prim.default_simps
+ val {induction, rules, tcs} =
+ proof_stage ss' theory
+ {f = f, R = R, rules = rules,
+ full_pats_TCs = full_pats_TCs,
+ TCs = TCs}
+ val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules)
+ in {induct = meta_outer
+ (normalize_thm [RSspec,RSmp] (induction RS spec')),
+ rules = rules',
+ tcs = (termination_goals rules') @ tcs}
+ end
+ handle Utils.ERR {mesg,func,module} =>
+ error (mesg ^
+ "\n (In TFL function " ^ module ^ "." ^ func ^ ")");
(*---------------------------------------------------------------------------
*
- * Definitions with synthesized termination relation temporarily
- * deleted -- it's not clear how to integrate this facility with
- * the Isabelle theory file scheme, which restricts
- * inference at theory-construction time.
- *
-
-local structure R = Rules
-in
-fun function theory eqs =
- let val dummy = writeln "Making definition.. "
- val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs
- val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
- val dummy = writeln "Definition made."
- val dummy = writeln "Proving induction theorem.. "
- val induction = Prim.mk_induction theory f R full_pats_TCs
- val dummy = writeln "Induction theorem proved."
- in {theory = theory,
- eq_ind = standard (induction RS (rules RS conjI))}
- end
-end;
-
-
-fun lazyR_def theory eqs =
- let val {rules,theory, ...} = Prim.lazyR_def theory eqs
- in {eqns=rules, theory=theory}
- end
- handle e => print_exn e;
- *
+ * 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 function_i thy fid congs eqs =
+ let val dum = Theory.requires thy "WF_Rel" "recursive function definitions"
+ val {rules,R,theory,full_pats_TCs,SV,...} =
+ Prim.lazyR_def thy fid congs eqs
+ val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
+ val dummy = writeln "Definition made.\nProving induction theorem.. "
+ val induction = Prim.mk_induction theory
+ {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
+ val dummy = writeln "Induction theorem proved."
+ in (theory,
+ (*return the conjoined induction rule and recursion equations,
+ with assumptions remaining to discharge*)
+ standard (induction RS (rules RS conjI)))
+ end
+
+ fun function thy fid congs seqs =
+ let val _ = writeln ("Deferred recursive function " ^ fid)
+ fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[]))
+ in function_i thy fid congs (map (read thy) seqs) end
+ handle Utils.ERR {mesg,...} => error mesg;
+
+ end;
+
end;
--- a/TFL/rules.new.sml Fri Apr 23 12:22:30 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,784 +0,0 @@
-(* Title: TFL/rules
- ID: $Id$
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-Emulation of HOL inference rules for TFL
-*)
-
-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;
-
-
-(*----------------------------------------------------------------------------
- * 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 = ""};
-
-
-(*----------------------------------------------------------------------------
- * Implication and the assumption list
- *
- * Assumptions get stuck on the meta-language assumption list. Implications
- * are in the object language, so discharging an assumption "A" from theorem
- * "B" results in something that looks like "A --> B".
- *---------------------------------------------------------------------------*)
-fun ASSUME ctm = Thm.assume (D.mk_prop ctm);
-
-
-(*---------------------------------------------------------------------------
- * Implication in TFL is -->. Meta-language implication (==>) is only used
- * in the implementation of some of the inference rules below.
- *---------------------------------------------------------------------------*)
-fun MP th1 th2 = th2 RS (th1 RS mp);
-
-fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI;
-
-fun DISCH_ALL thm = Utils.itlist DISCH (#hyps (crep_thm thm)) thm;
-
-
-fun FILTER_DISCH_ALL P thm =
- let fun check tm = U.holds P (#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 = ""};
-
-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];
-
-fun LIST_CONJ [] = raise RULES_ERR{func = "LIST_CONJ", mesg = "empty list"}
- | LIST_CONJ [th] = th
- | LIST_CONJ (th::rst) = MP(MP(conjI COMP (impI RS impI)) th) (LIST_CONJ rst);
-
-
-(*----------------------------------------------------------------------------
- * Disjunction
- *---------------------------------------------------------------------------*)
-local val {prop,sign,...} = rep_thm disjI1
- val [P,Q] = term_vars prop
- val disj1 = forall_intr (cterm_of sign Q) disjI1
-in
-fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
-end;
-
-local val {prop,sign,...} = rep_thm disjI2
- val [P,Q] = term_vars prop
- val disj2 = forall_intr (cterm_of sign P) disjI2
-in
-fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
-end;
-
-
-(*----------------------------------------------------------------------------
- *
- * A1 |- M1, ..., An |- Mn
- * ---------------------------------------------------
- * [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
- *
- *---------------------------------------------------------------------------*)
-
-
-fun EVEN_ORS thms =
- let fun blue ldisjs [] _ = []
- | blue ldisjs (th::rst) rdisjs =
- let val tail = tl rdisjs
- val rdisj_tl = D.list_mk_disj tail
- in itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)
- :: blue (ldisjs@[cconcl th]) rst tail
- end handle _ => [itlist DISJ2 ldisjs th]
- in
- blue [] thms (map cconcl thms)
- end;
-
-
-(*----------------------------------------------------------------------------
- *
- * A |- P \/ Q B,P |- R C,Q |- R
- * ---------------------------------------------------
- * A U B U C |- R
- *
- *---------------------------------------------------------------------------*)
-local val [p1,p2,p3] = goal HOL.thy "(P | Q) ==> (P --> R) ==> (Q --> R) ==> R"
- val 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);
-
-local fun rew_conv mss = Thm.rewrite_cterm (true,false,false) mss (K(K None))
-in
-fun simpl_conv ss thl ctm =
- rew_conv (Thm.mss_of (#simps (Thm.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 ("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(Const("all",_) $ (a as Abs _)) = S.dest_abs a
- | dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};
-
-val is_all = Utils.can dest_all;
-
-fun strip_all fm =
- if (is_all fm)
- then let val {Bvar,Body} = dest_all fm
- val (bvs,core) = strip_all Body
- in ((Bvar::bvs), core)
- end
- else ([],fm);
-
-fun break_all(Const("all",_) $ Abs (_,_,body)) = body
- | break_all _ = raise RULES_ERR{func = "break_all", mesg = "not a !!"};
-
-fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =
- let val (L,core) = list_break_all body
- in ((s,ty)::L, core)
- end
- | list_break_all tm = ([],tm);
-
-(*---------------------------------------------------------------------------
- * Rename a term of the form
- *
- * !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
- * ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
- * to one of
- *
- * !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
- * ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
- *
- * This prevents name problems in extraction, and helps the result to read
- * better. There is a problem with varstructs, since they can introduce more
- * than n variables, and some extra reasoning needs to be done.
- *---------------------------------------------------------------------------*)
-
-fun get ([],_,L) = rev L
- | get (ant::rst,n,L) =
- case (list_break_all ant)
- of ([],_) => get (rst, n+1,L)
- | (vlist,body) =>
- let val eq = Logic.strip_imp_concl body
- val (f,args) = S.strip_comb (get_lhs eq)
- val (vstrl,_) = S.strip_abs f
- val names = 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);
-
-(* Note: rename_params_rule counts from 1, not 0 *)
-fun rename thm =
- let val {prop,sign,...} = rep_thm thm
- val tych = cterm_of sign
- val ants = Logic.strip_imp_prems prop
- val news = get (ants,1,[])
- in
- U.rev_itlist rename_params_rule news thm
- end;
-
-
-(*---------------------------------------------------------------------------
- * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
- *---------------------------------------------------------------------------*)
-
-fun list_beta_conv tm =
- let fun rbeta th = transitive th (beta_conversion(#2(D.dest_eq(cconcl th))))
- fun iter [] = reflexive tm
- | iter (v::rst) = rbeta (combination(iter rst) (reflexive v))
- in iter end;
-
-
-(*---------------------------------------------------------------------------
- * Trace information for the rewriter
- *---------------------------------------------------------------------------*)
-val term_ref = ref[] : term list ref
-val mss_ref = ref [] : meta_simpset list ref;
-val thm_ref = ref [] : thm list ref;
-val tracing = ref false;
-
-fun say s = if !tracing then 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};
-
-fun list_mk_aabs (vstrl,tm) =
- U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
-
-fun dest_aabs tm =
- let val {Bvar,Body} = S.dest_abs tm
- in (Bvar,Body)
- end handle _ => let val {varstruct,body} = S.dest_pabs tm
- in (varstruct,body)
- end;
-
-fun strip_aabs tm =
- let val (vstr,body) = dest_aabs tm
- val (bvs, core) = strip_aabs body
- in (vstr::bvs, core)
- end
- handle _ => ([],tm);
-
-fun dest_combn tm 0 = (tm,[])
- | dest_combn tm n =
- let val {Rator,Rand} = S.dest_comb tm
- val (f,rands) = dest_combn Rator (n-1)
- in (f,Rand::rands)
- end;
-
-
-
-
-local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
- fun mk_fst tm =
- let val ty 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 M n =
- let val (f,args) = dest_combn M n
- val dummy = dest_aabs f
- in (strip_aabs f,args)
- end;
-
-fun pbeta_redex M n = U.can (U.C dest_pbeta_redex n) M;
-
-fun dest_impl tm =
- let val ants = Logic.strip_imp_prems tm
- val eq = Logic.strip_imp_concl tm
- in (ants,get_lhs eq)
- end;
-
-fun restricted t = is_some (S.find_term
- (fn (Const("cut",_)) =>true | _ => false)
- t)
-
-fun CONTEXT_REWRITE_RULE (ss, func, R, cut_lemma, congs) th =
- let val pbeta_reduce = simpl_conv 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 mp) RS eq_reflection
- fun prover 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 = Thm.rewrite_cterm(false,true,false)mss' prover lhs
- handle _ => reflexive lhs
- 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,_),args) = dest_pbeta_redex 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 = Thm.rewrite_cterm (false,true,false) mss' prover Q1
- handle _ => reflexive Q1
- 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 _ =>
- ((Q2eeqQ3 RS meta_eq_to_obj_eq)
- RS ((thA RS meta_eq_to_obj_eq) RS trans))
- RS eq_reflection
- val impth = implies_intr_list ants1 QeeqQ3
- val impth1 = impth RS meta_eq_to_obj_eq
- (* Need to abstract *)
- val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
- in ant_th COMP thm
- end
- fun q_eliminate (thm,imp,sign) =
- let val (vlist,imp_body) = strip_all imp
- val (ants,Q) = dest_impl imp_body
- in if (pbeta_redex Q) (length vlist)
- then pq_eliminate (thm,sign,vlist,imp_body,Q)
- else
- let val tych = cterm_of sign
- val ants1 = map tych ants
- val mss' = add_prems(mss, map ASSUME ants1)
- val Q_eeq_Q1 = Thm.rewrite_cterm(false,true,false) mss'
- prover (tych Q)
- handle _ => reflexive (tych Q)
- val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
- val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
- val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
- in
- ant_th COMP thm
- end end
-
- fun eliminate thm =
- case (rep_thm thm)
- of {prop = (Const("==>",_) $ imp $ _), sign, ...} =>
- eliminate
- (if not(is_all imp)
- then uq_eliminate (thm,imp,sign)
- else q_eliminate (thm,imp,sign))
- (* Assume that the leading constant is ==, *)
- | _ => thm (* if it is not a ==> *)
- in Some(eliminate (rename thm))
- end handle _ => None
-
- fun restrict_prover mss thm =
- let val 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,[]), [func,R])
- in U.itlist Forall vlist tm
- end
- (*--------------------------------------------------------------
- * This actually isn't quite right, since it will think that
- * not-fully applied occs. of "f" in the context mean that the
- * current call is nested. The real solution is to pass in a
- * term "f v1..vn" which is a pattern that any full application
- * of "f" will match.
- *-------------------------------------------------------------*)
- val func_name = #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
- in
- (if (is_cong thm) then cong_prover else restrict_prover) mss thm
- end
- val ctm = cprop_of th
- val th1 = Thm.rewrite_cterm(false,true,false) (add_congs(mss_of [cut_lemma'], congs))
- prover 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/rules.sig Fri Apr 23 12:22:30 1999 +0200
+++ b/TFL/rules.sig Fri Apr 23 12:23:21 1999 +0200
@@ -52,8 +52,8 @@
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 : simpset * term * term * thm * thm list
+ val tracing : bool ref
+ val CONTEXT_REWRITE_RULE : term * term list * thm * thm list
-> thm -> thm * term list
val RIGHT_ASSOC : thm -> thm
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/rules.sml Fri Apr 23 12:23:21 1999 +0200
@@ -0,0 +1,788 @@
+(* Title: TFL/rules
+ ID: $Id$
+ Author: Konrad Slind, Cambridge University Computer Laboratory
+ Copyright 1997 University of Cambridge
+
+Emulation of HOL inference rules for TFL
+*)
+
+
+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;
+
+
+(*----------------------------------------------------------------------------
+ * 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 = ""};
+
+
+(*----------------------------------------------------------------------------
+ * 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 = ""};
+
+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];
+
+fun LIST_CONJ [] = raise RULES_ERR{func = "LIST_CONJ", mesg = "empty list"}
+ | LIST_CONJ [th] = th
+ | LIST_CONJ (th::rst) = MP(MP(conjI COMP (impI RS impI)) th) (LIST_CONJ rst);
+
+
+(*----------------------------------------------------------------------------
+ * Disjunction
+ *---------------------------------------------------------------------------*)
+local val {prop,sign,...} = rep_thm disjI1
+ val [P,Q] = term_vars prop
+ val disj1 = forall_intr (cterm_of sign Q) disjI1
+in
+fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
+end;
+
+local val {prop,sign,...} = rep_thm disjI2
+ val [P,Q] = term_vars prop
+ val disj2 = forall_intr (cterm_of sign P) disjI2
+in
+fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
+end;
+
+
+(*----------------------------------------------------------------------------
+ *
+ * A1 |- M1, ..., An |- Mn
+ * ---------------------------------------------------
+ * [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
+ *
+ *---------------------------------------------------------------------------*)
+
+
+fun EVEN_ORS thms =
+ let fun blue ldisjs [] _ = []
+ | blue ldisjs (th::rst) rdisjs =
+ let val tail = tl rdisjs
+ val rdisj_tl = D.list_mk_disj tail
+ in itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)
+ :: blue (ldisjs@[cconcl th]) rst tail
+ end handle _ => [itlist DISJ2 ldisjs th]
+ in
+ blue [] thms (map cconcl thms)
+ end;
+
+
+(*----------------------------------------------------------------------------
+ *
+ * A |- P \/ Q B,P |- R C,Q |- R
+ * ---------------------------------------------------
+ * A U B U C |- R
+ *
+ *---------------------------------------------------------------------------*)
+local val [p1,p2,p3] = goal HOL.thy "(P | Q) ==> (P --> R) ==> (Q --> R) ==> R"
+ val 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);
+
+local fun rew_conv mss = Thm.rewrite_cterm (true,false,false) mss (K(K None))
+in
+fun simpl_conv ss thl ctm =
+ rew_conv (Thm.mss_of (#simps (Thm.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 ("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(Const("all",_) $ (a as Abs _)) = S.dest_abs a
+ | dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};
+
+val is_all = Utils.can dest_all;
+
+fun strip_all fm =
+ if (is_all fm)
+ then let val {Bvar,Body} = dest_all fm
+ val (bvs,core) = strip_all Body
+ in ((Bvar::bvs), core)
+ end
+ else ([],fm);
+
+fun break_all(Const("all",_) $ Abs (_,_,body)) = body
+ | break_all _ = raise RULES_ERR{func = "break_all", mesg = "not a !!"};
+
+fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =
+ let val (L,core) = list_break_all body
+ in ((s,ty)::L, core)
+ end
+ | list_break_all tm = ([],tm);
+
+(*---------------------------------------------------------------------------
+ * Rename a term of the form
+ *
+ * !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
+ * ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
+ * to one of
+ *
+ * !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
+ * ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
+ *
+ * This prevents name problems in extraction, and helps the result to read
+ * better. There is a problem with varstructs, since they can introduce more
+ * than n variables, and some extra reasoning needs to be done.
+ *---------------------------------------------------------------------------*)
+
+fun get ([],_,L) = rev L
+ | get (ant::rst,n,L) =
+ case (list_break_all ant)
+ of ([],_) => get (rst, n+1,L)
+ | (vlist,body) =>
+ let val eq = Logic.strip_imp_concl body
+ val (f,args) = S.strip_comb (get_lhs eq)
+ val (vstrl,_) = S.strip_abs f
+ val names = 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);
+
+(* Note: rename_params_rule counts from 1, not 0 *)
+fun rename thm =
+ let val {prop,sign,...} = rep_thm thm
+ val tych = cterm_of sign
+ val ants = Logic.strip_imp_prems prop
+ val news = get (ants,1,[])
+ in
+ U.rev_itlist rename_params_rule news thm
+ end;
+
+
+(*---------------------------------------------------------------------------
+ * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
+ *---------------------------------------------------------------------------*)
+
+fun list_beta_conv tm =
+ let fun rbeta th = transitive th (beta_conversion(#2(D.dest_eq(cconcl th))))
+ fun iter [] = reflexive tm
+ | iter (v::rst) = rbeta (combination(iter rst) (reflexive v))
+ in iter end;
+
+
+(*---------------------------------------------------------------------------
+ * Trace information for the rewriter
+ *---------------------------------------------------------------------------*)
+val term_ref = ref[] : term list ref
+val mss_ref = ref [] : meta_simpset list ref;
+val thm_ref = ref [] : thm list ref;
+val tracing = ref false;
+
+fun say s = if !tracing then 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};
+
+fun list_mk_aabs (vstrl,tm) =
+ U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
+
+fun dest_aabs tm =
+ let val {Bvar,Body} = S.dest_abs tm
+ in (Bvar,Body)
+ end handle _ => let val {varstruct,body} = S.dest_pabs tm
+ in (varstruct,body)
+ end;
+
+fun strip_aabs tm =
+ let val (vstr,body) = dest_aabs tm
+ val (bvs, core) = strip_aabs body
+ in (vstr::bvs, core)
+ end
+ handle _ => ([],tm);
+
+fun dest_combn tm 0 = (tm,[])
+ | dest_combn tm n =
+ let val {Rator,Rand} = S.dest_comb tm
+ val (f,rands) = dest_combn Rator (n-1)
+ in (f,Rand::rands)
+ end;
+
+
+
+
+local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
+ fun mk_fst tm =
+ let val ty 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 M n =
+ let val (f,args) = dest_combn M n
+ val dummy = dest_aabs f
+ in (strip_aabs f,args)
+ end;
+
+fun pbeta_redex M n = U.can (U.C dest_pbeta_redex n) M;
+
+fun dest_impl tm =
+ let val ants = Logic.strip_imp_prems tm
+ val eq = Logic.strip_imp_concl tm
+ in (ants,get_lhs eq)
+ end;
+
+fun restricted t = is_some (S.find_term
+ (fn (Const("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 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 = Thm.rewrite_cterm(false,true,false)mss' prover lhs
+ handle _ => reflexive lhs
+ 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,_),args) = dest_pbeta_redex 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 = Thm.rewrite_cterm (false,true,false) mss' prover Q1
+ handle _ => reflexive Q1
+ 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 _ =>
+ ((Q2eeqQ3 RS meta_eq_to_obj_eq)
+ RS ((thA RS meta_eq_to_obj_eq) RS trans))
+ RS eq_reflection
+ val impth = implies_intr_list ants1 QeeqQ3
+ val impth1 = impth RS meta_eq_to_obj_eq
+ (* Need to abstract *)
+ val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
+ in ant_th COMP thm
+ end
+ fun q_eliminate (thm,imp,sign) =
+ let val (vlist,imp_body) = strip_all imp
+ val (ants,Q) = dest_impl imp_body
+ in if (pbeta_redex Q) (length vlist)
+ then pq_eliminate (thm,sign,vlist,imp_body,Q)
+ else
+ let val tych = cterm_of sign
+ val ants1 = map tych ants
+ val mss' = add_prems(mss, map ASSUME ants1)
+ val Q_eeq_Q1 = Thm.rewrite_cterm(false,true,false) mss'
+ prover (tych Q)
+ handle _ => reflexive (tych Q)
+ val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
+ val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
+ val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
+ in
+ ant_th COMP thm
+ end end
+
+ fun eliminate thm =
+ case (rep_thm thm)
+ of {prop = (Const("==>",_) $ imp $ _), sign, ...} =>
+ eliminate
+ (if not(is_all imp)
+ then uq_eliminate (thm,imp,sign)
+ else q_eliminate (thm,imp,sign))
+ (* Assume that the leading constant is ==, *)
+ | _ => thm (* if it is not a ==> *)
+ in Some(eliminate (rename thm))
+ end handle _ => None
+
+ fun restrict_prover mss thm =
+ let val 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
+ in
+ (if (is_cong thm) then cong_prover else restrict_prover) mss thm
+ end
+ val ctm = cprop_of th
+ val th1 = Thm.rewrite_cterm(false,true,false) (add_congs(mss_of [cut_lemma'], congs))
+ prover 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/sys.sml Fri Apr 23 12:22:30 1999 +0200
+++ b/TFL/sys.sml Fri Apr 23 12:23:21 1999 +0200
@@ -26,7 +26,7 @@
use "usyntax.sml";
use "thms.sml";
use "dcterm.sml";
-use "rules.new.sml";
+use "rules.sml";
use "thry.sml";
--- a/TFL/tfl.sig Fri Apr 23 12:22:30 1999 +0200
+++ b/TFL/tfl.sig Fri Apr 23 12:23:21 1999 +0200
@@ -8,6 +8,13 @@
signature TFL_sig =
sig
+
+ val trace : bool ref
+
+ val default_simps : thm list (*simprules used for deriving rules...*)
+
+ val congs : thm list -> thm list (*fn to make congruent rules*)
+
datatype pattern = GIVEN of term * int
| OMITTED of term * int
@@ -17,30 +24,37 @@
val wfrec_definition0 : theory -> string -> term -> term -> theory
- val post_definition : simpset * thm list -> theory * (thm * pattern list)
- -> {theory : theory,
+ val post_definition : thm list -> theory * (thm * pattern list)
+ -> {theory : theory,
rules : thm,
TCs : term list list,
full_pats_TCs : (term * term list) list,
patterns : pattern list}
-(*CURRENTLY UNUSED
- val wfrec_eqns : simpset * thm list -> theory -> term list
- -> {WFR : term,
+ val wfrec_eqns : theory -> xstring
+ -> thm list (* congruence rules *)
+ -> term list
+ -> {WFR : term, SV : term list,
proto_def : term,
extracta :(thm * term list) list,
pats : pattern list}
- val lazyR_def : theory
+ val lazyR_def : theory -> xstring
+ -> thm list (* congruence rules *)
-> term list
- -> {theory:theory,
- rules :thm,
- R :term,
- full_pats_TCs :(term * term list) list,
- patterns: pattern list}
----------------------*)
+ -> {theory : theory,
+ rules : thm,
+ R : term,
+ SV : term list,
+ full_pats_TCs : (term * term list) list,
+ patterns : pattern list}
- val mk_induction : theory -> term -> term -> (term * term list) list -> thm
+ val mk_induction : theory
+ -> {fconst:term,
+ R : term,
+ SV : term list,
+ pat_TCs_list : (term * term list) list}
+ -> thm
val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
-> theory
--- a/TFL/tfl.sml Fri Apr 23 12:22:30 1999 +0200
+++ b/TFL/tfl.sml Fri Apr 23 12:23:21 1999 +0200
@@ -9,6 +9,8 @@
structure Prim : TFL_sig =
struct
+val trace = ref false;
+
(* Abbreviations *)
structure R = Rules;
structure S = USyntax;
@@ -31,6 +33,23 @@
(*---------------------------------------------------------------------------
+ handling of user-supplied congruence rules: lcp*)
+
+(*Convert conclusion from = to ==*)
+val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th);
+
+(*default congruence rules include those for LET and IF*)
+val default_congs = eq_reflect_list [Thms.LET_CONG, if_cong];
+
+fun congs ths = default_congs @ eq_reflect_list ths;
+
+val default_simps =
+ [less_Suc_eq RS iffD2, lex_prod_def, measure_def, inv_image_def];
+
+
+
+
+(*---------------------------------------------------------------------------
* The next function is common to pattern-match translation and
* proof of completeness of cases for the induction theorem.
*
@@ -314,6 +333,12 @@
*---------------------------------------------------------------------------*)
+(*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)
@@ -335,10 +360,7 @@
val wfrec_R_M = map_term_types poly_tvars
(wfrec $ map_term_types poly_tvars R)
$ functional
- val (def_term, _) =
- Sign.infer_types (Theory.sign_of thy) (K None) (K None) [] false
- ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M],
- propT)
+ val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M)
in PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy end
end;
@@ -379,7 +401,8 @@
| givens (GIVEN(tm,_)::pats) = tm :: givens pats
| givens (OMITTED _::pats) = givens pats;
-fun post_definition (ss, tflCongs) (theory, (def, pats)) =
+(*called only by Tfl.simplify_defn*)
+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
@@ -392,9 +415,7 @@
val (case_rewrites,context_congs) = extraction_thms theory
val corollaries' = map(rewrite_rule case_rewrites) corollaries
val extract = R.CONTEXT_REWRITE_RULE
- (ss, f, R,
- R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
- tflCongs@context_congs)
+ (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)
@@ -402,23 +423,29 @@
in
{theory = theory, (* holds def, if it's needed *)
rules = rules1,
- full_pats_TCs = merge (map pat_of pats)
- (ListPair.zip (given_pats, TCs)),
+ full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
TCs = TCs,
patterns = pats}
end;
+
(*---------------------------------------------------------------------------
* Perform the extraction without making the definition. Definition and
- * extraction commute for the non-nested case. For hol90 users, this
- * function can be invoked without being in draft mode.
- * CURRENTLY UNUSED
-fun wfrec_eqns (ss, tflCongs) thy eqns =
- let val {functional,pats} = mk_functional thy eqns
+ * extraction commute for the non-nested case. (Deferred recdefs)
+ *---------------------------------------------------------------------------*)
+fun wfrec_eqns thy fid tflCongs eqns =
+ let val {functional as Abs(Name, Ty, _), pats} = mk_functional thy eqns
val given_pats = givens pats
- val {Bvar = f, Body} = S.dest_abs functional
- val {Bvar = x, ...} = S.dest_abs Body
- val (Name, Type("fun", [f_dty, f_rty])) = dest_Free f
+ val f = #1 (S.strip_comb(#lhs(S.dest_eq (hd eqns))))
+ (* val f = Free(Name,Ty) *)
+ val Type("fun", [f_dty, f_rty]) = Ty
+ val dummy = if Name<>fid then
+ raise TFL_ERR{func = "lazyR_def",
+ mesg = "Expected a definition of " ^
+ quote fid ^ " but found one of " ^
+ quote Name}
+ else ()
+ val SV = S.free_vars_lr functional (* schema variables *)
val (case_rewrites,context_congs) = extraction_thms thy
val tych = Thry.typecheck thy
val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
@@ -427,20 +454,25 @@
Rtype)
val WFREC_THM = R.ISPECL [tych R, tych f] 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
- val extract = R.CONTEXT_REWRITE_RULE
- (ss, f, R1,
- R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA,
- tflCongs@context_congs)
- in {proto_def=proto_def,
+ fun extract X = R.CONTEXT_REWRITE_RULE
+ (f, R1::SV, cut_apply, tflCongs@context_congs) X
+ in {proto_def = (*Use == rather than = for definitions*)
+ mk_const_def (Theory.sign_of thy)
+ (Name, Ty, S.rhs proto_def),
+ SV=SV,
WFR=WFR,
pats=pats,
extracta = map extract corollaries'}
end;
- *---------------------------------------------------------------------------*)
(*---------------------------------------------------------------------------
@@ -448,37 +480,56 @@
* 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).
- * CURRENTLY UNUSED
-fun lazyR_def ss thy eqns =
- let val {proto_def,WFR,pats,extracta} = wfrec_eqns ss thy eqns
+ *---------------------------------------------------------------------------*)
+fun lazyR_def thy fid tflCongs eqns =
+ let val {proto_def,WFR,pats,extracta,SV} =
+ wfrec_eqns thy fid (congs tflCongs) eqns
val R1 = S.rand WFR
- val f = S.lhs proto_def
- val (Name,_) = dest_Free f
+ val f = #1 (Logic.dest_equals 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 theory =
thy
- |> PureThy.add_defs_i [Thm.no_attributes (Name ^ "_def", subst_free[(R1,R')] proto_def)];
- val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq)
+ |> PureThy.add_defs_i
+ [Thm.no_attributes (fid ^ "_def", proto_def')];
+ val def = get_axiom theory (fid ^ "_def") RS meta_eq_to_obj_eq
+ 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 baz = R.DISCH (tych proto_def)
- (U.itlist (R.DISCH o tych) full_rqt (R.LIST_CONJ extractants))
+ 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 def' = R.MP (R.SPEC (tych fconst)
- (R.SPEC (tych R') (R.GENL[tych R1, tych f] baz)))
+ (R.SPEC (tych R')
+ (R.GENL[tych R1, tych f_free] baz)))
def
- val body_th = R.LIST_CONJ (map (R.ASSUME o tych) full_rqt)
+ 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,
+ 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;
- *---------------------------------------------------------------------------*)
@@ -617,7 +668,7 @@
*
* 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
@@ -644,12 +695,38 @@
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
+ 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: we prove
- * <something>.
+ * 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]
@@ -711,7 +788,7 @@
* recursion induction (Rinduct) by proving the antecedent of Sinduct from
* the antecedent of Rinduct.
*---------------------------------------------------------------------------*)
-fun mk_induction thy f R pat_TCs_list =
+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
@@ -722,12 +799,12 @@
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 f P) pat_TCs_list
+ 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 f thy) tasks
+ val proved_cases = map (prove_case fconst thy) tasks
val v = Free (variant (foldr add_term_names (map concl proved_cases, []))
"v",
domain)
@@ -803,8 +880,20 @@
* 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 tc_eq = simplifier (tych tc)
+ 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 _ =>
--- a/TFL/thms.sig Fri Apr 23 12:22:30 1999 +0200
+++ b/TFL/thms.sig Fri Apr 23 12:23:21 1999 +0200
@@ -9,7 +9,6 @@
val WF_INDUCTION_THM:thm
val WFREC_COROLLARY :thm
val CUT_DEF :thm
- val CUT_LEMMA :thm
val SELECT_AX :thm
val LET_CONG :thm
--- a/TFL/thms.sml Fri Apr 23 12:22:30 1999 +0200
+++ b/TFL/thms.sml Fri Apr 23 12:23:21 1999 +0200
@@ -6,9 +6,8 @@
structure Thms : Thms_sig =
struct
- val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"
- val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct"
- val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply"
+ val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec"
+ val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct"
val CUT_DEF = cut_def
local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
--- a/TFL/usyntax.sml Fri Apr 23 12:22:30 1999 +0200
+++ b/TFL/usyntax.sml Fri Apr 23 12:23:21 1999 +0200
@@ -214,7 +214,6 @@
end;
-(* Garbage - ought to be dropped *)
val lhs = #lhs o dest_eq
val rhs = #rhs o dest_eq
val rand = #Rand o dest_comb