# HG changeset patch # User krauss # Date 1193650629 -3600 # Node ID 78943ac46f6d37a27103a35b931c9353c240ac14 # Parent 5ded95dda5df7b2de0b5236885cc3e3d26e0a777 fun/function: generate case names for induction rules diff -r 5ded95dda5df -r 78943ac46f6d src/HOL/NumberTheory/Fib.thy --- a/src/HOL/NumberTheory/Fib.thy Sun Oct 28 13:18:00 2007 +0100 +++ b/src/HOL/NumberTheory/Fib.thy Mon Oct 29 10:37:09 2007 +0100 @@ -43,7 +43,7 @@ next case 2 show ?case by (simp add: fib_2) next - case 3 thus ?case by (simp add: fib_2 add_mult_distrib2) + case fib_2 thus ?case by (simp add: fib.simps add_mult_distrib2) qed lemma fib_Suc_neq_0: "fib (Suc n) \ 0" @@ -72,9 +72,9 @@ next case 2 thus ?case by (simp add: fib_2 mod_Suc) next - case (3 x) + case (fib_2 x) have "Suc 0 \ x mod 2 \ x mod 2 = 0" by presburger - with "3.hyps" show ?case by (simp add: fib_2 add_mult_distrib add_mult_distrib2) + with "fib_2.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2) qed text{*We now obtain a version for the natural numbers via the coercion diff -r 5ded95dda5df -r 78943ac46f6d src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Sun Oct 28 13:18:00 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Oct 29 10:37:09 2007 +0100 @@ -52,6 +52,7 @@ (* contains no logical entities: invariant under morphisms *) add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory, + case_names : string list, fs : term list, R : term, @@ -61,12 +62,13 @@ termination: thm } -fun morph_fundef_data (FundefCtxData {add_simps, fs, R, psimps, pinducts, termination, defname}) phi = +fun morph_fundef_data (FundefCtxData {add_simps, case_names, fs, R, + psimps, pinducts, termination, defname}) phi = let val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi val name = Morphism.name phi in - FundefCtxData { add_simps = add_simps, + FundefCtxData { add_simps = add_simps, case_names = case_names, fs = map term fs, R = term R, psimps = fact psimps, pinducts = fact pinducts, termination = thm termination, defname = name defname } @@ -260,22 +262,29 @@ type fixes = ((string * typ) * mixfix) list type 'a spec = ((bstring * Attrib.src list) * 'a list) list type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec - -> (term list * (thm list -> thm spec) * (thm list -> thm list list)) + -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all +fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k + | mk_case_names _ n 0 = [] + | mk_case_names _ n 1 = [n] + | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) + fun empty_preproc check _ _ ctxt fixes spec = let val (nas,tss) = split_list spec - val _ = check ctxt fixes (flat tss) val ts = flat tss + val _ = check ctxt fixes ts val fnames = map (fst o fst) fixes val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) |> map (map snd) + + val cnames = map_index (fn (i, (n,_)) => mk_case_names i n 1) nas |> flat in - (ts, curry op ~~ nas o Library.unflat tss, sort) + (ts, curry op ~~ nas o Library.unflat tss, sort, cnames) end structure Preprocessor = GenericDataFun diff -r 5ded95dda5df -r 78943ac46f6d src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Sun Oct 28 13:18:00 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Mon Oct 29 10:37:09 2007 +0100 @@ -258,14 +258,14 @@ val eqs = map the_single eqss val feqs = eqs - |> tap (check_defs ctxt fixes) (* Standard checks *) - |> tap (map (check_pats ctxt)) (* More checks for sequential mode *) - |> curry op ~~ flags' + |> tap (check_defs ctxt fixes) (* Standard checks *) + |> tap (map (check_pats ctxt)) (* More checks for sequential mode *) + |> curry op ~~ flags' - val compleqs = add_catchall ctxt fixes feqs (* Completion *) + val compleqs = add_catchall ctxt fixes feqs (* Completion *) - val spliteqs = warn_if_redundant ctxt feqs - (FundefSplit.split_some_equations ctxt compleqs) + val spliteqs = warn_if_redundant ctxt feqs + (FundefSplit.split_some_equations ctxt compleqs) fun restore_spec thms = nas ~~ Library.take (length nas, Library.unflat spliteqs thms) @@ -277,8 +277,14 @@ fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) |> map (map snd) + + val nas' = nas @ replicate (length spliteqs - length nas) ("",[]) + + val case_names = map_index (fn (i, ((n, _), es)) => mk_case_names i n (length es)) + (nas' ~~ spliteqs) + |> flat in - (flat spliteqs, restore_spec, sort) + (flat spliteqs, restore_spec, sort, case_names) end else FundefCommon.empty_preproc check_defs config flags ctxt fixes spec diff -r 5ded95dda5df -r 78943ac46f6d src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Sun Oct 28 13:18:00 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Oct 29 10:37:09 2007 +0100 @@ -59,7 +59,7 @@ fold2 add_for_f fnames simps_by_f lthy) end -fun fundef_afterqed config fixes post defname cont sort_cont [[proof]] lthy = +fun fundef_afterqed config fixes post defname cont sort_cont cnames [[proof]] lthy = let val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = cont (Goal.close_result proof) @@ -73,31 +73,34 @@ |> addsmps "psimps" [] psimps ||> fold_option (snd oo addsmps "simps" []) trsimps ||>> note_theorem ((qualify "pinduct", - [Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) + [Attrib.internal (K (RuleCases.case_names cnames)), + Attrib.internal (K (RuleCases.consumes 1)), + Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) ||>> note_theorem ((qualify "termination", []), [termination]) - ||> (snd o note_theorem ((qualify "cases", []), [cases])) + ||> (snd o note_theorem ((qualify "cases", + [Attrib.internal (K (RuleCases.case_names cnames))]), [cases])) ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros - val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps', + val cdata = FundefCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps', pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname } val _ = Specification.print_consts lthy (K false) (map fst fixes) in lthy |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata) - end (* FIXME: Add cases for induct and cases thm *) + end fun gen_add_fundef prep fixspec eqnss config flags lthy = let val ((fixes, spec), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy - val (eqs, post, sort_cont) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec + val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec val defname = mk_defname fixes val ((goalstate, cont), lthy) = FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy - val afterqed = fundef_afterqed config fixes post defname cont sort_cont + val afterqed = fundef_afterqed config fixes post defname cont sort_cont cnames in lthy |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]] @@ -106,7 +109,7 @@ fun total_termination_afterqed data [[totality]] lthy = let - val FundefCtxData { add_simps, psimps, pinducts, defname, ... } = data + val FundefCtxData { add_simps, case_names, psimps, pinducts, defname, ... } = data val totality = Goal.close_result totality @@ -122,7 +125,7 @@ in lthy |> add_simps "simps" allatts tsimps |> snd - |> note_theorem ((qualify "induct", []), tinduct) |> snd + |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd end