1.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Apr 22 11:10:23 2009 +0200
     1.2 +++ b/src/HOL/ex/predicate_compile.ML	Mon May 11 09:18:42 2009 +0200
     1.3 @@ -14,8 +14,12 @@
     1.4    val code_ind_intros_attrib : attribute
     1.5    val code_ind_cases_attrib : attribute
     1.6    val setup : theory -> theory
     1.7 +  val code_pred : string -> Proof.context -> Proof.state
     1.8 +  val code_pred_cmd : string -> Proof.context -> Proof.state
     1.9    val print_alternative_rules : theory -> theory
    1.10    val do_proofs: bool ref
    1.11 +  val pred_intros : theory -> string -> thm list
    1.12 +  val get_nparams : theory -> string -> int
    1.13  end;
    1.14  
    1.15  structure Predicate_Compile: PREDICATE_COMPILE =
    1.16 @@ -1340,6 +1344,57 @@
    1.17    Attrib.setup @{binding code_ind_cases} (Scan.succeed code_ind_cases_attrib)
    1.18      "adding alternative elimination rules for code generation of inductive predicates";
    1.19  
    1.20 +(* generation of case rules from user-given introduction rules *)
    1.21 +
    1.22 +   fun mk_casesrule introrules nparams ctxt = let
    1.23 +    val intros = map prop_of introrules
    1.24 +    val (pred, (params, args)) = strip_intro_concl (hd intros) nparams
    1.25 +    val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
    1.26 +    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
    1.27 +    val (argnames, ctxt2) = Variable.variant_fixes
    1.28 +      (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
    1.29 +    val argvs = map Free (argnames ~~ (map fastype_of args))
    1.30 +    fun mk_case intro = let
    1.31 +        val (_, (_, args)) = strip_intro_concl intro nparams
    1.32 +        val prems = Logic.strip_imp_prems intro
    1.33 +        val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
    1.34 +        val frees = (fold o fold_aterms)
    1.35 +          (fn t as Free _ =>
    1.36 +              if member (op aconv) params t then I else insert (op aconv) t
    1.37 +           | _ => I) (args @ prems) []
    1.38 +        in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
    1.39 +    val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
    1.40 +    val cases = map mk_case intros
    1.41 +    val (_, ctxt3) = ProofContext.add_assms_i Assumption.assume_export
    1.42 +              [((Binding.name AutoBind.assmsN, []), map (fn t => (t, [])) (assm :: cases))]
    1.43 +              ctxt2
    1.44 +  in (pred, prop, ctxt3) end;
    1.45 +
    1.46 +(* setup for user interface *)
    1.47 +
    1.48 +  fun generic_code_pred prep_const raw_const lthy =
    1.49 +    let
    1.50 +      val thy = (ProofContext.theory_of lthy)
    1.51 +      val const = prep_const thy raw_const
    1.52 +      val nparams = get_nparams thy const
    1.53 +      val intro_rules = pred_intros thy const
    1.54 +      val (((tfrees, frees), fact), ctxt') =
    1.55 +        Variable.import_thms true intro_rules lthy;
    1.56 +      val (pred, prop, ctxt'') = mk_casesrule fact nparams ctxt'
    1.57 +      val (predname, _) = dest_Const pred
    1.58 +      fun after_qed [[th]] ctxt'' =
    1.59 +        LocalTheory.note Thm.theoremK
    1.60 +          ((Binding.name (Long_Name.base_name predname ^ "_cases"),
    1.61 +            [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) ctxt''
    1.62 +        |> snd
    1.63 +        |> ProofContext.theory (create_def_equation predname)
    1.64 +    in
    1.65 +      Proof.theorem_i NONE after_qed [[(prop, [])]] ctxt''
    1.66 +    end;
    1.67 +
    1.68 +  val code_pred = generic_code_pred (K I);
    1.69 +  val code_pred_cmd = generic_code_pred Code_Unit.read_const
    1.70 +
    1.71  end;
    1.72  
    1.73  fun pred_compile name thy = Predicate_Compile.create_def_equation