src/HOL/Nominal/nominal_permeq.ML
author urbanc
Tue Jul 04 17:26:02 2006 +0200 (2006-07-04)
changeset 19993 e0a5783d708f
parent 19987 b97607d4d9a5
child 20289 ba7a7c56bed5
permissions -rw-r--r--
added simplification rules to the fresh_guess tactic
     1 (*  Title:      HOL/Nominal/nominal_permeq.ML
     2     ID:         $Id$
     3     Author:     Christian Urban, TU Muenchen
     4 
     5 Methods for simplifying permutations and
     6 for analysing equations involving permutations.
     7 *)
     8 
     9 signature NOMINAL_PERMEQ =
    10 sig
    11   val perm_simp_tac : simpset -> int -> tactic
    12   val perm_full_simp_tac : simpset -> int -> tactic
    13   val supports_tac : simpset -> int -> tactic
    14   val finite_guess_tac : simpset -> int -> tactic
    15   val fresh_guess_tac : simpset -> int -> tactic
    16 
    17   val perm_eq_meth : Method.src -> ProofContext.context -> Method.method
    18   val perm_eq_meth_debug : Method.src -> ProofContext.context -> Method.method
    19   val perm_full_eq_meth : Method.src -> ProofContext.context -> Method.method
    20   val perm_full_eq_meth_debug : Method.src -> ProofContext.context -> Method.method
    21   val supports_meth : Method.src -> ProofContext.context -> Method.method
    22   val supports_meth_debug : Method.src -> ProofContext.context -> Method.method
    23   val finite_gs_meth : Method.src -> ProofContext.context -> Method.method
    24   val finite_gs_meth_debug : Method.src -> ProofContext.context -> Method.method
    25   val fresh_gs_meth : Method.src -> ProofContext.context -> Method.method
    26   val fresh_gs_meth_debug : Method.src -> ProofContext.context -> Method.method
    27 end
    28 
    29 structure NominalPermeq : NOMINAL_PERMEQ =
    30 struct
    31 
    32 (* pulls out dynamically a thm via the proof state *)
    33 fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
    34 fun dynamic_thm st name = PureThy.get_thm (theory_of_thm st) (Name name);
    35 
    36 (* a tactic simplyfying permutations *)
    37 val perm_fun_def = thm "Nominal.perm_fun_def"
    38 val perm_eq_app = thm "Nominal.pt_fun_app_eq"
    39 
    40 fun perm_eval_tac ss i = ("general simplification step", fn st =>
    41     let
    42         fun perm_eval_simproc sg ss redex =
    43         let 
    44 	   (* the "application" case below is only applicable when the head   *)
    45            (* of f is not a constant  or when it is a permuattion with two or *) 
    46            (* more arguments                                                  *)
    47            fun applicable t = 
    48 	       (case (strip_comb t) of
    49 		  (Const ("Nominal.perm",_),ts) => (length ts) >= 2
    50 		| (Const _,_) => false
    51 		| _ => true)
    52 
    53 	in
    54         (case redex of 
    55         (* case pi o (f x) == (pi o f) (pi o x)          *)
    56         (* special treatment according to the head of f  *)
    57         (Const("Nominal.perm",
    58           Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
    59 	   (case (applicable f) of
    60                 false => NONE  
    61               | _ => 
    62 		let
    63 		    val name = Sign.base_name n
    64 		    val at_inst     = dynamic_thm st ("at_"^name^"_inst")
    65 		    val pt_inst     = dynamic_thm st ("pt_"^name^"_inst")  
    66 		in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end)
    67 
    68         (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
    69         | (Const("Nominal.perm",_) $ pi $ (Abs _)) => SOME (perm_fun_def)
    70 
    71         (* no redex otherwise *) 
    72         | _ => NONE) end
    73 
    74 	val perm_eval =
    75 	    Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 
    76 	    ["Nominal.perm pi x"] perm_eval_simproc;
    77 
    78       (* these lemmas are created dynamically according to the atom types *) 
    79       val perm_swap        = dynamic_thms st "perm_swap"
    80       val perm_fresh       = dynamic_thms st "perm_fresh_fresh"
    81       val perm_bij         = dynamic_thms st "perm_bij"
    82       val perm_pi_simp     = dynamic_thms st "perm_pi_simp"
    83       val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp)
    84     in
    85       asm_full_simp_tac (ss' addsimprocs [perm_eval]) i st
    86     end);
    87 
    88 (* applies the perm_compose rule such that                             *)
    89 (*                                                                     *)
    90 (*   pi o (pi' o lhs) = rhs                                            *)
    91 (*                                                                     *)
    92 (* is transformed to                                                   *) 
    93 (*                                                                     *)
    94 (*  (pi o pi') o (pi' o lhs) = rhs                                     *)
    95 (*                                                                     *)
    96 (* this rule would loop in the simplifier, so some trick is used with  *)
    97 (* generating perm_aux'es for the outermost permutation and then un-   *)
    98 (* folding the definition                                              *)
    99 val pt_perm_compose_aux = thm "pt_perm_compose_aux";
   100 val cp1_aux             = thm "cp1_aux";
   101 val perm_aux_fold       = thm "perm_aux_fold"; 
   102 
   103 fun perm_compose_tac ss i = 
   104     let
   105 	fun perm_compose_simproc sg ss redex =
   106 	(case redex of
   107            (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
   108              [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
   109                Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
   110                 pi2 $ t)) =>
   111         let
   112 	    val tname' = Sign.base_name tname
   113             val uname' = Sign.base_name uname
   114         in
   115             if pi1 <> pi2 then  (* only apply the composition rule in this case *)
   116                if T = U then    
   117                 SOME (Drule.instantiate'
   118 	              [SOME (ctyp_of sg (fastype_of t))]
   119 		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
   120 		      (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
   121 	               PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose_aux)))
   122                else
   123                 SOME (Drule.instantiate'
   124 	              [SOME (ctyp_of sg (fastype_of t))]
   125 		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
   126 		      (mk_meta_eq (PureThy.get_thm sg (Name ("cp_"^tname'^"_"^uname'^"_inst")) RS 
   127                        cp1_aux)))
   128             else NONE
   129         end
   130        | _ => NONE);
   131 	  
   132       val perm_compose  =
   133 	Simplifier.simproc (the_context()) "perm_compose" 
   134 	["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc;
   135 
   136       val ss' = Simplifier.theory_context (the_context ()) empty_ss	  
   137 
   138     in
   139 	("analysing permutation compositions on the lhs",
   140          EVERY [rtac trans i,
   141                 asm_full_simp_tac (ss' addsimprocs [perm_compose]) i,
   142                 asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i])
   143     end
   144 
   145 (* applying Stefan's smart congruence tac *)
   146 fun apply_cong_tac i = 
   147     ("application of congruence",
   148      (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
   149 
   150 (* unfolds the definition of permutations     *)
   151 (* applied to functions such that             *)
   152 (*                                            *)
   153 (*   pi o f = rhs                             *)  
   154 (*                                            *)
   155 (* is transformed to                          *)
   156 (*                                            *)
   157 (*   %x. pi o (f ((rev pi) o x)) = rhs        *)
   158 fun unfold_perm_fun_def_tac i = 
   159     let
   160 	val perm_fun_def = thm "Nominal.perm_fun_def"
   161     in
   162 	("unfolding of permutations on functions", 
   163          rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
   164     end
   165 
   166 (* applies the ext-rule such that      *)
   167 (*                                     *)
   168 (*    f = g    goes to /\x. f x = g x  *)
   169 fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
   170 
   171 (* FIXME FIXME FIXME *)
   172 (* should be able to analyse pi o fresh_fun () = fresh_fun instances *) 
   173 fun fresh_fun_eqvt_tac i =
   174     let
   175 	val fresh_fun_equiv = thm "Nominal.fresh_fun_equiv_ineq"
   176     in
   177 	("fresh_fun equivariance", rtac (fresh_fun_equiv RS trans) i)
   178     end		       
   179 		       
   180 (* debugging *)
   181 fun DEBUG_tac (msg,tac) = 
   182     CHANGED (EVERY [tac, print_tac ("after "^msg)]); 
   183 fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
   184 
   185 (* Main Tactics *)
   186 fun perm_simp_tac tactical ss i = 
   187     DETERM (tactical (perm_eval_tac ss i));
   188 
   189 (* perm_full_simp_tac is perm_simp_tac plus additional tactics    *)
   190 (* to decide equation that come from support problems             *)
   191 (* since it contains looping rules the "recursion" - depth is set *)
   192 (* to 10 - this seems to be sufficient in most cases              *)
   193 fun perm_full_simp_tac tactical ss =
   194   let fun perm_full_simp_tac_aux tactical ss n = 
   195 	  if n=0 then K all_tac
   196 	  else DETERM o 
   197 	       (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
   198                        fn i => tactical (perm_eval_tac ss i),
   199 		       fn i => tactical (perm_compose_tac ss i),
   200 		       fn i => tactical (apply_cong_tac i), 
   201                        fn i => tactical (unfold_perm_fun_def_tac i),
   202                        fn i => tactical (ext_fun_tac i), 
   203                        fn i => tactical (fresh_fun_eqvt_tac i)]
   204 		      THEN_ALL_NEW (TRY o (perm_full_simp_tac_aux tactical ss (n-1))))
   205   in perm_full_simp_tac_aux tactical ss 10 end;
   206 
   207 (* tactic that first unfolds the support definition           *)
   208 (* and strips off the intros, then applies perm_full_simp_tac *)
   209 fun supports_tac tactical ss i =
   210   let 
   211       val supports_def = thm "Nominal.op supports_def";
   212       val fresh_def    = thm "Nominal.fresh_def";
   213       val fresh_prod   = thm "Nominal.fresh_prod";
   214       val simps        = [supports_def,symmetric fresh_def,fresh_prod]
   215   in
   216       EVERY [tactical ("unfolding of supports   ", simp_tac (HOL_basic_ss addsimps simps) i),
   217              tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
   218              tactical ("geting rid of the imps  ", rtac impI i),
   219              tactical ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
   220              tactical ("applying perm_full_simp ", perm_full_simp_tac tactical ss i
   221                                                    (*perm_simp_tac tactical ss i*))]
   222   end;
   223 
   224 
   225 (* tactic that guesses the finite-support of a goal       *)
   226 (* it collects all free variables and tries to show       *)
   227 (* that the support of these free variables (op supports) *)
   228 (* the goal                                               *)
   229 fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j - i) ins vs
   230   | collect_vars i (v as Free _) vs = v ins vs
   231   | collect_vars i (v as Var _) vs = v ins vs
   232   | collect_vars i (Const _) vs = vs
   233   | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
   234   | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
   235 
   236 val supports_rule = thm "supports_finite";
   237 
   238 val supp_prod = thm "supp_prod";
   239 val supp_unit = thm "supp_unit";
   240 
   241 fun finite_guess_tac tactical ss i st =
   242     let val goal = List.nth(cprems_of st, i-1)
   243     in
   244       case Logic.strip_assums_concl (term_of goal) of
   245           _ $ (Const ("op :", _) $ (Const ("Nominal.supp", T) $ x) $
   246             Const ("Finite_Set.Finites", _)) =>
   247           let
   248             val cert = Thm.cterm_of (sign_of_thm st);
   249             val ps = Logic.strip_params (term_of goal);
   250             val Ts = rev (map snd ps);
   251             val vs = collect_vars 0 x [];
   252             val s = foldr (fn (v, s) =>
   253                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
   254               HOLogic.unit vs;
   255             val s' = list_abs (ps,
   256               Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
   257             val supports_rule' = Thm.lift_rule goal supports_rule;
   258             val _ $ (_ $ S $ _) =
   259               Logic.strip_assums_concl (hd (prems_of supports_rule'));
   260             val supports_rule'' = Drule.cterm_instantiate
   261               [(cert (head_of S), cert s')] supports_rule'
   262             val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites.emptyI]
   263           in
   264             (tactical ("guessing of the right supports-set",
   265                       EVERY [compose_tac (false, supports_rule'', 2) i,
   266                              asm_full_simp_tac ss' (i+1),
   267                              supports_tac tactical ss i])) st
   268           end
   269         | _ => Seq.empty
   270     end
   271     handle Subscript => Seq.empty
   272 
   273 val supports_fresh_rule = thm "supports_fresh";
   274 val fresh_def           = thm "Nominal.fresh_def";
   275 val fresh_prod          = thm "Nominal.fresh_prod";
   276 val fresh_unit          = thm "Nominal.fresh_unit";
   277 
   278 fun fresh_guess_tac tactical ss i st =
   279     let 
   280 	val goal = List.nth(cprems_of st, i-1)
   281     in
   282       case Logic.strip_assums_concl (term_of goal) of
   283           _ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => 
   284           let
   285             val cert = Thm.cterm_of (sign_of_thm st);
   286             val ps = Logic.strip_params (term_of goal);
   287             val Ts = rev (map snd ps);
   288             val vs = collect_vars 0 t [];
   289             val s = foldr (fn (v, s) =>
   290                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
   291               HOLogic.unit vs;
   292             val s' = list_abs (ps,
   293               Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
   294             val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
   295             val _ $ (_ $ S $ _) =
   296               Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
   297             val supports_fresh_rule'' = Drule.cterm_instantiate
   298               [(cert (head_of S), cert s')] supports_fresh_rule'
   299 	    val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit]
   300             val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites.emptyI]
   301             (* FIXME sometimes these rewrite rules are already in the ss, *)
   302             (* which produces a warning                                   *)
   303           in
   304             (tactical ("guessing of the right set that supports the goal",
   305                       EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
   306                              asm_full_simp_tac ss1 (i+2),
   307                              asm_full_simp_tac ss2 (i+1), 
   308                              supports_tac tactical ss i])) st
   309           end
   310         | _ => Seq.empty
   311     end
   312     handle Subscript => Seq.empty
   313 
   314 fun simp_meth_setup tac =
   315   Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
   316   (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
   317 
   318 val perm_eq_meth            = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
   319 val perm_eq_meth_debug      = simp_meth_setup (perm_simp_tac DEBUG_tac);
   320 val perm_full_eq_meth       = simp_meth_setup (perm_full_simp_tac NO_DEBUG_tac);
   321 val perm_full_eq_meth_debug = simp_meth_setup (perm_full_simp_tac DEBUG_tac);
   322 val supports_meth           = simp_meth_setup (supports_tac NO_DEBUG_tac);
   323 val supports_meth_debug     = simp_meth_setup (supports_tac DEBUG_tac);
   324 val finite_gs_meth          = simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
   325 val finite_gs_meth_debug    = simp_meth_setup (finite_guess_tac DEBUG_tac);
   326 val fresh_gs_meth           = simp_meth_setup (fresh_guess_tac NO_DEBUG_tac);
   327 val fresh_gs_meth_debug     = simp_meth_setup (fresh_guess_tac DEBUG_tac);
   328 
   329 (* FIXME: get rid of "debug" versions? *)
   330 val perm_simp_tac = perm_simp_tac NO_DEBUG_tac;
   331 val perm_full_simp_tac = perm_full_simp_tac NO_DEBUG_tac;
   332 val supports_tac = supports_tac NO_DEBUG_tac;
   333 val finite_guess_tac = finite_guess_tac NO_DEBUG_tac;
   334 val fresh_guess_tac = fresh_guess_tac NO_DEBUG_tac;
   335 
   336 end