src/HOL/Nominal/nominal_permeq.ML
author urbanc
Thu Apr 27 01:41:30 2006 +0200 (2006-04-27)
changeset 19477 a95176d0f0dd
parent 19350 2e1c7ca05ee0
child 19494 2e909d5309f4
permissions -rw-r--r--
isar-keywords.el
- I am not sure what has changed here

nominal.thy
- includes a number of new lemmas (including freshness
and perm_aux things)

nominal_atoms.ML
- no particular changes here

nominal_permeq.ML
- a new version of the decision procedure using
for permutation composition the constant perm_aux

examples
- various adjustments
berghofe@17870
     1
(* $Id$ *)
berghofe@17870
     2
urbanc@19477
     3
(* METHODS FOR SIMPLIFYING PERMUTATIONS AND     *)
urbanc@19477
     4
(* FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
berghofe@17870
     5
berghofe@17870
     6
local
berghofe@17870
     7
urbanc@18012
     8
(* pulls out dynamically a thm via the simpset *)
urbanc@19477
     9
fun dynamic_thms ss name = ProofContext.get_thms (Simplifier.the_context ss) (Name name);
urbanc@19477
    10
fun dynamic_thm ss name = ProofContext.get_thm (Simplifier.the_context ss) (Name name);
urbanc@18012
    11
urbanc@19477
    12
(* a tactic simplyfying permutations *)
urbanc@19477
    13
val perm_fun_def = thm "nominal.perm_fun_def"
urbanc@19477
    14
val perm_eq_app = thm "nominal.pt_fun_app_eq"
urbanc@19477
    15
urbanc@19139
    16
fun perm_eval_tac ss i =
urbanc@18012
    17
    let
urbanc@19139
    18
        fun perm_eval_simproc sg ss redex =
urbanc@19169
    19
        let 
urbanc@19477
    20
	   (* the "application" case below is only applicable when the head   *)
urbanc@19169
    21
           (* of f is not a constant  or when it is a permuattion with two or *) 
urbanc@19169
    22
           (* more arguments                                                  *)
urbanc@19169
    23
           fun applicable t = 
urbanc@19169
    24
	       (case (strip_comb t) of
urbanc@19169
    25
		  (Const ("nominal.perm",_),ts) => (length ts) >= 2
urbanc@19169
    26
		| (Const _,_) => false
urbanc@19169
    27
		| _ => true)
urbanc@19169
    28
urbanc@19169
    29
	in
urbanc@19139
    30
        (case redex of 
urbanc@19169
    31
        (* case pi o (f x) == (pi o f) (pi o x)          *)
urbanc@19169
    32
        (* special treatment according to the head of f  *)
urbanc@19144
    33
        (Const("nominal.perm",
urbanc@19169
    34
          Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
urbanc@19169
    35
	   (case (applicable f) of
urbanc@19169
    36
                false => NONE  
urbanc@19163
    37
              | _ => 
urbanc@19163
    38
		let
urbanc@19163
    39
		    val name = Sign.base_name n
urbanc@19163
    40
		    val at_inst     = dynamic_thm ss ("at_"^name^"_inst")
urbanc@19163
    41
		    val pt_inst     = dynamic_thm ss ("pt_"^name^"_inst")  
urbanc@19163
    42
		in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end)
urbanc@19139
    43
urbanc@19139
    44
        (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
urbanc@19477
    45
        | (Const("nominal.perm",_) $ pi $ (Abs _)) => SOME (perm_fun_def)
urbanc@19139
    46
urbanc@19139
    47
        (* no redex otherwise *) 
urbanc@19169
    48
        | _ => NONE) end
urbanc@19139
    49
urbanc@19139
    50
	val perm_eval =
urbanc@19139
    51
	    Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 
urbanc@19139
    52
	    ["nominal.perm pi x"] perm_eval_simproc;
urbanc@19139
    53
urbanc@19477
    54
      (* these lemmas are created dynamically according to the atom types *) 
urbanc@19477
    55
      val perm_swap        = dynamic_thms ss "perm_swap"
urbanc@19477
    56
      val perm_fresh       = dynamic_thms ss "perm_fresh_fresh"
urbanc@19477
    57
      val perm_bij         = dynamic_thms ss "perm_bij"
urbanc@19477
    58
      val perm_pi_simp     = dynamic_thms ss "perm_pi_simp"
urbanc@19477
    59
      val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp)
urbanc@19477
    60
    in
urbanc@19477
    61
	("general simplification step", asm_full_simp_tac (ss' addsimprocs [perm_eval]) i)
urbanc@19477
    62
    end;
urbanc@19477
    63
urbanc@19477
    64
(* applies the perm_compose rule such that                             *)
urbanc@19477
    65
(*                                                                     *)
urbanc@19477
    66
(*   pi o (pi' o lhs) = rhs                                            *)
urbanc@19477
    67
(*                                                                     *)
urbanc@19477
    68
(* is transformed to                                                   *) 
urbanc@19477
    69
(*                                                                     *)
urbanc@19477
    70
(*  (pi o pi') o (pi' o lhs) = rhs                                     *)
urbanc@19477
    71
(*                                                                     *)
urbanc@19477
    72
(* this rule would loop in the simplifier, so some trick is used with  *)
urbanc@19477
    73
(* generating perm_aux'es for the outermost permutation and then un-   *)
urbanc@19477
    74
(* folding the definition                                              *)
urbanc@19477
    75
val pt_perm_compose_aux = thm "pt_perm_compose_aux";
urbanc@19477
    76
val cp1_aux             = thm "cp1_aux";
urbanc@19477
    77
val perm_aux_fold       = thm "perm_aux_fold"; 
urbanc@19477
    78
urbanc@19477
    79
fun perm_compose_tac ss i = 
urbanc@19477
    80
    let
urbanc@19477
    81
	fun perm_compose_simproc sg ss redex =
urbanc@19477
    82
	(case redex of
urbanc@19477
    83
           (Const ("nominal.perm", Type ("fun", [Type ("List.list", 
urbanc@19477
    84
             [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("nominal.perm", 
urbanc@19477
    85
               Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
urbanc@19477
    86
                pi2 $ t)) =>
urbanc@19350
    87
        let
urbanc@19350
    88
	    val tname' = Sign.base_name tname
urbanc@19477
    89
            val uname' = Sign.base_name uname
urbanc@19350
    90
        in
urbanc@19477
    91
            if pi1 <> pi2 then  (* only apply the composition rule in this case *)
urbanc@19477
    92
               if T = U then    
urbanc@19350
    93
                SOME (Drule.instantiate'
urbanc@19350
    94
	              [SOME (ctyp_of sg (fastype_of t))]
urbanc@19350
    95
		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
urbanc@19350
    96
		      (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
urbanc@19477
    97
	               PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose_aux)))
urbanc@19477
    98
               else
urbanc@19477
    99
                SOME (Drule.instantiate'
urbanc@19477
   100
	              [SOME (ctyp_of sg (fastype_of t))]
urbanc@19477
   101
		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
urbanc@19477
   102
		      (mk_meta_eq (PureThy.get_thm sg (Name ("cp_"^tname'^"_"^uname'^"_inst")) RS 
urbanc@19477
   103
                       cp1_aux)))
urbanc@19350
   104
            else NONE
urbanc@19350
   105
        end
urbanc@19350
   106
       | _ => NONE);
urbanc@19477
   107
	  
urbanc@19477
   108
      val perm_compose  =
urbanc@19350
   109
	Simplifier.simproc (the_context()) "perm_compose" 
urbanc@19477
   110
	["nominal.perm pi1 (nominal.perm pi2 t)"] perm_compose_simproc;
urbanc@19477
   111
urbanc@19477
   112
      val ss' = Simplifier.theory_context (the_context ()) empty_ss	  
urbanc@19477
   113
urbanc@18012
   114
    in
urbanc@19477
   115
	("analysing permutation compositions on the lhs",
urbanc@19477
   116
         EVERY [rtac trans i,
urbanc@19477
   117
                asm_full_simp_tac (ss' addsimprocs [perm_compose]) i,
urbanc@19477
   118
                asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i])
urbanc@18012
   119
    end
urbanc@18012
   120
urbanc@18012
   121
(* applying Stefan's smart congruence tac *)
urbanc@18012
   122
fun apply_cong_tac i = 
urbanc@18012
   123
    ("application of congruence",
urbanc@19477
   124
     (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
berghofe@17870
   125
urbanc@19477
   126
(* unfolds the definition of permutations     *)
urbanc@19477
   127
(* applied to functions such that             *)
urbanc@19477
   128
(*                                            *)
urbanc@19477
   129
(*   pi o f = rhs                             *)  
urbanc@19477
   130
(*                                            *)
urbanc@19477
   131
(* is transformed to                          *)
urbanc@19477
   132
(*                                            *)
urbanc@19477
   133
(*   %x. pi o (f ((rev pi) o x)) = rhs        *)
urbanc@18012
   134
fun unfold_perm_fun_def_tac i = 
urbanc@18012
   135
    let
urbanc@18012
   136
	val perm_fun_def = thm "nominal.perm_fun_def"
urbanc@18012
   137
    in
urbanc@18012
   138
	("unfolding of permutations on functions", 
urbanc@19477
   139
         rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
berghofe@17870
   140
    end
berghofe@17870
   141
urbanc@19477
   142
(* applies the ext-rule such that      *)
urbanc@19477
   143
(*                                     *)
urbanc@19477
   144
(*    f = g    goes to /\x. f x = g x  *)
urbanc@19477
   145
fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
berghofe@17870
   146
urbanc@19477
   147
(* FIXME FIXME FIXME *)
urbanc@19477
   148
(* should be able to analyse pi o fresh_fun () = fresh_fun instances *) 
urbanc@19477
   149
fun fresh_fun_eqvt_tac i =
urbanc@19477
   150
    let
urbanc@19477
   151
	val fresh_fun_equiv = thm "nominal.fresh_fun_equiv_ineq"
urbanc@19477
   152
    in
urbanc@19477
   153
	("fresh_fun equivariance", rtac (fresh_fun_equiv RS trans) i)
urbanc@19477
   154
    end		       
urbanc@19477
   155
		       
berghofe@17870
   156
(* debugging *)
berghofe@17870
   157
fun DEBUG_tac (msg,tac) = 
urbanc@19169
   158
    CHANGED (EVERY [tac, print_tac ("after "^msg)]); 
berghofe@17870
   159
fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
berghofe@17870
   160
urbanc@19477
   161
(* Main Tactics *)
urbanc@18012
   162
fun perm_simp_tac tactical ss i = 
urbanc@19139
   163
    DETERM (tactical (perm_eval_tac ss i));
urbanc@19139
   164
urbanc@19477
   165
(* perm_full_simp_tac is perm_simp_tac plus additional tactics    *)
urbanc@19477
   166
(* to decide equation that come from support problems             *)
urbanc@19477
   167
(* since it contains looping rules the "recursion" - depth is set *)
urbanc@19477
   168
(* to 10 - this seems to be sufficient in most cases              *)
urbanc@19477
   169
fun perm_full_simp_tac tactical ss =
urbanc@19477
   170
  let fun perm_full_simp_tac_aux tactical ss n = 
urbanc@19477
   171
	  if n=0 then K all_tac
urbanc@19477
   172
	  else DETERM o 
urbanc@19477
   173
	       (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
urbanc@19477
   174
                       fn i => tactical (perm_eval_tac ss i),
urbanc@19477
   175
		       fn i => tactical (perm_compose_tac ss i),
urbanc@19477
   176
		       fn i => tactical (apply_cong_tac i), 
urbanc@19477
   177
                       fn i => tactical (unfold_perm_fun_def_tac i),
urbanc@19477
   178
                       fn i => tactical (ext_fun_tac i), 
urbanc@19477
   179
                       fn i => tactical (fresh_fun_eqvt_tac i)]
urbanc@19477
   180
		      THEN_ALL_NEW (TRY o (perm_full_simp_tac_aux tactical ss (n-1))))
urbanc@19477
   181
  in perm_full_simp_tac_aux tactical ss 10 end;
urbanc@19151
   182
urbanc@19477
   183
(* tactic that first unfolds the support definition           *)
urbanc@19477
   184
(* and strips off the intros, then applies perm_full_simp_tac *)
urbanc@18012
   185
fun supports_tac tactical ss i =
urbanc@18012
   186
  let 
urbanc@18012
   187
      val supports_def = thm "nominal.op supports_def";
urbanc@18012
   188
      val fresh_def    = thm "nominal.fresh_def";
urbanc@18012
   189
      val fresh_prod   = thm "nominal.fresh_prod";
urbanc@18012
   190
      val simps        = [supports_def,symmetric fresh_def,fresh_prod]
berghofe@17870
   191
  in
urbanc@19477
   192
      EVERY [tactical ("unfolding of supports   ", simp_tac (HOL_basic_ss addsimps simps) i),
urbanc@19477
   193
             tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
urbanc@19477
   194
             tactical ("geting rid of the imps  ", rtac impI i),
urbanc@19477
   195
             tactical ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
urbanc@19477
   196
             tactical ("applying perm_full_simp ", perm_full_simp_tac tactical ss i
urbanc@19477
   197
                                                   (*perm_simp_tac tactical ss i*))]
berghofe@17870
   198
  end;
berghofe@17870
   199
urbanc@19151
   200
urbanc@19477
   201
(* tactic that guesses the finite-support of a goal       *)
urbanc@19477
   202
(* it collects all free variables and tries to show       *)
urbanc@19477
   203
(* that the support of these free variables (op supports) *)
urbanc@19477
   204
(* the goal                                               *)
urbanc@19151
   205
fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j - i) ins vs
urbanc@19151
   206
  | collect_vars i (v as Free _) vs = v ins vs
urbanc@19151
   207
  | collect_vars i (v as Var _) vs = v ins vs
urbanc@19151
   208
  | collect_vars i (Const _) vs = vs
urbanc@19151
   209
  | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
urbanc@19151
   210
  | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
urbanc@19151
   211
urbanc@19151
   212
val supports_rule = thm "supports_finite";
urbanc@19151
   213
urbanc@19151
   214
fun finite_guess_tac tactical ss i st =
urbanc@19151
   215
    let val goal = List.nth(cprems_of st, i-1)
urbanc@19151
   216
    in
urbanc@19151
   217
      case Logic.strip_assums_concl (term_of goal) of
urbanc@19151
   218
          _ $ (Const ("op :", _) $ (Const ("nominal.supp", T) $ x) $
urbanc@19151
   219
            Const ("Finite_Set.Finites", _)) =>
urbanc@19151
   220
          let
urbanc@19151
   221
            val cert = Thm.cterm_of (sign_of_thm st);
urbanc@19151
   222
            val ps = Logic.strip_params (term_of goal);
urbanc@19151
   223
            val Ts = rev (map snd ps);
urbanc@19151
   224
            val vs = collect_vars 0 x [];
urbanc@19151
   225
            val s = foldr (fn (v, s) =>
urbanc@19151
   226
                HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
urbanc@19151
   227
              HOLogic.unit vs;
urbanc@19151
   228
            val s' = list_abs (ps,
urbanc@19151
   229
              Const ("nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
urbanc@19151
   230
            val supports_rule' = Thm.lift_rule goal supports_rule;
urbanc@19151
   231
            val _ $ (_ $ S $ _) =
urbanc@19151
   232
              Logic.strip_assums_concl (hd (prems_of supports_rule'));
urbanc@19151
   233
            val supports_rule'' = Drule.cterm_instantiate
urbanc@19151
   234
              [(cert (head_of S), cert s')] supports_rule'
urbanc@19151
   235
          in
urbanc@19151
   236
            (tactical ("guessing of the right supports-set",
urbanc@19151
   237
                      EVERY [compose_tac (false, supports_rule'', 2) i,
urbanc@19151
   238
                             asm_full_simp_tac ss (i+1),
urbanc@19151
   239
                             supports_tac tactical ss i])) st
urbanc@19151
   240
          end
urbanc@19151
   241
        | _ => Seq.empty
urbanc@19151
   242
    end
urbanc@19151
   243
    handle Subscript => Seq.empty
urbanc@19151
   244
berghofe@17870
   245
in             
berghofe@17870
   246
urbanc@18012
   247
fun simp_meth_setup tac =
urbanc@18046
   248
  Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
urbanc@18012
   249
  (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
berghofe@17870
   250
urbanc@19477
   251
val perm_eq_meth            = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
urbanc@19477
   252
val perm_eq_meth_debug      = simp_meth_setup (perm_simp_tac DEBUG_tac);
urbanc@19477
   253
val perm_full_eq_meth       = simp_meth_setup (perm_full_simp_tac NO_DEBUG_tac);
urbanc@19477
   254
val perm_full_eq_meth_debug = simp_meth_setup (perm_full_simp_tac DEBUG_tac);
urbanc@19477
   255
val supports_meth           = simp_meth_setup (supports_tac NO_DEBUG_tac);
urbanc@19477
   256
val supports_meth_debug     = simp_meth_setup (supports_tac DEBUG_tac);
urbanc@19477
   257
val finite_gs_meth          = simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
urbanc@19477
   258
val finite_gs_meth_debug    = simp_meth_setup (finite_guess_tac DEBUG_tac);
berghofe@17870
   259
berghofe@17870
   260
end
berghofe@17870
   261
berghofe@17870
   262
berghofe@17870
   263