src/HOL/Tools/function_package/fundef_package.ML
changeset 25222 78943ac46f6d
parent 25201 e6fe58b640ce
child 26129 14f6dbb195c4
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sun Oct 28 13:18:00 2007 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Oct 29 10:37:09 2007 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4         fold2 add_for_f fnames simps_by_f lthy)
     1.5      end
     1.6  
     1.7 -fun fundef_afterqed config fixes post defname cont sort_cont [[proof]] lthy =
     1.8 +fun fundef_afterqed config fixes post defname cont sort_cont cnames [[proof]] lthy =
     1.9      let
    1.10        val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    1.11            cont (Goal.close_result proof)
    1.12 @@ -73,31 +73,34 @@
    1.13              |> addsmps "psimps" [] psimps
    1.14              ||> fold_option (snd oo addsmps "simps" []) trsimps
    1.15              ||>> note_theorem ((qualify "pinduct",
    1.16 -                                [Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
    1.17 +                   [Attrib.internal (K (RuleCases.case_names cnames)),
    1.18 +                    Attrib.internal (K (RuleCases.consumes 1)),
    1.19 +                    Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
    1.20              ||>> note_theorem ((qualify "termination", []), [termination])
    1.21 -            ||> (snd o note_theorem ((qualify "cases", []), [cases]))
    1.22 +            ||> (snd o note_theorem ((qualify "cases", 
    1.23 +                   [Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
    1.24              ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
    1.25  
    1.26 -      val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
    1.27 +      val cdata = FundefCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
    1.28                                    pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname }
    1.29        val _ = Specification.print_consts lthy (K false) (map fst fixes)
    1.30      in
    1.31        lthy 
    1.32          |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata)
    1.33 -    end (* FIXME: Add cases for induct and cases thm *)
    1.34 +    end
    1.35  
    1.36  
    1.37  fun gen_add_fundef prep fixspec eqnss config flags lthy =
    1.38      let
    1.39        val ((fixes, spec), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
    1.40 -      val (eqs, post, sort_cont) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    1.41 +      val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    1.42  
    1.43        val defname = mk_defname fixes
    1.44  
    1.45        val ((goalstate, cont), lthy) =
    1.46            FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy
    1.47  
    1.48 -      val afterqed = fundef_afterqed config fixes post defname cont sort_cont
    1.49 +      val afterqed = fundef_afterqed config fixes post defname cont sort_cont cnames
    1.50      in
    1.51        lthy
    1.52          |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
    1.53 @@ -106,7 +109,7 @@
    1.54  
    1.55  fun total_termination_afterqed data [[totality]] lthy =
    1.56      let
    1.57 -      val FundefCtxData { add_simps, psimps, pinducts, defname, ... } = data
    1.58 +      val FundefCtxData { add_simps, case_names, psimps, pinducts, defname, ... } = data
    1.59  
    1.60        val totality = Goal.close_result totality
    1.61  
    1.62 @@ -122,7 +125,7 @@
    1.63      in
    1.64        lthy
    1.65          |> add_simps "simps" allatts tsimps |> snd
    1.66 -        |> note_theorem ((qualify "induct", []), tinduct) |> snd
    1.67 +        |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd
    1.68      end
    1.69  
    1.70