src/HOL/Nominal/nominal_permeq.ML
author urbanc
Sun Feb 26 22:24:05 2006 +0100 (2006-02-26)
changeset 19139 af69e41eab5d
parent 18434 a31e52a3e6ef
child 19144 9c8793c62d0c
permissions -rw-r--r--
improved the decision-procedure for permutations;
now uses a simproc

FIXME:
the simproc still needs to be adapted for arbitrary
atom types
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@19139
    13
(* FIXME: make it usable for all atom-types *)
urbanc@18012
    14
(* initial simplification step in the tactic *)
urbanc@19139
    15
fun perm_eval_tac ss i =
urbanc@18012
    16
    let
urbanc@19139
    17
        val perm_eq_app   = thm "nominal.pt_fun_app_eq";
urbanc@19139
    18
        val at_inst       = dynamic_thm ss "at_name_inst";
urbanc@19139
    19
        val pt_inst       = dynamic_thm ss "pt_name_inst";
urbanc@19139
    20
urbanc@19139
    21
        fun perm_eval_simproc sg ss redex =
urbanc@19139
    22
        (case redex of 
urbanc@19139
    23
        (* case pi o (f x) == (pi o f) (pi o x)    *)
urbanc@19139
    24
        (* special treatment in cases of constants *)
urbanc@19139
    25
        (Const("nominal.perm",Type("fun",[Type("List.list",[Type("*",[ty,_])]),_])) $ pi $ (f $ x)) 
urbanc@19139
    26
        => let
urbanc@19139
    27
             val _ = warning ("type: "^Sign.string_of_typ (sign_of (the_context())) ty)
urbanc@19139
    28
           in
urbanc@19139
    29
urbanc@19139
    30
           (case f of
urbanc@19139
    31
                    (* nothing to do on constants *)
urbanc@19139
    32
                    (* FIXME: proper treatment of constants *)
urbanc@19139
    33
                      Const(_,_)                   => NONE
urbanc@19139
    34
                    | (Const(_,_) $ _)             => NONE
urbanc@19139
    35
                    | ((Const(_,_) $ _) $ _)       => NONE
urbanc@19139
    36
                    | (((Const(_,_) $ _) $ _) $ _) => NONE
urbanc@19139
    37
                    | _ => 
urbanc@19139
    38
                       (* FIXME: analyse type here or at "pty"*)
urbanc@19139
    39
		       SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection))
urbanc@19139
    40
            end
urbanc@19139
    41
urbanc@19139
    42
        (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
urbanc@19139
    43
        | (Const("nominal.perm",_) $ pi $ (Abs _)) 
urbanc@19139
    44
        => let 
urbanc@19139
    45
             val perm_fun_def = thm "nominal.perm_fun_def"
urbanc@19139
    46
           in SOME (perm_fun_def) end
urbanc@19139
    47
urbanc@19139
    48
        (* no redex otherwise *) 
urbanc@19139
    49
        | _ => NONE);
urbanc@19139
    50
urbanc@19139
    51
	val perm_eval =
urbanc@19139
    52
	    Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 
urbanc@19139
    53
	    ["nominal.perm pi x"] perm_eval_simproc;
urbanc@19139
    54
urbanc@18279
    55
        (* these lemmas are created dynamically according to the atom types *) 
urbanc@19139
    56
	val perm_swap     = dynamic_thms ss "perm_swap";
urbanc@19139
    57
        val perm_fresh    = dynamic_thms ss "perm_fresh_fresh";
urbanc@19139
    58
        val perm_bij      = dynamic_thms ss "perm_bij";
urbanc@19139
    59
        val perm_compose' = dynamic_thms ss "perm_compose'";
urbanc@19139
    60
        val perm_pi_simp  = dynamic_thms ss "perm_pi_simp";
urbanc@19139
    61
        val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_compose'@perm_pi_simp)
urbanc@19139
    62
                     addsimprocs [perm_eval];
urbanc@19139
    63
                    
urbanc@18012
    64
    in
urbanc@18012
    65
      ("general simplification step", FIRST [rtac conjI i, asm_full_simp_tac ss' i])
urbanc@18012
    66
    end;
berghofe@17870
    67
urbanc@18434
    68
(* applies the perm_compose rule - this rule would loop in the simplifier     *)
urbanc@18434
    69
(* in case there are more atom-types we have to check every possible instance *)
urbanc@19139
    70
(* of perm_compose                                                            *)
urbanc@18012
    71
fun apply_perm_compose_tac ss i = 
urbanc@18012
    72
    let
urbanc@18434
    73
	val perm_compose = dynamic_thms ss "perm_compose"; 
urbanc@18434
    74
        val tacs = map (fn thm => (rtac (thm RS trans) i)) perm_compose
urbanc@18012
    75
    in
urbanc@18434
    76
	("analysing permutation compositions on the lhs",FIRST (tacs))
urbanc@18012
    77
    end
urbanc@18012
    78
urbanc@18012
    79
(* applying Stefan's smart congruence tac *)
urbanc@18012
    80
fun apply_cong_tac i = 
urbanc@18012
    81
    ("application of congruence",
urbanc@18012
    82
     (fn st => DatatypeAux.cong_tac  i st handle Subscript => no_tac st));
berghofe@17870
    83
berghofe@17870
    84
(* unfolds the definition of permutations applied to functions *)
urbanc@18012
    85
fun unfold_perm_fun_def_tac i = 
urbanc@18012
    86
    let
urbanc@18012
    87
	val perm_fun_def = thm "nominal.perm_fun_def"
urbanc@18012
    88
    in
urbanc@18012
    89
	("unfolding of permutations on functions", 
urbanc@18012
    90
	 simp_tac (HOL_basic_ss addsimps [perm_fun_def]) i)
berghofe@17870
    91
    end
berghofe@17870
    92
urbanc@18012
    93
(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
urbanc@18012
    94
fun expand_fun_eq_tac i =    
urbanc@18012
    95
    ("extensionality expansion of functions",
urbanc@18012
    96
    EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) i, REPEAT_DETERM (rtac allI i)]);
berghofe@17870
    97
berghofe@17870
    98
(* debugging *)
berghofe@17870
    99
fun DEBUG_tac (msg,tac) = 
urbanc@18012
   100
    EVERY [CHANGED tac, print_tac ("after "^msg)]; 
berghofe@17870
   101
fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
berghofe@17870
   102
berghofe@17870
   103
(* Main Tactic *)
urbanc@18012
   104
urbanc@18012
   105
fun perm_simp_tac tactical ss i = 
urbanc@19139
   106
    DETERM (tactical (perm_eval_tac ss i));
urbanc@19139
   107
urbanc@19139
   108
(* perm_simp_tac plus additional tactics to decide            *)
urbanc@19139
   109
(* support problems                                           *)
urbanc@19139
   110
(* the "repeating"-depth is set to 40 - this seems sufficient *)
urbanc@19139
   111
fun perm_supports_tac tactical ss i = 
urbanc@18012
   112
    DETERM (REPEAT_DETERM_N 40 
urbanc@19139
   113
      (FIRST[tactical (perm_eval_tac ss i),
urbanc@18012
   114
             tactical (apply_perm_compose_tac ss i),
urbanc@18012
   115
             tactical (apply_cong_tac i), 
urbanc@18012
   116
             tactical (unfold_perm_fun_def_tac i),
urbanc@18012
   117
             tactical (expand_fun_eq_tac i)]));
berghofe@17870
   118
urbanc@19139
   119
(* tactic that first unfolds the support definition          *)
urbanc@19139
   120
(* and strips off the intros, then applies perm_supports_tac *)
urbanc@18012
   121
fun supports_tac tactical ss i =
urbanc@18012
   122
  let 
urbanc@18012
   123
      val supports_def = thm "nominal.op supports_def";
urbanc@18012
   124
      val fresh_def    = thm "nominal.fresh_def";
urbanc@18012
   125
      val fresh_prod   = thm "nominal.fresh_prod";
urbanc@18012
   126
      val simps        = [supports_def,symmetric fresh_def,fresh_prod]
berghofe@17870
   127
  in
urbanc@18012
   128
      EVERY [tactical ("unfolding of supports ",simp_tac (HOL_basic_ss addsimps simps) i),
urbanc@18012
   129
             tactical ("stripping of foralls  " ,REPEAT_DETERM (rtac allI i)),
urbanc@18012
   130
             tactical ("geting rid of the imps",rtac impI i),
urbanc@18012
   131
             tactical ("eliminating conjuncts ",REPEAT_DETERM (etac  conjE i)),
urbanc@19139
   132
             tactical ("applying perm_simp    ",perm_supports_tac tactical ss i)]
berghofe@17870
   133
  end;
berghofe@17870
   134
berghofe@17870
   135
in             
berghofe@17870
   136
berghofe@17870
   137
urbanc@18012
   138
fun simp_meth_setup tac =
urbanc@18046
   139
  Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
urbanc@18012
   140
  (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
berghofe@17870
   141
urbanc@18012
   142
val perm_eq_meth        = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
urbanc@18012
   143
val perm_eq_meth_debug  = simp_meth_setup (perm_simp_tac DEBUG_tac);
urbanc@18012
   144
val supports_meth       = simp_meth_setup (supports_tac NO_DEBUG_tac);
urbanc@18012
   145
val supports_meth_debug = simp_meth_setup (supports_tac DEBUG_tac);
berghofe@17870
   146
berghofe@17870
   147
end
berghofe@17870
   148
berghofe@17870
   149
berghofe@17870
   150