# HG changeset patch # User bulwahn # Date 1244749046 -7200 # Node ID 0047df9eb34730ce05f00538d012b9b9bedbd326 # Parent 995d6b90e9d6a326d91ba0db2400735cf966d36d improved infrastructure of predicate compiler for adding manual introduction rules diff -r 995d6b90e9d6 -r 0047df9eb347 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Jun 11 12:06:13 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Jun 11 21:37:26 2009 +0200 @@ -7,8 +7,6 @@ | "even n \ odd (Suc n)" | "odd n \ even (Suc n)" - - code_pred even . thm odd.equation @@ -57,19 +55,42 @@ (*FIXME values 10 "{(ys, zs). partition (\n. n mod 2 = 0) [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" *) -thm tranclp.intros -(* lemma [code_pred_intros]: "r a b ==> tranclp r a b" "r a b ==> tranclp r b c ==> tranclp r a c" by auto -*) -(* -code_pred tranclp . + + +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 + +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 +qed thm tranclp.equation -*) + inductive succ :: "nat \ nat \ bool" where "succ 0 1" | "succ m n \ succ (Suc m) (Suc n)" @@ -77,8 +98,7 @@ code_pred succ . thm succ.equation - -(* TODO: requires alternative rules for trancl *) +(* FIXME: why does this not terminate? *) (* values 20 "{n. tranclp succ 10 n}" values "{n. tranclp succ n 10}" diff -r 995d6b90e9d6 -r 0047df9eb347 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Thu Jun 11 12:06:13 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Thu Jun 11 21:37:26 2009 +0200 @@ -135,6 +135,7 @@ cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_mode ms)) modes)); + datatype predfun_data = PredfunData of { name : string, definition : thm, @@ -180,9 +181,7 @@ (* queries *) fun lookup_pred_data thy name = - case try (Graph.get_node (PredData.get thy)) name of - SOME pred_data => SOME (rep_pred_data pred_data) - | NONE => NONE + Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name) fun the_pred_data thy name = case lookup_pred_data thy name of NONE => error ("No such predicate " ^ quote name) @@ -243,16 +242,73 @@ in thy end; *) + +fun imp_prems_conv cv ct = + case Thm.term_of ct of + Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct + | _ => Conv.all_conv ct + +fun Trueprop_conv cv ct = + case Thm.term_of ct of + Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct + | _ => error "Trueprop_conv" + +fun preprocess_intro thy rule = + Conv.fconv_rule + (imp_prems_conv + (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq}))))) + (Thm.transfer thy rule) + +fun preprocess_elim thy nargs elimrule = let + fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) = + HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs) + | replace_eqs t = t + fun preprocess_case t = let + val params = Logic.strip_params t + val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t) + val assums_hyp' = assums1 @ (map replace_eqs assums2) + in list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t)) end + val prems = Thm.prems_of elimrule + val cases' = map preprocess_case (tl prems) + val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule) + in + Thm.equal_elim + (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}]) + (cterm_of thy elimrule'))) + elimrule + end; + +fun fetch_pred_data thy name = + case try (InductivePackage.the_inductive (ProofContext.init thy)) name of + SOME (info as (_, result)) => + let + fun is_intro_of intro = + let + val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) + in (fst (dest_Const const) = name) end; + val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result)) + val elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info))) + val nparams = length (InductivePackage.params_of (#raw_induct result)) + in (intros, elim, nparams) end + | NONE => error ("No such predicate: " ^ quote name) + (* updaters *) fun add_predfun name mode data = let val add = apsnd (cons (mode, mk_predfun_data data)) in PredData.map (Graph.map_node name (map_pred_data add)) end -fun add_intro thm = let +fun add_intro thm thy = let val (name, _) = dest_Const (fst (strip_intro_concl 0 (prop_of thm))) - fun set (intros, elim, nparams) = (thm::intros, elim, nparams) - in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end + fun cons_intro gr = + case try (Graph.get_node gr) name of + SOME pred_data => Graph.map_node name (map_pred_data + (apfst (fn (intro, elim, nparams) => (thm::intro, elim, nparams)))) gr + | NONE => + let + val nparams = the_default 0 (try (#3 o fetch_pred_data thy) name) + in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), [])) gr end; + in PredData.map cons_intro thy end fun set_elim thm = let val (name, _) = dest_Const (fst @@ -813,42 +869,6 @@ fun is_Type (Type _) = true | is_Type _ = false -fun imp_prems_conv cv ct = - case Thm.term_of ct of - Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct - | _ => Conv.all_conv ct - -fun Trueprop_conv cv ct = - case Thm.term_of ct of - Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct - | _ => error "Trueprop_conv" - -fun preprocess_intro thy rule = - Conv.fconv_rule - (imp_prems_conv - (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq}))))) - (Thm.transfer thy rule) - -fun preprocess_elim thy nargs elimrule = let - fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) = - HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs) - | replace_eqs t = t - fun preprocess_case t = let - val params = Logic.strip_params t - val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t) - val assums_hyp' = assums1 @ (map replace_eqs assums2) - in list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t)) end - val prems = Thm.prems_of elimrule - val cases' = map preprocess_case (tl prems) - val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule) - in - Thm.equal_elim - (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}]) - (cterm_of thy elimrule'))) - elimrule - end; - - (* returns true if t is an application of an datatype constructor *) (* which then consequently would be splitted *) (* else false *) @@ -1367,7 +1387,7 @@ fun mk_casesrule ctxt nparams introrules = let - val intros = map prop_of introrules + val intros = map (Logic.unvarify o prop_of) introrules val (pred, (params, args)) = strip_intro_concl nparams (hd intros) val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) @@ -1388,26 +1408,13 @@ in Logic.list_implies (assm :: cases, prop) end; (* code dependency graph *) - -fun fetch_pred_data thy name = - case try (InductivePackage.the_inductive (ProofContext.init thy)) name of - SOME (info as (_, result)) => - let - fun is_intro_of intro = - let - val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) - in (fst (dest_Const const) = name) end; - val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result)) - val elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info))) - val nparams = length (InductivePackage.params_of (#raw_induct result)) - in mk_pred_data ((intros, SOME elim, nparams), []) end - | NONE => error ("No such predicate: " ^ quote name) -fun dependencies_of (thy : theory) name = +fun dependencies_of thy name = let fun is_inductive_predicate thy name = is_some (try (InductivePackage.the_inductive (ProofContext.init thy)) name) - val data = fetch_pred_data thy name + val (intro, elim, nparams) = fetch_pred_data thy name + val data = mk_pred_data ((intro, SOME elim, nparams), []) val intros = map Thm.prop_of (#intros (rep_pred_data data)) val keys = fold Term.add_consts intros [] |> map fst |> filter (is_inductive_predicate thy)