# HG changeset patch
# User bulwahn
# Date 1244824438 -7200
# Node ID 1c143f6a2226df0b37b5382e8feb99b6c58d012c
# Parent  f9c35a72390ad82dfb5c1de99d565ce8bad4499d
added cases to code_pred command

diff -r f9c35a72390a -r 1c143f6a2226 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Fri Jun 12 07:23:45 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Fri Jun 12 18:33:58 2009 +0200
@@ -61,34 +61,12 @@
 "r a b ==> tranclp r b c ==> tranclp r a c" 
 by auto
 
-
-lemma converse_tranclpE:
-  assumes "tranclp r x z "
-  assumes "r x z ==> P"
-  assumes "\<And> y. [| r x y; tranclp r y z |] ==> P"
-  shows P
-proof -
-  from tranclpD[OF assms(1)]
-  obtain y where "r x y" and "rtranclp r y z" by iprover
-  with assms(2-3) rtranclpD[OF this(2)] this(1)
-  show P by iprover
-qed  
-
 (* Setup requires quick and dirty proof *)
 (*
 code_pred tranclp
 proof -
-  assume tranclp: "tranclp r a1 a2"
-     and step: "\<And> a c b. a1 = a ==> a2 = c ==> r a b ==> tranclp r b c ==> thesis"
-     and base: "\<And> a b. a1 = a ==> a2 = b ==> r a b ==> thesis"
-  show thesis
-  proof (cases rule: converse_tranclpE[OF tranclp])
-    case 1
-    from 1 base show thesis by auto
-  next
-    case 2
-    from 2 step show thesis by auto
-  qed
+  case tranclp
+  from this converse_tranclpE[OF this(1)] show thesis by metis
 qed
 
 thm tranclp.equation
diff -r f9c35a72390a -r 1c143f6a2226 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Fri Jun 12 07:23:45 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Fri Jun 12 18:33:58 2009 +0200
@@ -1465,12 +1465,20 @@
       let
         val nparams = nparams_of thy' const
         val intros = intros_of thy' const
-      in mk_casesrule lthy' nparams intros end
+      in mk_casesrule lthy' nparams intros end  
     val cases_rules = map mk_cases preds
+    val cases =
+      map (fn case_rule => RuleCases.Case {fixes = [],
+        assumes = [("", Logic.strip_imp_prems case_rule)],
+        binds = [], cases = []}) cases_rules
+    val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
+    val _ = Output.tracing (commas (map fst case_env))
+    val lthy'' = ProofContext.add_cases true case_env lthy'
+    
     fun after_qed thms =
       LocalTheory.theory (fold set_elim (map the_single thms) #> add_equations const)
   in
-    Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy'
+    Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
   end;
 
 structure P = OuterParse