--- 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) \<noteq> 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 \<noteq> x mod 2 \<longrightarrow> 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
--- 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
--- 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
--- 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