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