paulson@3302: (* Title: TFL/post paulson@3302: ID: $Id$ paulson@3302: Author: Konrad Slind, Cambridge University Computer Laboratory paulson@3302: Copyright 1997 University of Cambridge paulson@3302: paulson@3302: Postprocessing of TFL definitions paulson@3302: *) paulson@3302: paulson@3191: signature TFL = paulson@3191: sig paulson@2112: structure Prim : TFL_sig paulson@2112: paulson@3191: val tgoalw : theory -> thm list -> thm list -> thm list paulson@3191: val tgoal: theory -> thm list -> thm list paulson@2112: paulson@3405: val std_postprocessor : simpset -> theory paulson@2112: -> {induction:thm, rules:thm, TCs:term list list} paulson@2112: -> {induction:thm, rules:thm, nested_tcs:thm list} paulson@2112: wenzelm@3927: val define_i : theory -> xstring -> term -> term list paulson@3405: -> theory * Prim.pattern list paulson@3331: wenzelm@3927: val define : theory -> xstring -> string -> string list paulson@3331: -> theory * Prim.pattern list paulson@2112: paulson@3459: val simplify_defn : simpset * thm list paulson@3459: -> theory * (string * Prim.pattern list) paulson@3191: -> {rules:thm list, induct:thm, tcs:term list} paulson@2112: paulson@3191: (*------------------------------------------------------------------------- paulson@3191: val function : theory -> term -> {theory:theory, eq_ind : thm} paulson@3191: val lazyR_def: theory -> term -> {theory:theory, eqns : thm} paulson@3191: *-------------------------------------------------------------------------*) paulson@2112: paulson@3191: end; paulson@3191: paulson@3191: paulson@3191: structure Tfl: TFL = paulson@2112: struct paulson@2112: structure Prim = Prim paulson@3391: structure S = USyntax paulson@2112: paulson@3191: (*--------------------------------------------------------------------------- paulson@3191: * Extract termination goals so that they can be put it into a goalstack, or paulson@3191: * have a tactic directly applied to them. paulson@3191: *--------------------------------------------------------------------------*) paulson@3191: fun termination_goals rules = paulson@3405: map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop) paulson@3191: (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, [])); paulson@3191: paulson@3405: (*--------------------------------------------------------------------------- paulson@3405: * Finds the termination conditions in (highly massaged) definition and paulson@3405: * puts them into a goalstack. paulson@3405: *--------------------------------------------------------------------------*) paulson@3405: fun tgoalw thy defs rules = paulson@3497: case termination_goals rules of paulson@3497: [] => error "tgoalw: no termination conditions to prove" paulson@3497: | L => goalw_cterm defs paulson@3497: (cterm_of (sign_of thy) paulson@3497: (HOLogic.mk_Trueprop(USyntax.list_mk_conj L))); paulson@2112: paulson@3405: fun tgoal thy = tgoalw thy []; paulson@2112: paulson@3405: (*--------------------------------------------------------------------------- paulson@3405: * Three postprocessors are applied to the definition. It paulson@3405: * attempts to prove wellfoundedness of the given relation, simplifies the paulson@3405: * non-proved termination conditions, and finally attempts to prove the paulson@3405: * simplified termination conditions. paulson@3405: *--------------------------------------------------------------------------*) paulson@3405: fun std_postprocessor ss = paulson@3405: Prim.postprocess paulson@3405: {WFtac = REPEAT (ares_tac [wf_measure, wf_inv_image, wf_lex_prod, paulson@3405: wf_less_than, wf_trancl] 1), paulson@3405: terminator = asm_simp_tac ss 1 wenzelm@4097: THEN TRY(CLASET' (fn cs => best_tac wenzelm@4097: (cs addSDs [not0_implies_Suc] addss ss)) 1), paulson@3405: simplifier = Rules.simpl_conv ss []}; paulson@2112: paulson@2112: paulson@2112: paulson@3391: val concl = #2 o Rules.dest_thm; paulson@2112: paulson@2112: (*--------------------------------------------------------------------------- paulson@3191: * Defining a function with an associated termination relation. paulson@3191: *---------------------------------------------------------------------------*) paulson@3331: fun define_i thy fid R eqs = paulson@3331: let val dummy = require_thy thy "WF_Rel" "recursive function definitions" paulson@3191: val {functional,pats} = Prim.mk_functional thy eqs paulson@3405: in (Prim.wfrec_definition0 thy fid R functional, pats) paulson@3191: end; paulson@3191: paulson@3191: (*lcp's version: takes strings; doesn't return "thm" paulson@3245: (whose signature is a draft and therefore useless) *) paulson@3331: fun define thy fid R eqs = paulson@3191: let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) paulson@3405: in define_i thy fid (read thy R) (map (read thy) eqs) end paulson@3191: handle Utils.ERR {mesg,...} => error mesg; paulson@3191: paulson@3191: (*--------------------------------------------------------------------------- paulson@3191: * Postprocess a definition made by "define". This is a separate stage of paulson@3191: * processing from the definition stage. paulson@2112: *---------------------------------------------------------------------------*) paulson@2112: local paulson@3391: structure R = Rules paulson@2112: structure U = Utils paulson@2112: paulson@3191: (* The rest of these local definitions are for the tricky nested case *) paulson@2112: val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl paulson@2112: paulson@2112: fun id_thm th = paulson@2112: let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th)))) paulson@3391: in lhs aconv rhs paulson@2112: end handle _ => false paulson@2112: paulson@2112: fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); paulson@2112: val P_imp_P_iff_True = prover "P --> (P= True)" RS mp; paulson@2112: val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; paulson@2112: fun mk_meta_eq r = case concl_of r of paulson@2112: Const("==",_)$_$_ => r paulson@2112: | _$(Const("op =",_)$_$_) => r RS eq_reflection paulson@2112: | _ => r RS P_imp_P_eq_True paulson@3405: paulson@3405: (*Is this the best way to invoke the simplifier??*) paulson@3245: fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L)) paulson@2112: paulson@2112: fun join_assums th = paulson@2112: let val {sign,...} = rep_thm th paulson@2112: val tych = cterm_of sign paulson@2112: val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) paulson@2112: val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) paulson@2112: val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) paulson@3245: val cntxt = gen_union (op aconv) (cntxtl, cntxtr) paulson@2112: in paulson@3191: R.GEN_ALL paulson@3191: (R.DISCH_ALL paulson@3191: (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) paulson@2112: end paulson@2112: val gen_all = S.gen_all paulson@2112: in paulson@3405: fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} = paulson@3271: let val dummy = prs "Proving induction theorem.. " paulson@3191: val ind = Prim.mk_induction theory f R full_pats_TCs paulson@3405: val dummy = prs "Proved induction theorem.\nPostprocessing.. " paulson@3405: val {rules, induction, nested_tcs} = paulson@3405: std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs} paulson@3191: in paulson@3191: case nested_tcs paulson@3271: of [] => (writeln "Postprocessing done."; paulson@3191: {induction=induction, rules=rules,tcs=[]}) paulson@3271: | L => let val dummy = prs "Simplifying nested TCs.. " paulson@2112: val (solved,simplified,stubborn) = paulson@2112: U.itlist (fn th => fn (So,Si,St) => paulson@2112: if (id_thm th) then (So, Si, th::St) else paulson@2112: if (solved th) then (th::So, Si, St) paulson@2112: else (So, th::Si, St)) nested_tcs ([],[],[]) paulson@2112: val simplified' = map join_assums simplified nipkow@3572: val rewr = full_simplify (ss addsimps (solved @ simplified')); paulson@3405: val induction' = rewr induction paulson@3405: and rules' = rewr rules paulson@3271: val dummy = writeln "Postprocessing done." paulson@2112: in paulson@2112: {induction = induction', paulson@2112: rules = rules', paulson@3191: tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) paulson@3191: (simplified@stubborn)} paulson@2112: end paulson@3391: end; paulson@3191: paulson@3191: paulson@3302: (*lcp: curry the predicate of the induction rule*) paulson@3302: fun curry_rule rl = Prod_Syntax.split_rule_var paulson@3271: (head_of (HOLogic.dest_Trueprop (concl_of rl)), paulson@3271: rl); paulson@3271: paulson@3191: (*lcp: put a theorem into Isabelle form, using meta-level connectives*) paulson@3191: val meta_outer = paulson@3302: curry_rule o standard o paulson@3271: rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI] paulson@3271: ORELSE' etac conjE)); paulson@3191: paulson@3191: (*Strip off the outer !P*) paulson@3191: val spec'= read_instantiate [("x","P::?'b=>bool")] spec; paulson@2112: paulson@3405: val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def]; paulson@2112: paulson@3459: (*Convert conclusion from = to ==*) paulson@3459: val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th); paulson@3459: paulson@3459: (*--------------------------------------------------------------------------- paulson@3459: * Install the basic context notions. Others (for nat and list and prod) paulson@3459: * have already been added in thry.sml paulson@3459: *---------------------------------------------------------------------------*) paulson@3459: val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong]; paulson@3459: paulson@3459: fun simplify_defn (ss, tflCongs) (thy,(id,pats)) = wenzelm@3978: let val dummy = deny (id mem (Sign.stamp_names_of (sign_of thy))) paulson@3208: ("Recursive definition " ^ id ^ paulson@3245: " would clash with the theory of the same name!") paulson@3405: val def = freezeT(get_def thy id) RS meta_eq_to_obj_eq paulson@3405: val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs) paulson@3191: val {theory,rules,TCs,full_pats_TCs,patterns} = paulson@3459: Prim.post_definition paulson@3459: (ss', defaultTflCongs @ eq_reflect_list tflCongs) paulson@3459: (thy, (def,pats)) paulson@3191: val {lhs=f,rhs} = S.dest_eq(concl def) paulson@3191: val (_,[R,_]) = S.strip_comb rhs paulson@3191: val {induction, rules, tcs} = paulson@3405: proof_stage ss' theory paulson@3245: {f = f, R = R, rules = rules, paulson@3245: full_pats_TCs = full_pats_TCs, paulson@3245: TCs = TCs} paulson@3191: val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules) paulson@3191: in {induct = meta_outer paulson@3245: (normalize_thm [RSspec,RSmp] (induction RS spec')), paulson@3245: rules = rules', paulson@3245: tcs = (termination_goals rules') @ tcs} paulson@3191: end paulson@3391: handle Utils.ERR {mesg,func,module} => paulson@3391: error (mesg ^ paulson@3405: "\n (In TFL function " ^ module ^ "." ^ func ^ ")"); paulson@2112: end; paulson@2112: paulson@3191: (*--------------------------------------------------------------------------- paulson@3191: * paulson@3191: * Definitions with synthesized termination relation temporarily paulson@3191: * deleted -- it's not clear how to integrate this facility with paulson@3191: * the Isabelle theory file scheme, which restricts paulson@3191: * inference at theory-construction time. paulson@3191: * paulson@2112: paulson@3391: local structure R = Rules paulson@2112: in paulson@2112: fun function theory eqs = paulson@3208: let val dummy = prs "Making definition.. " paulson@2112: val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs paulson@2112: val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) paulson@3208: val dummy = prs "Definition made.\n" paulson@3208: val dummy = prs "Proving induction theorem.. " paulson@2112: val induction = Prim.mk_induction theory f R full_pats_TCs paulson@3208: val dummy = prs "Induction theorem proved.\n" paulson@2112: in {theory = theory, paulson@2112: eq_ind = standard (induction RS (rules RS conjI))} paulson@2112: end paulson@2112: end; paulson@2112: paulson@2112: paulson@2112: fun lazyR_def theory eqs = paulson@2112: let val {rules,theory, ...} = Prim.lazyR_def theory eqs paulson@2112: in {eqns=rules, theory=theory} paulson@2112: end paulson@3391: handle e => print_exn e; paulson@3191: * paulson@3191: * paulson@3191: *---------------------------------------------------------------------------*) paulson@2112: end;