removed True_implies (cf. True_implies_equals);
(* Title: HOL/Tools/function_package/fundef_prep.ML
ID: $Id$
Author: Alexander Krauss, TU Muenchen
A package for general recursive function definitions.
Preparation step: makes auxiliary definitions and generates
proof obligations.
*)
signature FUNDEF_PREP =
sig
val prepare_fundef : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list
-> FundefCommon.prep_result * theory
end
structure FundefPrep (*: FUNDEF_PREP*) =
struct
open FundefCommon
open FundefAbbrev
(* Theory dependencies. *)
val Pair_inject = thm "Product_Type.Pair_inject";
val acc_induct_rule = thm "Accessible_Part.acc_induct_rule"
val ex1_implies_ex = thm "FunDef.fundef_ex1_existence"
val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness"
val ex1_implies_iff = thm "FunDef.fundef_ex1_iff"
val conjunctionI = thm "conjunctionI";
fun split_list3 [] = ([],[],[])
| split_list3 ((x,y,z)::xyzs) =
let
val (xs, ys, zs) = split_list3 xyzs
in
(x::xs,y::ys,z::zs)
end
fun build_tree thy f congs ctx (qs, gs, lhs, rhs) =
let
(* FIXME: Save precomputed dependencies in a theory data slot *)
val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
val (_(*FIXME*), ctx') = ProofContext.add_fixes_i (map (fn Free (n, T) => (n, SOME T, NoSyn)) qs) ctx
in
FundefCtxTree.mk_tree thy congs_deps f ctx' rhs
end
fun find_calls tree =
let
fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
| add_Ri _ _ _ _ = raise Match
in
rev (FundefCtxTree.traverse_tree add_Ri tree [])
end
(* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
fun mk_primed_vars thy glrs =
let
val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
fun rename_vars (qs,gs,lhs,rhs) =
let
val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs
val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
in
(qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
end
in
map rename_vars glrs
end
(* Chooses fresh free names, declares G and R, defines f and returns a record
with all the information *)
fun setup_context f glrs defname thy =
let
val Const (f_fullname, fT) = f
val fname = Sign.base_name f_fullname
val domT = domain_type fT
val ranT = range_type fT
val GT = mk_relT (domT, ranT)
val RT = mk_relT (domT, domT)
val G_name = defname ^ "_graph"
val R_name = defname ^ "_rel"
val gfixes = [("h_fd", domT --> ranT),
("y_fd", ranT),
("x_fd", domT),
("z_fd", domT),
("a_fd", domT),
("D_fd", HOLogic.mk_setT domT),
("P_fd", domT --> boolT),
("Pb_fd", boolT),
("f_fd", fT)]
val (fxnames, ctx) = (ProofContext.init thy)
|> ProofContext.add_fixes_i (map (fn (n,T) => (n, SOME T, NoSyn)) gfixes)
val [h, y, x, z, a, D, P, Pbool, fvar] = map (fn (n,(_,T)) => Free (n, T)) (fxnames ~~ gfixes)
val Free (fvarname, _) = fvar
val glrs' = mk_primed_vars thy glrs
val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
val G = Const (Sign.full_name thy G_name, GT)
val R = Const (Sign.full_name thy R_name, RT)
val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
val f_eq = Logic.mk_equals (f $ x,
Const ("The", (ranT --> boolT) --> ranT) $
Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
in
(Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, ctx=ctx}, thy)
end
(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
(implies $ Trueprop (mk_eq (lhs, lhs'))
$ Trueprop (mk_eq (rhs, rhs')))
|> fold_rev (curry Logic.mk_implies) (gs @ gs')
|> fold_rev mk_forall (qs @ qs')
(* all proof obligations *)
fun mk_compat_proof_obligations glrs glrs' =
map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (unordered_pairs (glrs ~~ glrs'))
fun mk_completeness names glrs =
let
val Names {domT, x, Pbool, ...} = names
fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
|> fold_rev (curry Logic.mk_implies) gs
|> fold_rev mk_forall qs
in
Trueprop Pbool
|> fold_rev (curry Logic.mk_implies o mk_case) glrs
|> mk_forall_rename (x, "x")
|> mk_forall_rename (Pbool, "P")
end
fun inductive_def_wrap defs (thy, const) =
let
val qdefs = map dest_all_all defs
val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) =
InductivePackage.add_inductive_i true (*verbose*)
false (*add_consts*)
"" (* no altname *)
false (* no coind *)
false (* elims, please *)
false (* induction thm please *)
[const] (* the constant *)
(map (fn (_,t) => (("", t),[])) qdefs) (* the intros *)
[] (* no special monos *)
thy
(* It would be nice if this worked... But this is actually HO-Unification... *)
(* fun inst (qs, intr) intr_gen =
Goal.init (cterm_of thy intr)
|> curry op COMP intr_gen
|> Goal.finish
|> fold_rev (forall_intr o cterm_of thy) qs*)
fun inst (qs, intr) intr_gen =
intr_gen
|> Thm.freezeT
|> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs
val intrs = map2 inst qdefs intrs_gen
val elim = elim_gen
|> Thm.freezeT
|> forall_intr_vars (* FIXME *)
in
(intrs, (thy, const, elim))
end
(*
* "!!qs xs. CS ==> G => (r, lhs) : R"
*)
fun mk_RIntro R (qs, gs, lhs, rhs) (rcfix, rcassm, rcarg) =
mk_relmem (rcarg, lhs) R
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|> fold_rev (curry Logic.mk_implies) gs
|> fold_rev (mk_forall o Free) rcfix
|> fold_rev mk_forall qs
fun mk_GIntro thy f_const f_var G (qs, gs, lhs, rhs) RCs =
let
fun mk_h_assm (rcfix, rcassm, rcarg) =
mk_relmem (rcarg, f_var $ rcarg) G
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|> fold_rev (mk_forall o Free) rcfix
in
mk_relmem (lhs, rhs) G
|> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
|> fold_rev (curry Logic.mk_implies) gs
|> Pattern.rewrite_term thy [(f_const, f_var)] []
|> fold_rev mk_forall (f_var :: qs)
end
fun mk_clause_info thy names no (qs,gs,lhs,rhs) tree RCs GIntro_thm RIntro_thms =
let
val Names {G, h, f, fvar, x, ...} = names
val cqs = map (cterm_of thy) qs
val ags = map (assume o cterm_of thy) gs
val used = [] (* XXX *)
(* FIXME: What is the relationship between this and mk_primed_vars? *)
val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs
val cqs' = map (cterm_of thy) qs'
val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
val ags' = map (assume o cterm_of thy o rename_vars) gs
val lhs' = rename_vars lhs
val rhs' = rename_vars rhs
val lGI = GIntro_thm
|> forall_elim (cterm_of thy f)
|> fold forall_elim cqs
|> fold implies_elim_swp ags
(* FIXME: Can be removed when inductive-package behaves nicely. *)
val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [])
(term_frees (snd (dest_all_all (prop_of GIntro_thm))))
fun mk_call_info (rcfix, rcassm, rcarg) RI =
let
val crcfix = map (cterm_of thy o Free) rcfix
val llRI = RI
|> fold forall_elim cqs
|> fold forall_elim crcfix
|> fold implies_elim_swp ags
|> fold implies_elim_swp rcassm
val h_assum =
mk_relmem (rcarg, h $ rcarg) G
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|> fold_rev (mk_forall o Free) rcfix
|> Pattern.rewrite_term thy [(f, h)] []
val Gh = assume (cterm_of thy h_assum)
val Gh' = assume (cterm_of thy (rename_vars h_assum))
in
RCInfo {RIvs=rcfix, Gh=Gh, Gh'=Gh', rcarg=rcarg, CCas=rcassm, llRI=llRI}
end
val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
val RC_infos = map2 mk_call_info RCs RIntro_thms
in
ClauseInfo
{
no=no,
qs=qs, gs=gs, lhs=lhs, rhs=rhs,
cqs=cqs, ags=ags,
cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs',
lGI=lGI, RCs=RC_infos,
tree=tree, case_hyp = case_hyp,
ordcqs'=ordcqs'
}
end
(* Copied from fundef_proof.ML: *)
(***********************************************)
(* Compat thms are stored in normal form (with vars) *)
(* replace this by a table later*)
fun store_compat_thms 0 thms = []
| store_compat_thms n thms =
let
val (thms1, thms2) = chop n thms
in
(thms1 :: store_compat_thms (n - 1) thms2)
end
(* needs i <= j *)
fun lookup_compat_thm i j cts =
nth (nth cts (i - 1)) (j - i)
(***********************************************)
(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
(* if j < i, then turn around *)
fun get_compat_thm thy cts clausei clausej =
let
val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
in if j < i then
let
val compat = lookup_compat_thm j i cts
in
compat (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
|> fold forall_elim (qsj' @ qsi) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *)
|> fold implies_elim_swp gsj'
|> fold implies_elim_swp gsi
|> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
end
else
let
val compat = lookup_compat_thm i j cts
in
compat (* "!!qi qj'. Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
|> fold forall_elim (qsi @ qsj') (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
|> fold implies_elim_swp gsi
|> fold implies_elim_swp gsj'
|> implies_elim_swp (assume lhsi_eq_lhsj')
|> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
end
end
(* Generates the replacement lemma with primed variables. A problem here is that one should not do
the complete requantification at the end to replace the variables. One should find a way to be more efficient
here. *)
fun mk_replacement_lemma thy (names:naming_context) ih_elim clause =
let
val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names
val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
val replace_lemma = (eql RS meta_eq_to_obj_eq)
|> implies_intr (cprop_of case_hyp)
|> fold_rev (implies_intr o cprop_of) h_assums
|> fold_rev (implies_intr o cprop_of) ags
|> fold_rev forall_intr cqs
|> fold forall_elim cqs'
|> fold implies_elim_swp ags'
|> fold implies_elim_swp h_assums'
in
replace_lemma
end
fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
let
val Names {f, h, y, ...} = names
val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
val compat = get_compat_thm thy compat_store clausei clausej
val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
in
(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
|> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
|> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
|> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
|> implies_intr (cprop_of y_eq_rhsj'h)
|> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
|> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
|> implies_elim_swp eq_pairs
|> fold_rev (implies_intr o cprop_of) Ghsj'
|> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
|> implies_intr (cprop_of eq_pairs)
|> fold_rev forall_intr ordcqs'j
end
fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
let
val Names {x, y, G, fvar, f, ranT, ...} = names
val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
|> fold_rev (implies_intr o cprop_of) CCas
|> fold_rev (forall_intr o cterm_of thy o Free) RIvs
val existence = lGI (*|> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])*)
|> fold (curry op COMP o prep_RC) RCs
val a = cterm_of thy (mk_prod (lhs, y))
val P = cterm_of thy (mk_eq (y, rhs))
val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
val uniqueness = G_cases
|> forall_elim a
|> forall_elim P
|> implies_elim_swp a_in_G
|> fold implies_elim_swp unique_clauses
|> implies_intr (cprop_of a_in_G)
|> forall_intr (cterm_of thy y)
val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
val exactly_one =
ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
|> curry (op COMP) existence
|> curry (op COMP) uniqueness
|> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
|> implies_intr (cprop_of case_hyp)
|> fold_rev (implies_intr o cprop_of) ags
|> fold_rev forall_intr cqs
val function_value =
existence
|> fold_rev (implies_intr o cprop_of) ags
|> implies_intr ihyp
|> implies_intr (cprop_of case_hyp)
|> forall_intr (cterm_of thy x)
|> forall_elim (cterm_of thy lhs)
|> curry (op RS) refl
in
(exactly_one, function_value)
end
fun prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim =
let
val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, Pbool, ...}:naming_context = names
val f_def_fr = Thm.freezeT f_def
val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)]
[SOME (cterm_of thy f), SOME (cterm_of thy G)])
#> curry op COMP (forall_intr_vars f_def_fr)
val inst_ex1_ex = instantiate_and_def ex1_implies_ex
val inst_ex1_un = instantiate_and_def ex1_implies_un
val inst_ex1_iff = instantiate_and_def ex1_implies_iff
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
val ihyp = all domT $ Abs ("z", domT,
implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
$ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
|> cterm_of thy
val ihyp_thm = assume ihyp |> forall_elim_vars 0
val ih_intro = ihyp_thm RS inst_ex1_ex
val ih_elim = ihyp_thm RS inst_ex1_un
val _ = Output.debug "Proving Replacement lemmas..."
val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
val _ = Output.debug "Proving cases for unique existence..."
val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *)
val graph_is_function = complete
|> forall_elim_vars 0
|> fold (curry op COMP) ex1s
|> implies_intr (ihyp)
|> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
|> forall_intr (cterm_of thy x)
|> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
|> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
|> Drule.close_derivation
val goal = complete COMP (graph_is_function COMP conjunctionI)
|> Drule.close_derivation
val goalI = Goal.protect goal
|> fold_rev (implies_intr o cprop_of) compat
|> implies_intr (cprop_of complete)
in
(prop_of goal, goalI, inst_ex1_iff, values)
end
(*
* This is the first step in a function definition.
*
* Defines the function, the graph and the termination relation, synthesizes completeness
* and comatibility conditions and returns everything.
*)
fun prepare_fundef thy congs defname f qglrs used =
let
val (names, thy) = setup_context f qglrs defname thy
val Names {G, R, ctx, glrs', fvar, ...} = names
val n = length qglrs
val trees = map (build_tree thy f congs ctx) qglrs
val RCss = map find_calls trees
val complete = mk_completeness names qglrs
|> cterm_of thy
|> assume
val compat = mk_compat_proof_obligations qglrs glrs'
|> map (assume o cterm_of thy)
val compat_store = compat
|> store_compat_thms n
val R_intross = map2 (fn qglr => map (mk_RIntro R qglr)) qglrs RCss
val G_intros = map2 (mk_GIntro thy f fvar G) qglrs RCss
val (GIntro_thms, (thy, _, G_elim)) = inductive_def_wrap G_intros (thy, G)
val (RIntro_thmss, (thy, _, R_elim)) = fold_burrow inductive_def_wrap R_intross (thy, R)
val clauses = map6 (mk_clause_info thy names) (1 upto n) qglrs trees RCss GIntro_thms RIntro_thmss
val (goal, goalI, ex1_iff, values) = prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim
in
(Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim},
thy)
end
end