--- a/src/HOL/FunDef.thy Mon Jan 22 16:53:33 2007 +0100
+++ b/src/HOL/FunDef.thy Mon Jan 22 17:29:43 2007 +0100
@@ -13,13 +13,11 @@
("Tools/function_package/fundef_lib.ML")
("Tools/function_package/inductive_wrap.ML")
("Tools/function_package/context_tree.ML")
-("Tools/function_package/fundef_prep.ML")
-("Tools/function_package/fundef_proof.ML")
+("Tools/function_package/fundef_core.ML")
("Tools/function_package/termination.ML")
("Tools/function_package/mutual.ML")
("Tools/function_package/pattern_split.ML")
("Tools/function_package/fundef_package.ML")
-(*("Tools/function_package/fundef_datatype.ML")*)
("Tools/function_package/auto_term.ML")
begin
@@ -71,6 +69,27 @@
done
+lemma not_accP_down:
+ assumes na: "\<not> accP R x"
+ obtains z where "R z x" and "\<not>accP R z"
+proof -
+ assume a: "\<And>z. \<lbrakk>R z x; \<not> accP R z\<rbrakk> \<Longrightarrow> thesis"
+
+ show thesis
+ proof (cases "\<forall>z. R z x \<longrightarrow> accP R z")
+ case True
+ hence "\<And>z. R z x \<Longrightarrow> accP R z" by auto
+ hence "accP R x"
+ by (rule accPI)
+ with na show thesis ..
+ next
+ case False then obtain z where "R z x" and "\<not>accP R z"
+ by auto
+ with a show thesis .
+ qed
+qed
+
+
lemma accP_subset:
assumes sub: "\<And>x y. R1 x y \<Longrightarrow> R2 x y"
shows "\<And>x. accP R2 x \<Longrightarrow> accP R1 x"
@@ -195,8 +214,7 @@
use "Tools/function_package/fundef_lib.ML"
use "Tools/function_package/inductive_wrap.ML"
use "Tools/function_package/context_tree.ML"
-use "Tools/function_package/fundef_prep.ML"
-use "Tools/function_package/fundef_proof.ML"
+use "Tools/function_package/fundef_core.ML"
use "Tools/function_package/termination.ML"
use "Tools/function_package/mutual.ML"
use "Tools/function_package/pattern_split.ML"
--- a/src/HOL/IsaMakefile Mon Jan 22 16:53:33 2007 +0100
+++ b/src/HOL/IsaMakefile Mon Jan 22 17:29:43 2007 +0100
@@ -107,8 +107,7 @@
Tools/function_package/fundef_datatype.ML \
Tools/function_package/fundef_lib.ML \
Tools/function_package/fundef_package.ML \
- Tools/function_package/fundef_prep.ML \
- Tools/function_package/fundef_proof.ML \
+ Tools/function_package/fundef_core.ML \
Tools/function_package/inductive_wrap.ML \
Tools/function_package/lexicographic_order.ML \
Tools/function_package/mutual.ML \
--- a/src/HOL/Tools/function_package/fundef_common.ML Mon Jan 22 16:53:33 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Jan 22 17:29:43 2007 +0100
@@ -12,7 +12,6 @@
(* Theory Dependencies *)
val acc_const_name = "FunDef.accP"
-val domintros = ref true;
val profile = ref false;
fun PROFILE msg = if !profile then timeap_msg msg else I
@@ -20,6 +19,7 @@
fun mk_acc domT R =
Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R
+(* FIXME, unused *)
val function_name = suffix "C"
val graph_name = suffix "_graph"
val rel_name = suffix "_rel"
@@ -35,163 +35,29 @@
| Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
| RCall of (term * ctx_tree)
-type glrs = (term list * term list * term * term) list
-datatype globals =
- Globals of {
- fvar: term,
- domT: typ,
- ranT: typ,
- h: term,
- y: term,
- x: term,
- z: term,
- a:term,
- P: term,
- D: term,
- Pbool:term
-}
-
-
-datatype rec_call_info =
- RCInfo of
- {
- RIvs: (string * typ) list, (* Call context: fixes and assumes *)
- CCas: thm list,
- rcarg: term, (* The recursive argument *)
-
- llRI: thm,
- h_assum: term
- }
-
-
-datatype clause_context =
- ClauseContext of
- {
- ctxt : Proof.context,
-
- qs : term list,
- gs : term list,
- lhs: term,
- rhs: term,
-
- cqs: cterm list,
- ags: thm list,
- case_hyp : thm
- }
-
-
-fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
- ClauseContext { ctxt = ProofContext.transfer thy ctxt,
- qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
-
-
-datatype clause_info =
- ClauseInfo of
- {
- no: int,
- qglr : ((string * typ) list * term list * term * term),
- cdata : clause_context,
-
- tree: ctx_tree,
- lGI: thm,
- RCs: rec_call_info list
- }
-
-
-
-
-type qgar = string * (string * typ) list * term list * term list * term
-
-fun name_of_fqgar (f, _, _, _, _) = f
-
-datatype mutual_part =
- MutualPart of
- {
- fvar : string * typ,
- cargTs: typ list,
- pthA: SumTools.sum_path,
- pthR: SumTools.sum_path,
- f_def: term,
-
- f: term option,
- f_defthm : thm option
- }
-
-
-datatype mutual_info =
- Mutual of
- {
- defname: string,
- fsum_var : string * typ,
-
- ST: typ,
- RST: typ,
- streeA: SumTools.sum_tree,
- streeR: SumTools.sum_tree,
-
- parts: mutual_part list,
- fqgars: qgar list,
- qglrs: ((string * typ) list * term list * term * term) list,
-
- fsum : term option
- }
-
-
-datatype prep_result =
- Prep of
- {
- globals: globals,
- f: term,
- G: term,
- R: term,
-
- goal: term,
- goalI: thm,
- values: thm list,
- clauses: clause_info list,
-
- R_cases: thm,
- ex1_iff: thm
- }
-
datatype fundef_result =
FundefResult of
{
f: term,
- G : term,
- R : term,
- completeness : thm,
-
- psimps : thm list,
- subset_pinduct : thm,
- simple_pinduct : thm,
- total_intro : thm,
- dom_intros : thm list
- }
-
-datatype fundef_mresult =
- FundefMResult of
- {
- f: term,
G: term,
R: term,
psimps : thm list,
+ trsimps : thm list option,
+
subset_pinducts : thm list,
simple_pinducts : thm list,
cases : thm,
termination : thm,
- domintros : thm list
+ domintros : thm list option
}
datatype fundef_context_data =
FundefCtxData of
{
- fixes : ((string * typ) * mixfix) list,
- spec : ((string * Attrib.src list) * term list) list list,
- mutual: mutual_info,
+ add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
f : term,
R : term,
@@ -261,6 +127,7 @@
| Preprocessor of string
| Target of xstring
| DomIntros
+ | Tailrec
datatype fundef_config
= FundefConfig of
@@ -269,23 +136,29 @@
default: string,
preprocessor: string option,
target: xstring option,
- domintros: bool
+ domintros: bool,
+ tailrec: bool
}
-val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false }
-val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false }
+val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE,
+ target=NONE, domintros=false, tailrec=false }
+
+val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE,
+ target=NONE, domintros=false, tailrec=false }
-fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros}) =
- FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros }
- | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros}) =
- FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros }
- | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros}) =
- FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros }
- | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros }) =
- FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros }
- | apply_opt Domintros (FundefConfig {sequential, default, preprocessor, target, domintros }) =
- FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true }
+fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
+ FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
+ | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
+ FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
+ | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
+ FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros, tailrec=tailrec }
+ | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
+ FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros, tailrec=tailrec }
+ | apply_opt DomIntros (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
+ FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true,tailrec=tailrec }
+ | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
+ FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true }
local structure P = OuterParse and K = OuterKeyword in
@@ -295,29 +168,18 @@
val option_parser = (P.$$$ "sequential" >> K Sequential)
|| ((P.reserved "default" |-- P.term) >> Default)
|| (P.reserved "domintros" >> K DomIntros)
+ || (P.reserved "tailrec" >> K Tailrec)
|| ((P.$$$ "in" |-- P.xname) >> Target)
fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") [])
>> (fn opts => fold apply_opt opts def)
+
end
-
-
-
-
-
-
-
-
-
-
-
-
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_core.ML Mon Jan 22 17:29:43 2007 +0100
@@ -0,0 +1,952 @@
+(* Title: HOL/Tools/function_package/fundef_core.ML
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Main functionality
+*)
+
+signature FUNDEF_CORE =
+sig
+ val prepare_fundef : FundefCommon.fundef_config
+ -> string (* defname *)
+ -> (string * typ * mixfix) (* defined symbol *)
+ -> ((string * typ) list * term list * term * term) list (* specification *)
+ -> string (* default_value, not parsed yet *)
+ -> local_theory
+
+ -> (term (* f *)
+ * thm (* goalstate *)
+ * (thm -> FundefCommon.fundef_result) (* continuation *)
+ ) * local_theory
+
+end
+
+structure FundefCore : FUNDEF_CORE =
+struct
+
+
+open FundefLib
+open FundefCommon
+open FundefAbbrev
+
+datatype globals =
+ Globals of {
+ fvar: term,
+ domT: typ,
+ ranT: typ,
+ h: term,
+ y: term,
+ x: term,
+ z: term,
+ a: term,
+ P: term,
+ D: term,
+ Pbool:term
+}
+
+
+datatype rec_call_info =
+ RCInfo of
+ {
+ RIvs: (string * typ) list, (* Call context: fixes and assumes *)
+ CCas: thm list,
+ rcarg: term, (* The recursive argument *)
+
+ llRI: thm,
+ h_assum: term
+ }
+
+
+datatype clause_context =
+ ClauseContext of
+ {
+ ctxt : Proof.context,
+
+ qs : term list,
+ gs : term list,
+ lhs: term,
+ rhs: term,
+
+ cqs: cterm list,
+ ags: thm list,
+ case_hyp : thm
+ }
+
+
+fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
+ ClauseContext { ctxt = ProofContext.transfer thy ctxt,
+ qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
+
+
+datatype clause_info =
+ ClauseInfo of
+ {
+ no: int,
+ qglr : ((string * typ) list * term list * term * term),
+ cdata : clause_context,
+
+ tree: ctx_tree,
+ lGI: thm,
+ RCs: rec_call_info list
+ }
+
+
+(* Theory dependencies. *)
+val Pair_inject = thm "Product_Type.Pair_inject";
+
+val acc_induct_rule = thm "FunDef.accP_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 acc_downward = thm "FunDef.accP_downward"
+val accI = thm "FunDef.accPI"
+val case_split = thm "HOL.case_split_thm"
+val fundef_default_value = thm "FunDef.fundef_default_value"
+val not_accP_down = thm "FunDef.not_accP_down"
+
+
+
+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
+
+
+(** building proof obligations *)
+
+fun mk_compat_proof_obligations domT ranT fvar f glrs =
+ let
+ fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
+ let
+ val shift = incr_boundvars (length qs')
+ in
+ (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
+ $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
+ |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
+ |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
+ |> curry abstract_over fvar
+ |> curry subst_bound f
+ end
+ in
+ map mk_impl (unordered_pairs glrs)
+ end
+
+
+fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
+ let
+ fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
+ Trueprop Pbool
+ |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ in
+ Trueprop Pbool
+ |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
+ |> mk_forall_rename ("x", x)
+ |> mk_forall_rename ("P", Pbool)
+ end
+
+(** making a context with it's own local bindings **)
+
+fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
+ let
+ val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
+ |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
+
+ val thy = ProofContext.theory_of ctxt'
+
+ fun inst t = subst_bounds (rev qs, t)
+ val gs = map inst pre_gs
+ val lhs = inst pre_lhs
+ val rhs = inst pre_rhs
+
+ val cqs = map (cterm_of thy) qs
+ val ags = map (assume o cterm_of thy) gs
+
+ val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
+ in
+ ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
+ cqs = cqs, ags = ags, case_hyp = case_hyp }
+ end
+
+
+(* lowlevel term function *)
+fun abstract_over_list vs body =
+ let
+ exception SAME;
+ fun abs lev v tm =
+ if v aconv tm then Bound lev
+ else
+ (case tm of
+ Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
+ | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
+ | _ => raise SAME);
+ in
+ fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
+ end
+
+
+
+fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
+ let
+ val Globals {h, fvar, x, ...} = globals
+
+ val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
+ val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+
+ (* Instantiate the GIntro thm with "f" and import into the clause context. *)
+ val lGI = GIntro_thm
+ |> forall_elim (cert f)
+ |> fold forall_elim cqs
+ |> fold implies_elim_swp ags
+
+ fun mk_call_info (rcfix, rcassm, rcarg) RI =
+ let
+ val llRI = RI
+ |> fold forall_elim cqs
+ |> fold (forall_elim o cert o Free) rcfix
+ |> fold implies_elim_swp ags
+ |> fold implies_elim_swp rcassm
+
+ val h_assum =
+ Trueprop (G $ rcarg $ (h $ rcarg))
+ |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ |> fold_rev (mk_forall o Free) rcfix
+ |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
+ |> abstract_over_list (rev qs)
+ in
+ RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
+ end
+
+ val RC_infos = map2 mk_call_info RCs RIntro_thms
+ in
+ ClauseInfo
+ {
+ no=no,
+ cdata=cdata,
+ qglr=qglr,
+
+ lGI=lGI,
+ RCs=RC_infos,
+ tree=tree
+ }
+ end
+
+
+
+
+
+
+
+(* 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
+
+(* expects 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 i j ctxi ctxj =
+ let
+ val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
+ val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
+
+ 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 (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
+ |> fold implies_elim_swp agsj
+ |> fold implies_elim_swp agsi
+ |> 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 (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
+ |> fold implies_elim_swp agsi
+ |> fold implies_elim_swp agsj
+ |> implies_elim_swp (assume lhsi_eq_lhsj)
+ |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
+ end
+ end
+
+
+
+
+(* Generates the replacement lemma in fully quantified form. *)
+fun mk_replacement_lemma thy h ih_elim clause =
+ let
+ val ClauseInfo {cdata=ClauseContext {qs, 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 {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) 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 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
+ |> Goal.close_result
+ in
+ replace_lemma
+ end
+
+
+fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
+ let
+ val Globals {h, y, x, fvar, ...} = globals
+ val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
+ val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
+
+ val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
+ = mk_clause_context x ctxti cdescj
+
+ val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
+ val compat = get_compat_thm thy compat_store i j cctxi cctxj
+ val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
+
+ val RLj_import =
+ RLj |> fold forall_elim cqsj'
+ |> fold implies_elim_swp agsj'
+ |> fold implies_elim_swp Ghsj'
+
+ 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' *)
+ in
+ (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
+ |> implies_elim RLj_import (* 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 *)
+ |> fold_rev (implies_intr o cprop_of) Ghsj'
+ |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
+ |> implies_intr (cprop_of y_eq_rhsj'h)
+ |> implies_intr (cprop_of lhsi_eq_lhsj')
+ |> fold_rev forall_intr (cterm_of thy h :: cqsj')
+ end
+
+
+
+fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
+ let
+ val Globals {x, y, ranT, fvar, ...} = globals
+ val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
+ val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
+
+ 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 = fold (curry op COMP o prep_RC) RCs lGI
+
+ val P = cterm_of thy (mk_eq (y, rhsC))
+ val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y)))
+
+ val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
+
+ val uniqueness = G_cases
+ |> forall_elim (cterm_of thy lhs)
+ |> forall_elim (cterm_of thy y)
+ |> forall_elim P
+ |> implies_elim_swp G_lhs_y
+ |> fold implies_elim_swp unique_clauses
+ |> implies_intr (cprop_of G_lhs_y)
+ |> forall_intr (cterm_of thy y)
+
+ val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
+
+ val exactly_one =
+ ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
+ |> 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
+ |> 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 globals G f R clauses complete compat compat_store G_elim f_def =
+ let
+ val Globals {h, domT, ranT, x, ...} = globals
+
+ (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
+ val ihyp = all domT $ Abs ("z", domT,
+ implies $ Trueprop (R $ Bound 0 $ x)
+ $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
+ Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
+ |> cterm_of thy
+
+ val ihyp_thm = assume ihyp |> forall_elim_vars 0
+ val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
+ val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
+
+ val _ = Output.debug (K "Proving Replacement lemmas...")
+ val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
+
+ val _ = Output.debug (K "Proving cases for unique existence...")
+ val (ex1s, values) =
+ split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
+
+ val _ = Output.debug (K "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_acc domT R $ x)))
+ |> 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)
+
+ val goalstate = Conjunction.intr graph_is_function complete
+ |> Goal.close_result
+ |> Goal.protect
+ |> fold_rev (implies_intr o cprop_of) compat
+ |> implies_intr (cprop_of complete)
+ in
+ (goalstate, values)
+ end
+
+
+fun define_graph Gname fvar domT ranT clauses RCss lthy =
+ let
+ val GT = domT --> ranT --> boolT
+ val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
+
+ fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
+ let
+ fun mk_h_assm (rcfix, rcassm, rcarg) =
+ Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
+ |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ |> fold_rev (mk_forall o Free) rcfix
+ in
+ Trueprop (Gvar $ lhs $ rhs)
+ |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev mk_forall (fvar :: qs)
+ end
+
+ val G_intros = map2 mk_GIntro clauses RCss
+
+ val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
+ FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
+ in
+ ((G, GIntro_thms, G_elim, G_induct), lthy)
+ end
+
+
+
+fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
+ let
+ val f_def =
+ Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
+ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
+ |> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *)
+
+ val ((f, (_, f_defthm)), lthy) =
+ LocalTheory.def Thm.internalK ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
+ in
+ ((f, f_defthm), lthy)
+ end
+
+
+fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
+ let
+
+ val RT = domT --> domT --> boolT
+ val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
+
+ fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
+ Trueprop (Rvar $ rcarg $ lhs)
+ |> 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_rename (map fst oqs ~~ qs)
+ (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
+
+ val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
+
+ val (RIntro_thmss, (R, R_elim, _, lthy)) =
+ fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
+ in
+ ((R, RIntro_thmss, R_elim), lthy)
+ end
+
+
+fun fix_globals domT ranT fvar ctxt =
+ let
+ val ([h, y, x, z, a, D, P, Pbool],ctxt') =
+ Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
+ in
+ (Globals {h = Free (h, domT --> ranT),
+ y = Free (y, ranT),
+ x = Free (x, domT),
+ z = Free (z, domT),
+ a = Free (a, domT),
+ D = Free (D, domT --> boolT),
+ P = Free (P, domT --> boolT),
+ Pbool = Free (Pbool, boolT),
+ fvar = fvar,
+ domT = domT,
+ ranT = ranT
+ },
+ ctxt')
+ end
+
+
+
+fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
+ let
+ fun inst_term t = subst_bound(f, abstract_over (fvar, t))
+ in
+ (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
+ end
+
+
+
+(**********************************************************
+ * PROVING THE RULES
+ **********************************************************)
+
+fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
+ let
+ val Globals {domT, z, ...} = globals
+
+ fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
+ let
+ 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
+ in
+ map2 mk_psimp clauses valthms
+ end
+
+
+(** Induction rule **)
+
+
+val acc_subset_induct = thm "FunDef.accP_subset_induct"
+
+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, 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
+
+
+
+(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
+fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause =
+ let
+ 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
+
+
+
+(** Termination rule **)
+
+val wf_induct_rule = thm "FunDef.wfP_induct_rule";
+val wf_in_rel = thm "FunDef.wf_in_rel";
+val in_rel_def = thm "FunDef.in_rel_def";
+
+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
+
+
+
+(* Tail recursion (probably very fragile)
+ *
+ * FIXME:
+ * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
+ * - Must we really replace the fvar by f here?
+ * - Splitting is not configured automatically: Problems with case?
+ *)
+fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
+ let
+ val Globals {domT, ranT, fvar, ...} = globals
+
+ val R_cases = forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
+
+ val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *)
+ Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
+ (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
+ (fn {prems=[a], ...} =>
+ ((rtac (G_induct OF [a]))
+ THEN_ALL_NEW (rtac accI)
+ THEN_ALL_NEW (etac R_cases)
+ THEN_ALL_NEW (SIMPSET' asm_full_simp_tac)) 1)
+
+ val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
+
+ fun mk_trsimp clause psimp =
+ let
+ val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
+ val thy = ProofContext.theory_of ctxt
+ val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
+
+ val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
+ val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
+ in
+ Goal.prove ctxt [] [] trsimp
+ (fn _ =>
+ rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
+ THEN (rtac (forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
+ THEN (SIMPSET (fn ss => asm_full_simp_tac (ss addsimps [default_thm]) 1))
+ THEN (etac not_accP_down 1)
+ THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps [default_thm])))) 1)
+ |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+ end
+ in
+ map2 mk_trsimp clauses psimps
+ end
+
+
+fun prepare_fundef config defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
+ let
+ val FundefConfig {domintros, tailrec, ...} = config
+
+ val fvar = Free (fname, fT)
+ val domT = domain_type fT
+ val ranT = range_type fT
+
+ val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
+
+ val congs = get_fundef_congs (Context.Proof lthy)
+ val (globals, ctxt') = fix_globals domT ranT fvar lthy
+
+ val Globals { x, h, ... } = globals
+
+ val clauses = map (mk_clause_context x ctxt') abstract_qglrs
+
+ val n = length abstract_qglrs
+
+ val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *)
+
+ fun build_tree (ClauseContext { ctxt, rhs, ...}) =
+ FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs
+
+ val trees = map build_tree clauses
+ val RCss = map find_calls trees
+
+ val ((G, GIntro_thms, G_elim, G_induct), lthy) =
+ PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
+
+ val ((f, f_defthm), lthy) =
+ PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
+
+ val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
+ val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
+
+ val ((R, RIntro_thmss, R_elim), lthy) =
+ PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
+
+ val (_, lthy) =
+ LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R) lthy
+
+ val newthy = ProofContext.theory_of lthy
+ val clauses = map (transfer_clause_ctx newthy) clauses
+
+ val cert = cterm_of (ProofContext.theory_of lthy)
+
+ val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
+
+ val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
+ val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
+
+ val compat_store = store_compat_thms n compat
+
+ val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
+
+ val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
+
+ fun mk_partial_rules provedgoal =
+ let
+ val newthy = theory_of_thm provedgoal (*FIXME*)
+
+ val (graph_is_function, complete_thm) =
+ provedgoal
+ |> Conjunction.elim
+ |> apfst (forall_elim_vars 0)
+
+ val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
+
+ val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
+
+ val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule"
+ (mk_partial_induct_rule newthy globals R complete_thm) xclauses
+
+
+ val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
+
+ val dom_intros = if domintros
+ then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses)
+ else NONE
+ val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
+
+ in
+ FundefResult {f=f, G=G, R=R, cases=complete_thm,
+ psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct],
+ termination=total_intro, trsimps=trsimps,
+ domintros=dom_intros}
+ end
+ in
+ ((f, goalstate, mk_partial_rules), lthy)
+ end
+
+
+
+
+end
--- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Jan 22 16:53:33 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Jan 22 17:29:43 2007 +0100
@@ -10,14 +10,34 @@
structure FundefLib = struct
+(* ==> library/string *)
fun plural sg pl [x] = sg
| plural sg pl _ = pl
+
+
+fun map_option f NONE = NONE
+ | map_option f (SOME x) = SOME (f x);
+
+fun fold_option f NONE y = y
+ | fold_option f (SOME x) y = f x y;
+
+fun fold_map_option f NONE y = (NONE, y)
+ | fold_map_option f (SOME x) y = apfst SOME (f x y);
+
+
+
+
+
+
+(* ??? *)
fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
+(* ==> logic.ML? *)
fun mk_forall v t = all (fastype_of v) $ lambda v t
-(* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
+(* lambda-abstracts over an arbitrarily nested tuple
+ ==> hologic.ML? *)
fun tupled_lambda vars t =
case vars of
(Free v) => lambda (Free v) t
@@ -86,16 +106,12 @@
(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
+(* ==> library *)
fun unordered_pairs [] = []
| unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
-(* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *)
-fun replace_frees assoc =
- map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
- | t => t)
-
-
+(* term.ML *)
fun forall_aterms P (t $ u) = forall_aterms P t andalso forall_aterms P u
| forall_aterms P (Abs (_, _, t)) = forall_aterms P t
| forall_aterms P a = P a
@@ -104,6 +120,11 @@
+(* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *)
+fun replace_frees assoc =
+ map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
+ | t => t)
+
fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
| rename_bound n _ = raise Match
@@ -116,7 +137,7 @@
fun forall_intr_rename (n, cv) thm =
let
val allthm = forall_intr cv thm
- val (_, abs) = Logic.dest_all (prop_of allthm)
+ val (_ $ abs) = prop_of allthm
in
Thm.rename_boundvars abs (Abs (n, dummyT, dummy_term)) allthm
end
@@ -127,11 +148,6 @@
Term.add_frees t []
|> filter_out (Variable.is_fixed ctxt o fst)
|> rev
-(*
- rev (fold_aterms (fn Free (v as (x, _)) =>
- if Variable.is_fixed ctxt x then I else insert (fn ((x, _),(y, _)) => x = y) v | _ => I) t [])
-*)
-
end
--- a/src/HOL/Tools/function_package/fundef_package.ML Mon Jan 22 16:53:33 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Jan 22 17:29:43 2007 +0100
@@ -40,6 +40,8 @@
val note_theorem = LocalTheory.note Thm.theoremK
+fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
+
fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
let val (xs, ys) = split_list ps
in xs ~~ f ys end
@@ -47,49 +49,46 @@
fun restore_spec_structure reps spec =
(burrow o burrow_snd o burrow o K) reps spec
-fun add_simps label moreatts mutual_info fixes psimps spec lthy =
+fun add_simps fixes spec sort label moreatts simps lthy =
let
val fnames = map (fst o fst) fixes
- val (saved_spec_psimps, lthy) =
- fold_map (fold_map note_theorem) (restore_spec_structure psimps spec) lthy
- val saved_psimps = flat (map snd (flat saved_spec_psimps))
+ val (saved_spec_simps, lthy) =
+ fold_map (fold_map note_theorem) (restore_spec_structure simps spec) lthy
+ val saved_simps = flat (map snd (flat saved_spec_simps))
- val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
+ val simps_by_f = sort saved_simps
- fun add_for_f fname psimps =
+ fun add_for_f fname simps =
note_theorem
((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts),
- psimps) #> snd
+ simps) #> snd
in
- (saved_psimps,
- fold2 add_for_f fnames psimps_by_f lthy)
+ (saved_simps,
+ fold2 add_for_f fnames simps_by_f lthy)
end
-fun fundef_afterqed config fixes spec mutual_info defname data [[result]] lthy =
+fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
let
- val FundefConfig { domintros, ...} = config
- val Prep {f, R, ...} = data
- val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
- val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
+ val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} =
+ cont (Goal.close_result proof)
+
val qualify = NameSpace.qualified defname
+ val addsimps = add_simps fixes spec sort_cont
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
- |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
- ||>> PROFILE "adding pinduct"
- (note_theorem ((qualify "pinduct",
- [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts))
- ||>> PROFILE "adding termination"
- (note_theorem ((qualify "termination", []), [termination]))
- ||> (snd o PROFILE "adding cases" (note_theorem ((qualify "cases", []), [cases])))
- ||> (snd o PROFILE "adding domintros" (note_theorem ((qualify "domintros", []), domintros)))
+ |> addsimps "psimps" [] psimps
+ ||> fold_option (snd oo addsimps "simps" []) trsimps
+ ||>> note_theorem ((qualify "pinduct",
+ [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts)
+ ||>> note_theorem ((qualify "termination", []), [termination])
+ ||> (snd o note_theorem ((qualify "cases", []), [cases]))
+ ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
- val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
+ val cdata = FundefCtxData { add_simps=addsimps, psimps=psimps',
pinducts=snd pinducts', termination=termination', f=f, R=R }
-
-
in
lthy (* FIXME proper handling of morphism *)
|> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *)
@@ -117,33 +116,36 @@
fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
let
- val FundefConfig {sequential, default, ...} = config
+ val FundefConfig {sequential, default, tailrec, ...} = config
val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
+
+ val defname = mk_defname fixes
+
val t_eqns = spec
|> flat |> map snd |> flat (* flatten external structure *)
- val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) =
- FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy
+ val ((goalstate, cont, sort_cont), lthy) =
+ FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy
- val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
+ val afterqed = fundef_afterqed config fixes spec defname cont sort_cont
in
- (name, lthy
- |> Proof.theorem_i NONE afterqed [[(goal, [])]]
- |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
+ (defname, lthy
+ |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
+ |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd)
end
fun total_termination_afterqed defname data [[totality]] lthy =
let
- val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data
+ val FundefCtxData { add_simps, psimps, pinducts, ... } = data
- val totality = PROFILE "closing" Goal.close_result totality
+ val totality = Goal.close_result totality
val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
- val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps
- val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts
+ val tsimps = map remove_domain_condition psimps
+ val tinduct = map remove_domain_condition pinducts
(* FIXME: How to generate code from (possibly) local contexts*)
val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
@@ -152,26 +154,26 @@
val qualify = NameSpace.qualified defname;
in
lthy
- |> PROFILE "adding tsimps" (add_simps "simps" allatts mutual fixes tsimps spec) |> snd
- |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
+ |> add_simps "simps" allatts tsimps |> snd
+ |> note_theorem ((qualify "induct", []), tinduct) |> snd
end
fun setup_termination_proof name_opt lthy =
let
- val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt
- val data = the (get_fundef_data name (Context.Proof lthy))
- handle Option.Option => raise ERROR ("No such function definition: " ^ name)
+ val defname = the_default (get_last_fundef (Context.Proof lthy)) name_opt
+ val data = the (get_fundef_data defname (Context.Proof lthy))
+ handle Option.Option => raise ERROR ("No such function definition: " ^ defname)
- val FundefCtxData {termination, f, R, ...} = data
- val goal = FundefTermination.mk_total_termination_goal f R
+ val FundefCtxData {termination, R, ...} = data
+ val goal = FundefTermination.mk_total_termination_goal R
in
lthy
|> ProofContext.note_thmss_i ""
[(("termination", [ContextRules.intro_query NONE]),
[([Goal.norm_result termination], [])])] |> snd
|> set_termination_rule termination
- |> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]]
+ |> Proof.theorem_i NONE (total_termination_afterqed defname data) [[(goal, [])]]
end
--- a/src/HOL/Tools/function_package/fundef_prep.ML Mon Jan 22 16:53:33 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,534 +0,0 @@
-(* 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 : string (* defname *)
- -> (string * typ * mixfix) (* defined symbol *)
- -> ((string * typ) list * term list * term * term) list (* specification *)
- -> string (* default_value, not parsed yet *)
- -> local_theory
- -> FundefCommon.prep_result * term * local_theory
-
-end
-
-structure FundefPrep : FUNDEF_PREP =
-struct
-
-
-open FundefLib
-open FundefCommon
-open FundefAbbrev
-
-(* Theory dependencies. *)
-val Pair_inject = thm "Product_Type.Pair_inject";
-
-val acc_induct_rule = thm "FunDef.accP_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 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
-
-
-fun mk_compat_proof_obligations domT ranT fvar f glrs =
- let
- fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
- let
- val shift = incr_boundvars (length qs')
- in
- (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
- $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
- |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
- |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
- |> curry abstract_over fvar
- |> curry subst_bound f
- end
- in
- map mk_impl (unordered_pairs glrs)
- end
-
-
-fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
- let
- fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
- Trueprop Pbool
- |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
- |> fold_rev (curry Logic.mk_implies) gs
- |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
- in
- Trueprop Pbool
- |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
- |> mk_forall_rename ("x", x)
- |> mk_forall_rename ("P", Pbool)
- end
-
-
-fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
- let
- val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
- |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
-
- val thy = ProofContext.theory_of ctxt'
-
- fun inst t = subst_bounds (rev qs, t)
- val gs = map inst pre_gs
- val lhs = inst pre_lhs
- val rhs = inst pre_rhs
-
- val cqs = map (cterm_of thy) qs
- val ags = map (assume o cterm_of thy) gs
-
- val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
- in
- ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
- cqs = cqs, ags = ags, case_hyp = case_hyp }
- end
-
-
-(* lowlevel term function *)
-fun abstract_over_list vs body =
- let
- exception SAME;
- fun abs lev v tm =
- if v aconv tm then Bound lev
- else
- (case tm of
- Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
- | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
- | _ => raise SAME);
- in
- fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
- end
-
-
-
-fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
- let
- val Globals {h, fvar, x, ...} = globals
-
- val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
- val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
-
- (* Instantiate the GIntro thm with "f" and import into the clause context. *)
- val lGI = GIntro_thm
- |> forall_elim (cert f)
- |> fold forall_elim cqs
- |> fold implies_elim_swp ags
-
- fun mk_call_info (rcfix, rcassm, rcarg) RI =
- let
- val llRI = RI
- |> fold forall_elim cqs
- |> fold (forall_elim o cert o Free) rcfix
- |> fold implies_elim_swp ags
- |> fold implies_elim_swp rcassm
-
- val h_assum =
- Trueprop (G $ rcarg $ (h $ rcarg))
- |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
- |> fold_rev (mk_forall o Free) rcfix
- |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
- |> abstract_over_list (rev qs)
- in
- RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
- end
-
- val RC_infos = map2 mk_call_info RCs RIntro_thms
- in
- ClauseInfo
- {
- no=no,
- cdata=cdata,
- qglr=qglr,
-
- lGI=lGI,
- RCs=RC_infos,
- tree=tree
- }
- end
-
-
-
-
-
-
-
-(* 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
-
-(* expects 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 i j ctxi ctxj =
- let
- val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
- val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
-
- 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 (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
- |> fold implies_elim_swp agsj
- |> fold implies_elim_swp agsi
- |> 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 (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
- |> fold implies_elim_swp agsi
- |> fold implies_elim_swp agsj
- |> implies_elim_swp (assume lhsi_eq_lhsj)
- |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
- end
- end
-
-
-
-
-(* Generates the replacement lemma in fully quantified form. *)
-fun mk_replacement_lemma thy h ih_elim clause =
- let
- val ClauseInfo {cdata=ClauseContext {qs, 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 {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) 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 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
- |> Goal.close_result
- in
- replace_lemma
- end
-
-
-fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
- let
- val Globals {h, y, x, fvar, ...} = globals
- val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
- val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
-
- val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
- = mk_clause_context x ctxti cdescj
-
- val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
- val compat = get_compat_thm thy compat_store i j cctxi cctxj
- val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
-
- val RLj_import =
- RLj |> fold forall_elim cqsj'
- |> fold implies_elim_swp agsj'
- |> fold implies_elim_swp Ghsj'
-
- 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' *)
- in
- (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
- |> implies_elim RLj_import (* 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 *)
- |> fold_rev (implies_intr o cprop_of) Ghsj'
- |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
- |> implies_intr (cprop_of y_eq_rhsj'h)
- |> implies_intr (cprop_of lhsi_eq_lhsj')
- |> fold_rev forall_intr (cterm_of thy h :: cqsj')
- end
-
-
-
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
- let
- val Globals {x, y, ranT, fvar, ...} = globals
- val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
- val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
-
- 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 = fold (curry op COMP o prep_RC) RCs lGI
-
- val P = cterm_of thy (mk_eq (y, rhsC))
- val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y)))
-
- val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
-
- val uniqueness = G_cases
- |> forall_elim (cterm_of thy lhs)
- |> forall_elim (cterm_of thy y)
- |> forall_elim P
- |> implies_elim_swp G_lhs_y
- |> fold implies_elim_swp unique_clauses
- |> implies_intr (cprop_of G_lhs_y)
- |> forall_intr (cterm_of thy y)
-
- val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
-
- val exactly_one =
- ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
- |> 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
- |> 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 globals G f R clauses complete compat compat_store G_elim f_def =
- let
- val Globals {h, domT, ranT, x, ...} = globals
-
- val inst_ex1_ex = f_def RS ex1_implies_ex
- val inst_ex1_un = f_def RS ex1_implies_un
- val inst_ex1_iff = f_def RS ex1_implies_iff
-
- (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
- val ihyp = all domT $ Abs ("z", domT,
- implies $ Trueprop (R $ Bound 0 $ x)
- $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
- Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
- |> 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 (fn () => "Proving Replacement lemmas...")
- val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
-
- val _ = Output.debug (fn () => "Proving cases for unique existence...")
- val (ex1s, values) =
- split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
-
- val _ = Output.debug (fn () => "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_acc domT R $ x)))
- |> 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)
-
- val goal = complete COMP (graph_is_function COMP conjunctionI)
- |> Goal.close_result
-
- 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
-
-
-fun define_graph Gname fvar domT ranT clauses RCss lthy =
- let
- val GT = domT --> ranT --> boolT
- val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
-
- fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
- let
- fun mk_h_assm (rcfix, rcassm, rcarg) =
- Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
- |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
- |> fold_rev (mk_forall o Free) rcfix
- in
- Trueprop (Gvar $ lhs $ rhs)
- |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
- |> fold_rev (curry Logic.mk_implies) gs
- |> fold_rev mk_forall (fvar :: qs)
- end
-
- val G_intros = map2 mk_GIntro clauses RCss
-
- val (GIntro_thms, (G, G_elim, lthy)) =
- FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
- in
- ((G, GIntro_thms, G_elim), lthy)
- end
-
-
-
-fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
- let
- val f_def =
- Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
- Abs ("y", ranT, G $ Bound 1 $ Bound 0))
- |> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *)
-
- val ((f, (_, f_defthm)), lthy) =
- LocalTheory.def Thm.internalK ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
- in
- ((f, f_defthm), lthy)
- end
-
-
-fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
- let
-
- val RT = domT --> domT --> boolT
- val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
-
- fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
- Trueprop (Rvar $ rcarg $ lhs)
- |> 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_rename (map fst oqs ~~ qs)
- (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
-
- val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
-
- val (RIntro_thmss, (R, R_elim, lthy)) =
- fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
- in
- ((R, RIntro_thmss, R_elim), lthy)
- end
-
-
-fun fix_globals domT ranT fvar ctxt =
- let
- val ([h, y, x, z, a, D, P, Pbool],ctxt') =
- Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
- in
- (Globals {h = Free (h, domT --> ranT),
- y = Free (y, ranT),
- x = Free (x, domT),
- z = Free (z, domT),
- a = Free (a, domT),
- D = Free (D, domT --> boolT),
- P = Free (P, domT --> boolT),
- Pbool = Free (Pbool, boolT),
- fvar = fvar,
- domT = domT,
- ranT = ranT
- },
- ctxt')
- end
-
-
-
-fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
- let
- fun inst_term t = subst_bound(f, abstract_over (fvar, t))
- in
- (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
- end
-
-
-
-fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
- let
- val fvar = Free (fname, fT)
- val domT = domain_type fT
- val ranT = range_type fT
-
- val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
-
- val congs = get_fundef_congs (Context.Proof lthy)
- val (globals, ctxt') = fix_globals domT ranT fvar lthy
-
- val Globals { x, h, ... } = globals
-
- val clauses = PROFILE "mk_clause_context" (map (mk_clause_context x ctxt')) abstract_qglrs
-
- val n = length abstract_qglrs
-
- val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *)
-
- fun build_tree (ClauseContext { ctxt, rhs, ...}) =
- FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs
-
- val trees = PROFILE "making trees" (map build_tree) clauses
- val RCss = PROFILE "finding calls" (map find_calls) trees
-
- val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
- val ((f, f_defthm), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
-
- val RCss = PROFILE "inst_RCs" (map (map (inst_RC (ProofContext.theory_of lthy) fvar f))) RCss
- val trees = PROFILE "inst_trees" (map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f)) trees
-
- val ((R, RIntro_thmss, R_elim), lthy) =
- PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
-
- val (_, lthy) = PROFILE "abbrev"
- (LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R)) lthy
-
- val newthy = ProofContext.theory_of lthy
- val clauses = map (transfer_clause_ctx newthy) clauses
-
- val cert = cterm_of (ProofContext.theory_of lthy)
-
- val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
-
- val complete = PROFILE "mk_compl" (mk_completeness globals clauses) abstract_qglrs |> cert |> assume
- val compat = PROFILE "mk_compat" (mk_compat_proof_obligations domT ranT fvar f) abstract_qglrs |> map (cert #> assume)
-
- val compat_store = store_compat_thms n compat
-
- val (goal, goalI, ex1_iff, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
- in
- (Prep {globals = globals, f = f, G = G, R = R, goal = goal, goalI = goalI, values = values, clauses = xclauses, ex1_iff = ex1_iff, R_cases = R_elim}, f,
- lthy)
- end
-
-
-
-
-end
--- a/src/HOL/Tools/function_package/fundef_proof.ML Mon Jan 22 16:53:33 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,327 +0,0 @@
-(* 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 result" Goal.close_result 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
-
-
--- a/src/HOL/Tools/function_package/inductive_wrap.ML Mon Jan 22 16:53:33 2007 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML Mon Jan 22 17:29:43 2007 +0100
@@ -11,7 +11,7 @@
sig
val inductive_def : term list
-> ((bstring * typ) * mixfix) * local_theory
- -> thm list * (term * thm * local_theory)
+ -> thm list * (term * thm * thm * local_theory)
end
structure FundefInductiveWrap =
@@ -40,7 +40,7 @@
let
val qdefs = map dest_all_all defs
- val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], ...}, lthy) =
+ val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
InductivePackage.add_inductive_i true (*verbose*)
"" (* no altname *)
false (* no coind *)
@@ -70,7 +70,7 @@
|> Term.strip_comb |> snd |> hd (* Trueprop *)
|> Term.strip_comb |> fst
in
- (intrs, (Rdef_real, elim, lthy))
+ (intrs, (Rdef_real, elim, induct, lthy))
end
end
--- a/src/HOL/Tools/function_package/mutual.ML Mon Jan 22 16:53:33 2007 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML Mon Jan 22 17:29:43 2007 +0100
@@ -9,17 +9,16 @@
signature FUNDEF_MUTUAL =
sig
- val prepare_fundef_mutual : ((string * typ) * mixfix) list
+ val prepare_fundef_mutual : FundefCommon.fundef_config
+ -> string (* defname *)
+ -> ((string * typ) * mixfix) list
-> term list
-> string (* default, unparsed term *)
-> local_theory
- -> ((FundefCommon.mutual_info * string * FundefCommon.prep_result) * local_theory)
-
-
- val mk_partial_rules_mutual : Proof.context -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm ->
- FundefCommon.fundef_mresult
-
- val sort_by_function : FundefCommon.mutual_info -> string list -> 'a list -> 'a list list
+ -> ((thm (* goalstate *)
+ * (thm -> FundefCommon.fundef_result) (* proof continuation *)
+ * (thm list -> thm list list) (* sorting continuation *)
+ ) * local_theory)
end
@@ -34,6 +33,45 @@
val sum_case_rules = thms "Datatype.sum.cases"
val split_apply = thm "Product_Type.split"
+type qgar = string * (string * typ) list * term list * term list * term
+
+fun name_of_fqgar (f, _, _, _, _) = f
+
+datatype mutual_part =
+ MutualPart of
+ {
+ fvar : string * typ,
+ cargTs: typ list,
+ pthA: SumTools.sum_path,
+ pthR: SumTools.sum_path,
+ f_def: term,
+
+ f: term option,
+ f_defthm : thm option
+ }
+
+
+datatype mutual_info =
+ Mutual of
+ {
+ fsum_var : string * typ,
+
+ ST: typ,
+ RST: typ,
+ streeA: SumTools.sum_tree,
+ streeR: SumTools.sum_tree,
+
+ parts: mutual_part list,
+ fqgars: qgar list,
+ qglrs: ((string * typ) list * term list * term * term) list,
+
+ fsum : term option
+ }
+
+
+
+
+
fun mutual_induct_Pnames n =
@@ -100,7 +138,7 @@
end;
-fun analyze_eqs ctxt fs eqs =
+fun analyze_eqs ctxt defname fs eqs =
let
val fnames = map fst fs
val (fqgars, arities) = fold_map (split_def ctxt fnames) eqs Symtab.empty
@@ -119,10 +157,9 @@
val (RST,streeR, pthsR) = SumTools.mk_tree_distinct resultTs
val (ST, streeA, pthsA) = SumTools.mk_tree argTs
- val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name fnames)
val fsum_type = ST --> RST
- val ([fsum_var_name], _) = Variable.add_fixes [ def_name ^ "_sum" ] ctxt
+ val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
val fsum_var = (fsum_var_name, fsum_type)
fun define (fvar as (n, T)) caTs pthA pthR =
@@ -150,7 +187,7 @@
val qglrs = map convert_eqs fqgars
in
- Mutual {defname=def_name,fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR,
+ Mutual {fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR,
parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
end
@@ -171,29 +208,15 @@
lthy')
end
- val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual
+ val Mutual { fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual
val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
in
- (Mutual { defname=defname, fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts',
+ (Mutual { fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts',
fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
lthy')
end
-fun prepare_fundef_mutual fixes eqss default lthy =
- let
- val mutual = analyze_eqs lthy (map fst fixes) eqss
- val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
-
- val (prep_result, fsum, lthy') =
- FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
-
- val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
- in
- ((mutual', defname, prep_result), lthy'')
- end
-
-
(* Beta-reduce both sides of a meta-equality *)
fun beta_norm_eq thm =
let
@@ -315,7 +338,7 @@
-fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result =
+fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {RST, parts, streeR, fqgars, ...}) proof =
let
val thy = ProofContext.theory_of lthy
@@ -323,8 +346,9 @@
val expand = Assumption.export false lthy (LocalTheory.target_of lthy)
val expand_term = Drule.term_rule thy expand
- val result = FundefProof.mk_partial_rules thy data prep_result
- val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
+ val result = inner_cont proof
+ val FundefResult {f, G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct],
+ termination,domintros} = result
val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} =>
mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def)))
@@ -333,18 +357,19 @@
fun mk_mpsimp fqgar sum_psimp =
in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
- val mpsimps = PROFILE "making mpsimps" (map2 mk_mpsimp fqgars) psimps
- val minducts = PROFILE "making mpinduct" (mutual_induct_rules thy simple_pinduct all_f_defs) m
- val termination = PROFILE "making mtermination" (full_simplify (HOL_basic_ss addsimps all_f_defs)) total_intro
+ val mpsimps = map2 mk_mpsimp fqgars psimps
+ val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
+ val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
+ val mtermination = full_simplify (HOL_basic_ss addsimps all_f_defs) termination
in
- FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R,
- psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
- cases=expand completeness, termination=expand termination,
- domintros=map expand dom_intros }
+ FundefResult { f=expand_term f, G=expand_term G, R=expand_term R,
+ psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
+ cases=expand cases, termination=expand mtermination,
+ domintros=map_option (map expand) domintros,
+ trsimps=map_option (map expand) trsimps}
end
-
-
+
(* puts an object in the "right bucket" *)
fun store_grouped P x [] = []
| store_grouped P x ((l, xs)::bs) =
@@ -356,5 +381,23 @@
(map (rpair []) names) (* in the empty buckets labeled with names *)
|> map (snd #> map snd) (* and remove the labels afterwards *)
+
+
+fun prepare_fundef_mutual config defname fixes eqss default lthy =
+ let
+ val mutual = analyze_eqs lthy defname (map fst fixes) eqss
+ val Mutual {fsum_var=(n, T), qglrs, ...} = mutual
+
+ val ((fsum, goalstate, cont), lthy') =
+ FundefCore.prepare_fundef config defname (n, T, NoSyn) qglrs default lthy
+
+ val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
+
+ val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
+ val sort_cont = sort_by_function mutual' (map (fst o fst) fixes)
+ in
+ ((goalstate, mutual_cont, sort_cont), lthy'')
+ end
+
end
--- a/src/HOL/Tools/function_package/termination.ML Mon Jan 22 16:53:33 2007 +0100
+++ b/src/HOL/Tools/function_package/termination.ML Mon Jan 22 17:29:43 2007 +0100
@@ -9,7 +9,7 @@
signature FUNDEF_TERMINATION =
sig
- val mk_total_termination_goal : term -> term -> term
+ val mk_total_termination_goal : term -> term
(* val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*)
end
@@ -21,9 +21,9 @@
open FundefCommon
open FundefAbbrev
-fun mk_total_termination_goal f R =
+fun mk_total_termination_goal R =
let
- val domT = domain_type (fastype_of f)
+ val domT = domain_type (fastype_of R)
val x = Free ("x", domT)
in
mk_forall x (Trueprop (mk_acc domT R $ x))
--- a/src/HOL/ex/Fundefs.thy Mon Jan 22 16:53:33 2007 +0100
+++ b/src/HOL/ex/Fundefs.thy Mon Jan 22 17:29:43 2007 +0100
@@ -24,7 +24,6 @@
text {* There is also a cases rule to distinguish cases along the definition *}
thm fib.cases
-thm fib.domintros
text {* total simp and induction rules: *}
thm fib.simps
@@ -172,8 +171,6 @@
thm evn_od.pinduct
thm evn_od.termination
-thm evn_od.domintros
-