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