--- a/src/HOL/Tools/function_package/fundef_prep.ML Mon Jun 19 18:02:49 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Mon Jun 19 18:25:34 2006 +0200
@@ -18,13 +18,23 @@
-structure FundefPrep : FUNDEF_PREP =
+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";
@@ -37,15 +47,27 @@
end
-fun build_tree thy f congs (qs, gs, lhs, rhs) =
+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 rhs
+ 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
@@ -63,104 +85,39 @@
end
-fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs =
- let
- val Names {domT, G, R, h, f, fvar, used, x, ...} = names
-
- val zv = Var (("z",0), domT) (* for generating h_assums *)
- val xv = Var (("x",0), domT)
- val rw_RI_to_h_assum = (mk_mem (mk_prod (zv, xv), R),
- mk_mem (mk_prod (zv, h $ zv), G))
- val rw_f_to_h = (f, h)
-
- val cqs = map (cterm_of thy) qs
-
- val vqs = map free_to_var qs
- val cvqs = map (cterm_of thy) vqs
-
- val ags = map (assume o cterm_of thy) gs
-
- val qs' = map (fn Free (v,T) => Free (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 localize = instantiate ([], cvqs ~~ cqs)
- #> fold implies_elim_swp ags
-
- val GI = Thm.freezeT GI
- val lGI = localize GI
-
- val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI))
-
- fun mk_call_info (RIvs, RI) =
- let
- fun mk_var0 (v,T) = Var ((v,0),T)
-
- val RI = Thm.freezeT RI
- val lRI = localize RI
- val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
- val plRI = prop_of lRI
- val GmAs = Logic.strip_imp_prems plRI
- val rcarg = case Logic.strip_imp_concl plRI of
- trueprop $ (memb $ (pair $ rcarg $ _) $ R) => rcarg
- | _ => raise Match
-
- val Gh_term = Pattern.rewrite_term thy [rw_RI_to_h_assum, rw_f_to_h] [] (prop_of lRIq)
- val Gh = assume (cterm_of thy Gh_term)
- val Gh' = assume (cterm_of thy (rename_vars Gh_term))
- in
- RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh', GmAs=GmAs, rcarg=rcarg}
- end
-
- val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
- in
- ClauseInfo
- {
- no=no,
- qs=qs, gs=gs, lhs=lhs, rhs=rhs,
- cqs=cqs, cvqs=cvqs, ags=ags,
- cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
- GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
- tree=tree, case_hyp = case_hyp
- }
- end
-
-
-
(* Chooses fresh free names, declares G and R, defines f and returns a record
with all the information *)
-fun setup_context (f, glrs, used) defname congs thy =
+fun setup_context f glrs defname thy =
let
- val trees = map (build_tree thy f congs) glrs
- val allused = fold FundefCtxTree.add_context_varnames trees used
-
val Const (f_fullname, fT) = f
val fname = Sign.base_name f_fullname
val domT = domain_type fT
val ranT = range_type fT
- val h = Free (variant allused "h", domT --> ranT)
- val y = Free (variant allused "y", ranT)
- val x = Free (variant allused "x", domT)
- val z = Free (variant allused "z", domT)
- val a = Free (variant allused "a", domT)
- val D = Free (variant allused "D", HOLogic.mk_setT domT)
- val P = Free (variant allused "P", domT --> boolT)
- val Pbool = Free (variant allused "P", boolT)
- val fvarname = variant allused "f"
- val fvar = Free (fvarname, domT --> ranT)
-
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
@@ -175,53 +132,24 @@
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, used=allused, trees=trees}, thy)
+ (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
-(* Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
+
+
+
+(* !!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')) (upairs (glrs ~~ glrs'))
-
-
-fun extract_Ris thy congs f R tree (qs, gs, lhs, rhs) =
- let
- fun add_Ri2 (fixes,assumes) (_ $ arg) _ (_, x) = ([], (FundefCtxTree.export_term (fixes, map prop_of assumes) (mk_relmem (arg, lhs) R)) :: x)
- | add_Ri2 _ _ _ _ = raise Match
-
- val preRis = rev (FundefCtxTree.traverse_tree add_Ri2 tree [])
- val (vRis, preRis_unq) = split_list (map dest_all_all preRis)
-
- val Ris = map (fold_rev (curry Logic.mk_implies) gs) preRis_unq
- in
- (map (map dest_Free) vRis, preRis, Ris)
- end
+ map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (unordered_pairs (glrs ~~ glrs'))
-fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
- let
- val Names { domT, R, G, f, fvar, h, y, Pbool, ... } = names
-
- val z = Var (("z",0), domT)
- val x = Var (("x",0), domT)
-
- val rew1 = (mk_mem (mk_prod (z, x), R),
- mk_mem (mk_prod (z, fvar $ z), G))
- val rew2 = (f, fvar)
-
- val prems = map (Pattern.rewrite_term thy [rew1, rew2] []) Ris
- val rhs' = Pattern.rewrite_term thy [rew2] [] rhs
- in
- mk_relmem (lhs, rhs') G
- |> fold_rev (curry Logic.mk_implies) prems
- |> fold_rev (curry Logic.mk_implies) gs
- end
fun mk_completeness names glrs =
let
@@ -234,61 +162,411 @@
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 extract_conditions thy names trees congs =
- let
- val Names {f, R, glrs, glrs', ...} = names
+fun inductive_def_wrap defs (thy, const) =
+ let
+ val qdefs = map dest_all_all defs
- val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
- val Gis = map2 (mk_GIntro thy names) glrs preRiss
- val complete = mk_completeness names glrs
- val compat = mk_compat_proof_obligations glrs glrs'
- in
- {G_intros = Gis, vRiss = vRiss, R_intross = Riss, complete = complete, compat = compat}
- end
-
-
-fun inductive_def defs (thy, const) =
- let
- val (thy, {intrs, elims = [elim], ...}) =
- InductivePackage.add_inductive_i true (*verbose*)
+ 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),[])) defs) (* the intros *)
+ (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, elim))
+ (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 (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 glrs used =
+fun prepare_fundef thy congs defname f qglrs used =
let
- val (names, thy) = setup_context (f, glrs, used) defname congs thy
- val Names {G, R, glrs, trees, ...} = names
+ val (names, thy) = setup_context f qglrs defname thy
+ val Names {G, R, ctx, glrs', fvar, ...} = names
- val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
+
+ 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 (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G)
- val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R)
+ val compat = mk_compat_proof_obligations qglrs glrs'
+ |> map (assume o cterm_of thy)
+
+ val compat_store = compat
+ |> store_compat_thms n
- val n = length glrs
- val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
+ 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, complete=complete, compat=compat, clauses = clauses},
+ (Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim},
thy)
end
--- a/src/HOL/Tools/function_package/fundef_proof.ML Mon Jun 19 18:02:49 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_proof.ML Mon Jun 19 18:25:34 2006 +0200
@@ -10,8 +10,8 @@
signature FUNDEF_PROOF =
sig
- val mk_partial_rules : theory -> thm list -> FundefCommon.prep_result
- -> thm -> thm list -> FundefCommon.fundef_result
+ val mk_partial_rules : theory -> FundefCommon.prep_result
+ -> thm -> FundefCommon.fundef_result
end
@@ -37,8 +37,8 @@
val ex1_implies_iff = thm "fundef_ex1_iff"
val acc_subset_induct = thm "acc_subset_induct"
-
-
+val conjunctionD1 = thm "conjunctionD1"
+val conjunctionD2 = thm "conjunctionD2"
@@ -56,10 +56,6 @@
|> (fn it => it COMP valthm)
|> implies_intr lhs_acc
|> asm_simplify (HOL_basic_ss addsimps [f_iff])
-(* |> fold forall_intr cqs
- |> forall_elim_vars 0
- |> varifyT
- |> Drule.close_derivation*)
end
@@ -88,7 +84,7 @@
$ Trueprop (P $ Bound 0))
|> cterm_of thy
- val aihyp = assume ihyp |> forall_elim_vars 0
+ val aihyp = assume ihyp
fun prove_case clause =
let
@@ -98,8 +94,13 @@
val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
val sih = full_simplify replace_x_ss aihyp
- (* FIXME: Variable order destroyed by forall_intr_vars *)
- val P_recs = map (fn RCInfo {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs (* [P rec1, P rec2, ... ] *)
+ 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
@@ -128,6 +129,7 @@
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)
@@ -164,8 +166,6 @@
-
-
(***********************************************)
(* Compat thms are stored in normal form (with vars) *)
@@ -187,7 +187,7 @@
(* recover the order of Vars *)
fun get_var_order thy clauses =
- map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
+ map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (unordered_pairs clauses)
(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
@@ -225,6 +225,8 @@
+
+
(* 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. *)
@@ -235,7 +237,7 @@
val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
- val Ris = map (fn RCInfo {lRIq, ...} => lRIq) RCs
+ 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
@@ -252,7 +254,7 @@
|> fold implies_elim_swp ags'
|> fold implies_elim_swp h_assums'
in
- replace_lemma
+ replace_lemma
end
@@ -296,10 +298,9 @@
val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
- fun prep_RC (RCInfo {lRIq,RIvs, ...}) = lRIq
- |> fold (forall_elim o cterm_of thy o Free) RIvs
- |> (fn it => it RS ih_intro_case)
- |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+ 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
@@ -353,7 +354,7 @@
in
Goal.init goal
|> (SINGLE (resolve_tac [accI] 1)) |> the
- |> (SINGLE (eresolve_tac [R_cases] 1)) |> the
+ |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1)) |> the
|> (SINGLE (CLASIMPSET auto_tac)) |> the
|> Goal.conclude
end
@@ -453,74 +454,32 @@
|> fold implies_intr hyps
|> implies_intr wfR'
|> forall_intr (cterm_of thy R')
- |> forall_elim_vars 0
- |> varifyT
end
-fun mk_partial_rules thy congs data complete_thm compat_thms =
+fun mk_partial_rules thy data provedgoal =
let
- val Prep {names, clauses, complete, compat, ...} = data
+ val Prep {names, clauses, values, R_cases, ex1_iff, ...} = data
val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
-(* val _ = Output.debug "closing derivation: completeness"
- val _ = Output.debug (Proofterm.size_of_proof (proof_of complete_thm))
- val _ = Output.debug (map (Proofterm.size_of_proof o proof_of) compat_thms)*)
- val complete_thm = Drule.close_derivation complete_thm
-(* val _ = Output.debug "closing derivation: compatibility"*)
- val compat_thms = map Drule.close_derivation compat_thms
-(* val _ = Output.debug " done"*)
+ val _ = print "Closing Derivation"
- val complete_thm_fr = Thm.freezeT complete_thm
- val compat_thms_fr = map Thm.freezeT compat_thms
- val f_def_fr = Thm.freezeT f_def
+ val provedgoal = Drule.close_derivation provedgoal
- 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
+ val _ = print "Getting gif"
- (* 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 graph_is_function = (provedgoal COMP conjunctionD1)
+ |> forall_elim_vars 0
- val _ = Output.debug "Proving Replacement lemmas..."
- val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
+ val _ = print "Getting cases"
- val n = length clauses
- val var_order = get_var_order thy clauses
- val compat_store = store_compat_thms n (var_order ~~ compat_thms_fr)
-
- val R_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R)))))) |> Thm.freezeT
- val G_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const G)))))) |> Thm.freezeT
-
- val _ = Output.debug "Proving cases for unique existence..."
- val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses repLemmas) clauses)
+ val complete_thm = provedgoal COMP conjunctionD2
- val _ = Output.debug "Proving: Graph is a function"
- val graph_is_function = complete_thm_fr
- |> 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" *)
- |> Drule.close_derivation
+ val _ = print "making f_iff"
- val f_iff = (graph_is_function RS inst_ex1_iff)
+ val f_iff = (graph_is_function RS ex1_iff)
val _ = Output.debug "Proving simplification rules"
val psimps = map2 (mk_psimp thy names f_iff graph_is_function) clauses values
@@ -534,7 +493,7 @@
val _ = Output.debug "Proving domain introduction rules"
val dom_intros = map (mk_domain_intro thy names R_cases) clauses
in
- FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm,
+ 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