# 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 "\ 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: "\ a c b. a1 = a ==> a2 = c ==> r a b ==> tranclp r b c ==> thesis" - and base: "\ 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