summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | urbanc |

Thu, 06 Apr 2006 17:29:40 +0200 | |

changeset 19350 | 2e1c7ca05ee0 |

parent 19349 | 36e537f89585 |

child 19351 | c33563c7c14c |

modified the perm_compose rule such that it
is applied as simplification rule (as simproc)
in the restricted case where the first
permutation is a swapping coming from a supports
problem
also deleted the perm_compose' rule from the set
of rules that are automatically tried

--- a/src/HOL/Nominal/nominal_permeq.ML Thu Apr 06 16:13:17 2006 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Thu Apr 06 17:29:40 2006 +0200 @@ -54,16 +54,54 @@ Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" ["nominal.perm pi x"] perm_eval_simproc; - (* these lemmas are created dynamically according to the atom types *) - val perm_swap = dynamic_thms ss "perm_swap" - val perm_fresh = dynamic_thms ss "perm_fresh_fresh" - val perm_bij = dynamic_thms ss "perm_bij" - val perm_compose' = dynamic_thms ss "perm_compose'" - val perm_pi_simp = dynamic_thms ss "perm_pi_simp" - val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_compose'@perm_pi_simp) + (* applies the pt_perm_compose lemma *) + (* *) + (* pi1 o (pi2 o x) = (pi1 o pi2) o (pi1 o x) *) + (* *) + (* in the restricted case where pi1 is a swapping *) + (* (a b) coming from a "supports problem"; in *) + (* this rule would cause loops in the simplifier *) + val pt_perm_compose = thm "pt_perm_compose"; + + fun perm_compose_simproc i sg ss redex = + (case redex of + (Const ("nominal.perm", _) $ (pi1 as Const ("List.list.Cons", _) $ + (Const ("Pair", _) $ Free (a as (_, T as Type (tname, _))) $ Free b) $ + Const ("List.list.Nil", _)) $ (Const ("nominal.perm", + Type ("fun", [Type ("List.list", [Type ("*", [U, _])]), _])) $ pi2 $ t)) => + let + val ({bounds = (_, xs), ...}, _) = rep_ss ss + val ai = find_index (fn (x, _) => x = a) xs + val bi = find_index (fn (x, _) => x = b) xs + val tname' = Sign.base_name tname + in + if ai = length xs - i - 1 andalso + bi = length xs - i - 2 andalso + T = U andalso pi1 <> pi2 then + SOME (Drule.instantiate' + [SOME (ctyp_of sg (fastype_of t))] + [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)] + (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")), + PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose))) + else NONE + end + | _ => NONE); + + fun perm_compose i = + Simplifier.simproc (the_context()) "perm_compose" + ["nominal.perm [(a, b)] (nominal.perm pi t)"] (perm_compose_simproc i); + + (* these lemmas are created dynamically according to the atom types *) + val perm_swap = dynamic_thms ss "perm_swap" + val perm_fresh = dynamic_thms ss "perm_fresh_fresh" + val perm_bij = dynamic_thms ss "perm_bij" + val perm_pi_simp = dynamic_thms ss "perm_pi_simp" + val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp) in ("general simplification step", - FIRST [rtac conjI i, asm_full_simp_tac (ss' addsimprocs [perm_eval]) i]) + FIRST [rtac conjI i, + SUBGOAL (fn (g, i) => asm_full_simp_tac + (ss' addsimprocs [perm_eval,perm_compose (length (Logic.strip_params g)-2)]) i) i]) end; (* applies the perm_compose rule - this rule would loop in the simplifier *) @@ -114,7 +152,7 @@ if n=0 then K all_tac else DETERM o (FIRST'[fn i => tactical (perm_eval_tac ss i), - fn i => tactical (apply_perm_compose_tac ss i), + (*fn i => tactical (apply_perm_compose_tac ss i),*) fn i => tactical (apply_cong_tac i), fn i => tactical (unfold_perm_fun_def_tac i), fn i => tactical (expand_fun_eq_tac i)]