First usable version of the new function definition package (HOL/function_packake/...).
Moved Accessible_Part.thy from Library to Main.
--- a/etc/isar-keywords-HOL-Nominal.el Fri May 05 16:50:58 2006 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el Fri May 05 17:17:21 2006 +0200
@@ -82,6 +82,7 @@
"fix"
"from"
"full_prf"
+ "function"
"global"
"guess"
"have"
@@ -174,6 +175,7 @@
"subsubsection"
"syntax"
"term"
+ "termination"
"text"
"text_raw"
"then"
@@ -423,11 +425,13 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
"corollary"
+ "function"
"instance"
"interpretation"
"lemma"
"recdef_tc"
"specification"
+ "termination"
"theorem"
"typedef"))
--- a/etc/isar-keywords.el Fri May 05 16:50:58 2006 +0200
+++ b/etc/isar-keywords.el Fri May 05 17:17:21 2006 +0200
@@ -49,6 +49,7 @@
"code_primclass"
"code_primconst"
"code_primtyco"
+ "code_purge"
"code_serialize"
"code_syntax_const"
"code_syntax_tyco"
@@ -85,6 +86,7 @@
"fixrec"
"from"
"full_prf"
+ "function"
"global"
"guess"
"have"
@@ -177,6 +179,7 @@
"subsubsection"
"syntax"
"term"
+ "termination"
"text"
"text_raw"
"then"
@@ -382,6 +385,7 @@
"code_primclass"
"code_primconst"
"code_primtyco"
+ "code_purge"
"code_serialize"
"code_syntax_const"
"code_syntax_tyco"
@@ -445,12 +449,14 @@
'("ax_specification"
"corollary"
"cpodef"
+ "function"
"instance"
"interpretation"
"lemma"
"pcpodef"
"recdef_tc"
"specification"
+ "termination"
"theorem"
"typedef"))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Accessible_Part.thy Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,123 @@
+(* Title: HOL/Accessible_Part.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+*)
+
+header {* The accessible part of a relation *}
+
+theory Accessible_Part
+imports Wellfounded_Recursion
+begin
+
+subsection {* Inductive definition *}
+
+text {*
+ Inductive definition of the accessible part @{term "acc r"} of a
+ relation; see also \cite{paulin-tlca}.
+*}
+
+consts
+ acc :: "('a \<times> 'a) set => 'a set"
+inductive "acc r"
+ intros
+ accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
+
+abbreviation
+ termi :: "('a \<times> 'a) set => 'a set"
+ "termi r == acc (r\<inverse>)"
+
+
+subsection {* Induction rules *}
+
+theorem acc_induct:
+ assumes major: "a \<in> acc r"
+ assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
+ shows "P a"
+ apply (rule major [THEN acc.induct])
+ apply (rule hyp)
+ apply (rule accI)
+ apply fast
+ apply fast
+ done
+
+theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
+
+theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
+ apply (erule acc.elims)
+ apply fast
+ done
+
+lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
+ apply (erule rtrancl_induct)
+ apply blast
+ apply (blast dest: acc_downward)
+ done
+
+theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
+ apply (blast dest: acc_downwards_aux)
+ done
+
+theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
+ apply (rule wfUNIVI)
+ apply (induct_tac P x rule: acc_induct)
+ apply blast
+ apply blast
+ done
+
+theorem acc_wfD: "wf r ==> x \<in> acc r"
+ apply (erule wf_induct)
+ apply (rule accI)
+ apply blast
+ done
+
+theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
+ apply (blast intro: acc_wfI dest: acc_wfD)
+ done
+
+
+(* Smaller relations have bigger accessible parts: *)
+lemma acc_subset:
+ assumes sub:"R1 \<subseteq> R2"
+ shows "acc R2 \<subseteq> acc R1"
+proof
+ fix x assume "x \<in> acc R2"
+ thus "x \<in> acc R1"
+ proof (induct x) -- "acc-induction"
+ fix x
+ assume ih: "\<And>y. (y, x) \<in> R2 \<Longrightarrow> y \<in> acc R1"
+
+ with sub show "x \<in> acc R1"
+ by (blast intro:accI)
+ qed
+qed
+
+
+
+(* This is a generalized induction theorem that works on
+ subsets of the accessible part. *)
+lemma acc_subset_induct:
+ assumes subset: "D \<subseteq> acc R"
+ assumes dcl: "\<And>x z. \<lbrakk>x \<in> D; (z, x)\<in>R\<rbrakk> \<Longrightarrow> z \<in> D"
+
+ assumes "x \<in> D"
+ assumes istep: "\<And>x. \<lbrakk>x \<in> D; (\<And>z. (z, x)\<in>R \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
+shows "P x"
+proof -
+ from `x \<in> D` and subset
+ have "x \<in> acc R" ..
+
+ thus "P x" using `x \<in> D`
+ proof (induct x)
+ fix x
+ assume "x \<in> D"
+ and "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<in> D \<Longrightarrow> P y"
+
+ with dcl and istep show "P x" by blast
+ qed
+qed
+
+
+
+
+end
--- a/src/HOL/Bali/DeclConcepts.thy Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy Fri May 05 17:17:21 2006 +0200
@@ -1914,12 +1914,12 @@
next
case Some
with dynM
- have termination: "?Termination"
+ have "termination": "?Termination"
by (auto)
with Some dynM
have "?Dynmethd_def dynC sig=Some dynM"
by (auto simp add: dynmethd_dynC_def)
- with subclseq_super_statC statM dynM termination
+ with subclseq_super_statC statM dynM "termination"
show ?thesis
by (auto simp add: dynmethd_def)
qed
--- a/src/HOL/Datatype.thy Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Datatype.thy Fri May 05 17:17:21 2006 +0200
@@ -6,7 +6,8 @@
header {* Datatypes *}
theory Datatype
-imports Datatype_Universe
+imports Datatype_Universe FunDef
+uses ("Tools/function_package/fundef_datatype.ML")
begin
subsection {* Representing primitive types *}
@@ -314,4 +315,9 @@
ml (target_atom "SOME")
haskell (target_atom "Just")
+
+use "Tools/function_package/fundef_datatype.ML"
+setup FundefDatatype.setup
+
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/FunDef.thy Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,49 @@
+theory FunDef
+imports Accessible_Part
+uses
+("Tools/function_package/fundef_common.ML")
+("Tools/function_package/fundef_lib.ML")
+("Tools/function_package/context_tree.ML")
+("Tools/function_package/fundef_prep.ML")
+("Tools/function_package/fundef_proof.ML")
+("Tools/function_package/termination.ML")
+("Tools/function_package/fundef_package.ML")
+begin
+
+lemma fundef_ex1_existence:
+assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
+assumes ex1: "\<exists>!y. (x,y)\<in>G"
+shows "(x, f x)\<in>G"
+ by (simp only:f_def, rule theI', rule ex1)
+
+lemma fundef_ex1_uniqueness:
+assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
+assumes ex1: "\<exists>!y. (x,y)\<in>G"
+assumes elm: "(x, h x)\<in>G"
+shows "h x = f x"
+ by (simp only:f_def, rule the1_equality[symmetric], rule ex1, rule elm)
+
+lemma fundef_ex1_iff:
+assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
+assumes ex1: "\<exists>!y. (x,y)\<in>G"
+shows "((x, y)\<in>G) = (f x = y)"
+ apply (auto simp:ex1 f_def the1_equality)
+ by (rule theI', rule ex1)
+
+lemma True_implies: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
+ by simp
+
+
+use "Tools/function_package/fundef_common.ML"
+use "Tools/function_package/fundef_lib.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/termination.ML"
+use "Tools/function_package/fundef_package.ML"
+
+setup FundefPackage.setup
+
+
+
+end
--- a/src/HOL/IsaMakefile Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/IsaMakefile Fri May 05 17:17:21 2006 +0200
@@ -120,7 +120,17 @@
antisym_setup.ML arith_data.ML blastdata.ML cladata.ML \
document/root.tex hologic.ML simpdata.ML ResAtpMethods.thy \
Tools/res_atp_provers.ML Tools/res_atp_methods.ML \
- Tools/res_hol_clause.ML
+ Tools/res_hol_clause.ML \
+ Tools/function_package/fundef_common.ML \
+ Tools/function_package/fundef_lib.ML \
+ Tools/function_package/context_tree.ML \
+ Tools/function_package/fundef_prep.ML \
+ Tools/function_package/fundef_proof.ML \
+ Tools/function_package/termination.ML \
+ Tools/function_package/fundef_package.ML \
+ Tools/function_package/auto_term.ML \
+ Tools/function_package/fundef_datatype.ML \
+ FunDef.thy Accessible_Part.thy
@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
@@ -184,7 +194,7 @@
HOL-Library: HOL $(LOG)/HOL-Library.gz
-$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
+$(LOG)/HOL-Library.gz: $(OUT)/HOL \
Library/SetsAndFunctions.thy Library/BigO.thy \
Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
Library/FuncSet.thy Library/Library.thy \
@@ -480,7 +490,7 @@
HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
-$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Library/Accessible_Part.thy \
+$(LOG)/HOL-Lambda.gz: $(OUT)/HOL \
Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \
@@ -740,7 +750,7 @@
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
-$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal Library/Accessible_Part.thy \
+$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy Nominal/Examples/Class.thy \
Nominal/Examples/Fsub.thy Nominal/Examples/Lambda_mu.thy \
Nominal/Examples/Iteration.thy Nominal/Examples/Lam_substs.thy \
--- a/src/HOL/Lambda/ListOrder.thy Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Lambda/ListOrder.thy Fri May 05 17:17:21 2006 +0200
@@ -6,7 +6,7 @@
header {* Lifting an order to lists of elements *}
-theory ListOrder imports Accessible_Part begin
+theory ListOrder imports Main begin
text {*
Lifting an order to lists of elements, relating exactly one
--- a/src/HOL/Library/Accessible_Part.thy Fri May 05 16:50:58 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-(* Title: HOL/Library/Accessible_Part.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-*)
-
-header {* The accessible part of a relation *}
-
-theory Accessible_Part
-imports Main
-begin
-
-subsection {* Inductive definition *}
-
-text {*
- Inductive definition of the accessible part @{term "acc r"} of a
- relation; see also \cite{paulin-tlca}.
-*}
-
-consts
- acc :: "('a \<times> 'a) set => 'a set"
-inductive "acc r"
- intros
- accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
-
-abbreviation
- termi :: "('a \<times> 'a) set => 'a set"
- "termi r == acc (r\<inverse>)"
-
-
-subsection {* Induction rules *}
-
-theorem acc_induct:
- assumes major: "a \<in> acc r"
- assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
- shows "P a"
- apply (rule major [THEN acc.induct])
- apply (rule hyp)
- apply (rule accI)
- apply fast
- apply fast
- done
-
-theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
-
-theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
- apply (erule acc.elims)
- apply fast
- done
-
-lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
- apply (erule rtrancl_induct)
- apply blast
- apply (blast dest: acc_downward)
- done
-
-theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
- apply (blast dest: acc_downwards_aux)
- done
-
-theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
- apply (rule wfUNIVI)
- apply (induct_tac P x rule: acc_induct)
- apply blast
- apply blast
- done
-
-theorem acc_wfD: "wf r ==> x \<in> acc r"
- apply (erule wf_induct)
- apply (rule accI)
- apply blast
- done
-
-theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
- apply (blast intro: acc_wfI dest: acc_wfD)
- done
-
-end
--- a/src/HOL/Library/Library.thy Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Library/Library.thy Fri May 05 17:17:21 2006 +0200
@@ -1,7 +1,6 @@
(*<*)
theory Library
imports
- Accessible_Part
BigO
Continuity
EfficientNat
--- a/src/HOL/Library/Multiset.thy Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Library/Multiset.thy Fri May 05 17:17:21 2006 +0200
@@ -6,7 +6,7 @@
header {* Multisets *}
theory Multiset
-imports Accessible_Part
+imports Main
begin
subsection {* The type of multisets *}
--- a/src/HOL/Nominal/Examples/SN.thy Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy Fri May 05 17:17:21 2006 +0200
@@ -1,7 +1,7 @@
(* $Id$ *)
theory SN
-imports Lam_substs Accessible_Part
+imports Lam_substs
begin
text {* Strong Normalisation proof from the Proofs and Types book *}
--- a/src/HOL/Recdef.thy Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Recdef.thy Fri May 05 17:17:21 2006 +0200
@@ -18,6 +18,7 @@
("../TFL/tfl.ML")
("../TFL/post.ML")
("Tools/recdef_package.ML")
+ ("Tools/function_package/auto_term.ML")
begin
lemma tfl_eq_True: "(x = True) --> x"
@@ -95,4 +96,8 @@
finally show "finite (UNIV :: 'a option set)" .
qed
+
+use "Tools/function_package/auto_term.ML"
+setup FundefAutoTerm.setup
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/auto_term.ML Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,52 @@
+(* Title: HOL/Tools/function_package/auto_term.ML
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+The auto_term method.
+*)
+
+
+signature FUNDEF_AUTO_TERM =
+sig
+ val setup : theory -> theory
+end
+
+structure FundefAutoTerm : FUNDEF_AUTO_TERM =
+struct
+
+open FundefCommon
+open FundefAbbrev
+
+
+
+fun auto_term_tac tc_intro_rule relstr wf_rules ss =
+ (resolve_tac [tc_intro_rule] 1) (* produce the usual goals *)
+ THEN (instantiate_tac [("R", relstr)]) (* instantiate with the given relation *)
+ THEN (ALLGOALS
+ (fn 1 => ares_tac wf_rules 1 (* Solve wellfoundedness *)
+ | i => asm_simp_tac ss i)) (* Simplify termination conditions *)
+
+fun mk_termination_meth relstr ctxt =
+ let
+ val {simps, congs, wfs} = RecdefPackage.get_local_hints ctxt
+ val ss = local_simpset_of ctxt addsimps simps
+
+ val intro_rule = ProofContext.get_thm ctxt (Name "termination_intro")
+ in
+ Method.RAW_METHOD (K (auto_term_tac
+ intro_rule
+ relstr
+ wfs
+ ss))
+ end
+
+
+
+val setup = Method.add_methods [("auto_term", Method.simple_args Args.name mk_termination_meth, "termination prover for recdef compatibility")]
+
+end
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/context_tree.ML Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,240 @@
+(* Title: HOL/Tools/function_package/context_tree.ML
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Builds and traverses trees of nested contexts along a term.
+*)
+
+
+signature FUNDEF_CTXTREE =
+sig
+ type ctx_tree
+
+ (* FIXME: This interface is a mess and needs to be cleaned up! *)
+ val cong_deps : thm -> int FundefCommon.IntGraph.T
+ val add_congs : thm list
+
+ val mk_tree: theory -> (thm * FundefCommon.depgraph) list -> term -> term -> FundefCommon.ctx_tree
+
+ val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list
+
+ val export_term : (string * typ) list * term list -> term -> term
+ val export_thm : theory -> (string * typ) list * term list -> thm -> thm
+ val import_thm : theory -> (string * typ) list * thm list -> thm -> thm
+
+
+ val traverse_tree :
+ ((string * typ) list * thm list -> term ->
+ (((string * typ) list * thm list) * thm) list ->
+ (((string * typ) list * thm list) * thm) list * 'b ->
+ (((string * typ) list * thm list) * thm) list * 'b)
+ -> FundefCommon.ctx_tree -> 'b -> 'b
+
+ val rewrite_by_tree : theory -> 'a -> term -> thm -> (thm * thm) list -> FundefCommon.ctx_tree -> thm * (thm * thm) list
+end
+
+structure FundefCtxTree : FUNDEF_CTXTREE =
+struct
+
+open FundefCommon
+
+
+(* Maps "Trueprop A = B" to "A" *)
+val rhs_of = snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
+(* Maps "A == B" to "B" *)
+val meta_rhs_of = snd o Logic.dest_equals
+
+
+
+(*** Dependency analysis for congruence rules ***)
+
+fun branch_vars t =
+ let val (assumes, term) = dest_implies_list (snd (dest_all_all t))
+ in (fold (curry add_term_vars) assumes [], term_vars term)
+ end
+
+fun cong_deps crule =
+ let
+ val branches = map branch_vars (prems_of crule)
+ val num_branches = (1 upto (length branches)) ~~ branches
+ in
+ IntGraph.empty
+ |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
+ |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
+ (product num_branches num_branches)
+ end
+
+val add_congs = map (fn c => c RS eq_reflection) [cong, ext]
+
+
+
+(* Called on the INSTANTIATED branches of the congruence rule *)
+fun mk_branch t =
+ let
+ val (fixes, impl) = dest_all_all t
+ val (assumes, term) = dest_implies_list impl
+ in
+ (map dest_Free fixes, assumes, rhs_of term)
+ end
+
+
+
+
+
+exception CTREE_INTERNAL of string
+
+fun find_cong_rule thy ((r,dep)::rs) t =
+ (let
+ val (c, subs) = (meta_rhs_of (concl_of r), prems_of r)
+
+ val subst = Pattern.match thy (c, t) (Vartab.empty, Vartab.empty)
+
+ val branches = map (mk_branch o Envir.beta_norm o Envir.subst_vars subst) subs
+ in
+ (r, dep, branches)
+ end
+ handle Pattern.MATCH => find_cong_rule thy rs t)
+ | find_cong_rule thy [] _ = raise CTREE_INTERNAL "No cong rule found!" (* Should never happen *)
+
+
+fun matchcall f (a $ b) = if a = f then SOME b else NONE
+ | matchcall f _ = NONE
+
+fun mk_tree thy congs f t =
+ case matchcall f t of
+ SOME arg => RCall (t, mk_tree thy congs f arg)
+ | NONE =>
+ if not (exists_Const (curry op = (dest_Const f)) t) then Leaf t
+ else
+ let val (r, dep, branches) = find_cong_rule thy congs t in
+ Cong (t, r, dep, map (fn (fixes, assumes, st) =>
+ (fixes, map (assume o cterm_of thy) assumes, mk_tree thy congs f st)) branches)
+ end
+
+
+fun add_context_varnames (Leaf _) = I
+ | add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (curry op ins_string o fst) fs o add_context_varnames st) sub
+ | add_context_varnames (RCall (_,st)) = add_context_varnames st
+
+
+(* Poor man's contexts: Only fixes and assumes *)
+fun compose (fs1, as1) (fs2, as2) = (fs1 @ fs2, as1 @ as2)
+
+fun export_term (fixes, assumes) =
+ fold_rev (curry Logic.mk_implies) assumes #> fold (mk_forall o Free) fixes
+
+fun export_thm thy (fixes, assumes) =
+ fold_rev (implies_intr o cterm_of thy) assumes
+ #> fold_rev (forall_intr o cterm_of thy o Free) fixes
+
+fun import_thm thy (fixes, athms) =
+ fold (forall_elim o cterm_of thy o Free) fixes
+ #> fold implies_elim_swp athms
+
+fun assume_in_ctxt thy (fixes, athms) prop =
+ let
+ val global_assum = export_term (fixes, map prop_of athms) prop
+ in
+ (global_assum,
+ assume (cterm_of thy global_assum) |> import_thm thy (fixes, athms))
+ end
+
+
+(* folds in the order of the dependencies of a graph. *)
+fun fold_deps G f x =
+ let
+ fun fill_table i (T, x) =
+ case Inttab.lookup T i of
+ SOME _ => (T, x)
+ | NONE =>
+ let
+ val (T', x') = fold fill_table (IntGraph.imm_succs G i) (T, x)
+ val (v, x'') = f (the o Inttab.lookup T') i x
+ in
+ (Inttab.update (i, v) T', x'')
+ end
+
+ val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
+ in
+ (Inttab.fold (cons o snd) T [], x)
+ end
+
+
+fun flatten xss = fold_rev append xss []
+
+fun traverse_tree rcOp tr x =
+ let
+ fun traverse_help ctx (Leaf _) u x = ([], x)
+ | traverse_help ctx (RCall (t, st)) u x =
+ rcOp ctx t u (traverse_help ctx st u x)
+ | traverse_help ctx (Cong (t, crule, deps, branches)) u x =
+ let
+ fun sub_step lu i x =
+ let
+ val (fixes, assumes, subtree) = nth branches (i - 1)
+ val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
+ val (subs, x') = traverse_help (compose ctx (fixes, assumes)) subtree used x
+ val exported_subs = map (apfst (compose (fixes, assumes))) subs
+ in
+ (exported_subs, x')
+ end
+ in
+ fold_deps deps sub_step x
+ |> apfst flatten
+ end
+ in
+ snd (traverse_help ([], []) tr [] x)
+ end
+
+
+fun is_refl thm = let val (l,r) = Logic.dest_equals (prop_of thm) in l = r end
+
+fun rewrite_by_tree thy f h ih x tr =
+ let
+ fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
+ | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
+ let
+ val (inner, (Ri,ha)::x') = rewrite_help fix f_as h_as x st
+
+ (* Need not use the simplifier here. Can use primitive steps! *)
+ val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
+
+ val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
+ val iRi = import_thm thy (fix, f_as) Ri (* a < lhs *)
+ val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
+ |> rew_ha
+
+ val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
+ val eq = implies_elim (implies_elim inst_ih iRi) iha
+
+ val h_a'_eq_f_a' = eq RS eq_reflection
+ val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
+ in
+ (result, x')
+ end
+ | rewrite_help fix f_as h_as x (Cong (t, crule, deps, branches)) =
+ let
+ fun sub_step lu i x =
+ let
+ val (fixes, assumes, st) = nth branches (i - 1)
+ val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
+ val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
+ val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
+
+ val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
+ val subeq_exp = export_thm thy (fixes, map prop_of assumes) (subeq RS meta_eq_to_obj_eq)
+ in
+ (subeq_exp, x')
+ end
+
+ val (subthms, x') = fold_deps deps sub_step x
+ in
+ (fold_rev (curry op COMP) subthms crule, x')
+ end
+
+ in
+ rewrite_help [] [] [] x tr
+ end
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_common.ML Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,182 @@
+(* Title: HOL/Tools/function_package/fundef_common.ML
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Common type definitions and other infrastructure.
+*)
+
+structure FundefCommon =
+struct
+
+(* Theory Dependencies *)
+val acc_const_name = "Accessible_Part.acc"
+
+
+
+(* Partial orders to represent dependencies *)
+structure IntGraph = GraphFun(type key = int val ord = int_ord);
+
+type depgraph = int IntGraph.T
+
+
+datatype ctx_tree
+ = Leaf of term
+ | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
+ | RCall of (term * ctx_tree)
+
+
+
+(* A record containing all the relevant symbols and types needed during the proof.
+ This is set up at the beginning and does not change. *)
+type naming_context =
+ { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ,
+ G: term, R: term, acc_R: term, h: term, y: term, x: term, z: term, a:term, P: term,
+ D: term, Pbool:term,
+ glrs: (term list * term list * term * term) list,
+ glrs': (term list * term list * term * term) list,
+ f_def: thm,
+ used: string list,
+ trees: ctx_tree list
+ }
+
+
+type rec_call_info =
+ {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm}
+
+type clause_info =
+ {
+ no: int,
+
+ qs: term list,
+ gs: term list,
+ lhs: term,
+ rhs: term,
+
+ cqs: cterm list,
+ cvqs: cterm list,
+ ags: thm list,
+
+ cqs': cterm list,
+ ags': thm list,
+ lhs': term,
+ rhs': term,
+ ordcqs': cterm list,
+
+ GI: thm,
+ lGI: thm,
+ RCs: rec_call_info list,
+
+ tree: ctx_tree,
+ case_hyp: thm
+ }
+
+
+type curry_info =
+ { argTs: typ list, curry_ss: simpset }
+
+
+type prep_result =
+ {
+ names: naming_context,
+ complete : term,
+ compat : term list,
+ clauses: clause_info list
+ }
+
+type fundef_result =
+ {
+ f: term,
+ G : term,
+ R : term,
+ completeness : thm,
+ compatibility : thm list,
+
+ psimps : thm list,
+ subset_pinduct : thm,
+ simple_pinduct : thm,
+ total_intro : thm,
+ dom_intros : thm list
+ }
+
+
+structure FundefData = TheoryDataFun
+(struct
+ val name = "HOL/function_def/data";
+ type T = string * fundef_result Symtab.table
+
+ val empty = ("", Symtab.empty);
+ val copy = I;
+ val extend = I;
+ fun merge _ ((l1,tab1),(l2,tab2)) = (l1, Symtab.merge (op =) (tab1, tab2))
+
+ fun print _ _ = ();
+end);
+
+
+structure FundefCongs = GenericDataFun
+(struct
+ val name = "HOL/function_def/congs"
+ type T = thm list
+ val empty = []
+ val extend = I
+ fun merge _ (l1, l2) = l1 @ l2
+ fun print _ _ = ()
+end);
+
+
+fun add_fundef_data name fundef_data =
+ FundefData.map (fn (_,tab) => (name, Symtab.update_new (name, fundef_data) tab))
+
+fun get_fundef_data name thy = Symtab.lookup (snd (FundefData.get thy)) name
+
+fun get_last_fundef thy = fst (FundefData.get thy)
+
+val map_fundef_congs = FundefCongs.map
+val get_fundef_congs = FundefCongs.get
+
+end
+
+
+
+(* Common Abbreviations *)
+
+structure FundefAbbrev =
+struct
+
+fun implies_elim_swp x y = implies_elim y x
+
+(* Some HOL things frequently used *)
+val boolT = HOLogic.boolT
+val mk_prod = HOLogic.mk_prod
+val mk_mem = HOLogic.mk_mem
+val mk_eq = HOLogic.mk_eq
+val Trueprop = HOLogic.mk_Trueprop
+
+val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
+fun mk_relmem (x,y) R = Trueprop (mk_mem (mk_prod (x, y), R))
+
+fun mk_subset T A B =
+ let val sT = HOLogic.mk_setT T
+ in Const ("Orderings.less_eq", sT --> sT --> boolT) $ A $ B end
+
+
+(* with explicit types: Needed with loose bounds *)
+fun mk_relmemT xT yT (x,y) R =
+ let
+ val pT = HOLogic.mk_prodT (xT, yT)
+ val RT = HOLogic.mk_setT pT
+ in
+ Const ("op :", [pT, RT] ---> boolT)
+ $ (HOLogic.pair_const xT yT $ x $ y)
+ $ R
+ end
+
+fun free_to_var (Free (v,T)) = Var ((v,0),T)
+ | free_to_var _ = raise Match
+
+fun var_to_free (Var ((v,_),T)) = Free (v,T)
+ | var_to_free _ = raise Match
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,167 @@
+(* Title: HOL/Tools/function_package/fundef_datatype.ML
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+A tactic to prove completeness of datatype patterns.
+*)
+
+signature FUNDEF_DATATYPE =
+sig
+ val pat_complete_tac: int -> tactic
+
+ val setup : theory -> theory
+end
+
+
+
+structure FundefDatatype : FUNDEF_DATATYPE =
+struct
+
+fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
+fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
+
+fun inst_free var inst thm =
+ forall_elim inst (forall_intr var thm)
+
+
+fun inst_case_thm thy x P thm =
+ let
+ val [Pv, xv] = term_vars (prop_of thm)
+ in
+ cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
+ end
+
+
+fun invent_vars constr i =
+ let
+ val Ts = binder_types (fastype_of constr)
+ val j = i + length Ts
+ val is = i upto (j - 1)
+ val avs = map2 mk_argvar is Ts
+ val pvs = map2 mk_patvar is Ts
+ in
+ (avs, pvs, j)
+ end
+
+
+fun filter_pats thy cons pvars [] = []
+ | filter_pats thy cons pvars (([], thm) :: pts) = raise Match
+ | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
+ case pat of
+ Free _ => let val inst = list_comb (cons, pvars)
+ in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm)
+ :: (filter_pats thy cons pvars pts) end
+ | _ => if fst (strip_comb pat) = cons
+ then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
+ else filter_pats thy cons pvars pts
+
+
+fun inst_constrs_of thy (T as Type (name, _)) =
+ map (fn (Cn,CT) => Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+ (the (DatatypePackage.get_datatype_constrs thy name))
+ | inst_constrs_of thy _ = raise Match
+
+
+fun transform_pat thy avars c_assum ([] , thm) = raise Match
+ | transform_pat thy avars c_assum (pat :: pats, thm) =
+ let
+ val (_, subps) = strip_comb pat
+ val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
+ val a_eqs = map assume eqs
+ val c_eq_pat = simplify (HOL_basic_ss addsimps a_eqs) c_assum
+ in
+ (subps @ pats, fold_rev implies_intr eqs
+ (implies_elim thm c_eq_pat))
+ end
+
+
+exception COMPLETENESS
+
+fun constr_case thy P idx (v :: vs) pats cons =
+ let
+ val (avars, pvars, newidx) = invent_vars cons idx
+ val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
+ val c_assum = assume c_hyp
+ val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
+ in
+ o_alg thy P newidx (avars @ vs) newpats
+ |> implies_intr c_hyp
+ |> fold_rev (forall_intr o cterm_of thy) avars
+ end
+ | constr_case _ _ _ _ _ _ = raise Match
+and o_alg thy P idx [] (([], Pthm) :: _) = Pthm
+ | o_alg thy P idx (v :: vs) [] = raise COMPLETENESS
+ | o_alg thy P idx (v :: vs) pts =
+ if forall (is_Free o hd o fst) pts (* Var case *)
+ then o_alg thy P idx vs (map (fn (pv :: pats, thm) =>
+ (pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
+ else (* Cons case *)
+ let
+ val T = fastype_of v
+ val (tname, _) = dest_Type T
+ val {exhaustion=case_thm, ...} = DatatypePackage.the_datatype thy tname
+ val constrs = inst_constrs_of thy T
+ val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
+ in
+ inst_case_thm thy v P case_thm
+ |> fold (curry op COMP) c_cases
+ end
+ | o_alg _ _ _ _ _ = raise Match
+
+
+fun prove_completeness thy x P qss pats =
+ let
+ fun mk_assum qs pat = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x,pat)),
+ HOLogic.mk_Trueprop P)
+ |> fold_rev mk_forall qs
+ |> cterm_of thy
+
+ val hyps = map2 mk_assum qss pats
+
+ fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
+
+ val assums = map2 inst_hyps hyps qss
+ in
+ o_alg thy P 2 [x] (map2 (pair o single) pats assums)
+ |> fold_rev implies_intr hyps
+ |> zero_var_indexes
+ |> forall_intr_frees
+ |> forall_elim_vars 0
+ end
+
+
+
+fun pat_complete_tac i thm =
+ let
+ val subgoal = nth (prems_of thm) (i - 1)
+ val assums = Logic.strip_imp_prems subgoal
+ val _ $ P = Logic.strip_imp_concl subgoal
+
+ fun pat_of assum =
+ let
+ val (qs, imp) = dest_all_all assum
+ in
+ case Logic.dest_implies imp of
+ (_ $ (_ $ x $ pat), _) => (x, (qs, pat))
+ | _ => raise COMPLETENESS
+ end
+
+ val (x, (qss, pats)) =
+ case (map pat_of assums) of
+ [] => raise COMPLETENESS
+ | rs as ((x,_) :: _)
+ => (x, split_list (snd (split_list rs)))
+
+ val complete_thm = prove_completeness (theory_of_thm thm) x P qss pats
+ in
+ Seq.single (Drule.compose_single(complete_thm, i, thm))
+ end
+ handle COMPLETENESS => Seq.empty
+
+
+
+val setup =
+ Method.add_methods [("pat_completeness", Method.no_args (Method.SIMPLE_METHOD (pat_complete_tac 1)), "Completeness prover for datatype patterns")]
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,64 @@
+(* Title: HOL/Tools/function_package/lib.ML
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Some fairly general functions that should probably go somewhere else...
+*)
+
+
+fun mk_forall (var as Free (v,T)) t =
+ all T $ Abs (v,T, abstract_over (var,t))
+ | mk_forall _ _ = raise Match
+
+(* Builds a quantification with a new name for the variable. *)
+fun mk_forall_rename ((v,T),newname) t =
+ all T $ Abs (newname,T, abstract_over (Free (v,T),t))
+
+(* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
+fun tupled_lambda vars t =
+ case vars of
+ (Free v) => lambda (Free v) t
+ | (Var v) => lambda (Var v) t
+ | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
+ (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
+ | _ => raise Match
+
+
+fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
+ let
+ val (n, body) = Term.dest_abs a
+ in
+ (Free (n, T), body)
+ end
+ | dest_all _ = raise Match
+
+
+(* Removes all quantifiers from a term, replacing bound variables by frees. *)
+fun dest_all_all (t as (Const ("all",_) $ _)) =
+ let
+ val (v,b) = dest_all t
+ val (vs, b') = dest_all_all b
+ in
+ (v :: vs, b')
+ end
+ | dest_all_all t = ([],t)
+
+(* unfold *)
+fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x)
+
+val dest_implies_list =
+ split_last o (unfold Logic.is_implies (fst o Logic.dest_implies) (snd o Logic.dest_implies) single)
+
+fun implies_elim_swp a b = implies_elim b a
+
+fun map3 _ [] [] [] = []
+ | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
+ | map3 _ _ _ _ = raise UnequalLengths;
+
+
+
+(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
+fun upairs [] = []
+ | upairs (x::xs) = map (pair x) (x::xs) @ upairs xs
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_package.ML Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,197 @@
+(* Title: HOL/Tools/function_package/fundef_package.ML
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Isar commands.
+
+*)
+
+signature FUNDEF_PACKAGE =
+sig
+ val add_fundef : ((bstring * Attrib.src list) * string) list -> theory -> Proof.state (* Need an _i variant *)
+
+ val cong_add: attribute
+ val cong_del: attribute
+
+ val setup : theory -> theory
+end
+
+
+structure FundefPackage : FUNDEF_PACKAGE =
+struct
+
+open FundefCommon
+
+val True_implies = thm "True_implies"
+
+
+(*#> FundefTermination.setup #> FundefDatatype.setup*)
+
+fun fundef_afterqed congs curry_info name data natts thmss thy =
+ let
+ val (complete_thm :: compat_thms) = map hd thmss
+ val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
+ val {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
+
+ val (names, attsrcs) = split_list natts
+ val atts = map (map (Attrib.attribute thy)) attsrcs
+
+ val accR = (#acc_R(#names(data)))
+ val dom_abbrev = Logic.mk_equals (Free ("dom", fastype_of accR), accR)
+
+ val thy = thy |> Theory.add_path name
+
+ val thy = thy |> Theory.add_path "psimps"
+ val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy;
+ val thy = thy |> Theory.parent_path
+
+ val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
+ val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy
+ val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy
+ val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy
+ val (_,thy) = PureThy.add_thms [(("pinduct", simple_pinduct), [RuleCases.case_names names, InductAttrib.induct_set ""])] thy
+ val (_, thy) = PureThy.add_thmss [(("psimps", psimps), [Simplifier.simp_add])] thy
+ val thy = thy |> Theory.parent_path
+ in
+ add_fundef_data name fundef_data thy
+ end
+
+fun add_fundef eqns_atts thy =
+ let
+ val (natts, eqns) = split_list eqns_atts
+
+ val congs = get_fundef_congs (Context.Theory thy)
+
+ val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs (map (Sign.read_prop thy) eqns) thy
+ val {complete, compat, ...} = data
+
+ val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
+ in
+ thy |> ProofContext.init
+ |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data natts) NONE ("", [])
+ (map (fn t => (("", []), [(t, ([], []))])) props)
+ end
+
+
+fun total_termination_afterqed name thmss thy =
+ let
+ val totality = hd (hd thmss)
+
+ val {psimps, simple_pinduct, ... }
+ = the (get_fundef_data name thy)
+
+ val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
+
+ val tsimps = map remove_domain_condition psimps
+ val tinduct = remove_domain_condition simple_pinduct
+
+ val thy = Theory.add_path name thy
+
+ (* Need the names and attributes. Apply the attributes again? *)
+(* val thy = thy |> Theory.add_path "simps"
+ val (_, thy) = PureThy.add_thms ((names ~~ tsimps) ~~ atts) thy;
+ val thy = thy |> Theory.parent_path*)
+
+ val (_, thy) = PureThy.add_thms [(("induct", tinduct), [])] thy
+ val (_, thy) = PureThy.add_thmss [(("simps", tsimps), [Simplifier.simp_add, RecfunCodegen.add NONE])] thy
+ val thy = Theory.parent_path thy
+ in
+ thy
+ end
+
+(*
+fun mk_partial_rules name D_name D domT idomT thmss thy =
+ let
+ val [subs, dcl] = (hd thmss)
+
+ val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
+ = the (Symtab.lookup (FundefData.get thy) name)
+
+ val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)]
+ [SOME (cterm_of thy D)]
+ subsetD)
+
+ val D_simps = map (curry op RS D_implies_dom) f_simps
+
+ val D_induct = subset_induct
+ |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
+ |> curry op COMP subs
+ |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
+ |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
+
+ val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
+ val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
+ in
+ thy3
+ end
+*)
+
+
+fun fundef_setup_termination_proof name NONE thy =
+ let
+ val name = if name = "" then get_last_fundef thy else name
+ val data = the (get_fundef_data name thy)
+
+ val {total_intro, ...} = data
+ val goal = FundefTermination.mk_total_termination_goal data
+ in
+ thy |> ProofContext.init
+ |> ProofContext.note_thmss_i [(("termination_intro",
+ [ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd
+ |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", [])
+ [(("", []), [(goal, ([], []))])]
+ end
+ | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
+ let
+ val name = if name = "" then get_last_fundef thy else name
+ val data = the (get_fundef_data name thy)
+ val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
+ in
+ thy |> ProofContext.init
+ |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
+ [(("", []), [(subs, ([], [])), (dcl, ([], []))])]
+ end
+
+
+
+
+(* congruence rules *)
+
+val cong_add = Thm.declaration_attribute (map_fundef_congs o cons o safe_mk_meta_eq);
+val cong_del = Thm.declaration_attribute (map_fundef_congs o remove (op =) o safe_mk_meta_eq);
+
+
+(* setup *)
+
+val setup = FundefData.init #> FundefCongs.init
+ #> Attrib.add_attributes
+ [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
+
+
+(* outer syntax *)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val function_decl =
+ Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
+
+val functionP =
+ OuterSyntax.command "function" "define general recursive functions" K.thy_goal
+ (function_decl >> (fn eqns =>
+ Toplevel.print o Toplevel.theory_to_proof (add_fundef eqns)));
+
+val terminationP =
+ OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
+ ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
+ >> (fn (name,dom) =>
+ Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
+
+val _ = OuterSyntax.add_parsers [functionP];
+val _ = OuterSyntax.add_parsers [terminationP];
+
+
+end;
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,355 @@
+(* 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_curried : thm list -> term list -> theory
+ -> FundefCommon.curry_info option * xstring * (FundefCommon.prep_result * theory)
+end
+
+
+
+
+
+structure FundefPrep : FUNDEF_PREP =
+struct
+
+
+open FundefCommon
+open FundefAbbrev
+
+
+
+
+fun split_list3 [] = ([],[],[])
+ | split_list3 ((x,y,z)::xyzs) =
+ let
+ val (xs, ys, zs) = split_list3 xyzs
+ in
+ (x::xs,y::ys,z::zs)
+ end
+
+
+fun build_tree thy f congs (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)
+ in
+ FundefCtxTree.mk_tree thy congs_deps f rhs
+ end
+
+
+fun analyze_eqs eqs =
+ let
+ fun dest_geq geq =
+ let
+ val qs = add_term_frees (geq, [])
+ in
+ case dest_implies_list geq of
+ (gs, Const ("Trueprop", _) $ (Const ("op =", _) $ (f $ lhs) $ rhs)) =>
+ (f, (qs, gs, lhs, rhs))
+ | _ => raise ERROR "Not a guarded equation"
+ end
+
+ val (fs, glrs) = split_list (map dest_geq eqs)
+
+ val f = (hd fs) (* should be equal and a constant... check! *)
+
+ val used = fold (curry add_term_names) eqs [] (* all names in the eqs *)
+ (* Must check for recursive calls in guards and new vars in rhss *)
+ in
+ (f, glrs, used)
+ end
+
+
+(* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
+fun mk_primed_vars thy glrs =
+ let
+ val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
+
+ fun rename_vars (qs,gs,lhs,rhs) =
+ let
+ val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
+ val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
+ in
+ (qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
+ end
+ in
+ map rename_vars glrs
+ end
+
+
+fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs =
+ let
+ val {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 = 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 = freezeT RI
+ val lRI = localize RI
+ val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
+
+ 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
+ {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
+ end
+
+ val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
+ in
+ {
+ 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) fname congs thy =
+ let
+ val trees = map (build_tree thy f congs) glrs
+ val allused = fold FundefCtxTree.add_context_varnames trees used
+
+ val Const (f_proper_name, fT) = f
+ val fxname = Sign.extern_const thy f_proper_name
+
+ 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 = fname ^ "_graph"
+ val R_name = fname ^ "_rel"
+
+ val glrs' = mk_primed_vars thy glrs
+
+ val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
+
+ val G = Const (Sign.intern_const thy G_name, GT)
+ val R = Const (Sign.intern_const thy R_name, RT)
+ val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
+
+ val f_eq = Logic.mk_equals (f $ x,
+ Const ("The", (ranT --> boolT) --> ranT) $
+ Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
+
+ val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", f_eq), [])] thy
+ in
+ ({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)
+ end
+
+
+(* 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')
+
+
+(* 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
+
+fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
+ let
+ val { 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
+ val {domT, x, Pbool, ...} = names
+
+ fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
+ |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev mk_forall qs
+ in
+ Trueprop Pbool
+ |> fold_rev (curry Logic.mk_implies o mk_case) glrs
+ end
+
+
+fun extract_conditions thy names trees congs =
+ let
+ val {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
+
+ 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*)
+ 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 *)
+ [] (* no special monos *)
+ thy
+ in
+ (intrs, (thy, elim))
+ 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 congs eqs fname thy =
+ let
+ val (names, thy) = setup_context (analyze_eqs eqs) fname congs thy
+ val {G, R, glrs, trees, ...} = names
+
+ val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
+
+ 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 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)
+ in
+ ({names = names, complete=complete, compat=compat, clauses = clauses},
+ thy)
+ end
+
+
+
+
+fun prepare_fundef_curried congs eqs thy =
+ let
+ val lhs1 = hd eqs
+ |> dest_implies_list |> snd
+ |> HOLogic.dest_Trueprop
+ |> HOLogic.dest_eq |> fst
+
+ val (f, args) = strip_comb lhs1
+ val Const(fname, fT) = f
+ val fxname = Sign.extern_const thy fname
+ in
+ if (length args < 2)
+ then (NONE, fxname, (prepare_fundef congs eqs fxname thy))
+ else
+ let
+ val (caTs, uaTs) = chop (length args) (binder_types fT)
+ val newtype = foldr1 HOLogic.mk_prodT caTs --> (uaTs ---> body_type fT)
+ val gxname = fxname ^ "_tupled"
+
+ val thy = Sign.add_consts_i [(gxname, newtype, NoSyn)] thy
+ val gc = Const (Sign.intern_const thy gxname, newtype)
+
+ val vars = map2 (fn i => fn T => Free ("x"^(string_of_int i), T))
+ (1 upto (length caTs)) caTs
+
+ val f_lambda = fold_rev lambda vars (gc $ foldr1 HOLogic.mk_prod vars)
+
+ val def = Logic.mk_equals (fold (curry ((op $) o Library.swap)) vars f,
+ gc $ foldr1 HOLogic.mk_prod vars)
+
+ val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy
+
+ val g_to_f_ss = HOL_basic_ss addsimps [symmetric f_def]
+ val eqs_tupled = map (Pattern.rewrite_term thy [(f, f_lambda)] []) eqs
+ in
+ (SOME {curry_ss = g_to_f_ss, argTs = caTs}, fxname, prepare_fundef congs eqs_tupled fxname thy)
+ end
+ end
+
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/fundef_proof.ML Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,585 @@
+(* 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_curried : theory -> thm list -> FundefCommon.curry_info option -> FundefCommon.prep_result
+ -> thm -> thm list -> FundefCommon.fundef_result
+end
+
+
+structure FundefProof : FUNDEF_PROOF =
+struct
+
+open FundefCommon
+open FundefAbbrev
+
+(* Theory dependencies *)
+val subsetD = thm "subsetD"
+val subset_refl = thm "subset_refl"
+val split_apply = thm "Product_Type.split"
+val wf_induct_rule = thm "wf_induct_rule";
+val Pair_inject = thm "Product_Type.Pair_inject";
+
+val acc_induct_rule = thm "acc_induct_rule" (* from: Accessible_Part *)
+val acc_downward = thm "acc_downward"
+val accI = thm "accI"
+
+val ex1_implies_ex = thm "fundef_ex1_existence" (* from: Fundef.thy *)
+val ex1_implies_un = thm "fundef_ex1_uniqueness"
+val ex1_implies_iff = thm "fundef_ex1_iff"
+val acc_subset_induct = thm "acc_subset_induct"
+
+
+
+
+
+
+fun mk_simp thy (names:naming_context) f_iff graph_is_function clause valthm =
+ let
+ val {R, acc_R, domT, z, ...} = names
+ val {qs, cqs, gs, lhs, rhs, ...} = clause
+ val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, acc_R))) (* "lhs : acc R" *)
+ val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *)
+ 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 forall_intr cqs
+ |> forall_elim_vars 0
+ |> varifyT
+ |> Drule.close_derivation
+ end
+
+
+
+
+fun mk_partial_induct_rule thy (names:naming_context) complete_thm clauses =
+ let
+ val {domT, R, acc_R, x, z, a, P, D, ...} = names
+
+ val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D))))
+ val a_D = cterm_of thy (Trueprop (mk_mem (a, D)))
+
+ val D_subset = cterm_of thy (Trueprop (mk_subset domT D acc_R))
+
+ val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
+ mk_forall x
+ (mk_forall z (Logic.mk_implies (Trueprop (mk_mem (x, D)),
+ Logic.mk_implies (mk_relmem (z, x) R,
+ Trueprop (mk_mem (z, D))))))
+ |> cterm_of thy
+
+
+ (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
+ val ihyp = all domT $ Abs ("z", domT,
+ implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
+ $ Trueprop (P $ Bound 0))
+ |> cterm_of thy
+
+ val aihyp = assume ihyp |> forall_elim_vars 0
+
+ fun prove_case clause =
+ let
+ val {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = 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
+
+ (* FIXME: Variable order destroyed by forall_intr_vars *)
+ val P_recs = map (fn {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) 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 (mk_mem (lhs, D)))
+ |> fold_rev mk_forall 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
+ |> 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
+ |> forall_intr_frees
+ |> forall_elim_vars 0
+
+ val simple_induct_rule =
+ subset_induct_rule
+ |> instantiate' [] [SOME (cterm_of thy acc_R)]
+ |> (curry op COMP) subset_refl
+ |> (curry op COMP) (acc_downward
+ |> (instantiate' [SOME (ctyp_of thy domT)]
+ (map (SOME o cterm_of thy) [x, R, z]))
+ |> forall_intr (cterm_of thy z)
+ |> forall_intr (cterm_of thy x))
+ in
+ (varifyT subset_induct_rule, varifyT simple_induct_rule)
+ end
+
+
+
+
+
+(***********************************************)
+(* Compat thms are stored in normal form (with vars) *)
+
+(* replace this by a table later*)
+fun store_compat_thms 0 cts = []
+ | store_compat_thms n cts =
+ let
+ val (cts1, cts2) = chop n cts
+ in
+ (cts1 :: store_compat_thms (n - 1) cts2)
+ end
+
+
+(* needs i <= j *)
+fun lookup_compat_thm i j cts =
+ nth (nth cts (i - 1)) (j - i)
+(***********************************************)
+
+
+(* recover the order of Vars *)
+fun get_var_order thy (clauses: clause_info list) =
+ map (fn ({cqs,...}, {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
+
+
+(* 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 {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
+ val {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 (var_ord, compat) = lookup_compat_thm j i cts
+ in
+ compat (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
+ |> instantiate ([],(var_ord ~~ (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 (var_ord, compat) = lookup_compat_thm i j cts
+ in
+ compat (* "?Gsi => ?Gsj' => ?lhsi = ?lhsj' ==> ?rhsi = ?rhsj'" *)
+ |> instantiate ([], (var_ord ~~ (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 {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names
+ val {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 #lRIq RCs
+ val h_assums = map #Gh RCs
+ val h_assums' = map #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:naming_context) compat_store (clausei:clause_info) (clausej:clause_info) RLj =
+ let
+ val {f, h, y, ...} = names
+ val {no=i, lhs=lhsi, case_hyp, ...} = clausei
+ val {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 {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:naming_context) ihyp ih_intro G_cases compat_store clauses rep_lemmas (clausei:clause_info) =
+ let
+ val {x, y, G, fvar, f, ranT, ...} = names
+ val {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 ({lRIq,RIvs, ...} : rec_call_info) = 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
+
+ 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
+ |> instantiate' [] [SOME a, SOME 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
+
+
+
+(* Does this work with Guards??? *)
+fun mk_domain_intro thy (names:naming_context) R_cases clause =
+ let
+ val {z, R, acc_R, ...} = names
+ val {qs, gs, lhs, rhs, ...} = clause
+
+ val z_lhs = cterm_of thy (HOLogic.mk_prod (z,lhs))
+ val z_acc = cterm_of thy (HOLogic.mk_mem (z,acc_R))
+
+ val icases = R_cases
+ |> instantiate' [] [SOME z_lhs, SOME z_acc]
+ |> forall_intr_frees
+ |> forall_elim_vars 0
+
+ val goal = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
+ in
+ Goal.init goal
+ |> SINGLE (resolve_tac [accI] 1) |> the
+ |> SINGLE (eresolve_tac [icases] 1) |> the
+ |> SINGLE (CLASIMPSET auto_tac) |> the
+ |> Goal.conclude
+ |> forall_intr_frees
+ |> forall_elim_vars 0
+ |> varifyT
+ end
+
+
+
+
+fun mk_nest_term_case thy (names:naming_context) R' ihyp clause =
+ let
+ val {x, z, ...} = names
+ val {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = 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 = mk_relmem (arg, lhs) R'
+ |> 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 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 zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs))))
+
+ val z_acc' = z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject)
+
+ val ethm = z_acc'
+ |> FundefCtxTree.export_thm thy (fixes, (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes))
+ |> fold_rev forall_intr 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 (names:naming_context) clauses =
+ let
+ val { R, acc_R, domT, x, z, ... } = names
+
+ val R_elim = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R))))))
+
+ val R' = Free ("R", fastype_of R)
+
+ val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wf", mk_relT (domT, domT) --> boolT) $ R')) (* "wf R'" *)
+
+ (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
+ val ihyp = all domT $ Abs ("z", domT,
+ implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R')
+ $ Trueprop ((Const ("op :", [domT, HOLogic.mk_setT domT] ---> boolT))
+ $ Bound 0 $ acc_R))
+ |> cterm_of thy
+
+ val ihyp_a = assume ihyp |> forall_elim_vars 0
+
+ val z_ltR_x = cterm_of thy (mk_relmem (z, x) R) (* "(z, x) : R" *)
+ val z_acc = cterm_of thy (mk_mem (z, acc_R))
+
+ val (hyps,cases) = fold (mk_nest_term_case thy names R' ihyp_a) clauses ([],[])
+ in
+ R_elim
+ |> freezeT
+ |> instantiate' [] [SOME (cterm_of thy (mk_prod (z,x))), SOME z_acc]
+ |> curry op COMP (assume z_ltR_x)
+ |> fold_rev (curry op COMP) cases
+ |> implies_intr z_ltR_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))
+ |> implies_elim_swp (assume wfR')
+ |> 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 =
+ let
+ val {names, clauses, complete, compat, ...} = data
+ val {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 complete_thm_fr = freezeT complete_thm
+ val compat_thms_fr = map freezeT compat_thms
+ val f_def_fr = 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 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)))))) |> freezeT
+ val G_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const G)))))) |> 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 _ = 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 f_iff = (graph_is_function RS inst_ex1_iff)
+
+ val _ = Output.debug "Proving simplification rules"
+ val psimps = map2 (mk_simp thy names f_iff graph_is_function) clauses values
+
+ val _ = Output.debug "Proving partial induction rule"
+ val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy names complete_thm clauses
+
+ val _ = Output.debug "Proving nested termination rule"
+ val total_intro = mk_nest_term_rule thy names clauses
+
+ val _ = Output.debug "Proving domain introduction rules"
+ val dom_intros = map (mk_domain_intro thy names R_cases) clauses
+ in
+ {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm,
+ psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
+ dom_intros=dom_intros}
+ end
+
+
+fun curry_induct_rule thy argTs induct =
+ let
+ val vnums = (1 upto (length argTs))
+ val avars = map2 (fn T => fn i => Var (("a",i), T)) argTs vnums
+ val atup = foldr1 HOLogic.mk_prod avars
+ val Q = Var (("P",1),argTs ---> HOLogic.boolT)
+ val P = tupled_lambda atup (list_comb (Q, avars))
+ in
+ induct |> freezeT
+ |> instantiate' [] [SOME (cterm_of thy atup), SOME (cterm_of thy P)]
+ |> zero_var_indexes
+ |> full_simplify (HOL_basic_ss addsimps [split_apply])
+ |> varifyT
+ end
+
+
+
+fun mk_partial_rules_curried thy congs NONE data complete_thm compat_thms =
+ mk_partial_rules thy congs data complete_thm compat_thms
+ | mk_partial_rules_curried thy congs (SOME {curry_ss, argTs}) data complete_thm compat_thms =
+ let
+ val {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} =
+ mk_partial_rules thy congs data complete_thm compat_thms
+ val cpsimps = map (simplify curry_ss) psimps
+ val cpinduct = full_simplify curry_ss simple_pinduct
+ |> curry_induct_rule thy argTs
+ val cdom_intros = map (full_simplify curry_ss) dom_intros
+ val ctotal_intro = full_simplify curry_ss total_intro
+ in
+ {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm,
+ psimps=cpsimps, subset_pinduct=subset_pinduct, simple_pinduct=cpinduct, total_intro=ctotal_intro, dom_intros=cdom_intros}
+ end
+
+end
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/termination.ML Fri May 05 17:17:21 2006 +0200
@@ -0,0 +1,67 @@
+(* Title: HOL/Tools/function_package/termination.ML
+ ID: $Id$
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Termination goals...
+*)
+
+
+signature FUNDEF_TERMINATION =
+sig
+ val mk_total_termination_goal : FundefCommon.fundef_result -> term
+ val mk_partial_termination_goal : theory -> FundefCommon.fundef_result -> string -> term * term
+end
+
+structure FundefTermination : FUNDEF_TERMINATION =
+struct
+
+
+open FundefCommon
+open FundefAbbrev
+
+fun mk_total_termination_goal (data: fundef_result) =
+ let
+ val {R, f, ... } = data
+
+ val domT = domain_type (fastype_of f)
+ val x = Free ("x", domT)
+ in
+ Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
+ end
+
+fun mk_partial_termination_goal thy (data: fundef_result) dom =
+ let
+ val {R, f, ... } = data
+
+ val domT = domain_type (fastype_of f)
+ val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom
+ val DT = type_of D
+ val idomT = HOLogic.dest_setT DT
+
+ val x = Free ("x", idomT)
+ val z = Free ("z", idomT)
+ val Rname = fst (dest_Const R)
+ val iRT = mk_relT (idomT, idomT)
+ val iR = Const (Rname, iRT)
+
+
+ val subs = HOLogic.mk_Trueprop
+ (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
+ (Const (acc_const_name, iRT --> DT) $ iR))
+ |> Type.freeze
+
+ val dcl = mk_forall x
+ (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
+ Logic.mk_implies (mk_relmem (z, x) iR,
+ Trueprop (mk_mem (z, D))))))
+ |> Type.freeze
+ in
+ (subs, dcl)
+ end
+
+end
+
+
+
+
--- a/src/HOL/Tools/recdef_package.ML Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Tools/recdef_package.ML Fri May 05 17:17:21 2006 +0200
@@ -30,7 +30,7 @@
val recdef_tc_i: bstring * attribute list -> string -> int option -> theory -> Proof.state
val setup: theory -> theory
-(* HACK: This has to be exported, since the new recdef-package uses the same hints *)
+(* HACK: This has to be exported, since the new fundef-package uses the same hints *)
val get_local_hints: ProofContext.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
val get_global_hints: theory -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
end;
@@ -300,7 +300,7 @@
LocalRecdefData.init #>
Attrib.add_attributes
[(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
- (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
+ (recdef_congN, Attrib.add_del_args (FundefPackage.cong_add o cong_add) (FundefPackage.cong_del o cong_del), "declaration of recdef cong rule"),
(recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];