# HG changeset patch
# User haftmann
# Date 1184570944 -7200
# Node ID b18557301bf9a0daf5def41779e65bc4bd24d74a
# Parent  f5e6932d05002ea097fe05e54a899ba7c42657cd
added function for case certificates

diff -r f5e6932d0500 -r b18557301bf9 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Mon Jul 16 09:29:03 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Mon Jul 16 09:29:04 2007 +0200
@@ -11,6 +11,7 @@
   val get_eq_datatype: theory -> string -> thm list
   val dest_case_expr: theory -> term
     -> ((string * typ) list * ((term * typ) * (term * term) list)) option
+  val get_case_cert: theory -> string -> thm
 
   type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
     -> theory -> theory
@@ -406,6 +407,36 @@
 
 end;
 
+fun get_case_cert thy tyco =
+  let
+    val raw_thms =
+      (#case_rewrites o DatatypePackage.the_datatype thy) tyco;
+    val thms as hd_thm :: _ = raw_thms
+      |> Conjunction.intr_balanced
+      |> Drule.unvarify
+      |> Conjunction.elim_balanced (length raw_thms)
+      |> map Simpdata.mk_meta_eq
+      |> map Drule.zero_var_indexes
+    val params = fold_aterms (fn (Free (v, _)) => insert (op =) v
+      | _ => I) (Thm.prop_of hd_thm) [];
+    val rhs = hd_thm
+      |> Thm.prop_of
+      |> Logic.dest_equals
+      |> fst
+      |> Term.strip_comb
+      |> apsnd (fst o split_last)
+      |> list_comb;
+    val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
+    val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
+  in
+    thms
+    |> Conjunction.intr_balanced
+    |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
+    |> Thm.implies_intr asm
+    |> Thm.generalize ([], params) 0
+    |> Thm.varifyT
+  end;
+
 
 
 (** codetypes for code 2nd generation **)
diff -r f5e6932d0500 -r b18557301bf9 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Mon Jul 16 09:29:03 2007 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Mon Jul 16 09:29:04 2007 +0200
@@ -8,7 +8,11 @@
 imports ExecutableContent
 begin
 
-code_gen "*" in SML in OCaml file - in OCaml file -
-code_gen in SML in OCaml file - in OCaml file -
+code_gen "*" in SML to CodegenTest
+  in OCaml file -
+  in Haskell file -
+code_gen in SML to CodegenTest
+  in OCaml file -
+  in Haskell file -
 
 end
diff -r f5e6932d0500 -r b18557301bf9 src/HOL/ex/Codegenerator_Rat.thy
--- a/src/HOL/ex/Codegenerator_Rat.thy	Mon Jul 16 09:29:03 2007 +0200
+++ b/src/HOL/ex/Codegenerator_Rat.thy	Mon Jul 16 09:29:04 2007 +0200
@@ -29,8 +29,10 @@
 definition
   "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
 
-code_gen foobar in SML in OCaml file - in Haskell file -
-ML {* ROOT.Codegenerator_Rat.foobar *}
+code_gen foobar in SML to Foo
+  in OCaml file -
+  in Haskell file -
+ML {* Foo.foobar *}
 
 code_module Foo
   contains foobar