src/HOL/Nominal/nominal_permeq.ML
author urbanc
Sat Oct 29 15:01:25 2005 +0200 (2005-10-29)
changeset 18046 b7389981170b
parent 18012 23e6cfda8c4b
child 18052 004515accc10
permissions -rw-r--r--
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
This means the syntax of the tactics supports_simp and perm_simp
are exactly like simp, namely

(supports_simp add: .... del: ...)

where the add's and del's are optional.
berghofe@17870
     1
(* $Id$ *)
berghofe@17870
     2
berghofe@17870
     3
(* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
berghofe@17870
     4
urbanc@18012
     5
(* tries until depth 40 the following (in that order):                     *)
urbanc@18012
     6
(*                                                                         *)
urbanc@18012
     7
(*  - simplification plus analysing perm_swaps, perm_fresh_fresh, perm_bij *)
urbanc@18012
     8
(*  - permutation compositions (on the left hand side of =)                *)
urbanc@18012
     9
(*  - simplification of permutation on applications and abstractions       *)
urbanc@18012
    10
(*  - analysing congruences (from Stefan Berghofer's datatype pkg)         *)
urbanc@18012
    11
(*  - unfolding permutation on functions                                   *)
urbanc@18012
    12
(*  - expanding equalities of functions                                    *)
urbanc@18012
    13
(*                                                                         *)
urbanc@18012
    14
(*  for supports - it first unfolds the definitions and strips of intros   *)
urbanc@18012
    15
berghofe@17870
    16
local
berghofe@17870
    17
urbanc@18012
    18
(* pulls out dynamically a thm via the simpset *)
urbanc@18012
    19
fun dynamic_thm ss name = 
urbanc@18012
    20
    ProofContext.get_thm (Simplifier.the_context ss) (Name name);
urbanc@18012
    21
urbanc@18012
    22
(* initial simplification step in the tactic *)
urbanc@18012
    23
fun initial_simp_tac ss i =
urbanc@18012
    24
    let
urbanc@18012
    25
	val perm_swap  = dynamic_thm ss "perm_swap";
urbanc@18012
    26
        val perm_fresh = dynamic_thm ss "perm_fresh_fresh";
urbanc@18012
    27
        val perm_bij   = dynamic_thm ss "perm_bij";
urbanc@18012
    28
        val ss' = ss addsimps [perm_swap,perm_fresh,perm_bij]
urbanc@18012
    29
    in
urbanc@18012
    30
      ("general simplification step", FIRST [rtac conjI i, asm_full_simp_tac ss' i])
urbanc@18012
    31
    end;
berghofe@17870
    32
berghofe@17870
    33
(* applies the perm_compose rule - this rule would loop in the simplifier *)
urbanc@18012
    34
fun apply_perm_compose_tac ss i = 
urbanc@18012
    35
    let
urbanc@18012
    36
	val perm_compose = dynamic_thm ss "perm_compose"; 
urbanc@18012
    37
    in
urbanc@18012
    38
	("analysing permutation compositions on the lhs",rtac (perm_compose RS trans)  i)
urbanc@18012
    39
    end
urbanc@18012
    40
urbanc@18012
    41
urbanc@18012
    42
(* applies the perm_eq_lam and perm_eq_app simplifications *)
urbanc@18012
    43
fun apply_app_lam_simp_tac ss i =
berghofe@17870
    44
    let 
urbanc@18012
    45
	val perm_app_eq  = dynamic_thm ss "perm_app_eq";
urbanc@18012
    46
        val perm_lam_eq  = dynamic_thm ss "perm_eq_lam"
urbanc@18012
    47
    in
urbanc@18012
    48
     ("simplification of permutations on applications and lambdas", 
urbanc@18012
    49
      asm_full_simp_tac (HOL_basic_ss addsimps [perm_app_eq,perm_lam_eq]) i)
urbanc@18012
    50
    end
urbanc@18012
    51
urbanc@18012
    52
(* applying Stefan's smart congruence tac *)
urbanc@18012
    53
fun apply_cong_tac i = 
urbanc@18012
    54
    ("application of congruence",
urbanc@18012
    55
     (fn st => DatatypeAux.cong_tac  i st handle Subscript => no_tac st));
berghofe@17870
    56
berghofe@17870
    57
(* unfolds the definition of permutations applied to functions *)
urbanc@18012
    58
fun unfold_perm_fun_def_tac i = 
urbanc@18012
    59
    let
urbanc@18012
    60
	val perm_fun_def = thm "nominal.perm_fun_def"
urbanc@18012
    61
    in
urbanc@18012
    62
	("unfolding of permutations on functions", 
urbanc@18012
    63
	 simp_tac (HOL_basic_ss addsimps [perm_fun_def]) i)
berghofe@17870
    64
    end
berghofe@17870
    65
urbanc@18012
    66
(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
urbanc@18012
    67
fun expand_fun_eq_tac i =    
urbanc@18012
    68
    ("extensionality expansion of functions",
urbanc@18012
    69
    EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) i, REPEAT_DETERM (rtac allI i)]);
berghofe@17870
    70
berghofe@17870
    71
(* debugging *)
berghofe@17870
    72
fun DEBUG_tac (msg,tac) = 
urbanc@18012
    73
    EVERY [CHANGED tac, print_tac ("after "^msg)]; 
berghofe@17870
    74
fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
berghofe@17870
    75
berghofe@17870
    76
(* Main Tactic *)
urbanc@18012
    77
berghofe@17870
    78
(* "repeating"-depth is set to 40 - this seems sufficient *)
urbanc@18012
    79
fun perm_simp_tac tactical ss i = 
urbanc@18012
    80
    DETERM (REPEAT_DETERM_N 40 
urbanc@18012
    81
      (FIRST[tactical (initial_simp_tac ss i),
urbanc@18012
    82
             tactical (apply_perm_compose_tac ss i),
urbanc@18012
    83
             tactical (apply_app_lam_simp_tac ss i),
urbanc@18012
    84
             tactical (apply_cong_tac i), 
urbanc@18012
    85
             tactical (unfold_perm_fun_def_tac i),
urbanc@18012
    86
             tactical (expand_fun_eq_tac i)]));
berghofe@17870
    87
urbanc@18012
    88
(* tactic that first unfolds the support definition *)
urbanc@18012
    89
(* and strips of intros, then applies perm_simp_tac *)
urbanc@18012
    90
fun supports_tac tactical ss i =
urbanc@18012
    91
  let 
urbanc@18012
    92
      val supports_def = thm "nominal.op supports_def";
urbanc@18012
    93
      val fresh_def    = thm "nominal.fresh_def";
urbanc@18012
    94
      val fresh_prod   = thm "nominal.fresh_prod";
urbanc@18012
    95
      val simps        = [supports_def,symmetric fresh_def,fresh_prod]
berghofe@17870
    96
  in
urbanc@18012
    97
      EVERY [tactical ("unfolding of supports ",simp_tac (HOL_basic_ss addsimps simps) i),
urbanc@18012
    98
             tactical ("stripping of foralls  " ,REPEAT_DETERM (rtac allI i)),
urbanc@18012
    99
             tactical ("geting rid of the imps",rtac impI i),
urbanc@18012
   100
             tactical ("eliminating conjuncts ",REPEAT_DETERM (etac  conjE i)),
urbanc@18012
   101
             tactical ("applying perm_simp    ",perm_simp_tac tactical ss i)]
berghofe@17870
   102
  end;
berghofe@17870
   103
berghofe@17870
   104
in             
berghofe@17870
   105
urbanc@18012
   106
(* FIXME simp_modifiers' 
berghofe@17870
   107
urbanc@18012
   108
(Markus needs to commit this)
urbanc@18012
   109
*)
urbanc@18012
   110
berghofe@17870
   111
urbanc@18012
   112
fun simp_meth_setup tac =
urbanc@18046
   113
  Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
urbanc@18012
   114
  (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
berghofe@17870
   115
urbanc@18012
   116
val perm_eq_meth        = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
urbanc@18012
   117
val perm_eq_meth_debug  = simp_meth_setup (perm_simp_tac DEBUG_tac);
urbanc@18012
   118
val supports_meth       = simp_meth_setup (supports_tac NO_DEBUG_tac);
urbanc@18012
   119
val supports_meth_debug = simp_meth_setup (supports_tac DEBUG_tac);
berghofe@17870
   120
berghofe@17870
   121
end
berghofe@17870
   122
berghofe@17870
   123
berghofe@17870
   124