# HG changeset patch # User paulson # Date 863692199 -7200 # Node ID 14bd6e5985f1b1d15084e16f5ed6ca18662124ad # Parent 5aa3756a4bf2f03590e7628202e269d4e4531294 TFL now integrated with HOL (more work needed) diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/README --- a/TFL/README Thu May 15 11:35:26 1997 +0200 +++ b/TFL/README Thu May 15 12:29:59 1997 +0200 @@ -2,5 +2,5 @@ 1. Invoke the current version of Isabelle-HOL. 2. use "sys.sml"; -3. cd examples/Subst -4. use "ROOT.ML"; +3. cd "examples/Subst"; or 3. cd "examples"; +4. use "ROOT.ML"; 4. use"test.sml"; diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/ROOT.ML --- a/TFL/ROOT.ML Thu May 15 11:35:26 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -(* Title: TFL/ROOT.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Builds and tests Slind's TFL package. -Should be executed in the subdirectory HOL. -*) - -use"sys.sml"; -cd"examples/Subst"; -use"ROOT.ML"; diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/WF1.ML --- a/TFL/WF1.ML Thu May 15 11:35:26 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,232 +0,0 @@ -(* Title: HOL/WF.ML - ID: $Id$ - Author: Konrad Slind - Copyright 1996 TU Munich - -For WF1.thy. -*) - -open WF1; - -(* TFL variants *) -goal WF.thy - "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))"; -by (strip_tac 1); -by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1); -by (assume_tac 1); -by (fast_tac HOL_cs 1); -qed"tfl_wf_induct"; - -goal WF.thy "!f R. (x,a):R --> (cut f R a)(x) = f(x)"; -by (strip_tac 1); -by (rtac cut_apply 1); -by (assume_tac 1); -qed"tfl_cut_apply"; - -goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)"; -by (strip_tac 1); -by (res_inst_tac [("r","R"), ("H","M"), - ("a","x"), ("f","f")] (eq_reflection RS def_wfrec) 1); -by (assume_tac 1); -by (assume_tac 1); -qed "tfl_wfrec"; - -(*---------------------------------------------------------------------------- - * Proof that the inverse image into a wellfounded relation is wellfounded. - * The proof is relatively sloppy - I map to another version of - * wellfoundedness (every n.e. set has an R-minimal element) and transport - * the proof for that formulation over. I also didn't remember the existence - * of "set_cs" so no doubt the proof can be dramatically shortened! - *---------------------------------------------------------------------------*) -goal HOL.thy "(~(!x. P x)) = (? x. ~(P x))"; -by (fast_tac HOL_cs 1); -val th1 = result(); - -goal HOL.thy "(~(? x. P x)) = (!x. ~(P x))"; -by (fast_tac HOL_cs 1); -val th2 = result(); - -goal HOL.thy "(~(x-->y)) = (x & (~ y))"; -by (fast_tac HOL_cs 1); -val th3 = result(); - -goal HOL.thy "((~ x) | y) = (x --> y)"; -by (fast_tac HOL_cs 1); -val th4 = result(); - -goal HOL.thy "(~(x & y)) = ((~ x) | (~ y))"; -by (fast_tac HOL_cs 1); -val th5 = result(); - -goal HOL.thy "(~(x | y)) = ((~ x) & (~ y))"; -by (fast_tac HOL_cs 1); -val th6 = result(); - -goal HOL.thy "(~(~x)) = x"; -by (fast_tac HOL_cs 1); -val th7 = result(); - -(* Using [th1,th2,th3,th4,th5,th6,th7] as rewrites drives negation inwards. *) -val NNF_rews = map (fn th => th RS eq_reflection)[th1,th2,th3,th4,th5,th6,th7]; - -(* The name "contrapos" is already taken. *) -goal HOL.thy "(P --> Q) = ((~ Q) --> (~ P))"; -by (fast_tac HOL_cs 1); -val ol_contrapos = result(); - -(* Maps to another version of wellfoundedness *) -val [p1] = goalw WF.thy [wf_def] -"wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))"; -by (rtac allI 1); -by (rtac (ol_contrapos RS ssubst) 1); -by (rewrite_tac NNF_rews); -by (rtac impI 1); -by (rtac ((p1 RS spec) RS mp) 1); -by (fast_tac HOL_cs 1); -val wf_minimal = result(); - -goalw WF.thy [wf_def] -"(!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b)))) --> wf R"; -by (rtac impI 1); -by (rtac allI 1); -by (rtac (ol_contrapos RS ssubst) 1); -by (rewrite_tac NNF_rews); -by (rtac impI 1); -by (etac allE 1); -by (dtac mp 1); -by (assume_tac 1); -by (fast_tac HOL_cs 1); -val minimal_wf = result(); - -val wf_eq_minimal = - standard ((wf_minimal COMP ((minimal_wf RS mp) COMP iffI)) RS sym); - -goalw WF1.thy [inv_image_def,wf_eq_minimal RS eq_reflection] -"wf(R) --> wf(inv_image R (f::'a=>'b))"; -by (strip_tac 1); -by (etac exE 1); -by (subgoal_tac "? (w::'b). ? (x::'a). Q x & (f x = w)" 1); -by (rtac exI 2); -by (rtac exI 2); -by (rtac conjI 2); -by (assume_tac 2); -by (rtac refl 2); - -by (etac allE 1); -by (dtac mp 1); -by (assume_tac 1); -by (eres_inst_tac [("P","? min. (? x. Q x & f x = min) & \ - \ (! b. (b, min) : R --> ~ (? x. Q x & f x = b))")] rev_mp 1); -by (etac thin_rl 1); -by (etac thin_rl 1); -by (rewrite_tac NNF_rews); -by (rtac impI 1); -by (etac exE 1); -by (etac conjE 1); -by (etac exE 1); -by (rtac exI 1); -by (etac conjE 1); -by (rtac conjI 1); -by (assume_tac 1); -by (hyp_subst_tac 1); -by (rtac allI 1); -by (rtac impI 1); -by (etac CollectE 1); -by (etac allE 1); -by (dtac mp 1); -by (rewrite_tac[fst_conv RS eq_reflection,snd_conv RS eq_reflection]); -by (assume_tac 1); -by (fast_tac HOL_cs 1); -val wf_inv_image = result() RS mp; - -(* from Nat.ML *) -goalw WF1.thy [wf_def] "wf(pred_nat)"; -by (strip_tac 1); -by (nat_ind_tac "x" 1); -by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, - make_elim Suc_inject]) 2); -by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1); -val wf_pred_nat = result(); - -goalw WF1.thy [wf_def,pred_list_def] "wf(pred_list)"; -by (strip_tac 1); -by (List.list.induct_tac "x" 1); -by (etac allE 1); -by (etac impE 1); -by (assume_tac 2); -by (strip_tac 1); -by (etac CollectE 1); -by (asm_full_simp_tac (!simpset) 1); - -by (etac allE 1); -by (etac impE 1); -by (assume_tac 2); -by (strip_tac 1); -by (etac CollectE 1); -by (etac exE 1); -by (asm_full_simp_tac (!simpset) 1); -by (etac conjE 1); -by (hyp_subst_tac 1); -by (assume_tac 1); -qed "wf_pred_list"; - -(*---------------------------------------------------------------------------- - * All measures are wellfounded. - *---------------------------------------------------------------------------*) - -goalw WF1.thy [measure_def] "wf (measure f)"; -by (rtac wf_inv_image 1); -by (rtac wf_trancl 1); -by (rtac wf_pred_nat 1); -qed "wf_measure"; - -(*---------------------------------------------------------------------------- - * Wellfoundedness of lexicographic combinations - *---------------------------------------------------------------------------*) - -val prems = goal Prod.thy "!a b. P((a,b)) ==> !p. P(p)"; -by (cut_facts_tac prems 1); -by (rtac allI 1); -by (rtac (surjective_pairing RS ssubst) 1); -by (fast_tac HOL_cs 1); -qed "split_all_pair"; - -val [wfa,wfb] = goalw WF1.thy [wf_def,lex_prod_def] - "[| wf(ra); wf(rb) |] ==> wf(ra**rb)"; -by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); -by (rtac (wfa RS spec RS mp) 1); -by (EVERY1 [rtac allI,rtac impI]); -by (rtac (wfb RS spec RS mp) 1); -by (fast_tac (set_cs addSEs [Pair_inject]) 1); -qed "wf_lex_prod"; - -(*---------------------------------------------------------------------------- - * Wellfoundedness of relational product - *---------------------------------------------------------------------------*) -val [wfa,wfb] = goalw WF1.thy [wf_def,rprod_def] - "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)"; -by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); -by (rtac (wfa RS spec RS mp) 1); -by (EVERY1 [rtac allI,rtac impI]); -by (rtac (wfb RS spec RS mp) 1); -by (fast_tac (set_cs addSEs [Pair_inject]) 1); -qed "wf_rel_prod"; - - -(*--------------------------------------------------------------------------- - * Wellfoundedness of subsets - *---------------------------------------------------------------------------*) - -goalw WF1.thy [wf_eq_minimal RS eq_reflection] - "wf(r) --> (!x y. (x,y):p --> (x,y):r) --> wf(p)"; -by (fast_tac set_cs 1); -qed "wf_subset"; - -(*--------------------------------------------------------------------------- - * Wellfoundedness of the empty relation. - *---------------------------------------------------------------------------*) - -goalw WF1.thy [wf_eq_minimal RS eq_reflection,emptyr_def] - "wf(emptyr)"; -by (fast_tac set_cs 1); -qed "wf_emptyr"; diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/WF1.thy --- a/TFL/WF1.thy Thu May 15 11:35:26 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -(* Derived wellfounded relations, plus customized-for-TFL theorems from WF *) - -WF1 = List + -consts - inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set" - measure :: "('a => nat) => ('a * 'a)set" - "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70) - rprod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" - emptyr :: "('a * 'b) set" - pred_list :: "('a list * 'a list) set" - -defs - inv_image_def "inv_image R f == {p. (f(fst p), f(snd p)) : R}" - - measure_def "measure == inv_image (trancl pred_nat)" - - lex_prod_def "ra**rb == {p. ? a a' b b'. - p = ((a,b),(a',b')) & - ((a,a') : ra | a=a' & (b,b') : rb)}" - - rprod_def "rprod ra rb == {p. ? a a' b b'. - p = ((a,b),(a',b')) & - ((a,a') : ra & (b,b') : rb)}" - - emptyr_def "emptyr == {}" - pred_list_def "pred_list == {p. ? h. snd p = h#(fst p)}" -end diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/post.sml --- a/TFL/post.sml Thu May 15 11:35:26 1997 +0200 +++ b/TFL/post.sml Thu May 15 12:29:59 1997 +0200 @@ -1,9 +1,9 @@ -structure Tfl - :sig +signature TFL = + sig structure Prim : TFL_sig - val tgoalw : theory -> thm list -> thm -> thm list - val tgoal: theory -> thm -> thm list + val tgoalw : theory -> thm list -> thm list -> thm list + val tgoal: theory -> thm list -> thm list val WF_TAC : thm list -> tactic @@ -12,27 +12,41 @@ -> {induction:thm, rules:thm, TCs:term list list} -> {induction:thm, rules:thm, nested_tcs:thm list} - val rfunction : theory - -> (thm list -> thm -> thm) - -> term -> term - -> {induction:thm, rules:thm, - tcs:term list, theory:theory} + val define_i : theory -> term -> term -> theory * (thm * Prim.pattern list) + val define : theory -> string -> string list -> theory * Prim.pattern list - val Rfunction : theory -> term -> term - -> {induction:thm, rules:thm, - theory:theory, tcs:term list} + val simplify_defn : 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} + (*------------------------------------------------------------------------- + val function : theory -> term -> {theory:theory, eq_ind : thm} + val lazyR_def: theory -> term -> {theory:theory, eqns : thm} + *-------------------------------------------------------------------------*) val tflcongs : theory -> thm list - end = + end; + + +structure Tfl: TFL = struct structure Prim = Prim + structure S = Prim.USyntax - fun tgoalw thy defs thm = - let val L = Prim.termination_goals thm +(*--------------------------------------------------------------------------- + * 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 (Logic.freeze_vars o S.drop_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 = + let val L = termination_goals rules open USyntax val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L)) in goalw_cterm defs g @@ -40,6 +54,9 @@ val tgoal = Utils.C tgoalw []; + (*--------------------------------------------------------------------------- + * Simple wellfoundedness prover. + *--------------------------------------------------------------------------*) fun WF_TAC thms = REPEAT(FIRST1(map rtac thms)) val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_pred_nat, wf_pred_list, wf_trancl]; @@ -49,38 +66,62 @@ mem_Collect_eq,lessI]) 1 THEN TRY(fast_tac set_cs 1); +val length_Cons = prove_goal List.thy "length(h#t) = Suc(length t)" + (fn _ => [Simp_tac 1]); + val simpls = [less_eq RS eq_reflection, lex_prod_def, measure_def, inv_image_def, fst_conv RS eq_reflection, snd_conv RS eq_reflection, - mem_Collect_eq RS eq_reflection(*, length_Cons RS eq_reflection*)]; + mem_Collect_eq RS eq_reflection, length_Cons RS eq_reflection]; + (*--------------------------------------------------------------------------- + * Does some standard things with the termination conditions of a definition: + * attempts to prove wellfoundedness of the given relation; simplifies the + * non-proven termination conditions; and finally attempts to prove the + * simplified termination conditions. + *--------------------------------------------------------------------------*) val std_postprocessor = Prim.postprocess{WFtac = WFtac, terminator = terminator, simplifier = Prim.Rules.simpl_conv simpls}; val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @ [pred_nat_def,pred_list_def]); + fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy)); -local structure S = Prim.USyntax -in -fun func_of_cond_eqn tm = - #1(S.strip_comb(#lhs(S.dest_eq(#2(S.strip_forall(#2(S.strip_imp tm))))))) -end; - - val concl = #2 o Prim.Rules.dest_thm; (*--------------------------------------------------------------------------- - * Defining a function with an associated termination relation. Lots of - * postprocessing takes place. + * Defining a function with an associated termination relation. + *---------------------------------------------------------------------------*) +fun define_i thy R eqs = + let val dummy = require_thy thy "WF_Rel" "recursive function definitions"; + + val {functional,pats} = Prim.mk_functional thy eqs + val (thm,thry) = Prim.wfrec_definition0 thy R functional + in (thry,(thm,pats)) + end; + +(*lcp's version: takes strings; doesn't return "thm" + (whose signature is a draft and therefore useless) *) +fun define thy R eqs = + let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) + val (thy',(_,pats)) = + define_i thy (read thy R) + (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs)) + in (thy',pats) 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 S = Prim.USyntax structure R = Prim.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 = @@ -96,6 +137,7 @@ | _$(Const("op =",_)$_$_) => r RS eq_reflection | _ => r RS P_imp_P_eq_True fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L)) +fun reducer thl = rewrite (map standard thl @ #simps(rep_ss HOL_ss)) fun join_assums th = let val {sign,...} = rep_thm th @@ -105,30 +147,28 @@ val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) val cntxt = U.union S.aconv cntxtl cntxtr in - R.GEN_ALL - (R.DISCH_ALL - (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) + R.GEN_ALL + (R.DISCH_ALL + (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) end val gen_all = S.gen_all in -fun rfunction theory reducer R eqs = - let val _ = prs "Making definition.. " - val {rules,theory, full_pats_TCs, - TCs,...} = Prim.gen_wfrec_definition theory {R=R,eqs=eqs} - val f = func_of_cond_eqn(concl(R.CONJUNCT1 rules handle _ => rules)) - val _ = prs "Definition made.\n" - val _ = prs "Proving induction theorem.. " - val ind = Prim.mk_induction theory f R full_pats_TCs - val _ = prs "Proved induction theorem.\n" - val pp = std_postprocessor theory - val _ = prs "Postprocessing.. " - val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs} - val normal_tcs = Prim.termination_goals rules - in - case nested_tcs - of [] => (prs "Postprocessing done.\n"; - {theory=theory, induction=induction, rules=rules,tcs=normal_tcs}) - | L => let val _ = prs "Simplifying nested TCs.. " +(*--------------------------------------------------------------------------- + * The "reducer" argument is + * (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss))); + *---------------------------------------------------------------------------*) +fun proof_stage theory reducer {f, R, rules, full_pats_TCs, TCs} = + let val dummy = output(std_out, "Proving induction theorem.. ") + val ind = Prim.mk_induction theory f R full_pats_TCs + val dummy = output(std_out, "Proved induction theorem.\n") + val pp = std_postprocessor theory + val dummy = output(std_out, "Postprocessing.. ") + val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs} + in + case nested_tcs + of [] => (output(std_out, "Postprocessing done.\n"); + {induction=induction, rules=rules,tcs=[]}) + | L => let val dummy = output(std_out, "Simplifying nested TCs.. ") val (solved,simplified,stubborn) = U.itlist (fn th => fn (So,Si,St) => if (id_thm th) then (So, Si, th::St) else @@ -137,38 +177,65 @@ val simplified' = map join_assums simplified val induction' = reducer (solved@simplified') induction val rules' = reducer (solved@simplified') rules - val _ = prs "Postprocessing done.\n" + val dummy = output(std_out, "Postprocessing done.\n") in {induction = induction', rules = rules', - tcs = normal_tcs @ - map (gen_all o S.rhs o #2 o S.strip_forall o concl) - (simplified@stubborn), - theory = theory} + tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) + (simplified@stubborn)} end - end - handle (e as Utils.ERR _) => Utils.Raise e - | e => print_exn e + end handle (e as Utils.ERR _) => Utils.Raise e + | e => print_exn e; + + +(*lcp: put a theorem into Isabelle form, using meta-level connectives*) +val meta_outer = + standard o rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI])); + + +(*Strip off the outer !P*) +val spec'= read_instantiate [("x","P::?'b=>bool")] spec; -fun Rfunction thry = - rfunction thry - (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss))); - - +fun simplify_defn (thy,(id,pats)) = + let val def = freezeT(get_def thy id RS meta_eq_to_obj_eq) + val {theory,rules,TCs,full_pats_TCs,patterns} = + Prim.post_definition (thy,(def,pats)) + val {lhs=f,rhs} = S.dest_eq(concl def) + val (_,[R,_]) = S.strip_comb rhs + val {induction, rules, tcs} = + proof_stage theory reducer + {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,...} => error mesg end; +(*--------------------------------------------------------------------------- + * + * 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 = Prim.Rules +local fun floutput s = (output(std_out,s); flush_out std_out) + structure R = Prim.Rules in fun function theory eqs = - let val _ = prs "Making definition.. " + let val dummy = floutput "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 _ = prs "Definition made.\n" - val _ = prs "Proving induction theorem.. " + val dummy = floutput "Definition made.\n" + val dummy = floutput "Proving induction theorem.. " val induction = Prim.mk_induction theory f R full_pats_TCs - val _ = prs "Induction theorem proved.\n" + val dummy = floutput "Induction theorem proved.\n" in {theory = theory, eq_ind = standard (induction RS (rules RS conjI))} end @@ -183,8 +250,17 @@ end handle (e as Utils.ERR _) => Utils.Raise e | e => print_exn e; + * + * + *---------------------------------------------------------------------------*) + + - val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG]; +(*--------------------------------------------------------------------------- + * Install the basic context notions. Others (for nat and list and prod) + * have already been added in thry.sml + *---------------------------------------------------------------------------*) +val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG]; end; diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/rules.new.sml --- a/TFL/rules.new.sml Thu May 15 11:35:26 1997 +0200 +++ b/TFL/rules.new.sml Thu May 15 12:29:59 1997 +0200 @@ -542,7 +542,7 @@ val thm_ref = ref [] : thm list ref; val tracing = ref false; -fun say s = if !tracing then prs s else (); +fun say s = if !tracing then (output(std_out,s); flush_out std_out) else (); fun print_thms s L = (say s; diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/sys.sml --- a/TFL/sys.sml Thu May 15 11:35:26 1997 +0200 +++ b/TFL/sys.sml Thu May 15 12:29:59 1997 +0200 @@ -29,8 +29,7 @@ * Supply implementations *---------------------------------------------------------------------------*) -val _ = use_thy"WF1"; (* Wellfoundedness theory *) - +(* Ignore "Time" exception raised at end of building theory. *) use "usyntax.sml"; use "thms.sml"; use"dcterm.sml"; use"rules.new.sml"; @@ -45,4 +44,3 @@ structure Thry = Thry); use"post.sml"; - diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/test.sml --- a/TFL/test.sml Thu May 15 11:35:26 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,301 +0,0 @@ -fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[]))); -fun read thy = term_of o cread thy; -fun Term s = read WF1.thy s; - -fun Rfunc thy R eqs = - let val {induction,rules,theory,tcs} = - timeit(fn () => Tfl.Rfunction thy (read thy R) (read thy eqs)) - in {induction=induction, rules=rules, theory=theory, - tcs = map (cterm_of (sign_of theory)) tcs} - end; - -val Rfunction = Rfunc WF1.thy; - -fun function tm = timeit (fn () => Tfl.function WF1.thy (Term tm)); - - -(*--------------------------------------------------------------------------- - * Factorial. Notice how functions without pattern matching are often harder - * to deal with than those with! Unfortunately, not all functions can be - * described purely by pattern matching, e.g., "variant" as below. - *---------------------------------------------------------------------------*) -function "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))"; - -Rfunction"pred_nat" - "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))"; - -function "(Fact 0 = (Suc 0)) & \ - \ (Fact (Suc x) = (Fact x * Suc x))"; - -Rfunction "pred_nat" - "(Fact 0 = (Suc 0)) & \ - \ (Fact (Suc x) = (Fact x * Suc x))"; - -(*--------------------------------------------------------------------------- - * Fibonacci. - *---------------------------------------------------------------------------*) -function "(Fib 0 = (Suc 0)) & \ - \ (Fib (Suc 0) = (Suc 0)) & \ - \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))"; - -(* "<" doesn't currently work smoothly *) -Rfunction"{p::(nat*nat). fst p < snd p}" - "(Fib 0 = (Suc 0)) & \ - \ (Fib (Suc 0) = (Suc 0)) & \ - \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))"; - - -(* "trancl pred" means "<" and works better *) -Rfunction"trancl pred_nat" - "(Fib 0 = (Suc 0)) & \ - \ (Fib (Suc 0) = (Suc 0)) & \ - \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))"; - -(*--------------------------------------------------------------------------- - * Ackermann. - *---------------------------------------------------------------------------*) -Rfunction"pred_nat ** pred_nat" - "(Ack (0,n) = (n + Suc 0)) & \ - \ (Ack (Suc m,0) = (Ack (m, Suc 0))) & \ - \ (Ack (Suc m, Suc n) = Ack (m, Ack (Suc m, n)))"; - -(*--------------------------------------------------------------------------- - * Almost primitive recursion. - *---------------------------------------------------------------------------*) -function"(map2(f, [], L) = []) & \ - \ (map2(f, h#t, []) = []) & \ - \ (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))"; - -(* Swap arguments *) -function"(map2(([],L), f) = []) & \ - \ (map2((h#t, []), f) = []) & \ - \ (map2((h1#t1, h2#t2), f) = f h1 h2 # map2((t1,t2),f))"; - -Rfunction - "measure((length o fst o snd)::('a=>'b=>'c)*'a list*'b list => nat)" - "(map2((f::'a=>'b=>'c), ([]::'a list), (L::'b list)) = []) & \ -\ (map2(f, h#t, []) = []) & \ -\ (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))"; - -(*--------------------------------------------------------------------------- - * Relation "R" holds stepwise in a list - *---------------------------------------------------------------------------*) -function"(finiteRchain ((R::'a=>'a=>bool), ([]::'a list)) = True) & \ - \ (finiteRchain (R, [x]) = True) & \ - \ (finiteRchain (R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))"; - - -Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)" - "(finiteRchain((R::'a=>'a=>bool), ([]::'a list)) = True) & \ - \ (finiteRchain(R, [x]) = True) & \ - \ (finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))"; - -(*--------------------------------------------------------------------------- - * Quicksort. - *---------------------------------------------------------------------------*) -function"(qsort(ord, []) = []) & \ - \ (qsort(ord, x#rst) = \ - \ qsort(ord,filter(not o ord x) rst) \ - \ @[x]@ \ - \ qsort(ord,filter(ord x) rst))"; - -Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)" - "(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \ - \ (qsort(ord, x#rst) = \ - \ qsort(ord,filter(not o ord x) rst) \ - \ @[x]@ \ - \ qsort(ord,filter(ord x) rst))"; - -(*--------------------------------------------------------------------------- - * Variant. - *---------------------------------------------------------------------------*) -function"variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)"; - -Rfunction - "measure(%(p::nat*nat list). length(filter(%y. fst(p) <= y) (snd p)))" - "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)"; - -(*--------------------------------------------------------------------------- - * Euclid's algorithm - *---------------------------------------------------------------------------*) -function"(gcd ((0::nat),(y::nat)) = y) & \ - \ (gcd (Suc x, 0) = Suc x) & \ - \ (gcd (Suc x, Suc y) = \ - \ (if (y <= x) then gcd(x - y, Suc y) \ - \ else gcd(Suc x, y - x)))"; - - -(*--------------------------------------------------------------------------- - * Wrong answer because Isabelle rewriter (going bottom-up) attempts to - * apply congruence rule for split to "split" but can't because split is only - * partly applied. It then fails, instead of just not doing the rewrite. - * Tobias has said he'll fix it. - * - * ... July 96 ... seems to have been fixed. - *---------------------------------------------------------------------------*) - -Rfunction"measure (split (op+) ::nat*nat=>nat)" - "(gcd ((0::nat),(y::nat)) = y) & \ - \ (gcd (Suc x, 0) = Suc x) & \ - \ (gcd (Suc x, Suc y) = \ - \ (if (y <= x) then gcd(x - y, Suc y) \ - \ else gcd(Suc x, y - x)))"; - -(*--------------------------------------------------------------------------- - * A simple nested function. - *---------------------------------------------------------------------------*) -Rfunction"trancl pred_nat" - "(g 0 = 0) & \ - \ (g(Suc x) = g(g x))"; - -(*--------------------------------------------------------------------------- - * A clever division algorithm. Primitive recursive. - *---------------------------------------------------------------------------*) -function"(Div(0,x) = (0,0)) & \ - \ (Div(Suc x, y) = \ - \ (let (q,r) = Div(x,y) \ - \ in if (y <= Suc r) then (Suc q,0) else (q, Suc r)))"; - -Rfunction"inv_image pred_nat (fst::nat*nat=>nat)" - "(Div(0,x) = (0,0)) & \ - \ (Div(Suc x, y) = \ - \ (let q = fst(Div(x,y)); \ - \ r = snd(Div(x,y)) \ - \ in \ - \ if (y <= Suc r) then (Suc q,0) else (q, Suc r)))"; - -(*--------------------------------------------------------------------------- - * Testing nested contexts. - *---------------------------------------------------------------------------*) -function"(f(0,x) = (0,0)) & \ - \ (f(Suc x, y) = \ - \ (let z = x \ - \ in \ - \ if (0'a=>bool), ([]::'a list)) = []) & \ - \ (qsort(ord, x#rst) = \ - \ (let (L1,L2) = (filter(not o ord x) rst, \ - \ filter (ord x) rst) \ - \ in \ - \ qsort(ord,L1)@[x]@qsort(ord,L2)))"; - -function"(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \ - \ (qsort(ord, x#rst) = \ - \ (let (L1,L2,P) = (filter(not o ord x) rst, \ - \ filter (ord x) rst, x) \ - \ in \ - \ qsort(ord,L1)@[x]@qsort(ord,L2)))"; - -function"(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \ - \ (qsort(ord, x#rst) = \ - \ (let (L1,L2) = (filter(not o ord x) rst, \ - \ filter (ord x) rst); \ - \ (p,q) = (x,rst) \ - \ in \ - \ qsort(ord,L1)@[x]@qsort(ord,L2)))"; - - -(*--------------------------------------------------------------------------- - * A biggish function - *---------------------------------------------------------------------------*) - -function"(acc1(A,[],s,xss,zs,xs) = \ -\ (if xs=[] then (xss, zs) \ -\ else acc1(A, zs,s,(xss @ [xs]),[],[]))) & \ -\ (acc1(A,(y#ys), s, xss, zs, xs) = \ -\ (let s' = s; \ -\ zs' = (if fst A s' then [] else zs@[y]); \ -\ xs' = (if fst A s' then xs@zs@[y] else xs) \ -\ in \ -\ acc1(A, ys, s', xss, zs', xs')))"; - - -(*--------------------------------------------------------------------------- - * Nested, with context. - *---------------------------------------------------------------------------*) -Rfunction"pred_nat" - "(k 0 = 0) & \ -\ (k (Suc n) = (let x = k (Suc 0) \ -\ in if (0=Suc 0) then k (Suc(Suc 0)) else n))"; - - -(*--------------------------------------------------------------------------- - * A function that partitions a list into two around a predicate "P". - *---------------------------------------------------------------------------*) -val {theory,induction,rules,tcs} = - Rfunction - "inv_image pred_list \ - \ ((fst o snd)::('a=>bool)*'a list*'a list*'a list => 'a list)" - - "(part(P::'a=>bool, [], l1,l2) = (l1,l2)) & \ -\ (part(P, h#rst, l1,l2) = \ -\ (if P h then part(P,rst, h#l1, l2) \ -\ else part(P,rst, l1, h#l2)))"; - - -(*--------------------------------------------------------------------------- - * Another quicksort. - *---------------------------------------------------------------------------*) -Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)" - "(fqsort(ord,[]) = []) & \ -\ (fqsort(ord, x#rst) = \ - \ (let less = fst(part((%y. ord y x), rst,([],[]))); \ - \ more = snd(part((%y. ord y x), rst,([],[]))) \ - \ in \ - \ fqsort(ord,less)@[x]@fqsort(ord,more)))"; - -Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)" - "(fqsort(ord,[]) = []) & \ -\ (fqsort(ord, x#rst) = \ - \ (let (less,more) = part((%y. ord y x), rst,([],[])) \ - \ in \ - \ fqsort(ord,less)@[x]@fqsort(ord,more)))"; - - -(* Should fail on repeated variables. *) -function"(And(x,[]) = x) & \ - \ (And(y, y#t) = And(y, t))"; - diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/test1.sml --- a/TFL/test1.sml Thu May 15 11:35:26 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,83 +0,0 @@ -(*--------------------------------------------------------------------------- - * Pattern matching extensions. - *---------------------------------------------------------------------------*) - -fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[]))); -fun read thy = term_of o cread thy; -fun Term s = read WF1.thy s; - -fun Rfunc thy R eqs = - let val {induction,rules,theory,tcs} = - timeit(fn () => Tfl.Rfunction thy (read thy R) (read thy eqs)) - in {induction=induction, rules=rules, theory=theory, - tcs = map (cterm_of (sign_of theory)) tcs} - end; - -fun def tm = timeit (fn () => Tfl.function WF1.thy (Term tm)); - - - - -(*--------------------------------------------------------------------------- - * Normal patterns - *---------------------------------------------------------------------------*) -def "(f(x,y) = x+y)"; - -def "(f1 0 = 1) & (f1 (Suc n) = 2)"; - -(*--------------------------------------------------------------------------- - * Omitted patterns - *---------------------------------------------------------------------------*) -def "(f2 0 = 1)"; - -def "(f3 (h#t) = h)"; - -def "(f4 [a,b] = a) & (f4 [b] = b)"; - -def "(f5 (0,0) = 0)"; - -def "(f6 (0,0) = 0) & (f6 (0,Suc x) = x) & (f6 (Suc x, y) = y+x)"; - -def "(f7 (Suc 0, h#t) = 1) & (f7 (Suc(Suc n),h1#h2#t) = h1)"; - -def "(f8 (Suc(Suc n),h1#h2#t) = h1)"; - - -(*--------------------------------------------------------------------------- - * Overlapping patterns - *---------------------------------------------------------------------------*) -def "(f9 (h1#h2#t) = t) & (f9 x = x)"; - -def "(g (x,0) = 1) & (g (0,x) = 2)"; - -def "(g1 (0,x) = x) & (g1 (x,0) = x)"; - -def "(g2 ([], a#b#x) = 1) & (g2 (a#b#x, y) = 2) & (g2 (z, a#y) = a)"; - -def "(g3 (x,y,0) = 1) & (g3 (x,0,y) = 2) & (g3 (0,x,y) = x)"; - -def "(g4 (0,y,z) = 1) & (g4 (x,0,z) = 2) & (g4 (x,y,0) = x)"; - -def "(g5(0,x,y,z) = 1) & (g5(w,0,y,z) = 2) & (g5(w,x,0,z) = z) & \ - \ (g5(w,x,y,0) = y)"; - -def "(g6 (0,w,x,y,z) = 1) & (g6 (v,0,x,y,z) = 2) & (g6 (v,w,0,y,z) = z) & \ - \ (g6 (v,w,x,0,z) = z) & (g6 (v,w,x,y,0) = 0)"; - -def "(g7 [x, 0] = x) & (g7 [Suc v] = 1) & (g7 z = 2)"; - -def "(g8 (h1#h2#h3#h4#h5#h6) = [h1,h2,h3,h4,h5]# g8 h6) & (g8 x = [x])"; - -(* Normal *) -def "(g9 (Suc(Suc x)) = 1) & (g9 (Suc x) = 2) & (g9 0 = 0)"; - -(*--------------------------------------------------------------------------- - * Inaccessible patterns - *---------------------------------------------------------------------------*) -def "(h x = 1) & (h x = 2)"; - -def "(h1 (x,0) = 1) & (h1 (x,Suc y) = 2) & \ - \ (h1 (x,y) = x) & (h1 (x,y) = y)"; - -def "(h2 (x,0) = 1) & (h2 (0,x) = 2) & \ - \ (h2 (0,0) = 0) & (h2 (x,y) = x)"; diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/tfl.sig --- a/TFL/tfl.sig Thu May 15 11:35:26 1997 +0200 +++ b/TFL/tfl.sig Thu May 15 12:29:59 1997 +0200 @@ -18,9 +18,15 @@ -> {functional:Preterm, pats: pattern list} - val prim_wfrec_definition : Thry - -> {R:Preterm, functional:Preterm} - -> {def:Thm, corollary:Thm, theory:Thry} + val wfrec_definition0 : Thry -> Preterm -> Preterm -> Thm * Thry + + val post_definition : Thry * (Thm * pattern list) + -> {theory : Thry, + rules : Thm, + TCs : Preterm list list, + full_pats_TCs : (Preterm * Preterm list) list, + patterns : pattern list} + val wfrec_eqns : Thry -> Preterm -> {WFR : Preterm, @@ -29,14 +35,6 @@ pats : pattern list} - val gen_wfrec_definition : Thry - -> {R:Preterm, eqs:Preterm} - -> {theory:Thry, - rules :Thm, - TCs : Preterm list list, - full_pats_TCs :(Preterm * Preterm list) list, - patterns : pattern list} - val lazyR_def : Thry -> Preterm -> {theory:Thry, @@ -55,8 +53,6 @@ -> {rules:Thm, induction:Thm, TCs:Preterm list list} -> {rules:Thm, induction:Thm, nested_tcs:Thm list} - val termination_goals : Thm -> Preterm list - structure Context : sig val read : unit -> Thm list diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/tfl.sml --- a/TFL/tfl.sml Thu May 15 11:35:26 1997 +0200 +++ b/TFL/tfl.sml Thu May 15 12:29:59 1997 +0200 @@ -306,14 +306,17 @@ local fun paired1{lhs,rhs} = (lhs,rhs) and paired2{Rator,Rand} = (Rator,Rand) fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s} + fun single [f] = f + | single fs = mk_functional_err (Int.toString (length fs) ^ + " distinct function names!") in fun mk_functional thy eqs = let val clauses = S.strip_conj eqs val (L,R) = U.unzip (map (paired1 o S.dest_eq o U.snd o S.strip_forall) clauses) val (funcs,pats) = U.unzip(map (paired2 o S.dest_comb) L) - val [f] = U.mk_set (S.aconv) funcs - handle _ => mk_functional_err "function name not unique" + val f = single (U.mk_set (S.aconv) funcs) + val fvar = if (S.is_var f) then f else S.mk_var(S.dest_const f) val _ = map (no_repeat_vars thy) pats val rows = U.zip (map (fn x => ([],[x])) pats) (map GIVEN (enumerate R)) val fvs = S.free_varsl R @@ -334,7 +337,8 @@ of [] => () | L => mk_functional_err("The following rows (counting from zero)\ \ are inaccessible: "^stringize L) - in {functional = S.list_mk_abs ([f,a], case_tm), + val case_tm' = S.subst [f |-> fvar] case_tm + in {functional = S.list_mk_abs ([fvar,a], case_tm'), pats = patts2} end end; @@ -346,39 +350,28 @@ *---------------------------------------------------------------------------*) -(*---------------------------------------------------------------------------- - * This basic principle of definition takes a functional M and a relation R - * and specializes the following theorem - * - * |- !M R f. (f = WFREC R M) ==> WF R ==> !x. f x = M (f%R,x) x - * - * to them (getting "th1", say). Then we make the definition "f = WFREC R M" - * and instantiate "th1" to the constant "f" (getting th2). Then we use the - * definition to delete the first antecedent to th2. Hence the result in - * the "corollary" field is - * - * |- WF R ==> !x. f x = M (f%R,x) x - * +(*--------------------------------------------------------------------------- + * R is already assumed to be type-copacetic with M *---------------------------------------------------------------------------*) +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 = #Name(S.dest_var f) + val (wfrec,_) = S.strip_comb rhs +in +fun wfrec_definition0 thy R functional = + let val {Bvar,...} = S.dest_abs functional + val {Name, Ty} = S.dest_var Bvar + val def_name = U.concat Name "_def" + val (_,ty_theta) = Thry.match_term thy f (S.mk_var{Name=fname,Ty=Ty}) + val wfrec' = S.inst ty_theta wfrec + val wfrec_R_M' = S.list_mk_comb(wfrec',[R,functional]) + val def_term = S.mk_eq{lhs=Bvar, rhs=wfrec_R_M'} + in + Thry.make_definition thy def_name def_term + end +end; -fun prim_wfrec_definition thy {R, functional} = - let val tych = Thry.typecheck thy - val {Bvar,...} = S.dest_abs functional - val {Name,...} = S.dest_var Bvar (* Intended name of definition *) - val cor1 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY - val cor2 = R.ISPEC (tych R) cor1 - val f_eq_WFREC_R_M = (#ant o S.dest_imp o #Body - o S.dest_forall o concl) cor2 - val {lhs,rhs} = S.dest_eq f_eq_WFREC_R_M - val {Ty, ...} = S.dest_var lhs - val def_term = S.mk_eq{lhs = S.mk_var{Name=Name,Ty=Ty}, rhs=rhs} - val (def_thm,thy1) = Thry.make_definition thy - (U.concat Name "_def") def_term - val (_,[f,_]) = (S.strip_comb o concl) def_thm - val cor3 = R.ISPEC (Thry.typecheck thy1 f) cor2 - in - {theory = thy1, def=def_thm, corollary=R.MP cor3 def_thm} - end; (*--------------------------------------------------------------------------- @@ -422,26 +415,16 @@ val givens = U.mapfilter not_omitted; -(*-------------------------------------------------------------------------- - * This is a wrapper for "prim_wfrec_definition": it builds a functional, - * calls "prim_wfrec_definition", then specializes the result. This gives a - * list of rewrite rules where the right hand sides are quite ugly, so we - * simplify to get rid of the case statements. In essence, this function - * performs pre- and post-processing for patterns. As well, after - * simplification, termination conditions are extracted. - *-------------------------------------------------------------------------*) - -fun gen_wfrec_definition thy {R, eqs} = - let val {functional,pats} = mk_functional thy eqs +fun post_definition (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 given_pats = givens pats - val {def,corollary,theory} = prim_wfrec_definition thy - {R=R, functional=functional} - val tych = Thry.typecheck theory - val {lhs=f,...} = S.dest_eq(concl def) val WFR = #ant(S.dest_imp(concl corollary)) + val R = #Rand(S.dest_comb WFR) val corollary' = R.UNDISCH corollary (* put WF R on assums *) val corollaries = map (U.C R.SPEC corollary' o tych) given_pats - val (case_rewrites,context_congs) = extraction_thms thy + val (case_rewrites,context_congs) = extraction_thms theory val corollaries' = map(R.simplify case_rewrites) corollaries fun xtract th = R.CONTEXT_REWRITE_RULE(f,R) {thms = [(R.ISPECL o map tych)[f,R] Thms.CUT_LEMMA], @@ -459,7 +442,6 @@ patterns = pats} end; - (*--------------------------------------------------------------------------- * Perform the extraction without making the definition. Definition and * extraction commute for the non-nested case. For hol90 users, this @@ -521,7 +503,7 @@ def val body_th = R.LIST_CONJ (map (R.ASSUME o tych) full_rqt) val bar = R.MP (R.BETA_RULE(R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX)) - body_th + body_th in {theory = theory, R=R1, rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def', full_pats_TCs = merge (map pat_of pats) (U.zip (givens pats) TCl), @@ -905,18 +887,4 @@ end; -(*--------------------------------------------------------------------------- - * Extract termination goals so that they can be put it into a goalstack, or - * have a tactic directly applied to them. - *--------------------------------------------------------------------------*) -local exception IS_NEG - fun strip_imp tm = if S.is_neg tm then raise IS_NEG else S.strip_imp tm -in -fun termination_goals rules = - U.itlist (fn th => fn A => - let val tcl = (#1 o S.strip_imp o #2 o S.strip_forall o concl) th - in tcl@A - end handle _ => A) (R.CONJUNCTS rules) (hyp rules) -end; - end; (* TFL *) diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/thms.sml --- a/TFL/thms.sml Thu May 15 11:35:26 1997 +0200 +++ b/TFL/thms.sml Thu May 15 12:29:59 1997 +0200 @@ -2,9 +2,9 @@ struct type Thm = Thm.thm - val WFREC_COROLLARY = get_thm WF1.thy "tfl_wfrec" - val WF_INDUCTION_THM = get_thm WF1.thy "tfl_wf_induct" - val CUT_LEMMA = get_thm WF1.thy "tfl_cut_apply" + val 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 CUT_DEF = cut_def local val _ = goal HOL.thy "!P x. P x --> P (Eps P)" diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/thry.sml --- a/TFL/thry.sml Thu May 15 11:35:26 1997 +0200 +++ b/TFL/thry.sml Thu May 15 12:29:59 1997 +0200 @@ -49,6 +49,14 @@ * refer to previous ones. The name for the new theory is automatically * generated from the name of the argument theory. *---------------------------------------------------------------------------*) + + +(*--------------------------------------------------------------------------- + * TFL attempts to make definitions where the lhs is a variable. Isabelle + * wants it to be a constant, so here we map it to a constant. Moreover, the + * theory should already have the constant, so we refrain from adding the + * constant to the theory. We just add the axiom and return the theory. + *---------------------------------------------------------------------------*) local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection)) val Const(eeq_name, ty) = eeq val prop = #2 (S.strip_type ty) @@ -59,17 +67,14 @@ val lhs1 = S.mk_const{Name = Name, Ty = Ty} val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop} val dtm = S.list_mk_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *) - val thry1 = add_consts_i [(Name,Ty,NoSyn)] parent - val thry2 = add_defs_i [(s,dtm)] thry1 - val parent_names = map ! (stamps_of_thy parent) - val newthy_name = variant parent_names (hd parent_names) - val new_thy = add_thyname newthy_name thry2 + val (_, tm', _) = Sign.infer_types (sign_of parent) + (K None) (K None) [] true ([dtm],propT) + val new_thy = add_defs_i [(s,tm')] parent in - ((get_axiom new_thy s) RS meta_eq_to_obj_eq, new_thy) - end + (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy) + end; end; - (*--------------------------------------------------------------------------- * Utility routine. Insert into list ordered by the key (a string). If two * keys are equal, the new element replaces the old. A more efficient option diff -r 5aa3756a4bf2 -r 14bd6e5985f1 TFL/utils.sml --- a/TFL/utils.sml Thu May 15 11:35:26 1997 +0200 +++ b/TFL/utils.sml Thu May 15 12:29:59 1997 +0200 @@ -19,7 +19,7 @@ val MESG_string = info_string "Message" end; -fun Raise (e as ERR sss) = (prs (ERR_string sss); raise e) +fun Raise (e as ERR sss) = (output(std_out, ERR_string sss); raise e) | Raise e = raise e;