src/HOL/Nominal/nominal_permeq.ML
author berghofe
Mon Oct 17 12:30:57 2005 +0200 (2005-10-17)
changeset 17870 c35381811d5c
child 18012 23e6cfda8c4b
permissions -rw-r--r--
Initial revision.
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
berghofe@17870
     7
(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
berghofe@17870
     8
val Expand_Fun_Eq_tac =    
berghofe@17870
     9
    ("extensionality on functions",
berghofe@17870
    10
    EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) 1, REPEAT_DETERM (rtac allI 1)]);
berghofe@17870
    11
berghofe@17870
    12
(* applies the perm_compose rule - this rule would loop in the simplifier *)
berghofe@17870
    13
fun Apply_Perm_Compose_tac ctxt = 
berghofe@17870
    14
    let 
berghofe@17870
    15
	val perm_compose = PureThy.get_thm (ProofContext.theory_of ctxt) (Name ("perm_compose"));
berghofe@17870
    16
    in ("analysing permutation compositions",rtac (perm_compose RS trans)  1)
berghofe@17870
    17
    end;
berghofe@17870
    18
berghofe@17870
    19
(* unfolds the definition of permutations applied to functions *)
berghofe@17870
    20
fun Unfold_Perm_Fun_Def_tac ctxt = 
berghofe@17870
    21
    let 
berghofe@17870
    22
	val perm_fun_def = PureThy.get_thm (ProofContext.theory_of ctxt) (Name ("nominal.perm_fun_def"))
berghofe@17870
    23
    in ("unfolding of perms on functions", simp_tac (HOL_basic_ss addsimps [perm_fun_def]) 1)
berghofe@17870
    24
    end
berghofe@17870
    25
    
berghofe@17870
    26
(* applies the perm_eq_lam and perm_eq_app simplifications *)
berghofe@17870
    27
fun Apply_SimProc_tac ctxt = 
berghofe@17870
    28
    let
berghofe@17870
    29
        val thy = ProofContext.theory_of ctxt;
berghofe@17870
    30
	val perm_app_eq = PureThy.get_thm thy (Name ("perm_app_eq"));
berghofe@17870
    31
        val perm_lam_eq = PureThy.get_thm thy (Name ("perm_eq_lam"));
berghofe@17870
    32
    in
berghofe@17870
    33
	("simplification of permutation on applications and lambdas", 
berghofe@17870
    34
	 asm_full_simp_tac (HOL_basic_ss addsimps [perm_app_eq,perm_lam_eq]) 1)
berghofe@17870
    35
    end;
berghofe@17870
    36
berghofe@17870
    37
(* applying Stefan's smart congruence tac *)
berghofe@17870
    38
val Apply_Cong_tac = ("application of congruence",
berghofe@17870
    39
                     (fn st => DatatypeAux.cong_tac  1 st handle Subscript => no_tac st));
berghofe@17870
    40
berghofe@17870
    41
(* initial simplification step in the tactic *)
berghofe@17870
    42
fun Initial_Simp_tac thms ctxt =
berghofe@17870
    43
    let
berghofe@17870
    44
	val thy = ProofContext.theory_of ctxt;
berghofe@17870
    45
	val perm_swap  = PureThy.get_thm thy (Name ("perm_swap"));
berghofe@17870
    46
        val perm_fresh = PureThy.get_thm thy (Name ("perm_fresh_fresh"));
berghofe@17870
    47
        val perm_bij   = PureThy.get_thm thy (Name ("perm_bij"));
berghofe@17870
    48
        val simps = (local_simpset_of ctxt) addsimps (thms @ [perm_swap,perm_fresh,perm_bij])
berghofe@17870
    49
    in
berghofe@17870
    50
      ("general simplification step", FIRST [rtac conjI 1, asm_full_simp_tac simps 1])
berghofe@17870
    51
    end;
berghofe@17870
    52
berghofe@17870
    53
berghofe@17870
    54
(* debugging *)
berghofe@17870
    55
fun DEBUG_tac (msg,tac) = 
berghofe@17870
    56
    EVERY [print_tac ("before application of "^msg), CHANGED tac, print_tac ("after "^msg)]; 
berghofe@17870
    57
fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
berghofe@17870
    58
berghofe@17870
    59
(* Main Tactic *)
berghofe@17870
    60
(* "repeating"-depth is set to 40 - this seems sufficient *)
berghofe@17870
    61
fun perm_simp_tac tactical thms ctxt = 
berghofe@17870
    62
    REPEAT_DETERM_N 40 
berghofe@17870
    63
      (FIRST[tactical (Initial_Simp_tac thms ctxt),
berghofe@17870
    64
             tactical (Apply_Perm_Compose_tac ctxt),
berghofe@17870
    65
             tactical (Apply_SimProc_tac ctxt),
berghofe@17870
    66
             tactical Apply_Cong_tac, 
berghofe@17870
    67
             tactical (Unfold_Perm_Fun_Def_tac ctxt),
berghofe@17870
    68
             tactical Expand_Fun_Eq_tac]);
berghofe@17870
    69
berghofe@17870
    70
(* tactic that unfolds first the support definition *)
berghofe@17870
    71
(* and then applies perm_simp                       *)
berghofe@17870
    72
fun supports_tac tactical thms ctxt =
berghofe@17870
    73
  let
berghofe@17870
    74
    val thy = ProofContext.theory_of ctxt;
berghofe@17870
    75
    val supports_def = PureThy.get_thm thy (Name ("nominal.op supports_def"));
berghofe@17870
    76
    val fresh_def    = PureThy.get_thm thy (Name ("nominal.fresh_def"));
berghofe@17870
    77
    val fresh_prod   = PureThy.get_thm thy (Name ("nominal.fresh_prod"));
berghofe@17870
    78
    val simps        = [supports_def,symmetric fresh_def,fresh_prod];
berghofe@17870
    79
berghofe@17870
    80
  in
berghofe@17870
    81
      EVERY [tactical ("unfolding of supports",simp_tac (HOL_basic_ss addsimps simps) 1),
berghofe@17870
    82
             tactical ("stripping of foralls " ,REPEAT_DETERM (rtac allI 1)),
berghofe@17870
    83
             tactical ("geting rid of the imp",rtac impI 1),
berghofe@17870
    84
             tactical ("eliminating conjuncts",REPEAT_DETERM (etac  conjE 1)),
berghofe@17870
    85
             tactical ("applying perm_simp   ",perm_simp_tac tactical thms ctxt)]
berghofe@17870
    86
  end;
berghofe@17870
    87
berghofe@17870
    88
in             
berghofe@17870
    89
berghofe@17870
    90
val perm_eq_meth = 
berghofe@17870
    91
    Method.thms_ctxt_args 
berghofe@17870
    92
	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (perm_simp_tac NO_DEBUG_tac thms ctxt)));
berghofe@17870
    93
berghofe@17870
    94
val perm_eq_meth_debug = 
berghofe@17870
    95
    Method.thms_ctxt_args 
berghofe@17870
    96
	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (perm_simp_tac DEBUG_tac thms ctxt)));
berghofe@17870
    97
berghofe@17870
    98
val supports_meth = 
berghofe@17870
    99
    Method.thms_ctxt_args 
berghofe@17870
   100
	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (supports_tac NO_DEBUG_tac thms ctxt)));
berghofe@17870
   101
berghofe@17870
   102
val supports_meth_debug = 
berghofe@17870
   103
    Method.thms_ctxt_args 
berghofe@17870
   104
	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (supports_tac DEBUG_tac thms ctxt)));
berghofe@17870
   105
berghofe@17870
   106
end
berghofe@17870
   107
berghofe@17870
   108
berghofe@17870
   109