HOL/Tools/function_package: Added support for mutual recursive definitions.
authorkrauss
Mon Jun 05 14:26:07 2006 +0200 (2006-06-05)
changeset 19770be5c23ebe1eb
parent 19769 c40ce2de2020
child 19771 b4a0da62126e
HOL/Tools/function_package: Added support for mutual recursive definitions.
src/HOL/Datatype.thy
src/HOL/FunDef.thy
src/HOL/List.thy
src/HOL/Recdef.thy
src/HOL/Tools/function_package/auto_term.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/mutual.ML
src/HOL/Tools/function_package/sum_tools.ML
src/HOL/Tools/function_package/termination.ML
src/HOL/Tools/recdef_package.ML
src/HOL/ex/Fundefs.thy
     1.1 --- a/src/HOL/Datatype.thy	Mon Jun 05 14:22:58 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Mon Jun 05 14:26:07 2006 +0200
     1.3 @@ -6,8 +6,7 @@
     1.4  header {* Datatypes *}
     1.5  
     1.6  theory Datatype
     1.7 -imports Datatype_Universe FunDef
     1.8 -uses ("Tools/function_package/fundef_datatype.ML")
     1.9 +imports Datatype_Universe
    1.10  begin
    1.11  
    1.12  subsection {* Representing primitive types *}
    1.13 @@ -316,8 +315,6 @@
    1.14      haskell (target_atom "Just")
    1.15  
    1.16  
    1.17 -use "Tools/function_package/fundef_datatype.ML"
    1.18 -setup FundefDatatype.setup
    1.19  
    1.20  
    1.21  end
     2.1 --- a/src/HOL/FunDef.thy	Mon Jun 05 14:22:58 2006 +0200
     2.2 +++ b/src/HOL/FunDef.thy	Mon Jun 05 14:26:07 2006 +0200
     2.3 @@ -1,13 +1,17 @@
     2.4  theory FunDef
     2.5 -imports Accessible_Part
     2.6 +imports Accessible_Part Datatype Recdef
     2.7  uses 
     2.8 +("Tools/function_package/sum_tools.ML")
     2.9  ("Tools/function_package/fundef_common.ML")
    2.10  ("Tools/function_package/fundef_lib.ML")
    2.11  ("Tools/function_package/context_tree.ML")
    2.12  ("Tools/function_package/fundef_prep.ML")
    2.13  ("Tools/function_package/fundef_proof.ML")
    2.14  ("Tools/function_package/termination.ML")
    2.15 +("Tools/function_package/mutual.ML")
    2.16  ("Tools/function_package/fundef_package.ML")
    2.17 +("Tools/function_package/fundef_datatype.ML")
    2.18 +("Tools/function_package/auto_term.ML")
    2.19  begin
    2.20  
    2.21  lemma fundef_ex1_existence:
    2.22 @@ -34,16 +38,52 @@
    2.23    by simp
    2.24  
    2.25  
    2.26 +subsection {* Projections *}
    2.27 +consts
    2.28 +  lpg::"(('a + 'b) * 'a) set"
    2.29 +  rpg::"(('a + 'b) * 'b) set"
    2.30 +
    2.31 +inductive lpg
    2.32 +intros
    2.33 +  "(Inl x, x) : lpg"
    2.34 +inductive rpg
    2.35 +intros
    2.36 +  "(Inr y, y) : rpg"
    2.37 +definition
    2.38 +  "lproj x = (THE y. (x,y) : lpg)"
    2.39 +  "rproj x = (THE y. (x,y) : rpg)"
    2.40 +
    2.41 +lemma lproj_inl:
    2.42 +  "lproj (Inl x) = x"
    2.43 +  by (auto simp:lproj_def intro: the_equality lpg.intros elim: lpg.cases)
    2.44 +lemma rproj_inr:
    2.45 +  "rproj (Inr x) = x"
    2.46 +  by (auto simp:rproj_def intro: the_equality rpg.intros elim: rpg.cases)
    2.47 +
    2.48 +
    2.49 +
    2.50 +
    2.51 +use "Tools/function_package/sum_tools.ML"
    2.52  use "Tools/function_package/fundef_common.ML"
    2.53  use "Tools/function_package/fundef_lib.ML"
    2.54  use "Tools/function_package/context_tree.ML"
    2.55  use "Tools/function_package/fundef_prep.ML"
    2.56  use "Tools/function_package/fundef_proof.ML"
    2.57  use "Tools/function_package/termination.ML"
    2.58 +use "Tools/function_package/mutual.ML"
    2.59  use "Tools/function_package/fundef_package.ML"
    2.60  
    2.61  setup FundefPackage.setup
    2.62  
    2.63 +use "Tools/function_package/fundef_datatype.ML"
    2.64 +setup FundefDatatype.setup
    2.65 +
    2.66 +use "Tools/function_package/auto_term.ML"
    2.67 +setup FundefAutoTerm.setup
    2.68 +
    2.69 +
    2.70 +lemmas [fundef_cong] = 
    2.71 +  let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
    2.72  
    2.73  
    2.74  end
     3.1 --- a/src/HOL/List.thy	Mon Jun 05 14:22:58 2006 +0200
     3.2 +++ b/src/HOL/List.thy	Mon Jun 05 14:26:07 2006 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* The datatype of finite lists *}
     3.5  
     3.6  theory List
     3.7 -imports PreList
     3.8 +imports PreList FunDef
     3.9  begin
    3.10  
    3.11  datatype 'a list =
    3.12 @@ -498,7 +498,7 @@
    3.13  lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
    3.14  by (induct xs) auto
    3.15  
    3.16 -lemma map_cong [recdef_cong]:
    3.17 +lemma map_cong [fundef_cong, recdef_cong]:
    3.18  "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
    3.19  -- {* a congruence rule for @{text map} *}
    3.20  by simp
    3.21 @@ -863,7 +863,7 @@
    3.22    (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
    3.23  by(auto dest:Cons_eq_filterD)
    3.24  
    3.25 -lemma filter_cong[recdef_cong]:
    3.26 +lemma filter_cong[fundef_cong, recdef_cong]:
    3.27   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
    3.28  apply simp
    3.29  apply(erule thin_rl)
    3.30 @@ -1363,12 +1363,12 @@
    3.31  apply(auto)
    3.32  done
    3.33  
    3.34 -lemma takeWhile_cong [recdef_cong]:
    3.35 +lemma takeWhile_cong [fundef_cong, recdef_cong]:
    3.36    "[| l = k; !!x. x : set l ==> P x = Q x |] 
    3.37    ==> takeWhile P l = takeWhile Q k"
    3.38    by (induct k fixing: l, simp_all)
    3.39  
    3.40 -lemma dropWhile_cong [recdef_cong]:
    3.41 +lemma dropWhile_cong [fundef_cong, recdef_cong]:
    3.42    "[| l = k; !!x. x : set l ==> P x = Q x |] 
    3.43    ==> dropWhile P l = dropWhile Q k"
    3.44    by (induct k fixing: l, simp_all)
    3.45 @@ -1613,12 +1613,12 @@
    3.46  lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
    3.47  by (induct xs) auto
    3.48  
    3.49 -lemma foldl_cong [recdef_cong]:
    3.50 +lemma foldl_cong [fundef_cong, recdef_cong]:
    3.51    "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
    3.52    ==> foldl f a l = foldl g b k"
    3.53    by (induct k fixing: a b l, simp_all)
    3.54  
    3.55 -lemma foldr_cong [recdef_cong]:
    3.56 +lemma foldr_cong [fundef_cong, recdef_cong]:
    3.57    "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
    3.58    ==> foldr f l a = foldr g k b"
    3.59    by (induct k fixing: a b l, simp_all)
     4.1 --- a/src/HOL/Recdef.thy	Mon Jun 05 14:22:58 2006 +0200
     4.2 +++ b/src/HOL/Recdef.thy	Mon Jun 05 14:26:07 2006 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* TFL: recursive function definitions *}
     4.5  
     4.6  theory Recdef
     4.7 -imports Wellfounded_Relations Datatype
     4.8 +imports Wellfounded_Relations
     4.9  uses
    4.10    ("../TFL/casesplit.ML")
    4.11    ("../TFL/utils.ML")
    4.12 @@ -18,7 +18,6 @@
    4.13    ("../TFL/tfl.ML")
    4.14    ("../TFL/post.ML")
    4.15    ("Tools/recdef_package.ML")
    4.16 -  ("Tools/function_package/auto_term.ML")
    4.17  begin
    4.18  
    4.19  lemma tfl_eq_True: "(x = True) --> x"
    4.20 @@ -97,7 +96,4 @@
    4.21  qed
    4.22  
    4.23  
    4.24 -use "Tools/function_package/auto_term.ML"
    4.25 -setup FundefAutoTerm.setup
    4.26 -
    4.27  end
     5.1 --- a/src/HOL/Tools/function_package/auto_term.ML	Mon Jun 05 14:22:58 2006 +0200
     5.2 +++ b/src/HOL/Tools/function_package/auto_term.ML	Mon Jun 05 14:26:07 2006 +0200
     5.3 @@ -32,7 +32,7 @@
     5.4  	val {simps, congs, wfs} = RecdefPackage.get_local_hints ctxt
     5.5  	val ss = local_simpset_of ctxt addsimps simps
     5.6  	    
     5.7 -	val intro_rule = ProofContext.get_thm ctxt (Name "termination_intro")
     5.8 +	val intro_rule = ProofContext.get_thm ctxt (Name "termination")
     5.9      in
    5.10  	Method.RAW_METHOD (K (auto_term_tac
    5.11  				  intro_rule
     6.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Jun 05 14:22:58 2006 +0200
     6.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Jun 05 14:26:07 2006 +0200
     6.3 @@ -22,6 +22,7 @@
     6.4    | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
     6.5    | RCall of (term * ctx_tree)
     6.6  
     6.7 +type glrs = (term list * term list * term * term) list
     6.8  
     6.9  
    6.10  (* A record containing all the relevant symbols and types needed during the proof.
    6.11 @@ -39,8 +40,18 @@
    6.12  
    6.13  
    6.14  datatype rec_call_info = 
    6.15 -  RCInfo of {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm} 
    6.16 -
    6.17 +  RCInfo 
    6.18 +  of {
    6.19 +  RI: thm, 
    6.20 +  RIvs: (string * typ) list,
    6.21 +  lRI: thm, 
    6.22 +  lRIq: thm, 
    6.23 +  Gh: thm, 
    6.24 +  Gh': thm,
    6.25 +  GmAs: term list,
    6.26 +  rcarg: term
    6.27 +} 
    6.28 +     
    6.29  datatype clause_info =
    6.30    ClauseInfo of 
    6.31       {
    6.32 @@ -73,6 +84,36 @@
    6.33  datatype curry_info =
    6.34    Curry of { argTs: typ list, curry_ss: simpset }
    6.35  
    6.36 +type inj_proj = ((term -> term) * (term -> term))
    6.37 +
    6.38 +type qgar = (string * typ) list * term list * term list * term
    6.39 +
    6.40 +datatype mutual_part =
    6.41 +  MutualPart of 
    6.42 +	 {
    6.43 +          f_name: string,
    6.44 +	  const: string * typ,
    6.45 +	  cargTs: typ list,
    6.46 +	  pthA: SumTools.sum_path,
    6.47 +	  pthR: SumTools.sum_path,
    6.48 +	  qgars: qgar list,
    6.49 +	  f_def: thm
    6.50 +	 }
    6.51 +	 
    6.52 +
    6.53 +datatype mutual_info =
    6.54 +  Mutual of 
    6.55 +	 { 
    6.56 +	  name: string, 
    6.57 +	  sum_const: string * typ,
    6.58 +	  ST: typ,
    6.59 +	  RST: typ,
    6.60 +	  streeA: SumTools.sum_tree,
    6.61 +	  streeR: SumTools.sum_tree,
    6.62 +	  parts: mutual_part list,
    6.63 +	  qglrss: (term list * term list * term * term) list list
    6.64 +	 }
    6.65 +
    6.66  
    6.67  datatype prep_result =
    6.68    Prep of
    6.69 @@ -99,11 +140,28 @@
    6.70        dom_intros : thm list
    6.71       }
    6.72  
    6.73 +datatype fundef_mresult =
    6.74 +  FundefMResult of
    6.75 +     {
    6.76 +      f: term,
    6.77 +      G : term,
    6.78 +      R : term,
    6.79 +
    6.80 +      psimps : thm list list, 
    6.81 +      subset_pinducts : thm list, 
    6.82 +      simple_pinducts : thm list, 
    6.83 +      cases : thm,
    6.84 +      termination : thm,
    6.85 +      domintros : thm list
    6.86 +     }
    6.87 +
    6.88 +
    6.89 +type result_with_names = fundef_mresult * mutual_info * string list list * attribute list list list
    6.90  
    6.91  structure FundefData = TheoryDataFun
    6.92  (struct
    6.93    val name = "HOL/function_def/data";
    6.94 -  type T = string * fundef_result Symtab.table
    6.95 +  type T = string * result_with_names Symtab.table
    6.96  
    6.97    val empty = ("", Symtab.empty);
    6.98    val copy = I;
     7.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jun 05 14:22:58 2006 +0200
     7.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jun 05 14:26:07 2006 +0200
     7.3 @@ -18,6 +18,7 @@
     7.4  structure FundefDatatype : FUNDEF_DATATYPE =
     7.5  struct
     7.6  
     7.7 +
     7.8  fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
     7.9  fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
    7.10  
     8.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jun 05 14:22:58 2006 +0200
     8.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jun 05 14:26:07 2006 +0200
     8.3 @@ -62,3 +62,6 @@
     8.4  fun upairs [] = []
     8.5    | upairs (x::xs) = map (pair x) (x::xs) @ upairs xs
     8.6  
     8.7 +
     8.8 +fun the_single [x] = x
     8.9 +  | the_single _ = sys_error "the_single"
    8.10 \ No newline at end of file
     9.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jun 05 14:22:58 2006 +0200
     9.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jun 05 14:26:07 2006 +0200
     9.3 @@ -9,12 +9,13 @@
     9.4  
     9.5  signature FUNDEF_PACKAGE = 
     9.6  sig
     9.7 -    val add_fundef : ((bstring * Attrib.src list) * string) list -> theory -> Proof.state (* Need an _i variant *)
     9.8 +    val add_fundef : ((bstring * Attrib.src list) * string) list list -> theory -> Proof.state (* Need an _i variant *)
     9.9  
    9.10      val cong_add: attribute
    9.11      val cong_del: attribute
    9.12  							 
    9.13      val setup : theory -> theory
    9.14 +    val get_congs : theory -> thm list
    9.15  end
    9.16  
    9.17  
    9.18 @@ -26,46 +27,73 @@
    9.19  val True_implies = thm "True_implies"
    9.20  
    9.21  
    9.22 +fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) (names, attss) thy =
    9.23 +    let 
    9.24 +      val thy = thy |> Theory.add_path f_name 
    9.25 +                
    9.26 +      val thy = thy |> Theory.add_path label
    9.27 +      val spsimps = map standard psimps
    9.28 +      val add_list = (names ~~ spsimps) ~~ attss
    9.29 +      val (_, thy) = PureThy.add_thms add_list thy
    9.30 +      val thy = thy |> Theory.parent_path
    9.31 +                
    9.32 +      val (_, thy) = PureThy.add_thmss [((label, spsimps), Simplifier.simp_add :: moreatts)] thy
    9.33 +      val thy = thy |> Theory.parent_path
    9.34 +    in
    9.35 +      thy
    9.36 +    end
    9.37 +    
    9.38 +
    9.39 +
    9.40 +
    9.41 +
    9.42 +
    9.43  fun fundef_afterqed congs curry_info name data names atts thmss thy =
    9.44      let
    9.45  	val (complete_thm :: compat_thms) = map hd thmss
    9.46 -	val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
    9.47 -	val FundefResult {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
    9.48 -
    9.49 +	val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
    9.50 +	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data
    9.51 +        val Mutual {parts, ...} = curry_info
    9.52  
    9.53  	val Prep {names = Names {acc_R=accR, ...}, ...} = data
    9.54  	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    9.55  	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    9.56  
    9.57 -	val thy = thy |> Theory.add_path name 
    9.58 -
    9.59 -	val thy = thy |> Theory.add_path "psimps"
    9.60 -	val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy;
    9.61 -	val thy = thy |> Theory.parent_path
    9.62 +        val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) (names ~~ atts) thy
    9.63  
    9.64 -	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy
    9.65 -	val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy
    9.66 -	val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy
    9.67 -	val (_,thy) = PureThy.add_thms [(("pinduct", simple_pinduct), [RuleCases.case_names names, InductAttrib.induct_set ""])] thy
    9.68 -	val (_, thy) = PureThy.add_thmss [(("psimps", psimps), [Simplifier.simp_add])] thy
    9.69 +	val thy = thy |> Theory.add_path name
    9.70 +	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names (flat names)])] thy
    9.71 +	val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
    9.72 +	val (_, thy) = PureThy.add_thms [(("termination", termination), [])] thy
    9.73 +	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names (flat names), InductAttrib.induct_set ""])] thy
    9.74  	val thy = thy |> Theory.parent_path
    9.75      in
    9.76 -	add_fundef_data name fundef_data thy
    9.77 +	add_fundef_data name (fundef_data, curry_info, names, atts) thy
    9.78      end
    9.79  
    9.80 -fun gen_add_fundef prep_att eqns_atts thy =
    9.81 +fun gen_add_fundef prep_att eqns_attss thy =
    9.82      let
    9.83 -	val (natts, eqns) = split_list eqns_atts
    9.84 -	val (names, raw_atts) = split_list natts
    9.85 +	fun split eqns_atts =
    9.86 +	    let 
    9.87 +		val (natts, eqns) = split_list eqns_atts
    9.88 +		val (names, raw_atts) = split_list natts
    9.89 +		val atts = map (map (prep_att thy)) raw_atts
    9.90 +	    in
    9.91 +		((names, atts), eqns)
    9.92 +	    end
    9.93  
    9.94 -	val atts = map (map (prep_att thy)) raw_atts
    9.95 +
    9.96 +	val (natts, eqns) = split_list (map split_list eqns_attss)
    9.97 +	val (names, raw_atts) = split_list (map split_list natts)
    9.98 +
    9.99 +	val atts = map (map (map (prep_att thy))) raw_atts
   9.100  
   9.101  	val congs = get_fundef_congs (Context.Theory thy)
   9.102  
   9.103 -	val t_eqns = map (Sign.read_prop thy) eqns
   9.104 -			 |> map (term_of o cterm_of thy) (* HACK to prevent strange things from happening with abbreviations *)
   9.105 +	val t_eqns = map (map (Sign.read_prop thy)) eqns
   9.106 +			 |> map (map (term_of o cterm_of thy)) (* HACK to prevent strange things from happening with abbreviations *)
   9.107  
   9.108 -	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs t_eqns thy
   9.109 +	val (curry_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
   9.110  	val Prep {complete, compat, ...} = data
   9.111  
   9.112  	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
   9.113 @@ -76,27 +104,23 @@
   9.114      end
   9.115  
   9.116  
   9.117 -fun total_termination_afterqed name thmss thy =
   9.118 +fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy =
   9.119      let
   9.120  	val totality = hd (hd thmss)
   9.121  
   9.122 -	val FundefResult {psimps, simple_pinduct, ... }
   9.123 +	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, names, atts)
   9.124  	  = the (get_fundef_data name thy)
   9.125  
   9.126  	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
   9.127  
   9.128 -	val tsimps = map remove_domain_condition psimps
   9.129 -	val tinduct = remove_domain_condition simple_pinduct
   9.130 +	val tsimps = map (map remove_domain_condition) psimps
   9.131 +	val tinduct = map remove_domain_condition simple_pinducts
   9.132 +
   9.133 +        val thy = fold2 (add_simps "simps" [RecfunCodegen.add NONE]) (parts ~~ tsimps) (names ~~ atts) thy
   9.134  
   9.135  	val thy = Theory.add_path name thy
   9.136  		  
   9.137 -		  (* Need the names and attributes. Apply the attributes again? *)
   9.138 -(*	val thy = thy |> Theory.add_path "simps"
   9.139 -	val (_, thy) = PureThy.add_thms ((names ~~ tsimps) ~~ atts) thy;
   9.140 -	val thy = thy |> Theory.parent_path*)
   9.141 -
   9.142 -	val (_, thy) = PureThy.add_thms [(("induct", tinduct), [])] thy 
   9.143 -	val (_, thy) = PureThy.add_thmss [(("simps", tsimps), [Simplifier.simp_add, RecfunCodegen.add NONE])] thy
   9.144 +	val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy 
   9.145  	val thy = Theory.parent_path thy
   9.146      in
   9.147  	thy
   9.148 @@ -135,13 +159,13 @@
   9.149  	val name = if name = "" then get_last_fundef thy else name
   9.150  	val data = the (get_fundef_data name thy)
   9.151  
   9.152 -	val FundefResult {total_intro, ...} = data
   9.153 +	val (res as FundefMResult {termination, ...}, mutual, _, _) = data
   9.154  	val goal = FundefTermination.mk_total_termination_goal data
   9.155      in
   9.156  	thy |> ProofContext.init
   9.157 -	    |> ProofContext.note_thmss_i [(("termination_intro", 
   9.158 -					    [ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd
   9.159 -	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", [])
   9.160 +	    |> ProofContext.note_thmss_i [(("termination", 
   9.161 +					    [ContextRules.intro_query NONE]), [([termination], [])])] |> snd
   9.162 +	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", [])
   9.163  	    [(("", []), [(goal, [])])]
   9.164      end	
   9.165    | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
   9.166 @@ -173,6 +197,9 @@
   9.167  		[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
   9.168  
   9.169  
   9.170 +val get_congs = FundefCommon.get_fundef_congs o Context.Theory
   9.171 +
   9.172 +
   9.173  (* outer syntax *)
   9.174  
   9.175  local structure P = OuterParse and K = OuterKeyword in
   9.176 @@ -182,8 +209,8 @@
   9.177  
   9.178  val functionP =
   9.179    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   9.180 -    (function_decl >> (fn eqns =>
   9.181 -      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqns)));
   9.182 +    (P.and_list1 function_decl >> (fn eqnss =>
   9.183 +      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss)));
   9.184  
   9.185  val terminationP =
   9.186    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
    10.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Mon Jun 05 14:22:58 2006 +0200
    10.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Mon Jun 05 14:26:07 2006 +0200
    10.3 @@ -11,6 +11,11 @@
    10.4  sig
    10.5      val prepare_fundef_curried : thm list -> term list -> theory
    10.6  				 -> FundefCommon.curry_info option * xstring * (FundefCommon.prep_result * theory)
    10.7 +
    10.8 +    val prepare_fundef_new : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list
    10.9 +			          -> FundefCommon.prep_result * theory
   10.10 +
   10.11 +
   10.12  end
   10.13  
   10.14  
   10.15 @@ -125,12 +130,17 @@
   10.16  		val RI = freezeT RI
   10.17  		val lRI = localize RI
   10.18  		val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
   10.19 +		val plRI = prop_of lRI
   10.20 +		val GmAs = Logic.strip_imp_prems plRI
   10.21 +		val rcarg = case Logic.strip_imp_concl plRI of
   10.22 +				trueprop $ (memb $ (pair $ rcarg $ _) $ R) => rcarg
   10.23 +			      | _ => raise Match
   10.24  			  
   10.25  		val Gh_term = Pattern.rewrite_term thy [rw_RI_to_h_assum, rw_f_to_h] [] (prop_of lRIq)
   10.26  		val Gh = assume (cterm_of thy Gh_term)
   10.27  		val Gh' = assume (cterm_of thy (rename_vars Gh_term))
   10.28  	    in
   10.29 -		RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
   10.30 +		RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh', GmAs=GmAs, rcarg=rcarg}
   10.31  	    end
   10.32  
   10.33  	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   10.34 @@ -151,7 +161,7 @@
   10.35  
   10.36  (* Chooses fresh free names, declares G and R, defines f and returns a record
   10.37     with all the information *)  
   10.38 -fun setup_context (f, glrs, used) fname congs thy =
   10.39 +fun setup_context (f, glrs, used) defname congs thy =
   10.40      let
   10.41  	val trees = map (build_tree thy f congs) glrs
   10.42  	val allused = fold FundefCtxTree.add_context_varnames trees used
   10.43 @@ -175,8 +185,8 @@
   10.44  
   10.45  	val GT = mk_relT (domT, ranT)
   10.46  	val RT = mk_relT (domT, domT)
   10.47 -	val G_name = fname ^ "_graph"
   10.48 -	val R_name = fname ^ "_rel"
   10.49 +	val G_name = defname ^ "_graph"
   10.50 +	val R_name = defname ^ "_rel"
   10.51  
   10.52  	val glrs' = mk_primed_vars thy glrs
   10.53  
   10.54 @@ -292,9 +302,9 @@
   10.55   * Defines the function, the graph and the termination relation, synthesizes completeness
   10.56   * and comatibility conditions and returns everything.
   10.57   *)
   10.58 -fun prepare_fundef congs eqs fname thy =
   10.59 +fun prepare_fundef congs eqs defname thy =
   10.60      let
   10.61 -	val (names, thy) = setup_context (analyze_eqs eqs) fname congs thy
   10.62 +	val (names, thy) = setup_context (analyze_eqs eqs) defname congs thy
   10.63  	val Names {G, R, glrs, trees, ...} = names
   10.64  
   10.65  	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
   10.66 @@ -310,6 +320,28 @@
   10.67      end
   10.68  
   10.69  
   10.70 +fun prepare_fundef_new thy congs defname f glrs used =
   10.71 +    let
   10.72 +	val (names, thy) = setup_context (f, glrs, used) defname congs thy
   10.73 +	val Names {G, R, glrs, trees, ...} = names
   10.74 +
   10.75 +	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
   10.76 +
   10.77 +	val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G)
   10.78 +	val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R)
   10.79 +
   10.80 +	val n = length glrs
   10.81 +	val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
   10.82 +    in
   10.83 +	(Prep {names = names, complete=complete, compat=compat, clauses = clauses},
   10.84 +	 thy) 
   10.85 +    end
   10.86 +
   10.87 +
   10.88 +
   10.89 +
   10.90 +
   10.91 +
   10.92  
   10.93  
   10.94  fun prepare_fundef_curried congs eqs thy =
    11.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Mon Jun 05 14:22:58 2006 +0200
    11.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Mon Jun 05 14:26:07 2006 +0200
    11.3 @@ -10,6 +10,9 @@
    11.4  signature FUNDEF_PROOF =
    11.5  sig
    11.6  
    11.7 +    val mk_partial_rules : theory -> thm list -> FundefCommon.prep_result 
    11.8 +			   -> thm -> thm list -> FundefCommon.fundef_result
    11.9 +
   11.10      val mk_partial_rules_curried : theory -> thm list -> FundefCommon.curry_info option -> FundefCommon.prep_result 
   11.11  				   -> thm -> thm list -> FundefCommon.fundef_result
   11.12  end
   11.13 @@ -42,7 +45,7 @@
   11.14  
   11.15  
   11.16      
   11.17 -fun mk_simp thy names f_iff graph_is_function clause valthm =
   11.18 +fun mk_psimp thy names f_iff graph_is_function clause valthm =
   11.19      let
   11.20  	val Names {R, acc_R, domT, z, ...} = names
   11.21  	val ClauseInfo {qs, cqs, gs, lhs, rhs, ...} = clause
   11.22 @@ -56,10 +59,10 @@
   11.23  	    |> (fn it => it COMP valthm)
   11.24  	    |> implies_intr lhs_acc 
   11.25  	    |> asm_simplify (HOL_basic_ss addsimps [f_iff])
   11.26 -	    |> fold forall_intr cqs
   11.27 +(*	    |> fold forall_intr cqs
   11.28  	    |> forall_elim_vars 0
   11.29  	    |> varifyT
   11.30 -	    |> Drule.close_derivation
   11.31 +	    |> Drule.close_derivation*)
   11.32      end
   11.33  
   11.34  
   11.35 @@ -143,20 +146,23 @@
   11.36  		|> implies_intr a_D
   11.37  		|> implies_intr D_dcl
   11.38  		|> implies_intr D_subset
   11.39 -		|> forall_intr_frees
   11.40 -		|> forall_elim_vars 0
   11.41 +
   11.42 +	val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
   11.43  
   11.44  	val simple_induct_rule =
   11.45  	    subset_induct_rule
   11.46 -		|> instantiate' [] [SOME (cterm_of thy acc_R)]
   11.47 +		|> forall_intr (cterm_of thy D)
   11.48 +		|> forall_elim (cterm_of thy acc_R)
   11.49  		|> (curry op COMP) subset_refl
   11.50  		|> (curry op COMP) (acc_downward
   11.51  					|> (instantiate' [SOME (ctyp_of thy domT)]
   11.52  							 (map (SOME o cterm_of thy) [x, R, z]))
   11.53  					|> forall_intr (cterm_of thy z)
   11.54  					|> forall_intr (cterm_of thy x))
   11.55 +		|> forall_intr (cterm_of thy a)
   11.56 +		|> forall_intr (cterm_of thy P)
   11.57      in
   11.58 -	(varifyT subset_induct_rule, varifyT simple_induct_rule)
   11.59 +	(subset_induct_all, simple_induct_rule)
   11.60      end
   11.61  
   11.62  
   11.63 @@ -344,25 +350,13 @@
   11.64      let
   11.65  	val Names {z, R, acc_R, ...} = names
   11.66  	val ClauseInfo {qs, gs, lhs, rhs, ...} = clause
   11.67 -
   11.68 -	val z_lhs = cterm_of thy (HOLogic.mk_prod (z,lhs))
   11.69 -	val z_acc = cterm_of thy (HOLogic.mk_mem (z,acc_R))
   11.70 -
   11.71 -	val icases = R_cases 
   11.72 -			 |> instantiate' [] [SOME z_lhs, SOME z_acc]
   11.73 -			 |> forall_intr_frees
   11.74 -			 |> forall_elim_vars 0
   11.75 -
   11.76  	val goal = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
   11.77      in
   11.78  	Goal.init goal 
   11.79 -		  |> SINGLE (resolve_tac [accI] 1) |> the
   11.80 -		  |> SINGLE (eresolve_tac [icases] 1)  |> the
   11.81 -		  |> SINGLE (CLASIMPSET auto_tac) |> the
   11.82 +		  |> (SINGLE (resolve_tac [accI] 1)) |> print |> the
   11.83 +		  |> (SINGLE (eresolve_tac [R_cases] 1))  |> print |> the
   11.84 +		  |> (SINGLE (CLASIMPSET auto_tac)) |> print |> the
   11.85  		  |> Goal.conclude
   11.86 -		  |> forall_intr_frees
   11.87 -		  |> forall_elim_vars 0
   11.88 -		  |> varifyT
   11.89      end
   11.90  
   11.91  
   11.92 @@ -530,7 +524,7 @@
   11.93  	val f_iff = (graph_is_function RS inst_ex1_iff)
   11.94  
   11.95  	val _ = Output.debug "Proving simplification rules"
   11.96 -	val psimps  = map2 (mk_simp thy names f_iff graph_is_function) clauses values
   11.97 +	val psimps  = map2 (mk_psimp thy names f_iff graph_is_function) clauses values
   11.98  
   11.99  	val _ = Output.debug "Proving partial induction rule"
  11.100  	val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy names complete_thm clauses
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Mon Jun 05 14:26:07 2006 +0200
    12.3 @@ -0,0 +1,264 @@
    12.4 +(*  Title:      HOL/Tools/function_package/mutual.ML
    12.5 +    ID:         $Id$
    12.6 +    Author:     Alexander Krauss, TU Muenchen
    12.7 +
    12.8 +A package for general recursive function definitions. 
    12.9 +Tools for mutual recursive definitions.
   12.10 +
   12.11 +*)
   12.12 +
   12.13 +signature FUNDEF_MUTUAL = 
   12.14 +sig
   12.15 +  
   12.16 +  val prepare_fundef_mutual : thm list -> term list list -> theory ->
   12.17 +                              (FundefCommon.mutual_info * string * (FundefCommon.prep_result * theory))
   12.18 +
   12.19 +
   12.20 +  val mk_partial_rules_mutual : theory -> thm list -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> thm list ->
   12.21 +                                FundefCommon.fundef_mresult
   12.22 +end
   12.23 +
   12.24 +
   12.25 +structure FundefMutual: FUNDEF_MUTUAL = 
   12.26 +struct
   12.27 +
   12.28 +open FundefCommon
   12.29 +
   12.30 +
   12.31 +
   12.32 +fun check_const (Const C) = C
   12.33 +  | check_const _ = raise ERROR "Head symbol of every left hand side must be a constant." (* FIXME: Output the equation here *)
   12.34 +
   12.35 +
   12.36 +
   12.37 +
   12.38 +
   12.39 +fun split_def geq =
   12.40 +    let
   12.41 +	val gs = Logic.strip_imp_prems geq
   12.42 +	val eq = Logic.strip_imp_concl geq
   12.43 +	val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
   12.44 +	val (fc, args) = strip_comb f_args
   12.45 +	val f = check_const fc
   12.46 +		    
   12.47 +	val qs = fold_rev Term.add_frees args []
   12.48 +		 
   12.49 +	val rhs_new_vars = (Term.add_frees rhs []) \\ qs
   12.50 +	val _ = if null rhs_new_vars then () 
   12.51 +		else raise ERROR "Variables occur on right hand side only: " (* FIXME: Output vars here *)
   12.52 +    in
   12.53 +	((f, length args), (qs, gs, args, rhs))
   12.54 +    end
   12.55 +
   12.56 +
   12.57 +fun analyze_eqs thy eqss =
   12.58 +    let
   12.59 +	fun all_equal ((x as ((n:string,T), k:int))::xs) = if forall (fn ((n',_),k') => n = n' andalso k = k') xs then x
   12.60 +							   else raise ERROR ("All equations in a block must describe the same "
   12.61 +									     ^ "constant and have the same number of arguments.")
   12.62 +								      
   12.63 +	val def_infoss = map (split_list o map split_def) eqss
   12.64 +	val (consts, qgarss) = split_list (map (fn (Cis, eqs) => (all_equal Cis, eqs)) def_infoss)
   12.65 +
   12.66 +	val cnames = map (fst o fst) consts
   12.67 +	val check_rcs = exists_Const (fn (n,_) => if n mem cnames 
   12.68 +						  then raise ERROR "Recursive Calls not allowed in premises." else false)
   12.69 +	val _ = forall (forall (fn (_, gs, _, _) => forall check_rcs gs)) qgarss
   12.70 +
   12.71 +	fun curried_types ((_,T), k) =
   12.72 +	    let
   12.73 +		val (caTs, uaTs) = chop k (binder_types T)
   12.74 +	    in 
   12.75 +		(caTs, uaTs ---> body_type T)
   12.76 +	    end
   12.77 +
   12.78 +	val (caTss, resultTs) = split_list (map curried_types consts)
   12.79 +	val argTs = map (foldr1 HOLogic.mk_prodT) caTss
   12.80 +
   12.81 +	val (RST,streeR, pthsR) = SumTools.mk_tree resultTs
   12.82 +	val (ST, streeA, pthsA) = SumTools.mk_tree argTs
   12.83 +
   12.84 +	val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name cnames)
   12.85 +	val sfun_xname = def_name ^ "_sum"
   12.86 +	val sfun_type = ST --> RST
   12.87 +
   12.88 +    	val thy = Sign.add_consts_i [(sfun_xname, sfun_type, NoSyn)] thy (* Add the sum function *)
   12.89 +	val sfun = Const (Sign.intern_const thy sfun_xname, sfun_type)
   12.90 +
   12.91 +	fun define (((((n, T), _), caTs), (pthA, pthR)), qgars) (thy, rews) = 
   12.92 +	    let 
   12.93 +		val fxname = Sign.extern_const thy n
   12.94 +		val f = Const (n, T)
   12.95 +		val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs
   12.96 +
   12.97 +		val f_exp = SumTools.mk_proj streeR pthR (sfun $ SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod vars))
   12.98 +		val def = Logic.mk_equals (list_comb (f, vars), f_exp)
   12.99 +
  12.100 +		val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy
  12.101 +		val rews' = (f, fold_rev lambda vars f_exp) :: rews
  12.102 +	    in
  12.103 +		(MutualPart {f_name=fxname, const=(n, T),cargTs=caTs,pthA=pthA,pthR=pthR,qgars=qgars,f_def=f_def}, (thy, rews'))
  12.104 +	    end
  12.105 +
  12.106 +	val _ = print pthsA
  12.107 +	val _ = print pthsR
  12.108 +
  12.109 +	val (parts, (thy, rews)) = fold_map define (((consts ~~ caTss)~~ (pthsA ~~ pthsR)) ~~ qgarss) (thy, [])
  12.110 +
  12.111 +	fun mk_qglrss (MutualPart {qgars, pthA, pthR, ...}) =
  12.112 +	    let
  12.113 +		fun convert_eqs (qs, gs, args, rhs) =
  12.114 +		    (map Free qs, gs, SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod args), 
  12.115 +		     SumTools.mk_inj streeR pthR (Pattern.rewrite_term thy rews [] rhs))
  12.116 +	    in
  12.117 +		map convert_eqs qgars
  12.118 +	    end
  12.119 +	    
  12.120 +	val qglrss = map mk_qglrss parts
  12.121 +    in
  12.122 +	(Mutual {name=def_name,sum_const=dest_Const sfun, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts, qglrss=qglrss}, thy)
  12.123 +    end
  12.124 +
  12.125 +
  12.126 +
  12.127 +
  12.128 +fun prepare_fundef_mutual congs eqss thy =
  12.129 +    let 
  12.130 +	val (mutual, thy) = analyze_eqs thy eqss
  12.131 +	val Mutual {name, sum_const, qglrss, ...} = mutual
  12.132 +	val global_glrs = flat qglrss
  12.133 +	val used = fold (fn (qs, _, _, _) => fold (curry op ins_string o fst o dest_Free) qs) global_glrs []
  12.134 +    in
  12.135 +	(mutual, name, FundefPrep.prepare_fundef_new thy congs name (Const sum_const) global_glrs used)
  12.136 +    end
  12.137 +
  12.138 +
  12.139 +(* Beta-reduce both sides of a meta-equality *)
  12.140 +fun beta_norm_eq thm = 
  12.141 +    let
  12.142 +	val (lhs, rhs) = dest_equals (cprop_of thm)
  12.143 +	val lhs_conv = beta_conversion false lhs 
  12.144 +	val rhs_conv = beta_conversion false rhs 
  12.145 +    in
  12.146 +	transitive (symmetric lhs_conv) (transitive thm rhs_conv)
  12.147 +    end
  12.148 +
  12.149 +
  12.150 +
  12.151 +
  12.152 +fun map_mutual2 f (Mutual {parts, ...}) =
  12.153 +    map2 (fn (p as MutualPart {qgars, ...}) => map2 (f p) qgars) parts
  12.154 +
  12.155 +
  12.156 +
  12.157 +fun recover_mutual_psimp thy RST streeR all_f_defs (MutualPart {f_def, pthR, ...}) (_,_,args,_) sum_psimp =
  12.158 +    let
  12.159 +	val [accCond] = cprems_of sum_psimp
  12.160 +	val plain_eq = implies_elim sum_psimp (assume accCond)
  12.161 +	val x = Free ("x", RST)
  12.162 +
  12.163 +	val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) f_def
  12.164 +    in
  12.165 +	reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x)))  (*  PR(x) == PR(x) *)
  12.166 +		  |> (fn it => combination it (plain_eq RS eq_reflection))
  12.167 +		  |> beta_norm_eq (*  PR(S(I(as))) == PR(IR(...)) *)
  12.168 +		  |> transitive f_def_inst (*  f ... == PR(IR(...)) *)
  12.169 +		  |> simplify (HOL_basic_ss addsimps [SumTools.projl_inl, SumTools.projr_inr]) (*  f ... == ... *)
  12.170 +		  |> simplify (HOL_basic_ss addsimps all_f_defs) (*  f ... == ... *)
  12.171 +		  |> (fn it => it RS meta_eq_to_obj_eq)
  12.172 +		  |> implies_intr accCond
  12.173 +    end
  12.174 +
  12.175 +
  12.176 +
  12.177 +
  12.178 +
  12.179 +fun mutual_induct_Pnames n = 
  12.180 +    if n < 5 then fst (chop n ["P","Q","R","S"])
  12.181 +    else map (fn i => "P" ^ string_of_int i) (1 upto n)
  12.182 +	 
  12.183 +	 
  12.184 +val sum_case_rules = thms "Datatype.sum.cases"
  12.185 +val split_apply = thm "Product_Type.split"
  12.186 +		     
  12.187 +		     
  12.188 +fun mutual_induct_rules thy induct all_f_defs (Mutual {qglrss, RST, parts, streeA, ...}) =
  12.189 +    let
  12.190 +	fun mk_P (MutualPart {cargTs, ...}) Pname =
  12.191 +	    let
  12.192 +		val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
  12.193 +		val atup = foldr1 HOLogic.mk_prod avars
  12.194 +	    in
  12.195 +		tupled_lambda atup (list_comb (Free (Pname, cargTs ---> HOLogic.boolT), avars))
  12.196 +	    end
  12.197 +	    
  12.198 +	val Ps = map2 mk_P parts (mutual_induct_Pnames (length parts))
  12.199 +	val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
  12.200 +		       
  12.201 +	val induct_inst = 
  12.202 +	    forall_elim (cterm_of thy case_exp) induct
  12.203 +			|> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
  12.204 +		        |> full_simplify (HOL_basic_ss addsimps all_f_defs) 
  12.205 +
  12.206 +	fun mk_proj rule (MutualPart {cargTs, pthA, ...}) =
  12.207 +	    let
  12.208 +		val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs
  12.209 +		val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs)
  12.210 +	    in
  12.211 +		rule 
  12.212 +		    |> forall_elim (cterm_of thy inj)
  12.213 +		    |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
  12.214 +	    end
  12.215 +
  12.216 +    in
  12.217 +	map (mk_proj induct_inst) parts
  12.218 +    end
  12.219 +    
  12.220 +    
  12.221 +
  12.222 +
  12.223 +
  12.224 +fun mk_partial_rules_mutual thy congs (m as Mutual {qglrss, RST, parts, streeR, ...}) data complete_thm compat_thms =
  12.225 +    let
  12.226 +	val result = FundefProof.mk_partial_rules thy congs data complete_thm compat_thms 
  12.227 +	val FundefResult {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
  12.228 +
  12.229 +	val sum_psimps = Library.unflat qglrss psimps
  12.230 +
  12.231 +	val all_f_defs = map (fn MutualPart {f_def, ...} => symmetric f_def) parts
  12.232 +	val mpsimps = map_mutual2 (recover_mutual_psimp thy RST streeR all_f_defs) m sum_psimps
  12.233 +	val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
  12.234 +        val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro
  12.235 +    in
  12.236 +	FundefMResult { f=f, G=G, R=R,
  12.237 +			psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
  12.238 +			cases=completeness, termination=termination, domintros=dom_intros}
  12.239 +    end
  12.240 +    
  12.241 +
  12.242 +end
  12.243 +
  12.244 +
  12.245 +
  12.246 +
  12.247 +
  12.248 +
  12.249 +
  12.250 +
  12.251 +
  12.252 +
  12.253 +
  12.254 +
  12.255 +
  12.256 +
  12.257 +
  12.258 +
  12.259 +
  12.260 +
  12.261 +
  12.262 +
  12.263 +
  12.264 +
  12.265 +
  12.266 +
  12.267 +
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Tools/function_package/sum_tools.ML	Mon Jun 05 14:26:07 2006 +0200
    13.3 @@ -0,0 +1,109 @@
    13.4 +(*  Title:      HOL/Tools/function_package/sum_tools.ML
    13.5 +    ID:         $Id$
    13.6 +    Author:     Alexander Krauss, TU Muenchen
    13.7 +
    13.8 +A package for general recursive function definitions. 
    13.9 +Tools for mutual recursive definitions. This could actually be useful for other packages, too, but needs
   13.10 +some cleanup first...
   13.11 +
   13.12 +*)
   13.13 +
   13.14 +signature SUM_TOOLS =
   13.15 +sig
   13.16 +  type sum_tree
   13.17 +  type sum_path
   13.18 +
   13.19 +  val projl_inl: thm
   13.20 +  val projr_inr: thm
   13.21 +
   13.22 +  val mk_tree : typ list -> typ * sum_tree * sum_path list
   13.23 +
   13.24 +  val mk_proj: sum_tree -> sum_path -> term -> term
   13.25 +  val mk_inj: sum_tree -> sum_path -> term -> term
   13.26 +
   13.27 +  val mk_sumcases: sum_tree -> typ -> term list -> term
   13.28 +end
   13.29 +
   13.30 +
   13.31 +structure SumTools: SUM_TOOLS =
   13.32 +struct
   13.33 +
   13.34 +val inlN = "Sum_Type.Inl"
   13.35 +val inrN = "Sum_Type.Inr"
   13.36 +val sumcaseN = "Datatype.sum.sum_case"
   13.37 +
   13.38 +val projlN = "FunDef.lproj"
   13.39 +val projrN = "FunDef.rproj"
   13.40 +val projl_inl = thm "FunDef.lproj_inl"
   13.41 +val projr_inr = thm "FunDef.rproj_inr"
   13.42 +
   13.43 +
   13.44 +
   13.45 +fun mk_sumT LT RT = Type ("+", [LT, RT])
   13.46 +fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
   13.47 +
   13.48 +
   13.49 +datatype sum_tree 
   13.50 +  = Leaf of typ
   13.51 +  | Branch of (typ * (typ * sum_tree) * (typ * sum_tree))
   13.52 +
   13.53 +type sum_path = bool list (* true: left, false: right *)
   13.54 +
   13.55 +fun sum_type_of (Leaf T) = T
   13.56 +  | sum_type_of (Branch (ST,(LT,_),(RT,_))) = ST
   13.57 +
   13.58 +
   13.59 +fun mk_tree Ts =
   13.60 +    let 
   13.61 +	fun mk_tree' 1 [T] = (T, Leaf T, [[]])
   13.62 +	  | mk_tree' n Ts =
   13.63 +	    let 
   13.64 +		val n2 = n div 2
   13.65 +		val (lTs, rTs) = chop n2 Ts
   13.66 +		val (TL, ltree, lpaths) = mk_tree' n2 lTs
   13.67 +		val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs
   13.68 +		val T = mk_sumT TL TR
   13.69 +		val pths = map (cons true) lpaths @ map (cons false) rpaths 
   13.70 +	    in
   13.71 +		(T, Branch (T, (TL, ltree), (TR, rtree)), pths)
   13.72 +	    end
   13.73 +    in
   13.74 +	mk_tree' (length Ts) Ts
   13.75 +    end
   13.76 +
   13.77 +
   13.78 +fun mk_inj (Leaf _) [] t = t
   13.79 +  | mk_inj (Branch (ST, (LT, tr), _)) (true::pth) t = 
   13.80 +    Const (inlN, LT --> ST) $ mk_inj tr pth t
   13.81 +  | mk_inj (Branch (ST, _, (RT, tr))) (false::pth) t = 
   13.82 +    Const (inrN, RT --> ST) $ mk_inj tr pth t
   13.83 +  | mk_inj _ _ _ = sys_error "mk_inj"
   13.84 +
   13.85 +fun mk_proj (Leaf _) [] t = t
   13.86 +  | mk_proj (Branch (ST, (LT, tr), _)) (true::pth) t = 
   13.87 +    mk_proj tr pth (Const (projlN, ST --> LT) $ t)
   13.88 +  | mk_proj (Branch (ST, _, (RT, tr))) (false::pth) t = 
   13.89 +    mk_proj tr pth (Const (projrN, ST --> RT) $ t)
   13.90 +  | mk_proj _ _ _ = sys_error "mk_proj"
   13.91 +
   13.92 +
   13.93 +fun mk_sumcases tree T ts =
   13.94 +    let
   13.95 +	fun mk_sumcases' (Leaf _) (t::ts) = (t,ts)
   13.96 +	  | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts =
   13.97 +	    let
   13.98 +		val (lcase, ts') = mk_sumcases' ltr ts
   13.99 +		val (rcase, ts'') = mk_sumcases' rtr ts'
  13.100 +	    in
  13.101 +		(mk_sumcase LT RT T lcase rcase, ts'')
  13.102 +	    end
  13.103 +	  | mk_sumcases' _ [] = sys_error "mk_sumcases"
  13.104 +    in
  13.105 +	fst (mk_sumcases' tree ts)
  13.106 +    end
  13.107 +
  13.108 +end
  13.109 +
  13.110 +
  13.111 +
  13.112 +
    14.1 --- a/src/HOL/Tools/function_package/termination.ML	Mon Jun 05 14:22:58 2006 +0200
    14.2 +++ b/src/HOL/Tools/function_package/termination.ML	Mon Jun 05 14:26:07 2006 +0200
    14.3 @@ -9,8 +9,8 @@
    14.4  
    14.5  signature FUNDEF_TERMINATION =
    14.6  sig
    14.7 -    val mk_total_termination_goal : FundefCommon.fundef_result -> term
    14.8 -    val mk_partial_termination_goal : theory -> FundefCommon.fundef_result -> string -> term * term
    14.9 +    val mk_total_termination_goal : FundefCommon.result_with_names -> term
   14.10 +    val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
   14.11  end
   14.12  
   14.13  structure FundefTermination : FUNDEF_TERMINATION =
   14.14 @@ -20,20 +20,16 @@
   14.15  open FundefCommon
   14.16  open FundefAbbrev
   14.17  
   14.18 -fun mk_total_termination_goal data =
   14.19 +fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _, _) =
   14.20      let
   14.21 -	val FundefResult {R, f, ... } = data
   14.22 -
   14.23  	val domT = domain_type (fastype_of f)
   14.24  	val x = Free ("x", domT)
   14.25      in
   14.26  	Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
   14.27      end
   14.28  
   14.29 -fun mk_partial_termination_goal thy data dom =
   14.30 +fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _, _) dom =
   14.31      let
   14.32 -	val FundefResult {R, f, ... } = data
   14.33 -
   14.34  	val domT = domain_type (fastype_of f)
   14.35  	val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom
   14.36  	val DT = type_of D
    15.1 --- a/src/HOL/Tools/recdef_package.ML	Mon Jun 05 14:22:58 2006 +0200
    15.2 +++ b/src/HOL/Tools/recdef_package.ML	Mon Jun 05 14:26:07 2006 +0200
    15.3 @@ -300,7 +300,7 @@
    15.4    LocalRecdefData.init #>
    15.5    Attrib.add_attributes
    15.6     [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
    15.7 -    (recdef_congN, Attrib.add_del_args (FundefPackage.cong_add o cong_add) (FundefPackage.cong_del o cong_del), "declaration of recdef cong rule"),
    15.8 +    (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
    15.9      (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];
   15.10  
   15.11  
    16.1 --- a/src/HOL/ex/Fundefs.thy	Mon Jun 05 14:22:58 2006 +0200
    16.2 +++ b/src/HOL/ex/Fundefs.thy	Mon Jun 05 14:26:07 2006 +0200
    16.3 @@ -5,11 +5,10 @@
    16.4  Examples of function definitions using the new "function" package.
    16.5  *)
    16.6  
    16.7 -theory Fundefs
    16.8 +theory Fundefs 
    16.9  imports Main
   16.10  begin
   16.11  
   16.12 -
   16.13  section {* Very basic *}
   16.14  
   16.15  consts fib :: "nat \<Rightarrow> nat"
   16.16 @@ -22,7 +21,7 @@
   16.17  
   16.18  text {* we get partial simp and induction rules: *}
   16.19  thm fib.psimps
   16.20 -thm fib.pinduct
   16.21 +thm pinduct
   16.22  
   16.23  text {* There is also a cases rule to distinguish cases along the definition *}
   16.24  thm fib.cases
   16.25 @@ -41,6 +40,8 @@
   16.26  function
   16.27    "add 0 y = y"
   16.28    "add (Suc x) y = Suc (add x y)"
   16.29 +thm add_rel.cases
   16.30 +
   16.31  by pat_completeness auto
   16.32  termination
   16.33    by (auto_term "measure fst")
   16.34 @@ -50,7 +51,6 @@
   16.35  
   16.36  section {* Nested recursion *}
   16.37  
   16.38 -
   16.39  consts nz :: "nat \<Rightarrow> nat"
   16.40  function
   16.41    "nz 0 = 0"
   16.42 @@ -61,7 +61,9 @@
   16.43    assumes trm: "x \<in> nz_dom"
   16.44    shows "nz x = 0"
   16.45  using trm
   16.46 -by induct auto
   16.47 +apply induct 
   16.48 +apply auto
   16.49 +done
   16.50  
   16.51  termination nz
   16.52    apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
   16.53 @@ -70,6 +72,36 @@
   16.54  thm nz.simps
   16.55  thm nz.induct
   16.56  
   16.57 +text {* Here comes McCarthy's 91-function *}
   16.58 +
   16.59 +consts f91 :: "nat => nat"
   16.60 +function 
   16.61 +  "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
   16.62 +by pat_completeness auto
   16.63 +
   16.64 +(* Prove a lemma before attempting a termination proof *)
   16.65 +lemma f91_estimate: 
   16.66 +  assumes trm: "n : f91_dom" 
   16.67 +  shows "n < f91 n + 11"
   16.68 +using trm by induct auto
   16.69 +
   16.70 +(* Now go for termination *)
   16.71 +termination
   16.72 +proof
   16.73 +  let ?R = "measure (%x. 101 - x)"
   16.74 +  show "wf ?R" ..
   16.75 +
   16.76 +  fix n::nat assume "~ 100 < n" (* Inner call *)
   16.77 +  thus "(n + 11, n) : ?R"
   16.78 +    by simp arith
   16.79 +
   16.80 +  assume inner_trm: "n + 11 : f91_dom" (* Outer call *)
   16.81 +  with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
   16.82 +  with `~ 100 < n` show "(f91 (n + 11), n) : ?R"
   16.83 +    by simp arith
   16.84 +qed
   16.85 +
   16.86 +
   16.87  
   16.88  section {* More general patterns *}
   16.89  
   16.90 @@ -84,7 +116,8 @@
   16.91    "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
   16.92                                  else gcd2 (x - y) (Suc y))"
   16.93  by pat_completeness auto
   16.94 -termination by (auto_term "measure (\<lambda>(x,y). x + y)")
   16.95 +termination 
   16.96 +  by (auto_term "measure (\<lambda>(x,y). x + y)")
   16.97  
   16.98  thm gcd2.simps
   16.99  thm gcd2.induct
  16.100 @@ -117,4 +150,34 @@
  16.101  thm ev.induct
  16.102  thm ev.cases
  16.103  
  16.104 +
  16.105 +section {* Mutual Recursion *}
  16.106 +
  16.107 +
  16.108 +consts
  16.109 +  evn :: "nat \<Rightarrow> bool"
  16.110 +  od :: "nat \<Rightarrow> bool"
  16.111 +
  16.112 +function
  16.113 +  "evn 0 = True"
  16.114 +  "evn (Suc n) = od n"
  16.115 +and
  16.116 +  "od 0 = False"
  16.117 +  "od (Suc n) = evn n"
  16.118 +  by pat_completeness auto
  16.119 +
  16.120 +thm evn.psimps
  16.121 +thm od.psimps
  16.122 +
  16.123 +thm evn_od.pinduct
  16.124 +thm evn_od.termination
  16.125 +thm evn_od.domintros
  16.126 +
  16.127 +termination
  16.128 +  by (auto_term "measure (sum_case (%n. n) (%n. n))")
  16.129 +
  16.130 +thm evn.simps
  16.131 +thm od.simps
  16.132 +
  16.133 +
  16.134  end