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