src/HOL/Nominal/nominal_permeq.ML
author urbanc
Thu Apr 06 17:29:40 2006 +0200 (2006-04-06)
changeset 19350 2e1c7ca05ee0
parent 19169 20a73345dd6e
child 19477 a95176d0f0dd
permissions -rw-r--r--
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
     1 (* $Id$ *)
     2 
     3 (* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
     4 
     5 local
     6 
     7 (* pulls out dynamically a thm via the simpset *)
     8 fun dynamic_thms ss name = 
     9     ProofContext.get_thms (Simplifier.the_context ss) (Name name);
    10 fun dynamic_thm ss name = 
    11     ProofContext.get_thm (Simplifier.the_context ss) (Name name);
    12 
    13 (* initial simplification step in the tactic *)
    14 fun perm_eval_tac ss i =
    15     let
    16         fun perm_eval_simproc sg ss redex =
    17         let 
    18 	   
    19            (* the "application" case below is only applicable when the head   *)
    20            (* of f is not a constant  or when it is a permuattion with two or *) 
    21            (* more arguments                                                  *)
    22            fun applicable t = 
    23 	       (case (strip_comb t) of
    24 		  (Const ("nominal.perm",_),ts) => (length ts) >= 2
    25 		| (Const _,_) => false
    26 		| _ => true)
    27 
    28 	in
    29         (case redex of 
    30         (* case pi o (f x) == (pi o f) (pi o x)          *)
    31         (* special treatment according to the head of f  *)
    32         (Const("nominal.perm",
    33           Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
    34 	   (case (applicable f) of
    35                 false => NONE  
    36               | _ => 
    37 		let
    38 		    val name = Sign.base_name n
    39 		    val at_inst     = dynamic_thm ss ("at_"^name^"_inst")
    40 		    val pt_inst     = dynamic_thm ss ("pt_"^name^"_inst")  
    41 		    val perm_eq_app = thm "nominal.pt_fun_app_eq"	  
    42 		in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end)
    43 
    44         (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
    45         | (Const("nominal.perm",_) $ pi $ (Abs _)) => 
    46            let 
    47                val perm_fun_def = thm "nominal.perm_fun_def"
    48            in SOME (perm_fun_def) end
    49 
    50         (* no redex otherwise *) 
    51         | _ => NONE) end
    52 
    53 	val perm_eval =
    54 	    Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 
    55 	    ["nominal.perm pi x"] perm_eval_simproc;
    56 
    57       (* applies the pt_perm_compose lemma              *)
    58       (*                                                *)
    59       (*     pi1 o (pi2 o x) = (pi1 o pi2) o (pi1 o x)  *)
    60       (*                                                *)
    61       (* in the restricted case where pi1 is a swapping *)
    62       (* (a b) coming from a "supports problem"; in     *)
    63       (* this rule would cause loops in the simplifier  *) 
    64       val pt_perm_compose = thm "pt_perm_compose";
    65 	  
    66       fun perm_compose_simproc i sg ss redex =
    67       (case redex of
    68         (Const ("nominal.perm", _) $ (pi1 as Const ("List.list.Cons", _) $
    69          (Const ("Pair", _) $ Free (a as (_, T as Type (tname, _))) $ Free b) $ 
    70            Const ("List.list.Nil", _)) $ (Const ("nominal.perm", 
    71             Type ("fun", [Type ("List.list", [Type ("*", [U, _])]), _])) $ pi2 $ t)) =>
    72         let
    73             val ({bounds = (_, xs), ...}, _) = rep_ss ss
    74             val ai = find_index (fn (x, _) => x = a) xs
    75 	    val bi = find_index (fn (x, _) => x = b) xs
    76 	    val tname' = Sign.base_name tname
    77         in
    78             if ai = length xs - i - 1 andalso 
    79                bi = length xs - i - 2 andalso 
    80                T = U andalso pi1 <> pi2 then
    81                 SOME (Drule.instantiate'
    82 	              [SOME (ctyp_of sg (fastype_of t))]
    83 		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
    84 		      (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
    85 	               PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose)))
    86             else NONE
    87         end
    88        | _ => NONE);
    89 
    90       fun perm_compose i =
    91 	Simplifier.simproc (the_context()) "perm_compose" 
    92 	["nominal.perm [(a, b)] (nominal.perm pi t)"] (perm_compose_simproc i);
    93          
    94       (* these lemmas are created dynamically according to the atom types *) 
    95       val perm_swap     = dynamic_thms ss "perm_swap"
    96       val perm_fresh    = dynamic_thms ss "perm_fresh_fresh"
    97       val perm_bij      = dynamic_thms ss "perm_bij"
    98       val perm_pi_simp  = dynamic_thms ss "perm_pi_simp"
    99       val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp)
   100     in
   101       ("general simplification step", 
   102         FIRST [rtac conjI i, 
   103                SUBGOAL (fn (g, i) => asm_full_simp_tac 
   104                  (ss' addsimprocs [perm_eval,perm_compose (length (Logic.strip_params g)-2)]) i) i])
   105     end;
   106 
   107 (* applies the perm_compose rule - this rule would loop in the simplifier     *)
   108 (* in case there are more atom-types we have to check every possible instance *)
   109 (* of perm_compose                                                            *)
   110 fun apply_perm_compose_tac ss i = 
   111     let
   112 	val perm_compose = dynamic_thms ss "perm_compose"; 
   113         val tacs = map (fn thm => (rtac (thm RS trans) i)) perm_compose
   114     in
   115 	("analysing permutation compositions on the lhs",FIRST (tacs))
   116     end
   117 
   118 (* applying Stefan's smart congruence tac *)
   119 fun apply_cong_tac i = 
   120     ("application of congruence",
   121      (fn st => DatatypeAux.cong_tac  i st handle Subscript => no_tac st));
   122 
   123 (* unfolds the definition of permutations applied to functions *)
   124 fun unfold_perm_fun_def_tac i = 
   125     let
   126 	val perm_fun_def = thm "nominal.perm_fun_def"
   127     in
   128 	("unfolding of permutations on functions", 
   129 	 simp_tac (HOL_basic_ss addsimps [perm_fun_def]) i)
   130     end
   131 
   132 (* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
   133 fun expand_fun_eq_tac i =    
   134     ("extensionality expansion of functions",
   135     EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) i, REPEAT_DETERM (rtac allI i)]);
   136 
   137 (* debugging *)
   138 fun DEBUG_tac (msg,tac) = 
   139     CHANGED (EVERY [tac, print_tac ("after "^msg)]); 
   140 fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
   141 
   142 (* Main Tactic *)
   143 
   144 fun perm_simp_tac tactical ss i = 
   145     DETERM (tactical (perm_eval_tac ss i));
   146 
   147 
   148 (* perm_simp_tac plus additional tactics to decide            *)
   149 (* support problems                                           *)
   150 (* the "recursion"-depth is set to 10 - this seems sufficient *)
   151 fun perm_supports_tac tactical ss n = 
   152     if n=0 then K all_tac
   153     else DETERM o 
   154          (FIRST'[fn i => tactical (perm_eval_tac ss i),
   155                  (*fn i => tactical (apply_perm_compose_tac ss i),*)
   156 		 fn i => tactical (apply_cong_tac i), 
   157                  fn i => tactical (unfold_perm_fun_def_tac i),
   158 		 fn i => tactical (expand_fun_eq_tac i)]
   159          THEN_ALL_NEW (TRY o (perm_supports_tac tactical ss (n-1))));
   160 
   161 (* tactic that first unfolds the support definition          *)
   162 (* and strips off the intros, then applies perm_supports_tac *)
   163 fun supports_tac tactical ss i =
   164   let 
   165       val supports_def = thm "nominal.op supports_def";
   166       val fresh_def    = thm "nominal.fresh_def";
   167       val fresh_prod   = thm "nominal.fresh_prod";
   168       val simps        = [supports_def,symmetric fresh_def,fresh_prod]
   169   in
   170       EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i),
   171              tactical ("stripping of foralls  ", REPEAT_DETERM (rtac allI i)),
   172              tactical ("geting rid of the imps", rtac impI i),
   173              tactical ("eliminating conjuncts ", REPEAT_DETERM (etac  conjE i)),
   174              tactical ("applying perm_simp    ", perm_supports_tac tactical ss 10 i)]
   175   end;
   176 
   177 
   178 (* tactic that guesses the finite-support of a goal *)
   179 
   180 fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j - i) ins vs
   181   | collect_vars i (v as Free _) vs = v ins vs
   182   | collect_vars i (v as Var _) vs = v ins vs
   183   | collect_vars i (Const _) vs = vs
   184   | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
   185   | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
   186 
   187 val supports_rule = thm "supports_finite";
   188 
   189 fun finite_guess_tac tactical ss i st =
   190     let val goal = List.nth(cprems_of st, i-1)
   191     in
   192       case Logic.strip_assums_concl (term_of goal) of
   193           _ $ (Const ("op :", _) $ (Const ("nominal.supp", T) $ x) $
   194             Const ("Finite_Set.Finites", _)) =>
   195           let
   196             val cert = Thm.cterm_of (sign_of_thm st);
   197             val ps = Logic.strip_params (term_of goal);
   198             val Ts = rev (map snd ps);
   199             val vs = collect_vars 0 x [];
   200             val s = foldr (fn (v, s) =>
   201                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
   202               HOLogic.unit vs;
   203             val s' = list_abs (ps,
   204               Const ("nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
   205             val supports_rule' = Thm.lift_rule goal supports_rule;
   206             val _ $ (_ $ S $ _) =
   207               Logic.strip_assums_concl (hd (prems_of supports_rule'));
   208             val supports_rule'' = Drule.cterm_instantiate
   209               [(cert (head_of S), cert s')] supports_rule'
   210           in
   211             (tactical ("guessing of the right supports-set",
   212                       EVERY [compose_tac (false, supports_rule'', 2) i,
   213                              asm_full_simp_tac ss (i+1),
   214                              supports_tac tactical ss i])) st
   215           end
   216         | _ => Seq.empty
   217     end
   218     handle Subscript => Seq.empty
   219 
   220 in             
   221 
   222 
   223 fun simp_meth_setup tac =
   224   Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
   225   (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
   226 
   227 val perm_eq_meth         = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
   228 val perm_eq_meth_debug   = simp_meth_setup (perm_simp_tac DEBUG_tac);
   229 val supports_meth        = simp_meth_setup (supports_tac NO_DEBUG_tac);
   230 val supports_meth_debug  = simp_meth_setup (supports_tac DEBUG_tac);
   231 val finite_gs_meth       = simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
   232 val finite_gs_meth_debug = simp_meth_setup (finite_guess_tac DEBUG_tac);
   233 
   234 end
   235 
   236 
   237