src/HOL/Nominal/nominal_permeq.ML
author urbanc
Sat Apr 07 11:36:35 2007 +0200 (2007-04-07)
changeset 22610 c8b5133045f3
parent 22609 40ade470e319
child 22656 13302b2d0948
permissions -rw-r--r--
tuned slightly the previous commit
     1 (*  Title:      HOL/Nominal/nominal_permeq.ML
     2     ID:         $Id$
     3     Authors:    Christian Urban, Julien Narboux, TU Muenchen
     4 
     5 Methods for simplifying permutations and
     6 for analysing equations involving permutations.
     7 *)
     8 
     9 (*
    10 FIXMES:
    11 
    12  - allow the user to give an explicit set S in the
    13    fresh_guess tactic which is then verified
    14 
    15  - the perm_compose tactic does not do an "outermost
    16    rewriting" and can therefore not deal with goals
    17    like
    18 
    19       [(a,b)] o pi1 o pi2 = ....
    20 
    21    rather it tries to permute pi1 over pi2, which 
    22    results in a failure when used with the 
    23    perm_(full)_simp tactics
    24 
    25 *)
    26 
    27 
    28 signature NOMINAL_PERMEQ =
    29 sig
    30   val perm_simp_tac : simpset -> int -> tactic
    31   val perm_full_simp_tac : simpset -> int -> tactic
    32   val supports_tac : simpset -> int -> tactic
    33   val finite_guess_tac : simpset -> int -> tactic
    34   val fresh_guess_tac : simpset -> int -> tactic
    35 
    36   val perm_simp_meth : Method.src -> Proof.context -> Proof.method
    37   val perm_simp_meth_debug : Method.src -> Proof.context -> Proof.method
    38   val perm_full_simp_meth : Method.src -> Proof.context -> Proof.method
    39   val perm_full_simp_meth_debug : Method.src -> Proof.context -> Proof.method
    40   val supports_meth : Method.src -> Proof.context -> Proof.method
    41   val supports_meth_debug : Method.src -> Proof.context -> Proof.method
    42   val finite_guess_meth : Method.src -> Proof.context -> Proof.method
    43   val finite_guess_meth_debug : Method.src -> Proof.context -> Proof.method
    44   val fresh_guess_meth : Method.src -> Proof.context -> Proof.method
    45   val fresh_guess_meth_debug : Method.src -> Proof.context -> Proof.method
    46 end
    47 
    48 structure NominalPermeq : NOMINAL_PERMEQ =
    49 struct
    50 
    51 (* some lemmas needed below *)
    52 val finite_emptyI = thm "finite.emptyI";
    53 val finite_Un     = thm "finite_Un";
    54 val conj_absorb   = thm "conj_absorb";
    55 val not_false     = thm "not_False_eq_True"
    56 val perm_fun_def  = thm "Nominal.perm_fun_def"
    57 val perm_eq_app   = thm "Nominal.pt_fun_app_eq"
    58 val supports_def  = thm "Nominal.op supports_def";
    59 val fresh_def     = thm "Nominal.fresh_def";
    60 val fresh_prod    = thm "Nominal.fresh_prod";
    61 val fresh_unit    = thm "Nominal.fresh_unit";
    62 val supports_rule = thm "supports_finite";
    63 val supp_prod     = thm "supp_prod";
    64 val supp_unit     = thm "supp_unit";
    65 val pt_perm_compose_aux = thm "pt_perm_compose_aux";
    66 val cp1_aux             = thm "cp1_aux";
    67 val perm_aux_fold       = thm "perm_aux_fold"; 
    68 val supports_fresh_rule = thm "supports_fresh";
    69 
    70 (* pulls out dynamically a thm via the proof state *)
    71 fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
    72 fun dynamic_thm  st name = PureThy.get_thm  (theory_of_thm st) (Name name);
    73 
    74 
    75 (* needed in the process of fully simplifying permutations *)
    76 val strong_congs = [thm "if_cong"]
    77 (* needed to avoid warnings about overwritten congs *)
    78 val weak_congs   = [thm "if_weak_cong"]
    79 
    80 (* a tactical which fails if the tactic taken as an argument generates does not solve the sub goal i *)
    81 
    82 fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac);
    83 
    84 (* debugging *)
    85 fun DEBUG_tac (msg,tac) = 
    86     CHANGED (EVERY [print_tac ("before "^msg), tac, print_tac ("after "^msg)]); 
    87 fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
    88 
    89 
    90 (* simproc that deals with instances of permutations in front *)
    91 (* of applications; just adding this rule to the simplifier   *)
    92 (* would loop; it also needs careful tuning with the simproc  *)
    93 (* for functions to avoid further possibilities for looping   *)
    94 fun perm_simproc_app st sg ss redex =
    95   let 
    96     (* the "application" case is only applicable when the head of f is not a *)
    97     (* constant or when (f x) is a permuation with two or more arguments     *)
    98     fun applicable_app t = 
    99           (case (strip_comb t) of
   100 	      (Const ("Nominal.perm",_),ts) => (length ts) >= 2
   101             | (Const _,_) => false
   102             | _ => true)
   103   in
   104     case redex of 
   105         (* case pi o (f x) == (pi o f) (pi o x)          *)
   106         (Const("Nominal.perm",
   107           Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
   108             (if (applicable_app f) then
   109               let
   110                 val name = Sign.base_name n
   111                 val at_inst     = dynamic_thm st ("at_"^name^"_inst")
   112                 val pt_inst     = dynamic_thm st ("pt_"^name^"_inst")  
   113               in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
   114             else NONE)
   115       | _ => NONE
   116   end
   117 
   118 (* a simproc that deals with instances in front of functions  *)
   119 fun perm_simproc_fun st sg ss redex = 
   120    let 
   121      fun applicable_fun t =
   122        (case (strip_comb t) of
   123           (Abs _ ,[]) => true
   124 	| (Const ("Nominal.perm",_),_) => false
   125         | (Const _, _) => true
   126 	| _ => false)
   127    in
   128      case redex of 
   129        (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
   130        (Const("Nominal.perm",_) $ pi $ f)  => 
   131           (if (applicable_fun f) then SOME (perm_fun_def) else NONE)
   132       | _ => NONE
   133    end
   134 
   135 (* function for simplyfying permutations *)
   136 fun perm_simp_gen dyn_thms f ss i = 
   137     ("general simplification of permutations", fn st =>
   138     let
   139 
   140        val perm_sp_fun = Simplifier.simproc (theory_of_thm st) "perm_simproc_fun" 
   141 	                 ["Nominal.perm pi x"] (perm_simproc_fun st);
   142 
   143        val perm_sp_app = Simplifier.simproc (theory_of_thm st) "perm_simproc_app" 
   144 	                 ["Nominal.perm pi x"] (perm_simproc_app st);
   145 
   146        val ss' = ss addsimps ((List.concat (map (dynamic_thms st) dyn_thms))@(f st))
   147                     delcongs weak_congs
   148                     addcongs strong_congs
   149                     addsimprocs [perm_sp_fun, perm_sp_app]
   150     in
   151       asm_full_simp_tac ss' i st
   152     end);
   153 
   154 (* general simplification of permutations and permutation that arose from eqvt-problems *)
   155 val perm_simp = 
   156     let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
   157     in 
   158 	perm_simp_gen simps (fn st => [])
   159     end;
   160 
   161 val eqvt_simp = 
   162     let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
   163 	fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st);
   164     in 
   165 	perm_simp_gen simps eqvts_thms
   166     end;
   167 
   168 (* FIXME removes the name lookup for these theorems use an ml value instead *)
   169 
   170 (* main simplification tactics for permutations *)
   171 (* FIXME: perm_simp_tac should simplify more permutations *)
   172 fun perm_simp_tac tactical ss i = DETERM (tactical (perm_simp ss i));
   173 fun eqvt_simp_tac tactical ss i = DETERM (tactical (eqvt_simp ss i)); 
   174 
   175 
   176 (* applies the perm_compose rule such that                             *)
   177 (*   pi o (pi' o lhs) = rhs                                            *)
   178 (* is transformed to                                                   *) 
   179 (*  (pi o pi') o (pi' o lhs) = rhs                                     *)
   180 (*                                                                     *)
   181 (* this rule would loop in the simplifier, so some trick is used with  *)
   182 (* generating perm_aux'es for the outermost permutation and then un-   *)
   183 (* folding the definition                                              *)
   184 fun perm_compose_tac ss i = 
   185     let
   186 	fun perm_compose_simproc sg ss redex =
   187 	(case redex of
   188            (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
   189              [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
   190                Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
   191                 pi2 $ t)) =>
   192         let
   193 	    val tname' = Sign.base_name tname
   194             val uname' = Sign.base_name uname
   195         in
   196             if pi1 <> pi2 then  (* only apply the composition rule in this case *)
   197                if T = U then    
   198                 SOME (Drule.instantiate'
   199 	              [SOME (ctyp_of sg (fastype_of t))]
   200 		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
   201 		      (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
   202 	               PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose_aux)))
   203                else
   204                 SOME (Drule.instantiate'
   205 	              [SOME (ctyp_of sg (fastype_of t))]
   206 		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
   207 		      (mk_meta_eq (PureThy.get_thm sg (Name ("cp_"^tname'^"_"^uname'^"_inst")) RS 
   208                        cp1_aux)))
   209             else NONE
   210         end
   211        | _ => NONE);
   212 	  
   213       val perm_compose  =
   214 	Simplifier.simproc (the_context()) "perm_compose" 
   215 	["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc;
   216 
   217       val ss' = Simplifier.theory_context (the_context ()) empty_ss (* FIXME: get rid of the_context *)	  
   218 
   219     in
   220 	("analysing permutation compositions on the lhs",
   221          EVERY [rtac trans i,
   222                 asm_full_simp_tac (ss' addsimprocs [perm_compose]) i,
   223                 asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i])
   224     end
   225 
   226 
   227 (* applying Stefan's smart congruence tac *)
   228 fun apply_cong_tac i = 
   229     ("application of congruence",
   230      (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
   231 
   232 
   233 (* unfolds the definition of permutations     *)
   234 (* applied to functions such that             *)
   235 (*     pi o f = rhs                           *)  
   236 (* is transformed to                          *)
   237 (*     %x. pi o (f ((rev pi) o x)) = rhs      *)
   238 fun unfold_perm_fun_def_tac i = 
   239     let
   240 	val perm_fun_def = thm "Nominal.perm_fun_def"
   241     in
   242 	("unfolding of permutations on functions", 
   243          rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
   244     end
   245 
   246 (* applies the ext-rule such that      *)
   247 (*                                     *)
   248 (*    f = g   goes to  /\x. f x = g x  *)
   249 fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
   250 
   251 
   252 (* perm_full_simp_tac is perm_simp plus additional tactics        *)
   253 (* to decide equation that come from support problems             *)
   254 (* since it contains looping rules the "recursion" - depth is set *)
   255 (* to 10 - this seems to be sufficient in most cases              *)
   256 fun perm_full_simp_tac tactical ss =
   257   let fun perm_full_simp_tac_aux tactical ss n = 
   258 	  if n=0 then K all_tac
   259 	  else DETERM o 
   260 	       (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
   261                        fn i => tactical (perm_simp ss i),
   262 		       fn i => tactical (perm_compose_tac ss i),
   263 		       fn i => tactical (apply_cong_tac i), 
   264                        fn i => tactical (unfold_perm_fun_def_tac i),
   265                        fn i => tactical (ext_fun_tac i)]
   266 		      THEN_ALL_NEW (TRY o (perm_full_simp_tac_aux tactical ss (n-1))))
   267   in perm_full_simp_tac_aux tactical ss 10 end;
   268 
   269 
   270 (* tactic that tries to solve "supports"-goals; first it *)
   271 (* unfolds the support definition and strips off the     *)
   272 (* intros, then applies eqvt_simp_tac                    *)
   273 fun supports_tac tactical ss i =
   274   let 
   275      val simps        = [supports_def,symmetric fresh_def,fresh_prod]
   276   in
   277       EVERY [tactical ("unfolding of supports   ", simp_tac (HOL_basic_ss addsimps simps) i),
   278              tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
   279              tactical ("geting rid of the imps  ", rtac impI i),
   280              tactical ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
   281              tactical ("applying eqvt_simp      ", eqvt_simp_tac tactical ss i )]
   282   end;
   283 
   284 
   285 (* tactic that guesses the finite-support of a goal        *)
   286 (* it first collects all free variables and tries to show  *)
   287 (* that the support of these free variables (op supports)  *)
   288 (* the goal                                                *)
   289 fun collect_vars i (Bound j) vs = if j < i then vs else insert (op =) (Bound (j - i)) vs
   290   | collect_vars i (v as Free _) vs = insert (op =) v vs
   291   | collect_vars i (v as Var _) vs = insert (op =) v vs
   292   | collect_vars i (Const _) vs = vs
   293   | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
   294   | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
   295 
   296 fun finite_guess_tac tactical ss i st =
   297     let val goal = List.nth(cprems_of st, i-1)
   298     in
   299       case Logic.strip_assums_concl (term_of goal) of
   300           _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
   301           let
   302             val cert = Thm.cterm_of (Thm.theory_of_thm st);
   303             val ps = Logic.strip_params (term_of goal);
   304             val Ts = rev (map snd ps);
   305             val vs = collect_vars 0 x [];
   306             val s = Library.foldr (fn (v, s) =>
   307                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
   308               (vs, HOLogic.unit);
   309             val s' = list_abs (ps,
   310               Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
   311             val supports_rule' = Thm.lift_rule goal supports_rule;
   312             val _ $ (_ $ S $ _) =
   313               Logic.strip_assums_concl (hd (prems_of supports_rule'));
   314             val supports_rule'' = Drule.cterm_instantiate
   315               [(cert (head_of S), cert s')] supports_rule'
   316             val fin_supp = dynamic_thms st ("fin_supp")
   317             val ss' = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
   318           in
   319             (tactical ("guessing of the right supports-set",
   320                       EVERY [compose_tac (false, supports_rule'', 2) i,
   321                              asm_full_simp_tac ss' (i+1),
   322                              supports_tac tactical ss i])) st
   323           end
   324         | _ => Seq.empty
   325     end
   326     handle Subscript => Seq.empty
   327 
   328 
   329 (* tactic that guesses whether an atom is fresh for an expression  *)
   330 (* it first collects all free variables and tries to show that the *) 
   331 (* support of these free variables (op supports) the goal          *)
   332 fun fresh_guess_tac tactical ss i st =
   333     let 
   334 	val goal = List.nth(cprems_of st, i-1)
   335         val fin_supp = dynamic_thms st ("fin_supp")
   336         val fresh_atm = dynamic_thms st ("fresh_atm")
   337 	val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
   338         val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
   339     in
   340       case Logic.strip_assums_concl (term_of goal) of
   341           _ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => 
   342           let
   343             val cert = Thm.cterm_of (Thm.theory_of_thm st);
   344             val ps = Logic.strip_params (term_of goal);
   345             val Ts = rev (map snd ps);
   346             val vs = collect_vars 0 t [];
   347             val s = Library.foldr (fn (v, s) =>
   348                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
   349               (vs, HOLogic.unit);
   350             val s' = list_abs (ps,
   351               Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
   352             val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
   353             val _ $ (_ $ S $ _) =
   354               Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
   355             val supports_fresh_rule'' = Drule.cterm_instantiate
   356               [(cert (head_of S), cert s')] supports_fresh_rule'
   357           in
   358             (tactical ("guessing of the right set that supports the goal", 
   359                       (EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
   360                              asm_full_simp_tac ss1 (i+2),
   361                              asm_full_simp_tac ss2 (i+1), 
   362                              supports_tac tactical ss i]))) st
   363           end
   364           (* when a term-constructor contains more than one binder, it is useful    *) 
   365           (* in nominal_primrecs to try whether the goal can be solved by an hammer *)
   366         | _ => (tactical ("if it is not of the form _\<sharp>_, then try the simplifier",   
   367                           (asm_full_simp_tac (HOL_ss addsimps [fresh_prod]@fresh_atm) i))) st
   368     end
   369     handle Subscript => Seq.empty;
   370 
   371 (* setup so that the simpset is used which is active at the moment when the tactic is called *)
   372 fun local_simp_meth_setup tac =
   373   Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
   374   (Method.SIMPLE_METHOD' o tac o local_simpset_of) ;
   375 
   376 (* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
   377 
   378 fun basic_simp_meth_setup tac =
   379   Method.sectioned_args 
   380    (fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l)))
   381    (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
   382    (fn _ => Method.SIMPLE_METHOD' o (fn ss => SOLVEI (tac ss)) o local_simpset_of);
   383 
   384 
   385 val perm_simp_meth            = local_simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
   386 val perm_simp_meth_debug      = local_simp_meth_setup (perm_simp_tac DEBUG_tac);
   387 val perm_full_simp_meth       = local_simp_meth_setup (perm_full_simp_tac NO_DEBUG_tac);
   388 val perm_full_simp_meth_debug = local_simp_meth_setup (perm_full_simp_tac DEBUG_tac);
   389 val supports_meth             = local_simp_meth_setup (supports_tac NO_DEBUG_tac);
   390 val supports_meth_debug       = local_simp_meth_setup (supports_tac DEBUG_tac);
   391 val finite_guess_meth         = basic_simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
   392 val finite_guess_meth_debug   = basic_simp_meth_setup (finite_guess_tac DEBUG_tac);
   393 val fresh_guess_meth          = basic_simp_meth_setup (fresh_guess_tac NO_DEBUG_tac);
   394 val fresh_guess_meth_debug    = basic_simp_meth_setup (fresh_guess_tac DEBUG_tac);
   395 
   396 val perm_simp_tac = perm_simp_tac NO_DEBUG_tac;
   397 val perm_full_simp_tac = perm_full_simp_tac NO_DEBUG_tac;
   398 val supports_tac = supports_tac NO_DEBUG_tac;
   399 val finite_guess_tac = finite_guess_tac NO_DEBUG_tac;
   400 val fresh_guess_tac = fresh_guess_tac NO_DEBUG_tac;
   401 
   402 end