--- 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
--- 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