First usable version of the new function definition package (HOL/function_packake/...).
authorkrauss
Fri May 05 17:17:21 2006 +0200 (2006-05-05)
changeset 19564d3e2f532459a
parent 19563 ddd36d9e6943
child 19565 67d1792dc0f2
First usable version of the new function definition package (HOL/function_packake/...).
Moved Accessible_Part.thy from Library to Main.
etc/isar-keywords-HOL-Nominal.el
etc/isar-keywords.el
src/HOL/Accessible_Part.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Datatype.thy
src/HOL/FunDef.thy
src/HOL/IsaMakefile
src/HOL/Lambda/ListOrder.thy
src/HOL/Library/Accessible_Part.thy
src/HOL/Library/Library.thy
src/HOL/Library/Multiset.thy
src/HOL/Nominal/Examples/SN.thy
src/HOL/Recdef.thy
src/HOL/Tools/function_package/auto_term.ML
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/function_package/fundef_proof.ML
src/HOL/Tools/function_package/termination.ML
src/HOL/Tools/recdef_package.ML
     1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Fri May 05 16:50:58 2006 +0200
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Fri May 05 17:17:21 2006 +0200
     1.3 @@ -82,6 +82,7 @@
     1.4      "fix"
     1.5      "from"
     1.6      "full_prf"
     1.7 +    "function"
     1.8      "global"
     1.9      "guess"
    1.10      "have"
    1.11 @@ -174,6 +175,7 @@
    1.12      "subsubsection"
    1.13      "syntax"
    1.14      "term"
    1.15 +    "termination"
    1.16      "text"
    1.17      "text_raw"
    1.18      "then"
    1.19 @@ -423,11 +425,13 @@
    1.20  (defconst isar-keywords-theory-goal
    1.21    '("ax_specification"
    1.22      "corollary"
    1.23 +    "function"
    1.24      "instance"
    1.25      "interpretation"
    1.26      "lemma"
    1.27      "recdef_tc"
    1.28      "specification"
    1.29 +    "termination"
    1.30      "theorem"
    1.31      "typedef"))
    1.32  
     2.1 --- a/etc/isar-keywords.el	Fri May 05 16:50:58 2006 +0200
     2.2 +++ b/etc/isar-keywords.el	Fri May 05 17:17:21 2006 +0200
     2.3 @@ -49,6 +49,7 @@
     2.4      "code_primclass"
     2.5      "code_primconst"
     2.6      "code_primtyco"
     2.7 +    "code_purge"
     2.8      "code_serialize"
     2.9      "code_syntax_const"
    2.10      "code_syntax_tyco"
    2.11 @@ -85,6 +86,7 @@
    2.12      "fixrec"
    2.13      "from"
    2.14      "full_prf"
    2.15 +    "function"
    2.16      "global"
    2.17      "guess"
    2.18      "have"
    2.19 @@ -177,6 +179,7 @@
    2.20      "subsubsection"
    2.21      "syntax"
    2.22      "term"
    2.23 +    "termination"
    2.24      "text"
    2.25      "text_raw"
    2.26      "then"
    2.27 @@ -382,6 +385,7 @@
    2.28      "code_primclass"
    2.29      "code_primconst"
    2.30      "code_primtyco"
    2.31 +    "code_purge"
    2.32      "code_serialize"
    2.33      "code_syntax_const"
    2.34      "code_syntax_tyco"
    2.35 @@ -445,12 +449,14 @@
    2.36    '("ax_specification"
    2.37      "corollary"
    2.38      "cpodef"
    2.39 +    "function"
    2.40      "instance"
    2.41      "interpretation"
    2.42      "lemma"
    2.43      "pcpodef"
    2.44      "recdef_tc"
    2.45      "specification"
    2.46 +    "termination"
    2.47      "theorem"
    2.48      "typedef"))
    2.49  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Accessible_Part.thy	Fri May 05 17:17:21 2006 +0200
     3.3 @@ -0,0 +1,123 @@
     3.4 +(*  Title:      HOL/Accessible_Part.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1994  University of Cambridge
     3.8 +*)
     3.9 +
    3.10 +header {* The accessible part of a relation *}
    3.11 +
    3.12 +theory Accessible_Part
    3.13 +imports Wellfounded_Recursion
    3.14 +begin
    3.15 +
    3.16 +subsection {* Inductive definition *}
    3.17 +
    3.18 +text {*
    3.19 + Inductive definition of the accessible part @{term "acc r"} of a
    3.20 + relation; see also \cite{paulin-tlca}.
    3.21 +*}
    3.22 +
    3.23 +consts
    3.24 +  acc :: "('a \<times> 'a) set => 'a set"
    3.25 +inductive "acc r"
    3.26 +  intros
    3.27 +    accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
    3.28 +
    3.29 +abbreviation
    3.30 +  termi :: "('a \<times> 'a) set => 'a set"
    3.31 +  "termi r == acc (r\<inverse>)"
    3.32 +
    3.33 +
    3.34 +subsection {* Induction rules *}
    3.35 +
    3.36 +theorem acc_induct:
    3.37 +  assumes major: "a \<in> acc r"
    3.38 +  assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
    3.39 +  shows "P a"
    3.40 +  apply (rule major [THEN acc.induct])
    3.41 +  apply (rule hyp)
    3.42 +   apply (rule accI)
    3.43 +   apply fast
    3.44 +  apply fast
    3.45 +  done
    3.46 +
    3.47 +theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
    3.48 +
    3.49 +theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
    3.50 +  apply (erule acc.elims)
    3.51 +  apply fast
    3.52 +  done
    3.53 +
    3.54 +lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
    3.55 +  apply (erule rtrancl_induct)
    3.56 +   apply blast
    3.57 +  apply (blast dest: acc_downward)
    3.58 +  done
    3.59 +
    3.60 +theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
    3.61 +  apply (blast dest: acc_downwards_aux)
    3.62 +  done
    3.63 +
    3.64 +theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
    3.65 +  apply (rule wfUNIVI)
    3.66 +  apply (induct_tac P x rule: acc_induct)
    3.67 +   apply blast
    3.68 +  apply blast
    3.69 +  done
    3.70 +
    3.71 +theorem acc_wfD: "wf r ==> x \<in> acc r"
    3.72 +  apply (erule wf_induct)
    3.73 +  apply (rule accI)
    3.74 +  apply blast
    3.75 +  done
    3.76 +
    3.77 +theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
    3.78 +  apply (blast intro: acc_wfI dest: acc_wfD)
    3.79 +  done
    3.80 +
    3.81 +
    3.82 +(* Smaller relations have bigger accessible parts: *)
    3.83 +lemma acc_subset:
    3.84 +  assumes sub:"R1 \<subseteq> R2"
    3.85 +  shows "acc R2 \<subseteq> acc R1"
    3.86 +proof
    3.87 +  fix x assume "x \<in> acc R2"
    3.88 +  thus "x \<in> acc R1"
    3.89 +  proof (induct x) -- "acc-induction"
    3.90 +    fix x
    3.91 +    assume ih: "\<And>y. (y, x) \<in> R2 \<Longrightarrow> y \<in> acc R1"
    3.92 +    
    3.93 +    with sub show "x \<in> acc R1"
    3.94 +      by (blast intro:accI)
    3.95 +  qed
    3.96 +qed
    3.97 +
    3.98 +
    3.99 +
   3.100 +(* This is a generalized induction theorem that works on
   3.101 +    subsets of the accessible part. *)
   3.102 +lemma acc_subset_induct:
   3.103 +  assumes subset: "D \<subseteq> acc R"
   3.104 +  assumes dcl: "\<And>x z. \<lbrakk>x \<in> D; (z, x)\<in>R\<rbrakk> \<Longrightarrow> z \<in> D"
   3.105 +
   3.106 +  assumes "x \<in> D"
   3.107 +  assumes istep: "\<And>x. \<lbrakk>x \<in> D; (\<And>z. (z, x)\<in>R \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
   3.108 +shows "P x"
   3.109 +proof -
   3.110 +  from `x \<in> D` and subset 
   3.111 +  have "x \<in> acc R" ..
   3.112 +
   3.113 +  thus "P x" using `x \<in> D`
   3.114 +  proof (induct x)
   3.115 +    fix x
   3.116 +    assume "x \<in> D"
   3.117 +      and "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<in> D \<Longrightarrow> P y"
   3.118 +
   3.119 +    with dcl and istep show "P x" by blast
   3.120 +  qed
   3.121 +qed
   3.122 +
   3.123 +
   3.124 +
   3.125 +
   3.126 +end
     4.1 --- a/src/HOL/Bali/DeclConcepts.thy	Fri May 05 16:50:58 2006 +0200
     4.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Fri May 05 17:17:21 2006 +0200
     4.3 @@ -1914,12 +1914,12 @@
     4.4  	   next
     4.5  	     case Some
     4.6  	     with dynM
     4.7 -	     have termination: "?Termination"
     4.8 +	     have "termination": "?Termination"
     4.9  	       by (auto)
    4.10  	     with Some dynM
    4.11  	     have "?Dynmethd_def dynC sig=Some dynM"
    4.12  	      by (auto simp add: dynmethd_dynC_def)
    4.13 -	     with subclseq_super_statC statM dynM termination
    4.14 +	     with subclseq_super_statC statM dynM "termination"
    4.15  	     show ?thesis
    4.16  	       by (auto simp add: dynmethd_def)
    4.17  	   qed
     5.1 --- a/src/HOL/Datatype.thy	Fri May 05 16:50:58 2006 +0200
     5.2 +++ b/src/HOL/Datatype.thy	Fri May 05 17:17:21 2006 +0200
     5.3 @@ -6,7 +6,8 @@
     5.4  header {* Datatypes *}
     5.5  
     5.6  theory Datatype
     5.7 -imports Datatype_Universe
     5.8 +imports Datatype_Universe FunDef
     5.9 +uses ("Tools/function_package/fundef_datatype.ML")
    5.10  begin
    5.11  
    5.12  subsection {* Representing primitive types *}
    5.13 @@ -314,4 +315,9 @@
    5.14      ml (target_atom "SOME")
    5.15      haskell (target_atom "Just")
    5.16  
    5.17 +
    5.18 +use "Tools/function_package/fundef_datatype.ML"
    5.19 +setup FundefDatatype.setup
    5.20 +
    5.21 +
    5.22  end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/FunDef.thy	Fri May 05 17:17:21 2006 +0200
     6.3 @@ -0,0 +1,49 @@
     6.4 +theory FunDef
     6.5 +imports Accessible_Part
     6.6 +uses 
     6.7 +("Tools/function_package/fundef_common.ML")
     6.8 +("Tools/function_package/fundef_lib.ML")
     6.9 +("Tools/function_package/context_tree.ML")
    6.10 +("Tools/function_package/fundef_prep.ML")
    6.11 +("Tools/function_package/fundef_proof.ML")
    6.12 +("Tools/function_package/termination.ML")
    6.13 +("Tools/function_package/fundef_package.ML")
    6.14 +begin
    6.15 +
    6.16 +lemma fundef_ex1_existence:
    6.17 +assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
    6.18 +assumes ex1: "\<exists>!y. (x,y)\<in>G"
    6.19 +shows "(x, f x)\<in>G"
    6.20 +  by (simp only:f_def, rule theI', rule ex1)
    6.21 +
    6.22 +lemma fundef_ex1_uniqueness:
    6.23 +assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
    6.24 +assumes ex1: "\<exists>!y. (x,y)\<in>G"
    6.25 +assumes elm: "(x, h x)\<in>G"
    6.26 +shows "h x = f x"
    6.27 +  by (simp only:f_def, rule the1_equality[symmetric], rule ex1, rule elm)
    6.28 +
    6.29 +lemma fundef_ex1_iff:
    6.30 +assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
    6.31 +assumes ex1: "\<exists>!y. (x,y)\<in>G"
    6.32 +shows "((x, y)\<in>G) = (f x = y)"
    6.33 +  apply (auto simp:ex1 f_def the1_equality)
    6.34 +  by (rule theI', rule ex1)
    6.35 +
    6.36 +lemma True_implies: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
    6.37 +  by simp
    6.38 +
    6.39 +
    6.40 +use "Tools/function_package/fundef_common.ML"
    6.41 +use "Tools/function_package/fundef_lib.ML"
    6.42 +use "Tools/function_package/context_tree.ML"
    6.43 +use "Tools/function_package/fundef_prep.ML"
    6.44 +use "Tools/function_package/fundef_proof.ML"
    6.45 +use "Tools/function_package/termination.ML"
    6.46 +use "Tools/function_package/fundef_package.ML"
    6.47 +
    6.48 +setup FundefPackage.setup
    6.49 +
    6.50 +
    6.51 +
    6.52 +end
     7.1 --- a/src/HOL/IsaMakefile	Fri May 05 16:50:58 2006 +0200
     7.2 +++ b/src/HOL/IsaMakefile	Fri May 05 17:17:21 2006 +0200
     7.3 @@ -120,7 +120,17 @@
     7.4    antisym_setup.ML arith_data.ML blastdata.ML cladata.ML			\
     7.5    document/root.tex hologic.ML simpdata.ML ResAtpMethods.thy 			\
     7.6    Tools/res_atp_provers.ML Tools/res_atp_methods.ML	\
     7.7 -  Tools/res_hol_clause.ML
     7.8 +  Tools/res_hol_clause.ML	\
     7.9 +  Tools/function_package/fundef_common.ML 	\
    7.10 +  Tools/function_package/fundef_lib.ML 	\
    7.11 +  Tools/function_package/context_tree.ML 	\
    7.12 +  Tools/function_package/fundef_prep.ML 	\
    7.13 +  Tools/function_package/fundef_proof.ML 	\
    7.14 +  Tools/function_package/termination.ML 	\
    7.15 +  Tools/function_package/fundef_package.ML 	\
    7.16 +  Tools/function_package/auto_term.ML 	\
    7.17 +  Tools/function_package/fundef_datatype.ML 	\
    7.18 +  FunDef.thy Accessible_Part.thy 
    7.19  	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
    7.20  
    7.21  
    7.22 @@ -184,7 +194,7 @@
    7.23  
    7.24  HOL-Library: HOL $(LOG)/HOL-Library.gz
    7.25  
    7.26 -$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
    7.27 +$(LOG)/HOL-Library.gz: $(OUT)/HOL \
    7.28    Library/SetsAndFunctions.thy Library/BigO.thy \
    7.29    Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
    7.30    Library/FuncSet.thy Library/Library.thy \
    7.31 @@ -480,7 +490,7 @@
    7.32  
    7.33  HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
    7.34  
    7.35 -$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Library/Accessible_Part.thy \
    7.36 +$(LOG)/HOL-Lambda.gz: $(OUT)/HOL \
    7.37    Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
    7.38    Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
    7.39    Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \
    7.40 @@ -740,7 +750,7 @@
    7.41  
    7.42  HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
    7.43  
    7.44 -$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal Library/Accessible_Part.thy	\
    7.45 +$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
    7.46    Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy Nominal/Examples/Class.thy	\
    7.47    Nominal/Examples/Fsub.thy Nominal/Examples/Lambda_mu.thy			\
    7.48    Nominal/Examples/Iteration.thy Nominal/Examples/Lam_substs.thy		\
     8.1 --- a/src/HOL/Lambda/ListOrder.thy	Fri May 05 16:50:58 2006 +0200
     8.2 +++ b/src/HOL/Lambda/ListOrder.thy	Fri May 05 17:17:21 2006 +0200
     8.3 @@ -6,7 +6,7 @@
     8.4  
     8.5  header {* Lifting an order to lists of elements *}
     8.6  
     8.7 -theory ListOrder imports Accessible_Part begin
     8.8 +theory ListOrder imports Main begin
     8.9  
    8.10  text {*
    8.11    Lifting an order to lists of elements, relating exactly one
     9.1 --- a/src/HOL/Library/Accessible_Part.thy	Fri May 05 16:50:58 2006 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,78 +0,0 @@
     9.4 -(*  Title:      HOL/Library/Accessible_Part.thy
     9.5 -    ID:         $Id$
     9.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 -    Copyright   1994  University of Cambridge
     9.8 -*)
     9.9 -
    9.10 -header {* The accessible part of a relation *}
    9.11 -
    9.12 -theory Accessible_Part
    9.13 -imports Main
    9.14 -begin
    9.15 -
    9.16 -subsection {* Inductive definition *}
    9.17 -
    9.18 -text {*
    9.19 - Inductive definition of the accessible part @{term "acc r"} of a
    9.20 - relation; see also \cite{paulin-tlca}.
    9.21 -*}
    9.22 -
    9.23 -consts
    9.24 -  acc :: "('a \<times> 'a) set => 'a set"
    9.25 -inductive "acc r"
    9.26 -  intros
    9.27 -    accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
    9.28 -
    9.29 -abbreviation
    9.30 -  termi :: "('a \<times> 'a) set => 'a set"
    9.31 -  "termi r == acc (r\<inverse>)"
    9.32 -
    9.33 -
    9.34 -subsection {* Induction rules *}
    9.35 -
    9.36 -theorem acc_induct:
    9.37 -  assumes major: "a \<in> acc r"
    9.38 -  assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
    9.39 -  shows "P a"
    9.40 -  apply (rule major [THEN acc.induct])
    9.41 -  apply (rule hyp)
    9.42 -   apply (rule accI)
    9.43 -   apply fast
    9.44 -  apply fast
    9.45 -  done
    9.46 -
    9.47 -theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
    9.48 -
    9.49 -theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
    9.50 -  apply (erule acc.elims)
    9.51 -  apply fast
    9.52 -  done
    9.53 -
    9.54 -lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
    9.55 -  apply (erule rtrancl_induct)
    9.56 -   apply blast
    9.57 -  apply (blast dest: acc_downward)
    9.58 -  done
    9.59 -
    9.60 -theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
    9.61 -  apply (blast dest: acc_downwards_aux)
    9.62 -  done
    9.63 -
    9.64 -theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
    9.65 -  apply (rule wfUNIVI)
    9.66 -  apply (induct_tac P x rule: acc_induct)
    9.67 -   apply blast
    9.68 -  apply blast
    9.69 -  done
    9.70 -
    9.71 -theorem acc_wfD: "wf r ==> x \<in> acc r"
    9.72 -  apply (erule wf_induct)
    9.73 -  apply (rule accI)
    9.74 -  apply blast
    9.75 -  done
    9.76 -
    9.77 -theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
    9.78 -  apply (blast intro: acc_wfI dest: acc_wfD)
    9.79 -  done
    9.80 -
    9.81 -end
    10.1 --- a/src/HOL/Library/Library.thy	Fri May 05 16:50:58 2006 +0200
    10.2 +++ b/src/HOL/Library/Library.thy	Fri May 05 17:17:21 2006 +0200
    10.3 @@ -1,7 +1,6 @@
    10.4  (*<*)
    10.5  theory Library
    10.6  imports
    10.7 -  Accessible_Part
    10.8    BigO
    10.9    Continuity
   10.10    EfficientNat
    11.1 --- a/src/HOL/Library/Multiset.thy	Fri May 05 16:50:58 2006 +0200
    11.2 +++ b/src/HOL/Library/Multiset.thy	Fri May 05 17:17:21 2006 +0200
    11.3 @@ -6,7 +6,7 @@
    11.4  header {* Multisets *}
    11.5  
    11.6  theory Multiset
    11.7 -imports Accessible_Part
    11.8 +imports Main
    11.9  begin
   11.10  
   11.11  subsection {* The type of multisets *}
    12.1 --- a/src/HOL/Nominal/Examples/SN.thy	Fri May 05 16:50:58 2006 +0200
    12.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Fri May 05 17:17:21 2006 +0200
    12.3 @@ -1,7 +1,7 @@
    12.4  (* $Id$ *)
    12.5  
    12.6  theory SN
    12.7 -imports Lam_substs Accessible_Part
    12.8 +imports Lam_substs
    12.9  begin
   12.10  
   12.11  text {* Strong Normalisation proof from the Proofs and Types book *}
    13.1 --- a/src/HOL/Recdef.thy	Fri May 05 16:50:58 2006 +0200
    13.2 +++ b/src/HOL/Recdef.thy	Fri May 05 17:17:21 2006 +0200
    13.3 @@ -18,6 +18,7 @@
    13.4    ("../TFL/tfl.ML")
    13.5    ("../TFL/post.ML")
    13.6    ("Tools/recdef_package.ML")
    13.7 +  ("Tools/function_package/auto_term.ML")
    13.8  begin
    13.9  
   13.10  lemma tfl_eq_True: "(x = True) --> x"
   13.11 @@ -95,4 +96,8 @@
   13.12    finally show "finite (UNIV :: 'a option set)" .
   13.13  qed
   13.14  
   13.15 +
   13.16 +use "Tools/function_package/auto_term.ML"
   13.17 +setup FundefAutoTerm.setup
   13.18 +
   13.19  end
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Tools/function_package/auto_term.ML	Fri May 05 17:17:21 2006 +0200
    14.3 @@ -0,0 +1,52 @@
    14.4 +(*  Title:      HOL/Tools/function_package/auto_term.ML
    14.5 +    ID:         $Id$
    14.6 +    Author:     Alexander Krauss, TU Muenchen
    14.7 +
    14.8 +A package for general recursive function definitions. 
    14.9 +The auto_term method.
   14.10 +*)
   14.11 +
   14.12 +
   14.13 +signature FUNDEF_AUTO_TERM =
   14.14 +sig
   14.15 +    val setup : theory -> theory
   14.16 +end
   14.17 +
   14.18 +structure FundefAutoTerm : FUNDEF_AUTO_TERM = 
   14.19 +struct
   14.20 +
   14.21 +open FundefCommon
   14.22 +open FundefAbbrev
   14.23 +
   14.24 +
   14.25 +
   14.26 +fun auto_term_tac tc_intro_rule relstr wf_rules ss =
   14.27 +    (resolve_tac [tc_intro_rule] 1)                    (* produce the usual goals *)
   14.28 +        THEN (instantiate_tac [("R", relstr)])    (* instantiate with the given relation *)
   14.29 +	THEN (ALLGOALS 
   14.30 +		  (fn 1 => ares_tac wf_rules 1    (* Solve wellfoundedness *)
   14.31 +		    | i => asm_simp_tac ss i))    (* Simplify termination conditions *)
   14.32 +
   14.33 +fun mk_termination_meth relstr ctxt =
   14.34 +    let
   14.35 +	val {simps, congs, wfs} = RecdefPackage.get_local_hints ctxt
   14.36 +	val ss = local_simpset_of ctxt addsimps simps
   14.37 +	    
   14.38 +	val intro_rule = ProofContext.get_thm ctxt (Name "termination_intro")
   14.39 +    in
   14.40 +	Method.RAW_METHOD (K (auto_term_tac
   14.41 +				  intro_rule
   14.42 +				  relstr
   14.43 +				  wfs
   14.44 +				  ss))
   14.45 +    end
   14.46 +
   14.47 +
   14.48 +
   14.49 +val setup = Method.add_methods [("auto_term", Method.simple_args Args.name mk_termination_meth, "termination prover for recdef compatibility")]
   14.50 +
   14.51 +end
   14.52 +
   14.53 +
   14.54 +
   14.55 +
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Fri May 05 17:17:21 2006 +0200
    15.3 @@ -0,0 +1,240 @@
    15.4 +(*  Title:      HOL/Tools/function_package/context_tree.ML
    15.5 +    ID:         $Id$
    15.6 +    Author:     Alexander Krauss, TU Muenchen
    15.7 +
    15.8 +A package for general recursive function definitions. 
    15.9 +Builds and traverses trees of nested contexts along a term.
   15.10 +*)
   15.11 +
   15.12 +
   15.13 +signature FUNDEF_CTXTREE =
   15.14 +sig
   15.15 +    type ctx_tree
   15.16 +
   15.17 +    (* FIXME: This interface is a mess and needs to be cleaned up! *)
   15.18 +    val cong_deps : thm -> int FundefCommon.IntGraph.T
   15.19 +    val add_congs : thm list
   15.20 +
   15.21 +    val mk_tree: theory -> (thm * FundefCommon.depgraph) list -> term -> term -> FundefCommon.ctx_tree
   15.22 +
   15.23 +    val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list
   15.24 +
   15.25 +    val export_term : (string * typ) list * term list -> term -> term
   15.26 +    val export_thm : theory -> (string * typ) list * term list -> thm -> thm
   15.27 +    val import_thm : theory -> (string * typ) list * thm list -> thm -> thm
   15.28 +
   15.29 +
   15.30 +    val traverse_tree : 
   15.31 +   ((string * typ) list * thm list -> term ->
   15.32 +   (((string * typ) list * thm list) * thm) list ->
   15.33 +   (((string * typ) list * thm list) * thm) list * 'b ->
   15.34 +   (((string * typ) list * thm list) * thm) list * 'b)
   15.35 +   -> FundefCommon.ctx_tree -> 'b -> 'b
   15.36 +
   15.37 +    val rewrite_by_tree : theory -> 'a -> term -> thm -> (thm * thm) list -> FundefCommon.ctx_tree -> thm * (thm * thm) list
   15.38 +end
   15.39 +
   15.40 +structure FundefCtxTree : FUNDEF_CTXTREE =
   15.41 +struct
   15.42 +
   15.43 +open FundefCommon
   15.44 +
   15.45 +
   15.46 +(* Maps "Trueprop A = B" to "A" *)
   15.47 +val rhs_of = snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
   15.48 +(* Maps "A == B" to "B" *)
   15.49 +val meta_rhs_of = snd o Logic.dest_equals
   15.50 +
   15.51 +
   15.52 +
   15.53 +(*** Dependency analysis for congruence rules ***)
   15.54 +
   15.55 +fun branch_vars t = 
   15.56 +    let	val (assumes, term) = dest_implies_list (snd (dest_all_all t))
   15.57 +    in (fold (curry add_term_vars) assumes [], term_vars term)
   15.58 +    end
   15.59 +
   15.60 +fun cong_deps crule =
   15.61 +    let
   15.62 +	val branches = map branch_vars (prems_of crule)
   15.63 +	val num_branches = (1 upto (length branches)) ~~ branches
   15.64 +    in
   15.65 +	IntGraph.empty
   15.66 +	    |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
   15.67 +	    |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
   15.68 +	    (product num_branches num_branches)
   15.69 +    end
   15.70 +    
   15.71 +val add_congs = map (fn c => c RS eq_reflection) [cong, ext] 
   15.72 +
   15.73 +
   15.74 +
   15.75 +(* Called on the INSTANTIATED branches of the congruence rule *)
   15.76 +fun mk_branch t = 
   15.77 +    let
   15.78 +	val (fixes, impl) = dest_all_all t
   15.79 +	val (assumes, term) = dest_implies_list impl
   15.80 +    in
   15.81 +	(map dest_Free fixes, assumes, rhs_of term)
   15.82 +    end
   15.83 +
   15.84 +
   15.85 +
   15.86 +
   15.87 +
   15.88 +exception CTREE_INTERNAL of string
   15.89 +
   15.90 +fun find_cong_rule thy ((r,dep)::rs) t =
   15.91 +    (let
   15.92 +	val (c, subs) = (meta_rhs_of (concl_of r), prems_of r)
   15.93 +
   15.94 +	val subst = Pattern.match thy (c, t) (Vartab.empty, Vartab.empty)
   15.95 +
   15.96 +	val branches = map (mk_branch o Envir.beta_norm o Envir.subst_vars subst) subs
   15.97 +     in
   15.98 +	 (r, dep, branches)
   15.99 +     end
  15.100 +    handle Pattern.MATCH => find_cong_rule thy rs t)
  15.101 +  | find_cong_rule thy [] _ = raise CTREE_INTERNAL "No cong rule found!" (* Should never happen *)
  15.102 +
  15.103 +
  15.104 +fun matchcall f (a $ b) = if a = f then SOME b else NONE
  15.105 +  | matchcall f _ = NONE
  15.106 +
  15.107 +fun mk_tree thy congs f t =
  15.108 +    case matchcall f t of
  15.109 +	SOME arg => RCall (t, mk_tree thy congs f arg)
  15.110 +      | NONE => 
  15.111 +	if not (exists_Const (curry op = (dest_Const f)) t) then Leaf t
  15.112 +	else 
  15.113 +	    let val (r, dep, branches) = find_cong_rule thy congs t in
  15.114 +		Cong (t, r, dep, map (fn (fixes, assumes, st) => 
  15.115 +					 (fixes, map (assume o cterm_of thy) assumes, mk_tree thy congs f st)) branches)
  15.116 +	    end
  15.117 +		
  15.118 +		
  15.119 +fun add_context_varnames (Leaf _) = I
  15.120 +  | add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (curry op ins_string o fst) fs o add_context_varnames st) sub
  15.121 +  | add_context_varnames (RCall (_,st)) = add_context_varnames st
  15.122 +    
  15.123 +
  15.124 +(* Poor man's contexts: Only fixes and assumes *)
  15.125 +fun compose (fs1, as1) (fs2, as2) = (fs1 @ fs2, as1 @ as2)
  15.126 +
  15.127 +fun export_term (fixes, assumes) =
  15.128 +    fold_rev (curry Logic.mk_implies) assumes #> fold (mk_forall o Free) fixes
  15.129 +
  15.130 +fun export_thm thy (fixes, assumes) =
  15.131 +    fold_rev (implies_intr o cterm_of thy) assumes
  15.132 + #> fold_rev (forall_intr o cterm_of thy o Free) fixes
  15.133 +
  15.134 +fun import_thm thy (fixes, athms) =
  15.135 +    fold (forall_elim o cterm_of thy o Free) fixes
  15.136 + #> fold implies_elim_swp athms
  15.137 +
  15.138 +fun assume_in_ctxt thy (fixes, athms) prop =
  15.139 +    let
  15.140 +	val global_assum = export_term (fixes, map prop_of athms) prop
  15.141 +    in
  15.142 +	(global_assum,
  15.143 +	 assume (cterm_of thy global_assum) |> import_thm thy (fixes, athms))
  15.144 +    end
  15.145 +
  15.146 +
  15.147 +(* folds in the order of the dependencies of a graph. *)
  15.148 +fun fold_deps G f x =
  15.149 +    let
  15.150 +	fun fill_table i (T, x) =
  15.151 +	    case Inttab.lookup T i of
  15.152 +		SOME _ => (T, x)
  15.153 +	      | NONE => 
  15.154 +		let
  15.155 +		    val (T', x') = fold fill_table (IntGraph.imm_succs G i) (T, x)
  15.156 +		    val (v, x'') = f (the o Inttab.lookup T') i x
  15.157 +		in
  15.158 +		    (Inttab.update (i, v) T', x'')
  15.159 +		end
  15.160 +
  15.161 +	val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
  15.162 +    in
  15.163 +	(Inttab.fold (cons o snd) T [], x)
  15.164 +    end
  15.165 +
  15.166 +
  15.167 +fun flatten xss = fold_rev append xss []
  15.168 +
  15.169 +fun traverse_tree rcOp tr x =
  15.170 +    let 
  15.171 +	fun traverse_help ctx (Leaf _) u x = ([], x)
  15.172 +	  | traverse_help ctx (RCall (t, st)) u x =
  15.173 +	    rcOp ctx t u (traverse_help ctx st u x)
  15.174 +	  | traverse_help ctx (Cong (t, crule, deps, branches)) u x =
  15.175 +	    let
  15.176 +		fun sub_step lu i x =
  15.177 +		    let
  15.178 +			val (fixes, assumes, subtree) = nth branches (i - 1)
  15.179 +			val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
  15.180 +			val (subs, x') = traverse_help (compose ctx (fixes, assumes)) subtree used x
  15.181 +			val exported_subs = map (apfst (compose (fixes, assumes))) subs
  15.182 +		    in
  15.183 +			(exported_subs, x')
  15.184 +		    end
  15.185 +	    in
  15.186 +		fold_deps deps sub_step x
  15.187 +			  |> apfst flatten
  15.188 +	    end
  15.189 +    in
  15.190 +	snd (traverse_help ([], []) tr [] x)
  15.191 +    end
  15.192 +
  15.193 +
  15.194 +fun is_refl thm = let val (l,r) = Logic.dest_equals (prop_of thm) in l = r end
  15.195 +
  15.196 +fun rewrite_by_tree thy f h ih x tr =
  15.197 +    let
  15.198 +	fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
  15.199 +	  | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
  15.200 +	    let
  15.201 +		val (inner, (Ri,ha)::x') = rewrite_help fix f_as h_as x st
  15.202 +					   
  15.203 +					   (* Need not use the simplifier here. Can use primitive steps! *)
  15.204 +		val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
  15.205 +			     
  15.206 +		val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
  15.207 +		val iRi = import_thm thy (fix, f_as) Ri (* a < lhs *)
  15.208 +		val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
  15.209 +				     |> rew_ha
  15.210 +
  15.211 +		val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
  15.212 +		val eq = implies_elim (implies_elim inst_ih iRi) iha
  15.213 +			 
  15.214 +		val h_a'_eq_f_a' = eq RS eq_reflection
  15.215 +		val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
  15.216 +	    in
  15.217 +		(result, x')
  15.218 +	    end
  15.219 +	  | rewrite_help fix f_as h_as x (Cong (t, crule, deps, branches)) =
  15.220 +	    let
  15.221 +		fun sub_step lu i x =
  15.222 +		    let
  15.223 +			val (fixes, assumes, st) = nth branches (i - 1)
  15.224 +			val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
  15.225 +			val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
  15.226 +			val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
  15.227 +
  15.228 +			val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
  15.229 +			val subeq_exp = export_thm thy (fixes, map prop_of assumes) (subeq RS meta_eq_to_obj_eq)
  15.230 +		    in
  15.231 +			(subeq_exp, x')
  15.232 +		    end
  15.233 +		    
  15.234 +		val (subthms, x') = fold_deps deps sub_step x
  15.235 +	    in
  15.236 +		(fold_rev (curry op COMP) subthms crule, x')
  15.237 +	    end
  15.238 +	    
  15.239 +    in
  15.240 +	rewrite_help [] [] [] x tr
  15.241 +    end
  15.242 +
  15.243 +end
  15.244 \ No newline at end of file
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri May 05 17:17:21 2006 +0200
    16.3 @@ -0,0 +1,182 @@
    16.4 +(*  Title:      HOL/Tools/function_package/fundef_common.ML
    16.5 +    ID:         $Id$
    16.6 +    Author:     Alexander Krauss, TU Muenchen
    16.7 +
    16.8 +A package for general recursive function definitions. 
    16.9 +Common type definitions and other infrastructure.
   16.10 +*)
   16.11 +
   16.12 +structure FundefCommon =
   16.13 +struct
   16.14 +
   16.15 +(* Theory Dependencies *)
   16.16 +val acc_const_name = "Accessible_Part.acc"
   16.17 +
   16.18 +
   16.19 +
   16.20 +(* Partial orders to represent dependencies *)
   16.21 +structure IntGraph = GraphFun(type key = int val ord = int_ord);
   16.22 +
   16.23 +type depgraph = int IntGraph.T
   16.24 +
   16.25 +
   16.26 +datatype ctx_tree 
   16.27 +  = Leaf of term
   16.28 +  | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
   16.29 +  | RCall of (term * ctx_tree)
   16.30 +
   16.31 +
   16.32 +
   16.33 +(* A record containing all the relevant symbols and types needed during the proof.
   16.34 +   This is set up at the beginning and does not change. *)
   16.35 +type naming_context =
   16.36 +     { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ,
   16.37 +       G: term, R: term, acc_R: term, h: term, y: term, x: term, z: term, a:term, P: term, 
   16.38 +       D: term, Pbool:term,
   16.39 +       glrs: (term list * term list * term * term) list,
   16.40 +       glrs': (term list * term list * term * term) list,
   16.41 +       f_def: thm,
   16.42 +       used: string list,
   16.43 +       trees: ctx_tree list
   16.44 +     }
   16.45 +
   16.46 +
   16.47 +type rec_call_info = 
   16.48 +     {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm} 
   16.49 +
   16.50 +type clause_info =
   16.51 +     {
   16.52 +      no: int,
   16.53 +
   16.54 +      qs: term list, 
   16.55 +      gs: term list,
   16.56 +      lhs: term,
   16.57 +      rhs: term,
   16.58 +
   16.59 +      cqs: cterm list,
   16.60 +      cvqs: cterm list,
   16.61 +      ags: thm list,
   16.62 +      
   16.63 +      cqs': cterm list, 
   16.64 +      ags': thm list,
   16.65 +      lhs': term,
   16.66 +      rhs': term,
   16.67 +      ordcqs': cterm list, 
   16.68 +
   16.69 +      GI: thm,
   16.70 +      lGI: thm,
   16.71 +      RCs: rec_call_info list,
   16.72 +
   16.73 +      tree: ctx_tree,
   16.74 +      case_hyp: thm
   16.75 +     }
   16.76 +
   16.77 +
   16.78 +type curry_info =
   16.79 +     { argTs: typ list, curry_ss: simpset }
   16.80 +
   16.81 +
   16.82 +type prep_result =
   16.83 +     {
   16.84 +      names: naming_context, 
   16.85 +      complete : term,
   16.86 +      compat : term list,
   16.87 +      clauses: clause_info list
   16.88 +     }
   16.89 +
   16.90 +type fundef_result =
   16.91 +     {
   16.92 +      f: term,
   16.93 +      G : term,
   16.94 +      R : term,
   16.95 +      completeness : thm,
   16.96 +      compatibility : thm list,
   16.97 +
   16.98 +      psimps : thm list, 
   16.99 +      subset_pinduct : thm, 
  16.100 +      simple_pinduct : thm, 
  16.101 +      total_intro : thm,
  16.102 +      dom_intros : thm list
  16.103 +     }
  16.104 +
  16.105 +
  16.106 +structure FundefData = TheoryDataFun
  16.107 +(struct
  16.108 +  val name = "HOL/function_def/data";
  16.109 +  type T = string * fundef_result Symtab.table
  16.110 +
  16.111 +  val empty = ("", Symtab.empty);
  16.112 +  val copy = I;
  16.113 +  val extend = I;
  16.114 +  fun merge _ ((l1,tab1),(l2,tab2)) = (l1, Symtab.merge (op =) (tab1, tab2))
  16.115 +
  16.116 +  fun print _ _ = ();
  16.117 +end);
  16.118 +
  16.119 +
  16.120 +structure FundefCongs = GenericDataFun
  16.121 +(struct
  16.122 +    val name = "HOL/function_def/congs"
  16.123 +    type T = thm list
  16.124 +    val empty = []
  16.125 +    val extend = I
  16.126 +    fun merge _ (l1, l2) = l1 @ l2
  16.127 +    fun print  _ _ = ()
  16.128 +end);
  16.129 +
  16.130 +
  16.131 +fun add_fundef_data name fundef_data =
  16.132 +    FundefData.map (fn (_,tab) => (name, Symtab.update_new (name, fundef_data) tab))
  16.133 +
  16.134 +fun get_fundef_data name thy = Symtab.lookup (snd (FundefData.get thy)) name
  16.135 +
  16.136 +fun get_last_fundef thy = fst (FundefData.get thy)
  16.137 +
  16.138 +val map_fundef_congs = FundefCongs.map 
  16.139 +val get_fundef_congs = FundefCongs.get
  16.140 +
  16.141 +end
  16.142 +
  16.143 +
  16.144 +
  16.145 +(* Common Abbreviations *)
  16.146 +
  16.147 +structure FundefAbbrev =
  16.148 +struct
  16.149 +
  16.150 +fun implies_elim_swp x y = implies_elim y x
  16.151 +
  16.152 +(* Some HOL things frequently used *)
  16.153 +val boolT = HOLogic.boolT
  16.154 +val mk_prod = HOLogic.mk_prod
  16.155 +val mk_mem = HOLogic.mk_mem
  16.156 +val mk_eq = HOLogic.mk_eq
  16.157 +val Trueprop = HOLogic.mk_Trueprop
  16.158 +
  16.159 +val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
  16.160 +fun mk_relmem (x,y) R = Trueprop (mk_mem (mk_prod (x, y), R))
  16.161 +
  16.162 +fun mk_subset T A B = 
  16.163 +    let val sT = HOLogic.mk_setT T
  16.164 +    in Const ("Orderings.less_eq", sT --> sT --> boolT) $ A $ B end
  16.165 +
  16.166 +
  16.167 +(* with explicit types: Needed with loose bounds *)
  16.168 +fun mk_relmemT xT yT (x,y) R = 
  16.169 +    let 
  16.170 +	val pT = HOLogic.mk_prodT (xT, yT)
  16.171 +	val RT = HOLogic.mk_setT pT
  16.172 +    in
  16.173 +	Const ("op :", [pT, RT] ---> boolT)
  16.174 +	      $ (HOLogic.pair_const xT yT $ x $ y)
  16.175 +	      $ R
  16.176 +    end
  16.177 +
  16.178 +fun free_to_var (Free (v,T)) = Var ((v,0),T)
  16.179 +  | free_to_var _ = raise Match
  16.180 +
  16.181 +fun var_to_free (Var ((v,_),T)) = Free (v,T)
  16.182 +  | var_to_free _ = raise Match
  16.183 +
  16.184 +
  16.185 +end
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri May 05 17:17:21 2006 +0200
    17.3 @@ -0,0 +1,167 @@
    17.4 +(*  Title:      HOL/Tools/function_package/fundef_datatype.ML
    17.5 +    ID:         $Id$
    17.6 +    Author:     Alexander Krauss, TU Muenchen
    17.7 +
    17.8 +A package for general recursive function definitions. 
    17.9 +A tactic to prove completeness of datatype patterns.
   17.10 +*)
   17.11 +
   17.12 +signature FUNDEF_DATATYPE = 
   17.13 +sig
   17.14 +    val pat_complete_tac: int -> tactic
   17.15 +
   17.16 +    val setup : theory -> theory
   17.17 +end
   17.18 +
   17.19 +
   17.20 +
   17.21 +structure FundefDatatype : FUNDEF_DATATYPE =
   17.22 +struct
   17.23 +
   17.24 +fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
   17.25 +fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
   17.26 +
   17.27 +fun inst_free var inst thm =
   17.28 +    forall_elim inst (forall_intr var thm)
   17.29 +
   17.30 +
   17.31 +fun inst_case_thm thy x P thm =
   17.32 +    let
   17.33 +	val [Pv, xv] = term_vars (prop_of thm)
   17.34 +    in
   17.35 +	cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
   17.36 +    end
   17.37 +
   17.38 +
   17.39 +fun invent_vars constr i =
   17.40 +    let
   17.41 +	val Ts = binder_types (fastype_of constr)
   17.42 +	val j = i + length Ts
   17.43 +	val is = i upto (j - 1)
   17.44 +	val avs = map2 mk_argvar is Ts
   17.45 +	val pvs = map2 mk_patvar is Ts
   17.46 +    in
   17.47 +	(avs, pvs, j)
   17.48 +    end
   17.49 +
   17.50 +
   17.51 +fun filter_pats thy cons pvars [] = []
   17.52 +  | filter_pats thy cons pvars (([], thm) :: pts) = raise Match
   17.53 +  | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) = 
   17.54 +    case pat of
   17.55 +	Free _ => let val inst = list_comb (cons, pvars)
   17.56 +		 in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm)
   17.57 +		    :: (filter_pats thy cons pvars pts) end
   17.58 +      | _ => if fst (strip_comb pat) = cons
   17.59 +	     then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
   17.60 +	     else filter_pats thy cons pvars pts
   17.61 +
   17.62 +
   17.63 +fun inst_constrs_of thy (T as Type (name, _)) =
   17.64 +	map (fn (Cn,CT) => Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
   17.65 +	    (the (DatatypePackage.get_datatype_constrs thy name))
   17.66 +  | inst_constrs_of thy _ = raise Match
   17.67 +
   17.68 +
   17.69 +fun transform_pat thy avars c_assum ([] , thm) = raise Match
   17.70 +  | transform_pat thy avars c_assum (pat :: pats, thm) =
   17.71 +    let
   17.72 +	val (_, subps) = strip_comb pat
   17.73 +	val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
   17.74 +	val a_eqs = map assume eqs
   17.75 +	val c_eq_pat = simplify (HOL_basic_ss addsimps a_eqs) c_assum
   17.76 +    in
   17.77 +	(subps @ pats, fold_rev implies_intr eqs
   17.78 +				(implies_elim thm c_eq_pat))
   17.79 +    end
   17.80 +
   17.81 +
   17.82 +exception COMPLETENESS
   17.83 +
   17.84 +fun constr_case thy P idx (v :: vs) pats cons =
   17.85 +    let
   17.86 +	val (avars, pvars, newidx) = invent_vars cons idx
   17.87 +	val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
   17.88 +	val c_assum = assume c_hyp
   17.89 +	val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
   17.90 +    in
   17.91 +	o_alg thy P newidx (avars @ vs) newpats
   17.92 +	      |> implies_intr c_hyp
   17.93 +	      |> fold_rev (forall_intr o cterm_of thy) avars
   17.94 +    end
   17.95 +  | constr_case _ _ _ _ _ _ = raise Match
   17.96 +and o_alg thy P idx [] (([], Pthm) :: _)  = Pthm
   17.97 +  | o_alg thy P idx (v :: vs) [] = raise COMPLETENESS
   17.98 +  | o_alg thy P idx (v :: vs) pts =
   17.99 +    if forall (is_Free o hd o fst) pts (* Var case *)
  17.100 +    then o_alg thy P idx vs (map (fn (pv :: pats, thm) =>
  17.101 +			       (pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
  17.102 +    else (* Cons case *)
  17.103 +	 let  
  17.104 +	     val T = fastype_of v
  17.105 +	     val (tname, _) = dest_Type T
  17.106 +	     val {exhaustion=case_thm, ...} = DatatypePackage.the_datatype thy tname
  17.107 +	     val constrs = inst_constrs_of thy T
  17.108 +	     val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
  17.109 +	 in 
  17.110 +	     inst_case_thm thy v P case_thm
  17.111 +			   |> fold (curry op COMP) c_cases
  17.112 +	 end
  17.113 +  | o_alg _ _ _ _ _ = raise Match
  17.114 +
  17.115 +			   
  17.116 +fun prove_completeness thy x P qss pats =
  17.117 +    let
  17.118 +	fun mk_assum qs pat = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x,pat)),
  17.119 +						HOLogic.mk_Trueprop P)
  17.120 +					       |> fold_rev mk_forall qs
  17.121 +					       |> cterm_of thy
  17.122 +
  17.123 +	val hyps = map2 mk_assum qss pats
  17.124 +
  17.125 +	fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
  17.126 +
  17.127 +	val assums = map2 inst_hyps hyps qss
  17.128 +    in
  17.129 +	o_alg thy P 2 [x] (map2 (pair o single) pats assums)
  17.130 +	      |> fold_rev implies_intr hyps
  17.131 +	      |> zero_var_indexes
  17.132 +	      |> forall_intr_frees
  17.133 +	      |> forall_elim_vars 0 
  17.134 +    end
  17.135 +
  17.136 +
  17.137 +
  17.138 +fun pat_complete_tac i thm =
  17.139 +    let 
  17.140 +	val subgoal = nth (prems_of thm) (i - 1)
  17.141 +	val assums = Logic.strip_imp_prems subgoal
  17.142 +	val _ $ P = Logic.strip_imp_concl subgoal
  17.143 +		    
  17.144 +	fun pat_of assum = 
  17.145 +	    let
  17.146 +		val (qs, imp) = dest_all_all assum
  17.147 +	    in
  17.148 +		case Logic.dest_implies imp of 
  17.149 +		    (_ $ (_ $ x $ pat), _) => (x, (qs, pat))
  17.150 +		  | _ => raise COMPLETENESS
  17.151 +	    end
  17.152 +
  17.153 +	val (x, (qss, pats)) = 
  17.154 +	    case (map pat_of assums) of
  17.155 +		[] => raise COMPLETENESS
  17.156 +	      | rs as ((x,_) :: _) 
  17.157 +		=> (x, split_list (snd (split_list rs)))
  17.158 +
  17.159 +	val complete_thm = prove_completeness (theory_of_thm thm) x P qss pats
  17.160 +    in
  17.161 +	Seq.single (Drule.compose_single(complete_thm, i, thm))
  17.162 +    end
  17.163 +    handle COMPLETENESS => Seq.empty
  17.164 +
  17.165 +
  17.166 +
  17.167 +val setup = 
  17.168 +    Method.add_methods [("pat_completeness", Method.no_args (Method.SIMPLE_METHOD (pat_complete_tac 1)), "Completeness prover for datatype patterns")]
  17.169 +
  17.170 +end
  17.171 \ No newline at end of file
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Fri May 05 17:17:21 2006 +0200
    18.3 @@ -0,0 +1,64 @@
    18.4 +(*  Title:      HOL/Tools/function_package/lib.ML
    18.5 +    ID:         $Id$
    18.6 +    Author:     Alexander Krauss, TU Muenchen
    18.7 +
    18.8 +A package for general recursive function definitions. 
    18.9 +Some fairly general functions that should probably go somewhere else... 
   18.10 +*)
   18.11 +
   18.12 +
   18.13 +fun mk_forall (var as Free (v,T)) t =
   18.14 +    all T $ Abs (v,T, abstract_over (var,t))
   18.15 +  | mk_forall _ _ = raise Match
   18.16 +
   18.17 +(* Builds a quantification with a new name for the variable. *)
   18.18 +fun mk_forall_rename ((v,T),newname) t =
   18.19 +    all T $ Abs (newname,T, abstract_over (Free (v,T),t))
   18.20 +
   18.21 +(* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
   18.22 +fun tupled_lambda vars t =
   18.23 +    case vars of
   18.24 +	(Free v) => lambda (Free v) t
   18.25 +      | (Var v) => lambda (Var v) t
   18.26 +      | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
   18.27 +	(HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
   18.28 +      | _ => raise Match
   18.29 +
   18.30 +
   18.31 +fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
   18.32 +    let
   18.33 +	val (n, body) = Term.dest_abs a
   18.34 +    in
   18.35 +	(Free (n, T), body)
   18.36 +    end
   18.37 +  | dest_all _ = raise Match
   18.38 +
   18.39 +
   18.40 +(* Removes all quantifiers from a term, replacing bound variables by frees. *)
   18.41 +fun dest_all_all (t as (Const ("all",_) $ _)) = 
   18.42 +    let
   18.43 +	val (v,b) = dest_all t
   18.44 +	val (vs, b') = dest_all_all b
   18.45 +    in
   18.46 +	(v :: vs, b')
   18.47 +    end
   18.48 +  | dest_all_all t = ([],t)
   18.49 +
   18.50 +(* unfold *)
   18.51 +fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x)
   18.52 +
   18.53 +val dest_implies_list = 
   18.54 +    split_last o (unfold Logic.is_implies (fst o Logic.dest_implies) (snd o Logic.dest_implies) single)
   18.55 +
   18.56 +fun implies_elim_swp a b = implies_elim b a
   18.57 +
   18.58 +fun map3 _ [] [] [] = []
   18.59 +  | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
   18.60 +  | map3 _ _ _ _ = raise UnequalLengths;
   18.61 +
   18.62 +
   18.63 +
   18.64 +(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
   18.65 +fun upairs [] = []
   18.66 +  | upairs (x::xs) = map (pair x) (x::xs) @ upairs xs
   18.67 +
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri May 05 17:17:21 2006 +0200
    19.3 @@ -0,0 +1,197 @@
    19.4 +(*  Title:      HOL/Tools/function_package/fundef_package.ML
    19.5 +    ID:         $Id$
    19.6 +    Author:     Alexander Krauss, TU Muenchen
    19.7 +
    19.8 +A package for general recursive function definitions. 
    19.9 +Isar commands.
   19.10 +
   19.11 +*)
   19.12 +
   19.13 +signature FUNDEF_PACKAGE = 
   19.14 +sig
   19.15 +    val add_fundef : ((bstring * Attrib.src list) * string) list -> theory -> Proof.state (* Need an _i variant *)
   19.16 +
   19.17 +    val cong_add: attribute
   19.18 +    val cong_del: attribute
   19.19 +							 
   19.20 +    val setup : theory -> theory
   19.21 +end
   19.22 +
   19.23 +
   19.24 +structure FundefPackage : FUNDEF_PACKAGE =
   19.25 +struct
   19.26 +
   19.27 +open FundefCommon
   19.28 +
   19.29 +val True_implies = thm "True_implies"
   19.30 +
   19.31 +
   19.32 +(*#> FundefTermination.setup #> FundefDatatype.setup*)
   19.33 +
   19.34 +fun fundef_afterqed congs curry_info name data natts thmss thy =
   19.35 +    let
   19.36 +	val (complete_thm :: compat_thms) = map hd thmss
   19.37 +	val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
   19.38 +	val {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
   19.39 +
   19.40 +	val (names, attsrcs) = split_list natts
   19.41 +	val atts = map (map (Attrib.attribute thy)) attsrcs
   19.42 +
   19.43 +	val accR = (#acc_R(#names(data)))
   19.44 +	val dom_abbrev = Logic.mk_equals (Free ("dom", fastype_of accR), accR)
   19.45 +
   19.46 +	val thy = thy |> Theory.add_path name 
   19.47 +
   19.48 +	val thy = thy |> Theory.add_path "psimps"
   19.49 +	val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy;
   19.50 +	val thy = thy |> Theory.parent_path
   19.51 +
   19.52 +	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
   19.53 +	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy
   19.54 +	val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy
   19.55 +	val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy
   19.56 +	val (_,thy) = PureThy.add_thms [(("pinduct", simple_pinduct), [RuleCases.case_names names, InductAttrib.induct_set ""])] thy
   19.57 +	val (_, thy) = PureThy.add_thmss [(("psimps", psimps), [Simplifier.simp_add])] thy
   19.58 +	val thy = thy |> Theory.parent_path
   19.59 +    in
   19.60 +	add_fundef_data name fundef_data thy
   19.61 +    end
   19.62 +
   19.63 +fun add_fundef eqns_atts thy =
   19.64 +    let
   19.65 +	val (natts, eqns) = split_list eqns_atts
   19.66 +
   19.67 +	val congs = get_fundef_congs (Context.Theory thy)
   19.68 +
   19.69 +	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs (map (Sign.read_prop thy) eqns) thy
   19.70 +	val {complete, compat, ...} = data
   19.71 +
   19.72 +	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
   19.73 +    in
   19.74 +	thy |> ProofContext.init
   19.75 +	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data natts) NONE ("", [])
   19.76 +	    (map (fn t => (("", []), [(t, ([], []))])) props)
   19.77 +    end
   19.78 +
   19.79 +
   19.80 +fun total_termination_afterqed name thmss thy =
   19.81 +    let
   19.82 +	val totality = hd (hd thmss)
   19.83 +
   19.84 +	val {psimps, simple_pinduct, ... }
   19.85 +	  = the (get_fundef_data name thy)
   19.86 +
   19.87 +	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
   19.88 +
   19.89 +	val tsimps = map remove_domain_condition psimps
   19.90 +	val tinduct = remove_domain_condition simple_pinduct
   19.91 +
   19.92 +	val thy = Theory.add_path name thy
   19.93 +		  
   19.94 +		  (* Need the names and attributes. Apply the attributes again? *)
   19.95 +(*	val thy = thy |> Theory.add_path "simps"
   19.96 +	val (_, thy) = PureThy.add_thms ((names ~~ tsimps) ~~ atts) thy;
   19.97 +	val thy = thy |> Theory.parent_path*)
   19.98 +
   19.99 +	val (_, thy) = PureThy.add_thms [(("induct", tinduct), [])] thy 
  19.100 +	val (_, thy) = PureThy.add_thmss [(("simps", tsimps), [Simplifier.simp_add, RecfunCodegen.add NONE])] thy
  19.101 +	val thy = Theory.parent_path thy
  19.102 +    in
  19.103 +	thy
  19.104 +    end
  19.105 +
  19.106 +(*
  19.107 +fun mk_partial_rules name D_name D domT idomT thmss thy =
  19.108 +    let
  19.109 +	val [subs, dcl] = (hd thmss)
  19.110 +
  19.111 +	val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
  19.112 +	  = the (Symtab.lookup (FundefData.get thy) name)
  19.113 +
  19.114 +	val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] 
  19.115 +						    [SOME (cterm_of thy D)]
  19.116 +						    subsetD)
  19.117 +
  19.118 +	val D_simps = map (curry op RS D_implies_dom) f_simps
  19.119 +
  19.120 +	val D_induct = subset_induct
  19.121 +			   |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
  19.122 +			   |> curry op COMP subs
  19.123 +			   |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
  19.124 +						 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
  19.125 +
  19.126 +	val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
  19.127 +	val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
  19.128 +    in
  19.129 +	thy3
  19.130 +    end
  19.131 +*)
  19.132 + 
  19.133 +
  19.134 +fun fundef_setup_termination_proof name NONE thy = 
  19.135 +    let
  19.136 +	val name = if name = "" then get_last_fundef thy else name
  19.137 +	val data = the (get_fundef_data name thy)
  19.138 +
  19.139 +	val {total_intro, ...} = data
  19.140 +	val goal = FundefTermination.mk_total_termination_goal data
  19.141 +    in
  19.142 +	thy |> ProofContext.init
  19.143 +	    |> ProofContext.note_thmss_i [(("termination_intro", 
  19.144 +					    [ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd
  19.145 +	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", [])
  19.146 +	    [(("", []), [(goal, ([], []))])]
  19.147 +    end	
  19.148 +  | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
  19.149 +    let
  19.150 +	val name = if name = "" then get_last_fundef thy else name
  19.151 +	val data = the (get_fundef_data name thy)
  19.152 +	val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
  19.153 +    in
  19.154 +	thy |> ProofContext.init
  19.155 +	    |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
  19.156 +	    [(("", []), [(subs, ([], [])), (dcl, ([], []))])]
  19.157 +    end	
  19.158 +
  19.159 +
  19.160 +
  19.161 +
  19.162 +(* congruence rules *)
  19.163 +
  19.164 +val cong_add = Thm.declaration_attribute (map_fundef_congs o cons o safe_mk_meta_eq);
  19.165 +val cong_del = Thm.declaration_attribute (map_fundef_congs o remove (op =) o safe_mk_meta_eq);
  19.166 +
  19.167 +
  19.168 +(* setup *)
  19.169 +
  19.170 +val setup = FundefData.init #> FundefCongs.init 
  19.171 +	#>  Attrib.add_attributes
  19.172 +		[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
  19.173 +
  19.174 +
  19.175 +(* outer syntax *)
  19.176 +
  19.177 +local structure P = OuterParse and K = OuterKeyword in
  19.178 +
  19.179 +val function_decl =
  19.180 +    Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
  19.181 +
  19.182 +val functionP =
  19.183 +  OuterSyntax.command "function" "define general recursive functions" K.thy_goal
  19.184 +    (function_decl >> (fn eqns =>
  19.185 +      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqns)));
  19.186 +
  19.187 +val terminationP =
  19.188 +  OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
  19.189 +  ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
  19.190 +       >> (fn (name,dom) =>
  19.191 +	      Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
  19.192 +
  19.193 +val _ = OuterSyntax.add_parsers [functionP];
  19.194 +val _ = OuterSyntax.add_parsers [terminationP];
  19.195 +
  19.196 +
  19.197 +end;
  19.198 +
  19.199 +
  19.200 +end
  19.201 \ No newline at end of file
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Fri May 05 17:17:21 2006 +0200
    20.3 @@ -0,0 +1,355 @@
    20.4 +(*  Title:      HOL/Tools/function_package/fundef_prep.ML
    20.5 +    ID:         $Id$
    20.6 +    Author:     Alexander Krauss, TU Muenchen
    20.7 +
    20.8 +A package for general recursive function definitions. 
    20.9 +Preparation step: makes auxiliary definitions and generates
   20.10 +proof obligations.
   20.11 +*)
   20.12 +
   20.13 +signature FUNDEF_PREP =
   20.14 +sig
   20.15 +    val prepare_fundef_curried : thm list -> term list -> theory
   20.16 +				 -> FundefCommon.curry_info option * xstring * (FundefCommon.prep_result * theory)
   20.17 +end
   20.18 +
   20.19 +
   20.20 +
   20.21 +
   20.22 +
   20.23 +structure FundefPrep : FUNDEF_PREP =
   20.24 +struct
   20.25 +
   20.26 +
   20.27 +open FundefCommon
   20.28 +open FundefAbbrev 
   20.29 +
   20.30 +
   20.31 +
   20.32 +
   20.33 +fun split_list3 [] = ([],[],[])
   20.34 +  | split_list3 ((x,y,z)::xyzs) = 
   20.35 +    let
   20.36 +	val (xs, ys, zs) = split_list3 xyzs
   20.37 +    in
   20.38 +	(x::xs,y::ys,z::zs)
   20.39 +    end
   20.40 +
   20.41 +
   20.42 +fun build_tree thy f congs (qs, gs, lhs, rhs) =
   20.43 +    let
   20.44 +	(* FIXME: Save precomputed dependencies in a theory data slot *)
   20.45 +	val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
   20.46 +    in
   20.47 +	FundefCtxTree.mk_tree thy congs_deps f rhs
   20.48 +    end
   20.49 +
   20.50 +
   20.51 +fun analyze_eqs eqs =
   20.52 +    let
   20.53 +	fun dest_geq geq = 
   20.54 +	    let
   20.55 +		val qs = add_term_frees (geq, [])
   20.56 +	    in
   20.57 +		case dest_implies_list geq of
   20.58 +		    (gs, Const ("Trueprop", _) $ (Const ("op =", _) $ (f $ lhs) $ rhs)) => 
   20.59 +		    (f, (qs, gs, lhs, rhs))
   20.60 +		  | _ => raise ERROR "Not a guarded equation"
   20.61 +	    end
   20.62 +			       
   20.63 +	val (fs, glrs) = split_list (map dest_geq eqs)
   20.64 +			 
   20.65 +	val f = (hd fs) (* should be equal and a constant... check! *)
   20.66 +
   20.67 +	val used = fold (curry add_term_names) eqs [] (* all names in the eqs *)
   20.68 +		   (* Must check for recursive calls in guards and new vars in rhss *)
   20.69 +    in
   20.70 +	(f, glrs, used)
   20.71 +    end
   20.72 +
   20.73 +
   20.74 +(* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
   20.75 +fun mk_primed_vars thy glrs =
   20.76 +    let
   20.77 +	val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
   20.78 +
   20.79 +	fun rename_vars (qs,gs,lhs,rhs) =
   20.80 +	    let
   20.81 +		val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
   20.82 +		val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
   20.83 +	    in
   20.84 +		(qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
   20.85 +	    end
   20.86 +    in
   20.87 +	map rename_vars glrs
   20.88 +    end
   20.89 +
   20.90 +
   20.91 +fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs =
   20.92 +    let
   20.93 +	val {domT, G, R, h, f, fvar, used, x, ...} = names
   20.94 +				 
   20.95 +	val zv = Var (("z",0), domT) (* for generating h_assums *)
   20.96 +	val xv = Var (("x",0), domT)
   20.97 +	val rw_RI_to_h_assum = (mk_mem (mk_prod (zv, xv), R),
   20.98 +				mk_mem (mk_prod (zv, h $ zv), G))
   20.99 +	val rw_f_to_h = (f, h)
  20.100 +			
  20.101 +	val cqs = map (cterm_of thy) qs
  20.102 +		  
  20.103 +	val vqs = map free_to_var qs
  20.104 +	val cvqs = map (cterm_of thy) vqs
  20.105 +
  20.106 +	val ags = map (assume o cterm_of thy) gs
  20.107 +		  
  20.108 +	val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
  20.109 +	val cqs' = map (cterm_of thy) qs'
  20.110 +
  20.111 +	val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
  20.112 +	val ags' = map (assume o cterm_of thy o rename_vars) gs
  20.113 +	val lhs' = rename_vars lhs
  20.114 +	val rhs' = rename_vars rhs
  20.115 +
  20.116 +	val localize = instantiate ([], cvqs ~~ cqs) 
  20.117 +					   #> fold implies_elim_swp ags
  20.118 +
  20.119 +	val GI = freezeT GI
  20.120 +	val lGI = localize GI
  20.121 +
  20.122 +	val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI))
  20.123 +			  
  20.124 +	fun mk_call_info (RIvs, RI) =
  20.125 +	    let
  20.126 +		fun mk_var0 (v,T) = Var ((v,0),T)
  20.127 +
  20.128 +		val RI = freezeT RI
  20.129 +		val lRI = localize RI
  20.130 +		val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
  20.131 +			  
  20.132 +		val Gh_term = Pattern.rewrite_term thy [rw_RI_to_h_assum, rw_f_to_h] [] (prop_of lRIq)
  20.133 +		val Gh = assume (cterm_of thy Gh_term)
  20.134 +		val Gh' = assume (cterm_of thy (rename_vars Gh_term))
  20.135 +	    in
  20.136 +		{RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
  20.137 +	    end
  20.138 +
  20.139 +	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
  20.140 +    in
  20.141 +	{
  20.142 +	 no=no,
  20.143 +	 qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
  20.144 +	 cqs=cqs, cvqs=cvqs, ags=ags,		 
  20.145 +	 cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
  20.146 +	 GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
  20.147 +	 tree=tree, case_hyp = case_hyp
  20.148 +	}
  20.149 +    end
  20.150 +
  20.151 +
  20.152 +
  20.153 +
  20.154 +(* Chooses fresh free names, declares G and R, defines f and returns a record
  20.155 +   with all the information *)  
  20.156 +fun setup_context (f, glrs, used) fname congs thy =
  20.157 +    let
  20.158 +	val trees = map (build_tree thy f congs) glrs
  20.159 +	val allused = fold FundefCtxTree.add_context_varnames trees used
  20.160 +
  20.161 +	val Const (f_proper_name, fT) = f
  20.162 +	val fxname = Sign.extern_const thy f_proper_name
  20.163 +
  20.164 +	val domT = domain_type fT 
  20.165 +	val ranT = range_type fT
  20.166 +
  20.167 +	val h = Free (variant allused "h", domT --> ranT)
  20.168 +	val y = Free (variant allused "y", ranT)
  20.169 +	val x = Free (variant allused "x", domT)
  20.170 +	val z = Free (variant allused "z", domT)
  20.171 +	val a = Free (variant allused "a", domT)
  20.172 +	val D = Free (variant allused "D", HOLogic.mk_setT domT)
  20.173 +	val P = Free (variant allused "P", domT --> boolT)
  20.174 +	val Pbool = Free (variant allused "P", boolT)
  20.175 +	val fvarname = variant allused "f"
  20.176 +	val fvar = Free (fvarname, domT --> ranT)
  20.177 +
  20.178 +	val GT = mk_relT (domT, ranT)
  20.179 +	val RT = mk_relT (domT, domT)
  20.180 +	val G_name = fname ^ "_graph"
  20.181 +	val R_name = fname ^ "_rel"
  20.182 +
  20.183 +	val glrs' = mk_primed_vars thy glrs
  20.184 +
  20.185 +	val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
  20.186 +
  20.187 +	val G = Const (Sign.intern_const thy G_name, GT)
  20.188 +	val R = Const (Sign.intern_const thy R_name, RT)
  20.189 +	val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
  20.190 +
  20.191 +	val f_eq = Logic.mk_equals (f $ x, 
  20.192 +				    Const ("The", (ranT --> boolT) --> ranT) $
  20.193 +					  Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
  20.194 +
  20.195 +	val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", f_eq), [])] thy
  20.196 +    in
  20.197 +	({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)
  20.198 +    end
  20.199 +
  20.200 +
  20.201 +(* Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
  20.202 +fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
  20.203 +    (implies $ Trueprop (mk_eq (lhs, lhs'))
  20.204 +	     $ Trueprop (mk_eq (rhs, rhs')))
  20.205 +	|> fold_rev (curry Logic.mk_implies) (gs @ gs')
  20.206 +
  20.207 +
  20.208 +(* all proof obligations *)
  20.209 +fun mk_compat_proof_obligations glrs glrs' =
  20.210 +    map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (upairs (glrs ~~ glrs'))
  20.211 +
  20.212 +
  20.213 +fun extract_Ris thy congs f R tree (qs, gs, lhs, rhs) =
  20.214 +    let
  20.215 +	fun add_Ri2 (fixes,assumes) (_ $ arg) _ (_, x) = ([], (FundefCtxTree.export_term (fixes, map prop_of assumes) (mk_relmem (arg, lhs) R)) :: x)
  20.216 +	  | add_Ri2 _ _ _ _ = raise Match
  20.217 +
  20.218 +	val preRis = rev (FundefCtxTree.traverse_tree add_Ri2 tree [])
  20.219 +	val (vRis, preRis_unq) = split_list (map dest_all_all preRis)
  20.220 +
  20.221 +	val Ris = map (fold_rev (curry Logic.mk_implies) gs) preRis_unq
  20.222 +    in
  20.223 +	(map (map dest_Free) vRis, preRis, Ris)
  20.224 +    end
  20.225 +
  20.226 +fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
  20.227 +    let
  20.228 +	val { domT, R, G, f, fvar, h, y, Pbool, ... } = names
  20.229 +
  20.230 +	val z = Var (("z",0), domT)
  20.231 +	val x = Var (("x",0), domT)
  20.232 +
  20.233 +	val rew1 = (mk_mem (mk_prod (z, x), R),
  20.234 +		    mk_mem (mk_prod (z, fvar $ z), G))
  20.235 +	val rew2 = (f, fvar)
  20.236 +
  20.237 +	val prems = map (Pattern.rewrite_term thy [rew1, rew2] []) Ris
  20.238 +	val rhs' = Pattern.rewrite_term thy [rew2] [] rhs 
  20.239 +    in
  20.240 +	mk_relmem (lhs, rhs') G
  20.241 +		  |> fold_rev (curry Logic.mk_implies) prems
  20.242 +		  |> fold_rev (curry Logic.mk_implies) gs
  20.243 +    end
  20.244 +
  20.245 +fun mk_completeness names glrs =
  20.246 +    let
  20.247 +	val {domT, x, Pbool, ...} = names
  20.248 +
  20.249 +	fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
  20.250 +						|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
  20.251 +						|> fold_rev (curry Logic.mk_implies) gs
  20.252 +						|> fold_rev mk_forall qs
  20.253 +    in
  20.254 +	Trueprop Pbool
  20.255 +		 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
  20.256 +    end
  20.257 +
  20.258 +
  20.259 +fun extract_conditions thy names trees congs =
  20.260 +    let
  20.261 +	val {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
  20.262 +
  20.263 +	val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
  20.264 +	val Gis = map2 (mk_GIntro thy names) glrs preRiss
  20.265 +	val complete = mk_completeness names glrs
  20.266 +	val compat = mk_compat_proof_obligations glrs glrs'
  20.267 +    in
  20.268 +	{G_intros = Gis, vRiss = vRiss, R_intross = Riss, complete = complete, compat = compat}
  20.269 +    end
  20.270 +
  20.271 +
  20.272 +fun inductive_def defs (thy, const) =
  20.273 +    let
  20.274 + 	val (thy, {intrs, elims = [elim], ...}) = 
  20.275 +	    InductivePackage.add_inductive_i true (*verbose*)
  20.276 +					     false (*add_consts*)
  20.277 +					     "" (* no altname *)
  20.278 +					     false (* no coind *)
  20.279 +					     false (* elims, please *)
  20.280 +					     false (* induction thm please *)
  20.281 +					     [const] (* the constant *)
  20.282 +					     (map (fn t=>(("", t),[])) defs) (* the intros *)
  20.283 +					     [] (* no special monos *)
  20.284 +					     thy
  20.285 +    in
  20.286 +	(intrs, (thy, elim))
  20.287 +    end
  20.288 +
  20.289 +
  20.290 +
  20.291 +(*
  20.292 + * This is the first step in a function definition.
  20.293 + *
  20.294 + * Defines the function, the graph and the termination relation, synthesizes completeness
  20.295 + * and comatibility conditions and returns everything.
  20.296 + *)
  20.297 +fun prepare_fundef congs eqs fname thy =
  20.298 +    let
  20.299 +	val (names, thy) = setup_context (analyze_eqs eqs) fname congs thy
  20.300 +	val {G, R, glrs, trees, ...} = names
  20.301 +
  20.302 +	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
  20.303 +
  20.304 +	val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G)
  20.305 +	val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R)
  20.306 +
  20.307 +	val n = length glrs
  20.308 +	val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
  20.309 +    in
  20.310 +	({names = names, complete=complete, compat=compat, clauses = clauses},
  20.311 +	 thy) 
  20.312 +    end
  20.313 +
  20.314 +
  20.315 +
  20.316 +
  20.317 +fun prepare_fundef_curried congs eqs thy =
  20.318 +    let
  20.319 +	val lhs1 = hd eqs
  20.320 +		   |> dest_implies_list |> snd
  20.321 +		   |> HOLogic.dest_Trueprop
  20.322 +		   |> HOLogic.dest_eq |> fst
  20.323 +
  20.324 +	val (f, args) = strip_comb lhs1
  20.325 +	val Const(fname, fT) = f
  20.326 +	val fxname = Sign.extern_const thy fname
  20.327 +    in
  20.328 +	if (length args < 2)
  20.329 +	then (NONE, fxname, (prepare_fundef congs eqs fxname thy))
  20.330 +	else
  20.331 +	    let
  20.332 +		val (caTs, uaTs) = chop (length args) (binder_types fT)
  20.333 +		val newtype = foldr1 HOLogic.mk_prodT caTs --> (uaTs ---> body_type fT)
  20.334 +		val gxname = fxname ^ "_tupled"
  20.335 +			     
  20.336 +    		val thy = Sign.add_consts_i [(gxname, newtype, NoSyn)] thy
  20.337 +		val gc = Const (Sign.intern_const thy gxname, newtype)
  20.338 +			 
  20.339 +		val vars = map2 (fn i => fn T => Free ("x"^(string_of_int i), T))
  20.340 +				(1 upto (length caTs)) caTs
  20.341 +
  20.342 +		val f_lambda = fold_rev lambda vars (gc $ foldr1 HOLogic.mk_prod vars)
  20.343 +			       
  20.344 +		val def = Logic.mk_equals (fold (curry ((op $) o Library.swap)) vars f,
  20.345 +					   gc $ foldr1 HOLogic.mk_prod vars)
  20.346 +			  
  20.347 +		val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy
  20.348 +				      
  20.349 +		val g_to_f_ss = HOL_basic_ss addsimps [symmetric f_def]
  20.350 +		val eqs_tupled = map (Pattern.rewrite_term thy [(f, f_lambda)] []) eqs
  20.351 +	    in
  20.352 +		(SOME {curry_ss = g_to_f_ss, argTs = caTs}, fxname, prepare_fundef congs eqs_tupled fxname thy)
  20.353 +	    end
  20.354 +    end
  20.355 +
  20.356 +
  20.357 +
  20.358 +end
  20.359 \ No newline at end of file
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Fri May 05 17:17:21 2006 +0200
    21.3 @@ -0,0 +1,585 @@
    21.4 +(*  Title:      HOL/Tools/function_package/fundef_proof.ML
    21.5 +    ID:         $Id$
    21.6 +    Author:     Alexander Krauss, TU Muenchen
    21.7 +
    21.8 +A package for general recursive function definitions. 
    21.9 +Internal proofs.
   21.10 +*)
   21.11 +
   21.12 +
   21.13 +signature FUNDEF_PROOF =
   21.14 +sig
   21.15 +
   21.16 +    val mk_partial_rules_curried : theory -> thm list -> FundefCommon.curry_info option -> FundefCommon.prep_result 
   21.17 +				   -> thm -> thm list -> FundefCommon.fundef_result
   21.18 +end
   21.19 +
   21.20 +
   21.21 +structure FundefProof : FUNDEF_PROOF = 
   21.22 +struct
   21.23 +
   21.24 +open FundefCommon
   21.25 +open FundefAbbrev
   21.26 +
   21.27 +(* Theory dependencies *)
   21.28 +val subsetD = thm "subsetD"
   21.29 +val subset_refl = thm "subset_refl"
   21.30 +val split_apply = thm "Product_Type.split"
   21.31 +val wf_induct_rule = thm "wf_induct_rule";
   21.32 +val Pair_inject = thm "Product_Type.Pair_inject";
   21.33 +
   21.34 +val acc_induct_rule = thm "acc_induct_rule" (* from: Accessible_Part *)
   21.35 +val acc_downward = thm "acc_downward"
   21.36 +val accI = thm "accI"
   21.37 +
   21.38 +val ex1_implies_ex = thm "fundef_ex1_existence"   (* from: Fundef.thy *) 
   21.39 +val ex1_implies_un = thm "fundef_ex1_uniqueness"
   21.40 +val ex1_implies_iff = thm "fundef_ex1_iff"
   21.41 +val acc_subset_induct = thm "acc_subset_induct"
   21.42 +
   21.43 +
   21.44 +
   21.45 +
   21.46 +
   21.47 +    
   21.48 +fun mk_simp thy (names:naming_context) f_iff graph_is_function clause valthm =
   21.49 +    let
   21.50 +	val {R, acc_R, domT, z, ...} = names
   21.51 +	val {qs, cqs, gs, lhs, rhs, ...} = clause
   21.52 +	val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, acc_R))) (* "lhs : acc R" *)
   21.53 +	val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *)
   21.54 +    in
   21.55 +	((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
   21.56 +	    |> (fn it => it COMP graph_is_function)
   21.57 +	    |> implies_intr z_smaller
   21.58 +	    |> forall_intr (cterm_of thy z)
   21.59 +	    |> (fn it => it COMP valthm)
   21.60 +	    |> implies_intr lhs_acc 
   21.61 +	    |> asm_simplify (HOL_basic_ss addsimps [f_iff])
   21.62 +	    |> fold forall_intr cqs
   21.63 +	    |> forall_elim_vars 0
   21.64 +	    |> varifyT
   21.65 +	    |> Drule.close_derivation
   21.66 +    end
   21.67 +
   21.68 +
   21.69 +
   21.70 +
   21.71 +fun mk_partial_induct_rule thy (names:naming_context) complete_thm clauses =
   21.72 +    let
   21.73 +	val {domT, R, acc_R, x, z, a, P, D, ...} = names
   21.74 +
   21.75 +	val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D))))
   21.76 +	val a_D = cterm_of thy (Trueprop (mk_mem (a, D)))
   21.77 +
   21.78 +	val D_subset = cterm_of thy (Trueprop (mk_subset domT D acc_R))
   21.79 +
   21.80 +	val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
   21.81 +	    mk_forall x
   21.82 +		      (mk_forall z (Logic.mk_implies (Trueprop (mk_mem (x, D)),
   21.83 +						      Logic.mk_implies (mk_relmem (z, x) R,
   21.84 +									Trueprop (mk_mem (z, D))))))
   21.85 +		      |> cterm_of thy
   21.86 +
   21.87 +
   21.88 +	(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   21.89 +	val ihyp = all domT $ Abs ("z", domT, 
   21.90 +				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
   21.91 +					   $ Trueprop (P $ Bound 0))
   21.92 +		       |> cterm_of thy
   21.93 +
   21.94 +	val aihyp = assume ihyp |> forall_elim_vars 0
   21.95 +
   21.96 +	fun prove_case clause =
   21.97 +	    let
   21.98 +		val {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause
   21.99 +								       
  21.100 +		val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
  21.101 +		val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
  21.102 +		val sih = full_simplify replace_x_ss aihyp
  21.103 +					
  21.104 +					(* FIXME: Variable order destroyed by forall_intr_vars *)
  21.105 +		val P_recs = map (fn {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs   (*  [P rec1, P rec2, ... ]  *)
  21.106 +			     
  21.107 +		val step = Trueprop (P $ lhs)
  21.108 +				    |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
  21.109 +				    |> fold_rev (curry Logic.mk_implies) gs
  21.110 +				    |> curry Logic.mk_implies (Trueprop (mk_mem (lhs, D)))
  21.111 +				    |> fold_rev mk_forall qs
  21.112 +				    |> cterm_of thy
  21.113 +			   
  21.114 +		val P_lhs = assume step
  21.115 +				   |> fold forall_elim cqs
  21.116 +				   |> implies_elim_swp lhs_D 
  21.117 +				   |> fold_rev implies_elim_swp ags
  21.118 +				   |> fold implies_elim_swp P_recs
  21.119 +			    
  21.120 +		val res = cterm_of thy (Trueprop (P $ x))
  21.121 +				   |> Simplifier.rewrite replace_x_ss
  21.122 +				   |> symmetric (* P lhs == P x *)
  21.123 +				   |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
  21.124 +				   |> implies_intr (cprop_of case_hyp)
  21.125 +				   |> fold_rev (implies_intr o cprop_of) ags
  21.126 +				   |> fold_rev forall_intr cqs
  21.127 +	    in
  21.128 +		(res, step)
  21.129 +	    end
  21.130 +
  21.131 +	val (cases, steps) = split_list (map prove_case clauses)
  21.132 +
  21.133 +	val istep =  complete_thm
  21.134 +			 |> fold (curry op COMP) cases (*  P x  *)
  21.135 +			 |> implies_intr ihyp
  21.136 +			 |> implies_intr (cprop_of x_D)
  21.137 +			 |> forall_intr (cterm_of thy x)
  21.138 +			   
  21.139 +	val subset_induct_rule = 
  21.140 +	    acc_subset_induct
  21.141 +		|> (curry op COMP) (assume D_subset)
  21.142 +		|> (curry op COMP) (assume D_dcl)
  21.143 +		|> (curry op COMP) (assume a_D)
  21.144 +		|> (curry op COMP) istep
  21.145 +		|> fold_rev implies_intr steps
  21.146 +		|> implies_intr a_D
  21.147 +		|> implies_intr D_dcl
  21.148 +		|> implies_intr D_subset
  21.149 +		|> forall_intr_frees
  21.150 +		|> forall_elim_vars 0
  21.151 +
  21.152 +	val simple_induct_rule =
  21.153 +	    subset_induct_rule
  21.154 +		|> instantiate' [] [SOME (cterm_of thy acc_R)]
  21.155 +		|> (curry op COMP) subset_refl
  21.156 +		|> (curry op COMP) (acc_downward
  21.157 +					|> (instantiate' [SOME (ctyp_of thy domT)]
  21.158 +							 (map (SOME o cterm_of thy) [x, R, z]))
  21.159 +					|> forall_intr (cterm_of thy z)
  21.160 +					|> forall_intr (cterm_of thy x))
  21.161 +    in
  21.162 +	(varifyT subset_induct_rule, varifyT simple_induct_rule)
  21.163 +    end
  21.164 +
  21.165 +
  21.166 +
  21.167 +
  21.168 +
  21.169 +(***********************************************)
  21.170 +(* Compat thms are stored in normal form (with vars) *)
  21.171 +
  21.172 +(* replace this by a table later*)
  21.173 +fun store_compat_thms 0 cts = []
  21.174 +  | store_compat_thms n cts =
  21.175 +    let
  21.176 +	val (cts1, cts2) = chop n cts
  21.177 +    in
  21.178 +	(cts1 :: store_compat_thms (n - 1) cts2)
  21.179 +    end
  21.180 +
  21.181 +
  21.182 +(* needs i <= j *)
  21.183 +fun lookup_compat_thm i j cts =
  21.184 +    nth (nth cts (i - 1)) (j - i)
  21.185 +(***********************************************)
  21.186 +
  21.187 +
  21.188 +(* recover the order of Vars *)
  21.189 +fun get_var_order thy (clauses: clause_info list) =
  21.190 +    map (fn ({cqs,...}, {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
  21.191 +
  21.192 +
  21.193 +(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
  21.194 +(* if j < i, then turn around *)
  21.195 +fun get_compat_thm thy cts clausei clausej =
  21.196 +    let 
  21.197 +	val {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
  21.198 +	val {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
  21.199 +
  21.200 +	val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
  21.201 +    in if j < i then
  21.202 +	   let 
  21.203 +	       val (var_ord, compat) = lookup_compat_thm j i cts
  21.204 +	   in
  21.205 +	       compat         (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
  21.206 +		|> instantiate ([],(var_ord ~~ (qsj' @ qsi))) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *)
  21.207 +		|> fold implies_elim_swp gsj'
  21.208 +		|> fold implies_elim_swp gsi
  21.209 +		|> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
  21.210 +	   end
  21.211 +       else
  21.212 +	   let
  21.213 +	       val (var_ord, compat) = lookup_compat_thm i j cts
  21.214 +	   in
  21.215 +	       compat        (* "?Gsi => ?Gsj' => ?lhsi = ?lhsj' ==> ?rhsi = ?rhsj'" *)
  21.216 +	         |> instantiate ([], (var_ord ~~ (qsi @ qsj'))) (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
  21.217 +		 |> fold implies_elim_swp gsi
  21.218 +		 |> fold implies_elim_swp gsj'
  21.219 +		 |> implies_elim_swp (assume lhsi_eq_lhsj')
  21.220 +		 |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
  21.221 +	   end
  21.222 +    end
  21.223 +
  21.224 +
  21.225 +
  21.226 +
  21.227 +
  21.228 +(* Generates the replacement lemma with primed variables. A problem here is that one should not do
  21.229 +the complete requantification at the end to replace the variables. One should find a way to be more efficient
  21.230 +here. *)
  21.231 +fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = 
  21.232 +    let 
  21.233 +	val {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
  21.234 +	val {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
  21.235 +
  21.236 +	val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
  21.237 +
  21.238 +	val Ris = map #lRIq RCs
  21.239 +	val h_assums = map #Gh RCs
  21.240 +	val h_assums' = map #Gh' RCs
  21.241 +
  21.242 +	val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
  21.243 +
  21.244 +	val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
  21.245 +
  21.246 +	val replace_lemma = (eql RS meta_eq_to_obj_eq)
  21.247 +				|> implies_intr (cprop_of case_hyp)
  21.248 +				|> fold_rev (implies_intr o cprop_of) h_assums
  21.249 +				|> fold_rev (implies_intr o cprop_of) ags
  21.250 +				|> fold_rev forall_intr cqs
  21.251 +				|> fold forall_elim cqs'
  21.252 +				|> fold implies_elim_swp ags'
  21.253 +				|> fold implies_elim_swp h_assums'
  21.254 +    in
  21.255 +	replace_lemma
  21.256 +    end
  21.257 +
  21.258 +
  21.259 +
  21.260 +
  21.261 +fun mk_uniqueness_clause thy (names:naming_context) compat_store (clausei:clause_info) (clausej:clause_info) RLj =
  21.262 +    let
  21.263 +	val {f, h, y, ...} = names
  21.264 +	val {no=i, lhs=lhsi, case_hyp, ...} = clausei
  21.265 +	val {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
  21.266 +
  21.267 +	val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
  21.268 +	val compat = get_compat_thm thy compat_store clausei clausej
  21.269 +	val Ghsj' = map (fn {Gh', ...} => Gh') RCsj
  21.270 +
  21.271 +	val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
  21.272 +	val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j'	*)
  21.273 +
  21.274 +	val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
  21.275 +    in
  21.276 +	(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
  21.277 +        |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
  21.278 +	|> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
  21.279 +	|> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
  21.280 +	|> implies_intr (cprop_of y_eq_rhsj'h)
  21.281 +	|> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
  21.282 +	|> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
  21.283 +	|> implies_elim_swp eq_pairs
  21.284 +	|> fold_rev (implies_intr o cprop_of) Ghsj' 
  21.285 +	|> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
  21.286 +	|> implies_intr (cprop_of eq_pairs)
  21.287 +	|> fold_rev forall_intr ordcqs'j
  21.288 +    end
  21.289 +
  21.290 +
  21.291 +
  21.292 +fun mk_uniqueness_case thy (names:naming_context) ihyp ih_intro G_cases compat_store clauses rep_lemmas (clausei:clause_info) =
  21.293 +    let
  21.294 +	val {x, y, G, fvar, f, ranT, ...} = names
  21.295 +	val {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
  21.296 +
  21.297 +	val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
  21.298 +
  21.299 +	fun prep_RC ({lRIq,RIvs, ...} : rec_call_info) = lRIq
  21.300 +							     |> fold (forall_elim o cterm_of thy o Free) RIvs
  21.301 +							     |> (fn it => it RS ih_intro_case)
  21.302 +							     |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  21.303 +
  21.304 +	val existence = lGI |> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])
  21.305 +			    |> fold (curry op COMP o prep_RC) RCs 
  21.306 +
  21.307 +
  21.308 +	val a = cterm_of thy (mk_prod (lhs, y))
  21.309 +	val P = cterm_of thy (mk_eq (y, rhs))
  21.310 +	val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
  21.311 +
  21.312 +	val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
  21.313 +
  21.314 +	val uniqueness = G_cases 
  21.315 +			     |> instantiate' [] [SOME a, SOME P]
  21.316 +			     |> implies_elim_swp a_in_G
  21.317 +			     |> fold implies_elim_swp unique_clauses
  21.318 +			     |> implies_intr (cprop_of a_in_G)
  21.319 +			     |> forall_intr (cterm_of thy y) 
  21.320 +
  21.321 +	val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
  21.322 +
  21.323 +	val exactly_one =
  21.324 +	    ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
  21.325 +		 |> curry (op COMP) existence
  21.326 +		 |> curry (op COMP) uniqueness
  21.327 +		 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
  21.328 +		 |> implies_intr (cprop_of case_hyp) 
  21.329 +		 |> fold_rev (implies_intr o cprop_of) ags
  21.330 +		 |> fold_rev forall_intr cqs
  21.331 +	val function_value =
  21.332 +	    existence 
  21.333 +		|> fold_rev (implies_intr o cprop_of) ags
  21.334 +		|> implies_intr ihyp
  21.335 +		|> implies_intr (cprop_of case_hyp)
  21.336 +		|> forall_intr (cterm_of thy x)
  21.337 +		|> forall_elim (cterm_of thy lhs)
  21.338 +		|> curry (op RS) refl
  21.339 +    in
  21.340 +	(exactly_one, function_value)
  21.341 +    end
  21.342 +
  21.343 +
  21.344 +
  21.345 +(* Does this work with Guards??? *)
  21.346 +fun mk_domain_intro thy (names:naming_context) R_cases clause =
  21.347 +    let
  21.348 +	val {z, R, acc_R, ...} = names
  21.349 +	val {qs, gs, lhs, rhs, ...} = clause
  21.350 +
  21.351 +	val z_lhs = cterm_of thy (HOLogic.mk_prod (z,lhs))
  21.352 +	val z_acc = cterm_of thy (HOLogic.mk_mem (z,acc_R))
  21.353 +
  21.354 +	val icases = R_cases 
  21.355 +			 |> instantiate' [] [SOME z_lhs, SOME z_acc]
  21.356 +			 |> forall_intr_frees
  21.357 +			 |> forall_elim_vars 0
  21.358 +
  21.359 +	val goal = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
  21.360 +    in
  21.361 +	Goal.init goal 
  21.362 +		  |> SINGLE (resolve_tac [accI] 1) |> the
  21.363 +		  |> SINGLE (eresolve_tac [icases] 1)  |> the
  21.364 +		  |> SINGLE (CLASIMPSET auto_tac) |> the
  21.365 +		  |> Goal.conclude
  21.366 +		  |> forall_intr_frees
  21.367 +		  |> forall_elim_vars 0
  21.368 +		  |> varifyT
  21.369 +    end
  21.370 +
  21.371 +
  21.372 +
  21.373 +
  21.374 +fun mk_nest_term_case thy (names:naming_context) R' ihyp clause =
  21.375 +    let
  21.376 +	val {x, z, ...} = names
  21.377 +	val {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause
  21.378 +
  21.379 +	val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
  21.380 +
  21.381 +	fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
  21.382 +	    let
  21.383 +		val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
  21.384 +
  21.385 +		val hyp = mk_relmem (arg, lhs) R'
  21.386 +				    |> fold_rev (curry Logic.mk_implies o prop_of) used
  21.387 +				    |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
  21.388 +				    |> fold_rev (curry Logic.mk_implies o prop_of) ags
  21.389 +				    |> fold_rev mk_forall qs
  21.390 +				    |> cterm_of thy
  21.391 +
  21.392 +		val thm = assume hyp
  21.393 +				 |> fold forall_elim cqs
  21.394 +				 |> fold implies_elim_swp ags
  21.395 +				 |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
  21.396 +				 |> fold implies_elim_swp used
  21.397 +
  21.398 +		val acc = thm COMP ih_case
  21.399 +
  21.400 +		val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
  21.401 +
  21.402 +		val arg_eq_z = (assume z_eq_arg) RS sym
  21.403 +
  21.404 +		val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
  21.405 +				     |> implies_intr (cprop_of case_hyp)
  21.406 +				     |> implies_intr z_eq_arg
  21.407 +
  21.408 +		val zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs))))
  21.409 +
  21.410 +		val z_acc' = z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject)
  21.411 +
  21.412 +		val ethm = z_acc'
  21.413 +			       |> FundefCtxTree.export_thm thy (fixes, (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes))
  21.414 +			       |> fold_rev forall_intr cqs
  21.415 +
  21.416 +
  21.417 +		val sub' = sub @ [(([],[]), acc)]
  21.418 +	    in
  21.419 +		(sub', (hyp :: hyps, ethm :: thms))
  21.420 +	    end
  21.421 +	  | step _ _ _ _ = raise Match
  21.422 +    in
  21.423 +	FundefCtxTree.traverse_tree step tree
  21.424 +    end
  21.425 +
  21.426 +
  21.427 +fun mk_nest_term_rule thy (names:naming_context) clauses =
  21.428 +    let
  21.429 +	val { R, acc_R, domT, x, z, ... } = names
  21.430 +
  21.431 +	val R_elim = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R))))))
  21.432 +
  21.433 +	val R' = Free ("R", fastype_of R)
  21.434 +
  21.435 +	val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wf", mk_relT (domT, domT) --> boolT) $ R')) (* "wf R'" *)
  21.436 +
  21.437 +	(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
  21.438 +	val ihyp = all domT $ Abs ("z", domT, 
  21.439 +				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R')
  21.440 +					   $ Trueprop ((Const ("op :", [domT, HOLogic.mk_setT domT] ---> boolT))
  21.441 +							   $ Bound 0 $ acc_R))
  21.442 +		       |> cterm_of thy
  21.443 +
  21.444 +	val ihyp_a = assume ihyp |> forall_elim_vars 0
  21.445 +
  21.446 +	val z_ltR_x = cterm_of thy (mk_relmem (z, x) R) (* "(z, x) : R" *)
  21.447 +	val z_acc = cterm_of thy (mk_mem (z, acc_R))
  21.448 +
  21.449 +	val (hyps,cases) = fold (mk_nest_term_case thy names R' ihyp_a) clauses ([],[])
  21.450 +    in
  21.451 +	R_elim
  21.452 +	    |> freezeT
  21.453 +	    |> instantiate' [] [SOME (cterm_of thy (mk_prod (z,x))), SOME z_acc]
  21.454 +	    |> curry op COMP (assume z_ltR_x)
  21.455 +	    |> fold_rev (curry op COMP) cases
  21.456 +	    |> implies_intr z_ltR_x
  21.457 +	    |> forall_intr (cterm_of thy z)
  21.458 +	    |> (fn it => it COMP accI)
  21.459 +	    |> implies_intr ihyp
  21.460 +	    |> forall_intr (cterm_of thy x)
  21.461 +	    |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
  21.462 +	    |> implies_elim_swp (assume wfR')
  21.463 +	    |> fold implies_intr hyps
  21.464 +	    |> implies_intr wfR'
  21.465 +	    |> forall_intr (cterm_of thy R')
  21.466 +	    |> forall_elim_vars 0
  21.467 +	    |> varifyT
  21.468 +    end
  21.469 +
  21.470 +
  21.471 +
  21.472 +
  21.473 +fun mk_partial_rules thy congs data complete_thm compat_thms =
  21.474 +    let
  21.475 +	val {names, clauses, complete, compat, ...} = data
  21.476 +	val {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
  21.477 +
  21.478 +(*	val _ = Output.debug "closing derivation: completeness"
  21.479 +	val _ = Output.debug (Proofterm.size_of_proof (proof_of complete_thm))
  21.480 +	val _ = Output.debug (map (Proofterm.size_of_proof o proof_of) compat_thms)*)
  21.481 +	val complete_thm = Drule.close_derivation complete_thm
  21.482 +(*	val _ = Output.debug "closing derivation: compatibility"*)
  21.483 +	val compat_thms = map Drule.close_derivation compat_thms
  21.484 +(*	val _ = Output.debug "  done"*)
  21.485 +
  21.486 +	val complete_thm_fr = freezeT complete_thm
  21.487 +	val compat_thms_fr = map freezeT compat_thms
  21.488 +	val f_def_fr = freezeT f_def
  21.489 +
  21.490 +	val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] 
  21.491 +						[SOME (cterm_of thy f), SOME (cterm_of thy G)])
  21.492 +				      #> curry op COMP (forall_intr_vars f_def_fr)
  21.493 +			  
  21.494 +	val inst_ex1_ex = instantiate_and_def ex1_implies_ex
  21.495 +	val inst_ex1_un = instantiate_and_def ex1_implies_un
  21.496 +	val inst_ex1_iff = instantiate_and_def ex1_implies_iff
  21.497 +
  21.498 +	(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
  21.499 +	val ihyp = all domT $ Abs ("z", domT, 
  21.500 +				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
  21.501 +					   $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
  21.502 +							     Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
  21.503 +		       |> cterm_of thy
  21.504 +		   
  21.505 +	val ihyp_thm = assume ihyp
  21.506 +			      |> forall_elim_vars 0
  21.507 +		       
  21.508 +	val ih_intro = ihyp_thm RS inst_ex1_ex
  21.509 +	val ih_elim = ihyp_thm RS inst_ex1_un
  21.510 +
  21.511 +	val _ = Output.debug "Proving Replacement lemmas..."
  21.512 +	val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
  21.513 +
  21.514 +	val n = length clauses
  21.515 +	val var_order = get_var_order thy clauses
  21.516 +	val compat_store = store_compat_thms n (var_order ~~ compat_thms_fr)
  21.517 +
  21.518 +	val R_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R)))))) |> freezeT
  21.519 +	val G_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const G)))))) |> freezeT
  21.520 +
  21.521 +	val _ = Output.debug "Proving cases for unique existence..."
  21.522 +	val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses repLemmas) clauses)
  21.523 +
  21.524 +	val _ = Output.debug "Proving: Graph is a function"
  21.525 +	val graph_is_function = complete_thm_fr
  21.526 +				    |> fold (curry op COMP) ex1s
  21.527 +				    |> implies_intr (ihyp)
  21.528 +				    |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
  21.529 +				    |> forall_intr (cterm_of thy x)
  21.530 +				    |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
  21.531 +				    |> Drule.close_derivation
  21.532 +
  21.533 +	val f_iff = (graph_is_function RS inst_ex1_iff)
  21.534 +
  21.535 +	val _ = Output.debug "Proving simplification rules"
  21.536 +	val psimps  = map2 (mk_simp thy names f_iff graph_is_function) clauses values
  21.537 +
  21.538 +	val _ = Output.debug "Proving partial induction rule"
  21.539 +	val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy names complete_thm clauses
  21.540 +
  21.541 +	val _ = Output.debug "Proving nested termination rule"
  21.542 +	val total_intro = mk_nest_term_rule thy names clauses
  21.543 +
  21.544 +	val _ = Output.debug "Proving domain introduction rules"
  21.545 +	val dom_intros = map (mk_domain_intro thy names R_cases) clauses
  21.546 +    in 
  21.547 +	{f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
  21.548 +	 psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
  21.549 +	 dom_intros=dom_intros}
  21.550 +    end
  21.551 +
  21.552 +
  21.553 +fun curry_induct_rule thy argTs induct =
  21.554 +    let
  21.555 +	val vnums = (1 upto (length argTs))
  21.556 +	val avars = map2 (fn T => fn i => Var (("a",i), T)) argTs vnums
  21.557 +	val atup = foldr1 HOLogic.mk_prod avars
  21.558 +	val Q = Var (("P",1),argTs ---> HOLogic.boolT)
  21.559 +	val P = tupled_lambda atup (list_comb (Q, avars))
  21.560 +    in
  21.561 +	induct |> freezeT
  21.562 +	       |> instantiate' [] [SOME (cterm_of thy atup), SOME (cterm_of thy P)]
  21.563 +	       |> zero_var_indexes
  21.564 +	       |> full_simplify (HOL_basic_ss addsimps [split_apply])
  21.565 +	       |> varifyT
  21.566 +    end
  21.567 +
  21.568 +
  21.569 +
  21.570 +fun mk_partial_rules_curried thy congs NONE data complete_thm compat_thms =
  21.571 +    mk_partial_rules thy congs data complete_thm compat_thms 
  21.572 +  | mk_partial_rules_curried thy congs (SOME {curry_ss, argTs}) data complete_thm compat_thms =
  21.573 +    let
  21.574 +	val {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} =
  21.575 +	    mk_partial_rules thy congs data complete_thm compat_thms 
  21.576 +	val cpsimps = map (simplify curry_ss) psimps
  21.577 +	val cpinduct = full_simplify curry_ss simple_pinduct
  21.578 +				     |> curry_induct_rule thy argTs
  21.579 +	val cdom_intros = map (full_simplify curry_ss) dom_intros
  21.580 +	val ctotal_intro = full_simplify curry_ss total_intro
  21.581 +    in
  21.582 +	{f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
  21.583 +	 psimps=cpsimps, subset_pinduct=subset_pinduct, simple_pinduct=cpinduct, total_intro=ctotal_intro, dom_intros=cdom_intros}
  21.584 +    end
  21.585 +
  21.586 +end
  21.587 +
  21.588 +
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/HOL/Tools/function_package/termination.ML	Fri May 05 17:17:21 2006 +0200
    22.3 @@ -0,0 +1,67 @@
    22.4 +(*  Title:      HOL/Tools/function_package/termination.ML
    22.5 +    ID:         $Id$
    22.6 +    Author:     Alexander Krauss, TU Muenchen
    22.7 +
    22.8 +A package for general recursive function definitions. 
    22.9 +Termination goals...
   22.10 +*)
   22.11 +
   22.12 +
   22.13 +signature FUNDEF_TERMINATION =
   22.14 +sig
   22.15 +    val mk_total_termination_goal : FundefCommon.fundef_result -> term
   22.16 +    val mk_partial_termination_goal : theory -> FundefCommon.fundef_result -> string -> term * term
   22.17 +end
   22.18 +
   22.19 +structure FundefTermination : FUNDEF_TERMINATION =
   22.20 +struct
   22.21 +
   22.22 +
   22.23 +open FundefCommon
   22.24 +open FundefAbbrev
   22.25 +
   22.26 +fun mk_total_termination_goal (data: fundef_result) =
   22.27 +    let
   22.28 +	val {R, f, ... } = data
   22.29 +
   22.30 +	val domT = domain_type (fastype_of f)
   22.31 +	val x = Free ("x", domT)
   22.32 +    in
   22.33 +	Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
   22.34 +    end
   22.35 +
   22.36 +fun mk_partial_termination_goal thy (data: fundef_result) dom =
   22.37 +    let
   22.38 +	val {R, f, ... } = data
   22.39 +
   22.40 +	val domT = domain_type (fastype_of f)
   22.41 +	val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom
   22.42 +	val DT = type_of D
   22.43 +	val idomT = HOLogic.dest_setT DT
   22.44 +
   22.45 +	val x = Free ("x", idomT)
   22.46 +	val z = Free ("z", idomT)
   22.47 +	val Rname = fst (dest_Const R)
   22.48 +	val iRT = mk_relT (idomT, idomT)
   22.49 +	val iR = Const (Rname, iRT)
   22.50 +		
   22.51 +
   22.52 +	val subs = HOLogic.mk_Trueprop 
   22.53 +			 (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
   22.54 +				(Const (acc_const_name, iRT --> DT) $ iR))
   22.55 +			 |> Type.freeze
   22.56 +
   22.57 +	val dcl = mk_forall x
   22.58 +			    (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
   22.59 +							    Logic.mk_implies (mk_relmem (z, x) iR,
   22.60 +									      Trueprop (mk_mem (z, D))))))
   22.61 +			    |> Type.freeze
   22.62 +    in
   22.63 +	(subs, dcl)
   22.64 +    end
   22.65 +
   22.66 +end
   22.67 +
   22.68 +
   22.69 +
   22.70 +
    23.1 --- a/src/HOL/Tools/recdef_package.ML	Fri May 05 16:50:58 2006 +0200
    23.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri May 05 17:17:21 2006 +0200
    23.3 @@ -30,7 +30,7 @@
    23.4    val recdef_tc_i: bstring * attribute list -> string -> int option -> theory -> Proof.state
    23.5    val setup: theory -> theory
    23.6  
    23.7 -(* HACK: This has to be exported, since the new recdef-package uses the same hints *)
    23.8 +(* HACK: This has to be exported, since the new fundef-package uses the same hints *)
    23.9    val get_local_hints: ProofContext.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
   23.10    val get_global_hints: theory -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
   23.11  end;
   23.12 @@ -300,7 +300,7 @@
   23.13    LocalRecdefData.init #>
   23.14    Attrib.add_attributes
   23.15     [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
   23.16 -    (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
   23.17 +    (recdef_congN, Attrib.add_del_args (FundefPackage.cong_add o cong_add) (FundefPackage.cong_del o cong_del), "declaration of recdef cong rule"),
   23.18      (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];
   23.19  
   23.20