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
(* $Id$ *)
(* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
local
(* pulls out dynamically a thm via the simpset *)
fun dynamic_thms ss name =
ProofContext.get_thms (Simplifier.the_context ss) (Name name);
fun dynamic_thm ss name =
ProofContext.get_thm (Simplifier.the_context ss) (Name name);
(* initial simplification step in the tactic *)
fun perm_eval_tac ss i =
let
fun perm_eval_simproc sg ss redex =
let
(* the "application" case below is only applicable when the head *)
(* of f is not a constant or when it is a permuattion with two or *)
(* more arguments *)
fun applicable t =
(case (strip_comb t) of
(Const ("nominal.perm",_),ts) => (length ts) >= 2
| (Const _,_) => false
| _ => true)
in
(case redex of
(* case pi o (f x) == (pi o f) (pi o x) *)
(* special treatment according to the head of f *)
(Const("nominal.perm",
Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
(case (applicable f) of
false => NONE
| _ =>
let
val name = Sign.base_name n
val at_inst = dynamic_thm ss ("at_"^name^"_inst")
val pt_inst = dynamic_thm ss ("pt_"^name^"_inst")
val perm_eq_app = thm "nominal.pt_fun_app_eq"
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end)
(* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
| (Const("nominal.perm",_) $ pi $ (Abs _)) =>
let
val perm_fun_def = thm "nominal.perm_fun_def"
in SOME (perm_fun_def) end
(* no redex otherwise *)
| _ => NONE) end
val perm_eval =
Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval"
["nominal.perm pi x"] perm_eval_simproc;
(* 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,
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 *)
(* in case there are more atom-types we have to check every possible instance *)
(* of perm_compose *)
fun apply_perm_compose_tac ss i =
let
val perm_compose = dynamic_thms ss "perm_compose";
val tacs = map (fn thm => (rtac (thm RS trans) i)) perm_compose
in
("analysing permutation compositions on the lhs",FIRST (tacs))
end
(* applying Stefan's smart congruence tac *)
fun apply_cong_tac i =
("application of congruence",
(fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
(* unfolds the definition of permutations applied to functions *)
fun unfold_perm_fun_def_tac i =
let
val perm_fun_def = thm "nominal.perm_fun_def"
in
("unfolding of permutations on functions",
simp_tac (HOL_basic_ss addsimps [perm_fun_def]) i)
end
(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
fun expand_fun_eq_tac i =
("extensionality expansion of functions",
EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) i, REPEAT_DETERM (rtac allI i)]);
(* debugging *)
fun DEBUG_tac (msg,tac) =
CHANGED (EVERY [tac, print_tac ("after "^msg)]);
fun NO_DEBUG_tac (_,tac) = CHANGED tac;
(* Main Tactic *)
fun perm_simp_tac tactical ss i =
DETERM (tactical (perm_eval_tac ss i));
(* perm_simp_tac plus additional tactics to decide *)
(* support problems *)
(* the "recursion"-depth is set to 10 - this seems sufficient *)
fun perm_supports_tac tactical ss n =
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_cong_tac i),
fn i => tactical (unfold_perm_fun_def_tac i),
fn i => tactical (expand_fun_eq_tac i)]
THEN_ALL_NEW (TRY o (perm_supports_tac tactical ss (n-1))));
(* tactic that first unfolds the support definition *)
(* and strips off the intros, then applies perm_supports_tac *)
fun supports_tac tactical ss i =
let
val supports_def = thm "nominal.op supports_def";
val fresh_def = thm "nominal.fresh_def";
val fresh_prod = thm "nominal.fresh_prod";
val simps = [supports_def,symmetric fresh_def,fresh_prod]
in
EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i),
tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)),
tactical ("geting rid of the imps", rtac impI i),
tactical ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)),
tactical ("applying perm_simp ", perm_supports_tac tactical ss 10 i)]
end;
(* tactic that guesses the finite-support of a goal *)
fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j - i) ins vs
| collect_vars i (v as Free _) vs = v ins vs
| collect_vars i (v as Var _) vs = v ins vs
| collect_vars i (Const _) vs = vs
| collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
| collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
val supports_rule = thm "supports_finite";
fun finite_guess_tac tactical ss i st =
let val goal = List.nth(cprems_of st, i-1)
in
case Logic.strip_assums_concl (term_of goal) of
_ $ (Const ("op :", _) $ (Const ("nominal.supp", T) $ x) $
Const ("Finite_Set.Finites", _)) =>
let
val cert = Thm.cterm_of (sign_of_thm st);
val ps = Logic.strip_params (term_of goal);
val Ts = rev (map snd ps);
val vs = collect_vars 0 x [];
val s = foldr (fn (v, s) =>
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
HOLogic.unit vs;
val s' = list_abs (ps,
Const ("nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
val supports_rule' = Thm.lift_rule goal supports_rule;
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (prems_of supports_rule'));
val supports_rule'' = Drule.cterm_instantiate
[(cert (head_of S), cert s')] supports_rule'
in
(tactical ("guessing of the right supports-set",
EVERY [compose_tac (false, supports_rule'', 2) i,
asm_full_simp_tac ss (i+1),
supports_tac tactical ss i])) st
end
| _ => Seq.empty
end
handle Subscript => Seq.empty
in
fun simp_meth_setup tac =
Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
(Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
val perm_eq_meth = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
val perm_eq_meth_debug = simp_meth_setup (perm_simp_tac DEBUG_tac);
val supports_meth = simp_meth_setup (supports_tac NO_DEBUG_tac);
val supports_meth_debug = simp_meth_setup (supports_tac DEBUG_tac);
val finite_gs_meth = simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
val finite_gs_meth_debug = simp_meth_setup (finite_guess_tac DEBUG_tac);
end