fun/function: generate case names for induction rules
authorkrauss
Mon, 29 Oct 2007 10:37:09 +0100
changeset 25222 78943ac46f6d
parent 25221 5ded95dda5df
child 25223 7463251e7273
fun/function: generate case names for induction rules
src/HOL/NumberTheory/Fib.thy
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_package.ML
--- 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