(* Title: HOL/Tools/function_package/fundef_proof.ML
ID: $Id$
Author: Alexander Krauss, TU Muenchen
A package for general recursive function definitions.
Internal proofs.
*)
signature FUNDEF_PROOF =
sig
val mk_partial_rules : theory -> FundefCommon.prep_result
-> thm -> FundefCommon.fundef_result
end
structure FundefProof : FUNDEF_PROOF =
struct
open FundefLib
open FundefCommon
open FundefAbbrev
(* Theory dependencies *)
val subsetD = thm "subsetD"
val split_apply = thm "Product_Type.split"
val wf_induct_rule = thm "FunDef.wfP_induct_rule";
val Pair_inject = thm "Product_Type.Pair_inject";
val wf_in_rel = thm "FunDef.wf_in_rel";
val in_rel_def = thm "FunDef.in_rel_def";
val acc_induct_rule = thm "FunDef.accP_induct_rule"
val acc_downward = thm "FunDef.accP_downward"
val accI = thm "FunDef.accPI"
val acc_subset_induct = thm "FunDef.accP_subset_induct"
val conjunctionD1 = thm "conjunctionD1"
val conjunctionD2 = thm "conjunctionD2"
fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
let
val Globals {domT, z, ...} = globals
val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
in
((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
|> (fn it => it COMP graph_is_function)
|> implies_intr z_smaller
|> forall_intr (cterm_of thy z)
|> (fn it => it COMP valthm)
|> implies_intr lhs_acc
|> asm_simplify (HOL_basic_ss addsimps [f_iff])
|> fold_rev (implies_intr o cprop_of) ags
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
fun mk_partial_induct_rule thy globals R complete_thm clauses =
let
val Globals {domT, x, z, a, P, D, ...} = globals
val acc_R = mk_acc domT R
val x_D = assume (cterm_of thy (Trueprop (D $ x)))
val a_D = cterm_of thy (Trueprop (D $ a))
val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
mk_forall x
(mk_forall z (Logic.mk_implies (Trueprop (D $ x),
Logic.mk_implies (Trueprop (R $ z $ x),
Trueprop (D $ z)))))
|> cterm_of thy
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
val ihyp = all domT $ Abs ("z", domT,
implies $ Trueprop (R $ Bound 0 $ x)
$ Trueprop (P $ Bound 0))
|> cterm_of thy
val aihyp = assume ihyp
fun prove_case clause =
let
val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs,
qglr = (oqs, _, _, _), ...} = clause
val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
val sih = full_simplify replace_x_ss aihyp
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
sih |> forall_elim (cterm_of thy rcarg)
|> implies_elim_swp llRI
|> fold_rev (implies_intr o cprop_of) CCas
|> fold_rev (forall_intr o cterm_of thy o Free) RIvs
val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
val step = Trueprop (P $ lhs)
|> fold_rev (curry Logic.mk_implies o prop_of) P_recs
|> fold_rev (curry Logic.mk_implies) gs
|> curry Logic.mk_implies (Trueprop (D $ lhs))
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|> cterm_of thy
val P_lhs = assume step
|> fold forall_elim cqs
|> implies_elim_swp lhs_D
|> fold_rev implies_elim_swp ags
|> fold implies_elim_swp P_recs
val res = cterm_of thy (Trueprop (P $ x))
|> Simplifier.rewrite replace_x_ss
|> symmetric (* P lhs == P x *)
|> (fn eql => equal_elim eql P_lhs) (* "P x" *)
|> implies_intr (cprop_of case_hyp)
|> fold_rev (implies_intr o cprop_of) ags
|> fold_rev forall_intr cqs
in
(res, step)
end
val (cases, steps) = split_list (map prove_case clauses)
val istep = complete_thm
|> forall_elim_vars 0
|> fold (curry op COMP) cases (* P x *)
|> implies_intr ihyp
|> implies_intr (cprop_of x_D)
|> forall_intr (cterm_of thy x)
val subset_induct_rule =
acc_subset_induct
|> (curry op COMP) (assume D_subset)
|> (curry op COMP) (assume D_dcl)
|> (curry op COMP) (assume a_D)
|> (curry op COMP) istep
|> fold_rev implies_intr steps
|> implies_intr a_D
|> implies_intr D_dcl
|> implies_intr D_subset
val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
val simple_induct_rule =
subset_induct_rule
|> forall_intr (cterm_of thy D)
|> forall_elim (cterm_of thy acc_R)
|> assume_tac 1 |> Seq.hd
|> (curry op COMP) (acc_downward
|> (instantiate' [SOME (ctyp_of thy domT)]
(map (SOME o cterm_of thy) [R, x, z]))
|> forall_intr (cterm_of thy z)
|> forall_intr (cterm_of thy x))
|> forall_intr (cterm_of thy a)
|> forall_intr (cterm_of thy P)
in
(subset_induct_all, simple_induct_rule)
end
(* Does this work with Guards??? *)
fun mk_domain_intro thy globals R R_cases clause =
let
val Globals {z, domT, ...} = globals
val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
qglr = (oqs, _, _, _), ...} = clause
val goal = Trueprop (mk_acc domT R $ lhs)
|> fold_rev (curry Logic.mk_implies) gs
|> cterm_of thy
in
Goal.init goal
|> (SINGLE (resolve_tac [accI] 1)) |> the
|> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1)) |> the
|> (SINGLE (CLASIMPSET auto_tac)) |> the
|> Goal.conclude
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
fun maybe_mk_domain_intro thy =
if !FundefCommon.domintros then mk_domain_intro thy
else K (K (K (K refl)))
fun mk_nest_term_case thy globals R' ihyp clause =
let
val Globals {x, z, ...} = globals
val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
qglr=(oqs, _, _, _), ...} = clause
val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
let
val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
val hyp = Trueprop (R' $ arg $ lhs)
|> fold_rev (curry Logic.mk_implies o prop_of) used
|> FundefCtxTree.export_term (fixes, map prop_of assumes)
|> fold_rev (curry Logic.mk_implies o prop_of) ags
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|> cterm_of thy
val thm = assume hyp
|> fold forall_elim cqs
|> fold implies_elim_swp ags
|> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *)
|> fold implies_elim_swp used
val acc = thm COMP ih_case
val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
val arg_eq_z = (assume z_eq_arg) RS sym
val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
|> implies_intr (cprop_of case_hyp)
|> implies_intr z_eq_arg
val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
|> FundefCtxTree.export_thm thy (fixes,
prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
val sub' = sub @ [(([],[]), acc)]
in
(sub', (hyp :: hyps, ethm :: thms))
end
| step _ _ _ _ = raise Match
in
FundefCtxTree.traverse_tree step tree
end
fun mk_nest_term_rule thy globals R R_cases clauses =
let
val Globals { domT, x, z, ... } = globals
val acc_R = mk_acc domT R
val R' = Free ("R", fastype_of R)
val Rrel = Free ("R", mk_relT (domT, domT))
val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
val ihyp = all domT $ Abs ("z", domT,
implies $ Trueprop (R' $ Bound 0 $ x)
$ Trueprop (acc_R $ Bound 0))
|> cterm_of thy
val ihyp_a = assume ihyp |> forall_elim_vars 0
val R_z_x = cterm_of thy (Trueprop (R $ z $ x))
val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
in
R_cases
|> forall_elim (cterm_of thy z)
|> forall_elim (cterm_of thy x)
|> forall_elim (cterm_of thy (acc_R $ z))
|> curry op COMP (assume R_z_x)
|> fold_rev (curry op COMP) cases
|> implies_intr R_z_x
|> forall_intr (cterm_of thy z)
|> (fn it => it COMP accI)
|> implies_intr ihyp
|> forall_intr (cterm_of thy x)
|> (fn it => Drule.compose_single(it,2,wf_induct_rule))
|> curry op RS (assume wfR')
|> fold implies_intr hyps
|> implies_intr wfR'
|> forall_intr (cterm_of thy R')
|> forall_elim (cterm_of thy (inrel_R))
|> curry op RS wf_in_rel
|> full_simplify (HOL_basic_ss addsimps [in_rel_def])
|> forall_intr (cterm_of thy Rrel)
end
fun mk_partial_rules thy data provedgoal =
let
val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
val provedgoal = PROFILE "Closing Derivation" Drule.close_derivation provedgoal
val graph_is_function = PROFILE "Getting function theorem" (fn x => (x COMP conjunctionD1) |> forall_elim_vars 0) provedgoal
val complete_thm = PROFILE "Getting cases" (curry op COMP provedgoal) conjunctionD2
val f_iff = PROFILE "Making f_iff" (curry op RS graph_is_function) ex1_iff
val psimps = PROFILE "Proving simplification rules" (map2 (mk_psimp thy globals R f_iff graph_is_function)) clauses values
val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule"
(mk_partial_induct_rule thy globals R complete_thm) clauses
val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule thy globals R R_cases) clauses
val dom_intros = PROFILE "Proving domain introduction rules" (map (maybe_mk_domain_intro thy globals R R_cases)) clauses
in
FundefResult {f=f, G=G, R=R, completeness=complete_thm,
psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
dom_intros=dom_intros}
end
end