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