src/HOL/Nominal/nominal_permeq.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46219 426ed18eba43
child 51717 9e7d1c139569
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
     1
(*  Title:      HOL/Nominal/nominal_permeq.ML
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
     2
    Author:     Christian Urban, TU Muenchen
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
     3
    Author:     Julien Narboux, TU Muenchen
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     4
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
     5
Methods for simplifying permutations and for analysing equations
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
     6
involving permutations. 
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
     7
*)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     8
20431
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
     9
(*
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    10
FIXMES:
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    11
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    12
 - allow the user to give an explicit set S in the
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    13
   fresh_guess tactic which is then verified
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    14
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    15
 - the perm_compose tactic does not do an "outermost
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    16
   rewriting" and can therefore not deal with goals
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    17
   like
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    18
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    19
      [(a,b)] o pi1 o pi2 = ....
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    20
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    21
   rather it tries to permute pi1 over pi2, which 
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    22
   results in a failure when used with the 
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    23
   perm_(full)_simp tactics
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    24
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    25
*)
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    26
eef4e9081bea added a FIXME-comment
urbanc
parents: 20289
diff changeset
    27
19987
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    28
signature NOMINAL_PERMEQ =
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    29
sig
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
    30
  val perm_simproc_fun : simproc
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
    31
  val perm_simproc_app : simproc
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
    32
19987
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    33
  val perm_simp_tac : simpset -> int -> tactic
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
    34
  val perm_extend_simp_tac : simpset -> int -> tactic
19987
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    35
  val supports_tac : simpset -> int -> tactic
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    36
  val finite_guess_tac : simpset -> int -> tactic
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    37
  val fresh_guess_tac : simpset -> int -> tactic
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    38
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    39
  val perm_simp_meth : (Proof.context -> Proof.method) context_parser
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    40
  val perm_simp_meth_debug : (Proof.context -> Proof.method) context_parser
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    41
  val perm_extend_simp_meth : (Proof.context -> Proof.method) context_parser
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    42
  val perm_extend_simp_meth_debug : (Proof.context -> Proof.method) context_parser
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    43
  val supports_meth : (Proof.context -> Proof.method) context_parser
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    44
  val supports_meth_debug : (Proof.context -> Proof.method) context_parser
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    45
  val finite_guess_meth : (Proof.context -> Proof.method) context_parser
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    46
  val finite_guess_meth_debug : (Proof.context -> Proof.method) context_parser
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    47
  val fresh_guess_meth : (Proof.context -> Proof.method) context_parser
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    48
  val fresh_guess_meth_debug : (Proof.context -> Proof.method) context_parser
19987
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    49
end
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    50
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    51
structure NominalPermeq : NOMINAL_PERMEQ =
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    52
struct
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    53
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    54
(* some lemmas needed below *)
24519
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    55
val finite_emptyI = @{thm "finite.emptyI"};
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    56
val finite_Un     = @{thm "finite_Un"};
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    57
val conj_absorb   = @{thm "conj_absorb"};
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    58
val not_false     = @{thm "not_False_eq_True"}
44684
8dde3352d5c4 assert Pure equations for theorem references; tuned
haftmann
parents: 43278
diff changeset
    59
val perm_fun_def  = Simpdata.mk_eq @{thm "Nominal.perm_fun_def"};
24519
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    60
val perm_eq_app   = @{thm "Nominal.pt_fun_app_eq"};
44684
8dde3352d5c4 assert Pure equations for theorem references; tuned
haftmann
parents: 43278
diff changeset
    61
val supports_def  = Simpdata.mk_eq @{thm "Nominal.supports_def"};
8dde3352d5c4 assert Pure equations for theorem references; tuned
haftmann
parents: 43278
diff changeset
    62
val fresh_def     = Simpdata.mk_eq @{thm "Nominal.fresh_def"};
24519
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    63
val fresh_prod    = @{thm "Nominal.fresh_prod"};
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    64
val fresh_unit    = @{thm "Nominal.fresh_unit"};
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    65
val supports_rule = @{thm "supports_finite"};
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    66
val supp_prod     = @{thm "supp_prod"};
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    67
val supp_unit     = @{thm "supp_unit"};
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    68
val pt_perm_compose_aux = @{thm "pt_perm_compose_aux"};
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    69
val cp1_aux             = @{thm "cp1_aux"};
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    70
val perm_aux_fold       = @{thm "perm_aux_fold"}; 
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    71
val supports_fresh_rule = @{thm "supports_fresh"};
21669
c68717c16013 removed legacy ML bindings;
wenzelm
parents: 21588
diff changeset
    72
19987
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
    73
(* pulls out dynamically a thm via the proof state *)
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38715
diff changeset
    74
fun dynamic_thms st name = Global_Theory.get_thms (theory_of_thm st) name;
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38715
diff changeset
    75
fun dynamic_thm  st name = Global_Theory.get_thm  (theory_of_thm st) name;
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    76
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    77
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    78
(* needed in the process of fully simplifying permutations *)
24519
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    79
val strong_congs = [@{thm "if_cong"}]
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    80
(* needed to avoid warnings about overwritten congs *)
24519
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
    81
val weak_congs   = [@{thm "if_weak_cong"}]
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    82
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    83
(* debugging *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    84
fun DEBUG_tac (msg,tac) = 
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    85
    CHANGED (EVERY [print_tac ("before "^msg), tac, print_tac ("after "^msg)]); 
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    86
fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    87
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    88
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    89
(* simproc that deals with instances of permutations in front *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    90
(* of applications; just adding this rule to the simplifier   *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    91
(* would loop; it also needs careful tuning with the simproc  *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    92
(* for functions to avoid further possibilities for looping   *)
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
    93
fun perm_simproc_app' sg ss redex =
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    94
  let 
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    95
    (* the "application" case is only applicable when the head of f is not a *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    96
    (* constant or when (f x) is a permuation with two or more arguments     *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    97
    fun applicable_app t = 
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
    98
          (case (strip_comb t) of
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
    99
              (Const ("Nominal.perm",_),ts) => (length ts) >= 2
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   100
            | (Const _,_) => false
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   101
            | _ => true)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   102
  in
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   103
    case redex of 
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
   104
        (* case pi o (f x) == (pi o f) (pi o x)          *)
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
   105
        (Const("Nominal.perm",
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37391
diff changeset
   106
          Type("fun",[Type("List.list",[Type(@{type_name Product_Type.prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   107
            (if (applicable_app f) then
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   108
              let
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   109
                val name = Long_Name.base_name n
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38715
diff changeset
   110
                val at_inst = Global_Theory.get_thm sg ("at_" ^ name ^ "_inst")
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38715
diff changeset
   111
                val pt_inst = Global_Theory.get_thm sg ("pt_" ^ name ^ "_inst")
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   112
              in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   113
            else NONE)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   114
      | _ => NONE
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   115
  end
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
   116
38715
6513ea67d95d renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents: 37678
diff changeset
   117
val perm_simproc_app = Simplifier.simproc_global @{theory} "perm_simproc_app"
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   118
  ["Nominal.perm pi x"] perm_simproc_app';
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   119
24519
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
   120
(* a simproc that deals with permutation instances in front of functions  *)
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   121
fun perm_simproc_fun' sg ss redex = 
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   122
   let 
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   123
     fun applicable_fun t =
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   124
       (case (strip_comb t) of
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   125
          (Abs _ ,[]) => true
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
   126
        | (Const ("Nominal.perm",_),_) => false
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   127
        | (Const _, _) => true
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
   128
        | _ => false)
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   129
   in
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   130
     case redex of 
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   131
       (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   132
       (Const("Nominal.perm",_) $ pi $ f)  => 
44830
haftmann
parents: 44693
diff changeset
   133
          (if applicable_fun f then SOME perm_fun_def else NONE)
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   134
      | _ => NONE
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   135
   end
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
   136
38715
6513ea67d95d renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents: 37678
diff changeset
   137
val perm_simproc_fun = Simplifier.simproc_global @{theory} "perm_simproc_fun"
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   138
  ["Nominal.perm pi x"] perm_simproc_fun';
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   139
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   140
(* function for simplyfying permutations          *)
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   141
(* stac contains the simplifiation tactic that is *)
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   142
(* applied (see (no_asm) options below            *)
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   143
fun perm_simp_gen stac dyn_thms eqvt_thms ss i = 
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   144
    ("general simplification of permutations", fn st =>
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   145
    let
35232
f588e1169c8b renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents: 34885
diff changeset
   146
       val ss' = Simplifier.global_context (theory_of_thm st) ss
26343
0dd2eab7b296 simplified get_thm(s): back to plain name argument;
wenzelm
parents: 26338
diff changeset
   147
         addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   148
         addsimprocs [perm_simproc_fun, perm_simproc_app]
45620
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 44830
diff changeset
   149
         |> fold Simplifier.del_cong weak_congs
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 44830
diff changeset
   150
         |> fold Simplifier.add_cong strong_congs
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   151
    in
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   152
      stac ss' i st
19987
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
   153
    end);
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   154
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   155
(* general simplification of permutations and permutation that arose from eqvt-problems *)
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   156
fun perm_simp stac ss = 
22610
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   157
    let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   158
    in 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
   159
        perm_simp_gen stac simps [] ss
22610
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   160
    end;
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   161
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   162
fun eqvt_simp stac ss = 
22610
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   163
    let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
   164
        val eqvts_thms = NominalThmDecls.get_eqvt_thms (Simplifier.the_context ss);
22610
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   165
    in 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
   166
        perm_simp_gen stac simps eqvts_thms ss
22610
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   167
    end;
22562
80b814fe284b rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents: 22541
diff changeset
   168
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   169
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   170
(* main simplification tactics for permutations *)
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   171
fun perm_simp_tac_gen_i stac tactical ss i = DETERM (tactical (perm_simp stac ss i));
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   172
fun eqvt_simp_tac_gen_i stac tactical ss i = DETERM (tactical (eqvt_simp stac ss i)); 
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   173
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   174
val perm_simp_tac_i          = perm_simp_tac_gen_i simp_tac
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   175
val perm_asm_simp_tac_i      = perm_simp_tac_gen_i asm_simp_tac
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   176
val perm_full_simp_tac_i     = perm_simp_tac_gen_i full_simp_tac
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   177
val perm_asm_lr_simp_tac_i   = perm_simp_tac_gen_i asm_lr_simp_tac
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   178
val perm_asm_full_simp_tac_i = perm_simp_tac_gen_i asm_full_simp_tac
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   179
val eqvt_asm_full_simp_tac_i = eqvt_simp_tac_gen_i asm_full_simp_tac
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   180
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   181
(* applies the perm_compose rule such that                             *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   182
(*   pi o (pi' o lhs) = rhs                                            *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   183
(* is transformed to                                                   *) 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   184
(*  (pi o pi') o (pi' o lhs) = rhs                                     *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   185
(*                                                                     *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   186
(* this rule would loop in the simplifier, so some trick is used with  *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   187
(* generating perm_aux'es for the outermost permutation and then un-   *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   188
(* folding the definition                                              *)
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   189
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   190
fun perm_compose_simproc' sg ss redex =
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   191
  (case redex of
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   192
     (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37391
diff changeset
   193
       [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37391
diff changeset
   194
         Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ 
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   195
          pi2 $ t)) =>
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   196
    let
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   197
      val tname' = Long_Name.base_name tname
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   198
      val uname' = Long_Name.base_name uname
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   199
    in
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   200
      if pi1 <> pi2 then  (* only apply the composition rule in this case *)
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   201
        if T = U then    
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   202
          SOME (Drule.instantiate'
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   203
            [SOME (ctyp_of sg (fastype_of t))]
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   204
            [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38715
diff changeset
   205
            (mk_meta_eq ([Global_Theory.get_thm sg ("pt_"^tname'^"_inst"),
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38715
diff changeset
   206
             Global_Theory.get_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   207
        else
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   208
          SOME (Drule.instantiate'
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   209
            [SOME (ctyp_of sg (fastype_of t))]
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   210
            [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 38715
diff changeset
   211
            (mk_meta_eq (Global_Theory.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS 
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   212
             cp1_aux)))
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   213
      else NONE
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   214
    end
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   215
  | _ => NONE);
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   216
38715
6513ea67d95d renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents: 37678
diff changeset
   217
val perm_compose_simproc = Simplifier.simproc_global @{theory} "perm_compose"
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   218
  ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   219
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   220
fun perm_compose_tac ss i = 
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   221
  ("analysing permutation compositions on the lhs",
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   222
   fn st => EVERY
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   223
     [rtac trans i,
35232
f588e1169c8b renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents: 34885
diff changeset
   224
      asm_full_simp_tac (Simplifier.global_context (theory_of_thm st) empty_ss
25997
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   225
        addsimprocs [perm_compose_simproc]) i,
0c0f5d990d7d Cleaned up simproc code.
berghofe
parents: 24571
diff changeset
   226
      asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i] st);
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   227
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32149
diff changeset
   228
fun apply_cong_tac i = ("application of congruence", cong_tac i);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   229
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   230
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   231
(* unfolds the definition of permutations     *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   232
(* applied to functions such that             *)
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   233
(*     pi o f = rhs                           *)  
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   234
(* is transformed to                          *)
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   235
(*     %x. pi o (f ((rev pi) o x)) = rhs      *)
24519
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
   236
fun unfold_perm_fun_def_tac i =
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
   237
    ("unfolding of permutations on functions", 
5c435b2ea137 made theorem-references safe
urbanc
parents: 22808
diff changeset
   238
      rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   239
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   240
(* applies the ext-rule such that      *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   241
(*                                     *)
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   242
(*    f = g   goes to  /\x. f x = g x  *)
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   243
fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   244
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   245
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   246
(* perm_extend_simp_tac_i is perm_simp plus additional tactics        *)
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   247
(* to decide equation that come from support problems             *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   248
(* since it contains looping rules the "recursion" - depth is set *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   249
(* to 10 - this seems to be sufficient in most cases              *)
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   250
fun perm_extend_simp_tac_i tactical ss =
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   251
  let fun perm_extend_simp_tac_aux tactical ss n = 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
   252
          if n=0 then K all_tac
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
   253
          else DETERM o 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
   254
               (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   255
                       fn i => tactical (perm_simp asm_full_simp_tac ss i),
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
   256
                       fn i => tactical (perm_compose_tac ss i),
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
   257
                       fn i => tactical (apply_cong_tac i), 
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   258
                       fn i => tactical (unfold_perm_fun_def_tac i),
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   259
                       fn i => tactical (ext_fun_tac i)]
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32733
diff changeset
   260
                      THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ss (n-1))))
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   261
  in perm_extend_simp_tac_aux tactical ss 10 end;
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   262
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   263
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   264
(* tactic that tries to solve "supports"-goals; first it *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   265
(* unfolds the support definition and strips off the     *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   266
(* intros, then applies eqvt_simp_tac                    *)
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   267
fun supports_tac_i tactical ss i =
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   268
  let 
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35232
diff changeset
   269
     val simps        = [supports_def, Thm.symmetric fresh_def, fresh_prod]
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   270
  in
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   271
      EVERY [tactical ("unfolding of supports   ", simp_tac (HOL_basic_ss addsimps simps) i),
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   272
             tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   273
             tactical ("geting rid of the imps  ", rtac impI i),
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   274
             tactical ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   275
             tactical ("applying eqvt_simp      ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ss i )]
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   276
  end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   277
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   278
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   279
(* tactic that guesses the finite-support of a goal        *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   280
(* it first collects all free variables and tries to show  *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   281
(* that the support of these free variables (op supports)  *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   282
(* the goal                                                *)
20854
f9cf9e62d11c insert replacing ins ins_int ins_string
haftmann
parents: 20431
diff changeset
   283
fun collect_vars i (Bound j) vs = if j < i then vs else insert (op =) (Bound (j - i)) vs
f9cf9e62d11c insert replacing ins ins_int ins_string
haftmann
parents: 20431
diff changeset
   284
  | collect_vars i (v as Free _) vs = insert (op =) v vs
f9cf9e62d11c insert replacing ins ins_int ins_string
haftmann
parents: 20431
diff changeset
   285
  | collect_vars i (v as Var _) vs = insert (op =) v vs
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   286
  | collect_vars i (Const _) vs = vs
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   287
  | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   288
  | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   289
43278
1fbdcebb364b more robust exception pattern General.Subscript;
wenzelm
parents: 42364
diff changeset
   290
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   291
fun finite_guess_tac_i tactical ss i st =
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41489
diff changeset
   292
    let val goal = nth (cprems_of st) (i - 1)
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   293
    in
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26343
diff changeset
   294
      case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of
22274
ce1459004c8d Adapted to changes in Finite_Set theory.
berghofe
parents: 21669
diff changeset
   295
          _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   296
          let
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 22565
diff changeset
   297
            val cert = Thm.cterm_of (Thm.theory_of_thm st);
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   298
            val ps = Logic.strip_params (term_of goal);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   299
            val Ts = rev (map snd ps);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   300
            val vs = collect_vars 0 x [];
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 32960
diff changeset
   301
            val s = fold_rev (fn v => fn s =>
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   302
                HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 32960
diff changeset
   303
              vs HOLogic.unit;
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45620
diff changeset
   304
            val s' = fold_rev Term.abs ps
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45620
diff changeset
   305
              (Const ("Nominal.supp", fastype_of1 (Ts, s) -->
44692
ccfc7c193d2b modify nominal packages to better respect set/pred distinction
huffman
parents: 43278
diff changeset
   306
                Term.range_type T) $ s);
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   307
            val supports_rule' = Thm.lift_rule goal supports_rule;
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   308
            val _ $ (_ $ S $ _) =
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   309
              Logic.strip_assums_concl (hd (prems_of supports_rule'));
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   310
            val supports_rule'' = Drule.cterm_instantiate
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   311
              [(cert (head_of S), cert s')] supports_rule'
26343
0dd2eab7b296 simplified get_thm(s): back to plain name argument;
wenzelm
parents: 26338
diff changeset
   312
            val fin_supp = dynamic_thms st ("fin_supp")
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   313
            val ss' = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   314
          in
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   315
            (tactical ("guessing of the right supports-set",
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   316
                      EVERY [compose_tac (false, supports_rule'', 2) i,
19987
b97607d4d9a5 - put declarations inside a structure (NominalPermeq)
berghofe
parents: 19858
diff changeset
   317
                             asm_full_simp_tac ss' (i+1),
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   318
                             supports_tac_i tactical ss i])) st
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   319
          end
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   320
        | _ => Seq.empty
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   321
    end
43278
1fbdcebb364b more robust exception pattern General.Subscript;
wenzelm
parents: 42364
diff changeset
   322
    handle General.Subscript => Seq.empty
1fbdcebb364b more robust exception pattern General.Subscript;
wenzelm
parents: 42364
diff changeset
   323
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   324
22595
293934e41dfd make fresh_guess fail if it does not solve the subgoal
narboux
parents: 22578
diff changeset
   325
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   326
(* tactic that guesses whether an atom is fresh for an expression  *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   327
(* it first collects all free variables and tries to show that the *) 
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   328
(* support of these free variables (op supports) the goal          *)
43278
1fbdcebb364b more robust exception pattern General.Subscript;
wenzelm
parents: 42364
diff changeset
   329
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   330
fun fresh_guess_tac_i tactical ss i st =
19857
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   331
    let 
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 41489
diff changeset
   332
        val goal = nth (cprems_of st) (i - 1)
26343
0dd2eab7b296 simplified get_thm(s): back to plain name argument;
wenzelm
parents: 26338
diff changeset
   333
        val fin_supp = dynamic_thms st ("fin_supp")
0dd2eab7b296 simplified get_thm(s): back to plain name argument;
wenzelm
parents: 26338
diff changeset
   334
        val fresh_atm = dynamic_thms st ("fresh_atm")
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35232
diff changeset
   335
        val ss1 = ss addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   336
        val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
19857
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   337
    in
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   338
      case Logic.strip_assums_concl (term_of goal) of
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   339
          _ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => 
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   340
          let
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 22565
diff changeset
   341
            val cert = Thm.cterm_of (Thm.theory_of_thm st);
19857
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   342
            val ps = Logic.strip_params (term_of goal);
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   343
            val Ts = rev (map snd ps);
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   344
            val vs = collect_vars 0 t [];
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 32960
diff changeset
   345
            val s = fold_rev (fn v => fn s =>
19857
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   346
                HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 32960
diff changeset
   347
              vs HOLogic.unit;
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45620
diff changeset
   348
            val s' =
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45620
diff changeset
   349
              fold_rev Term.abs ps
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45620
diff changeset
   350
                (Const ("Nominal.supp", fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
19857
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   351
            val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   352
            val _ $ (_ $ S $ _) =
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   353
              Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   354
            val supports_fresh_rule'' = Drule.cterm_instantiate
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   355
              [(cert (head_of S), cert s')] supports_fresh_rule'
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   356
          in
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   357
            (tactical ("guessing of the right set that supports the goal", 
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   358
                      (EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
19993
e0a5783d708f added simplification rules to the fresh_guess tactic
urbanc
parents: 19987
diff changeset
   359
                             asm_full_simp_tac ss1 (i+2),
e0a5783d708f added simplification rules to the fresh_guess tactic
urbanc
parents: 19987
diff changeset
   360
                             asm_full_simp_tac ss2 (i+1), 
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   361
                             supports_tac_i tactical ss i]))) st
19857
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   362
          end
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   363
          (* when a term-constructor contains more than one binder, it is useful    *) 
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   364
          (* in nominal_primrecs to try whether the goal can be solved by an hammer *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   365
        | _ => (tactical ("if it is not of the form _\<sharp>_, then try the simplifier",   
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   366
                          (asm_full_simp_tac (HOL_ss addsimps [fresh_prod]@fresh_atm) i))) st
19857
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   367
    end
43278
1fbdcebb364b more robust exception pattern General.Subscript;
wenzelm
parents: 42364
diff changeset
   368
    handle General.Subscript => Seq.empty;
1fbdcebb364b more robust exception pattern General.Subscript;
wenzelm
parents: 42364
diff changeset
   369
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   370
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   371
val eqvt_simp_tac        = eqvt_asm_full_simp_tac_i NO_DEBUG_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   372
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   373
val perm_simp_tac        = perm_asm_full_simp_tac_i NO_DEBUG_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   374
val perm_extend_simp_tac = perm_extend_simp_tac_i NO_DEBUG_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   375
val supports_tac         = supports_tac_i NO_DEBUG_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   376
val finite_guess_tac     = finite_guess_tac_i NO_DEBUG_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   377
val fresh_guess_tac      = fresh_guess_tac_i NO_DEBUG_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   378
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   379
val dperm_simp_tac        = perm_asm_full_simp_tac_i DEBUG_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   380
val dperm_extend_simp_tac = perm_extend_simp_tac_i DEBUG_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   381
val dsupports_tac         = supports_tac_i DEBUG_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   382
val dfinite_guess_tac     = finite_guess_tac_i DEBUG_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   383
val dfresh_guess_tac      = fresh_guess_tac_i DEBUG_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   384
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   385
(* Code opied from the Simplifer for setting up the perm_simp method   *)
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   386
(* behaves nearly identical to the simp-method, for example can handle *)
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   387
(* options like (no_asm) etc.                                          *) 
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   388
val no_asmN = "no_asm";
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   389
val no_asm_useN = "no_asm_use";
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   390
val no_asm_simpN = "no_asm_simp";
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   391
val asm_lrN = "asm_lr";
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   392
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   393
val perm_simp_options =
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   394
 (Args.parens (Args.$$$ no_asmN) >> K (perm_simp_tac_i NO_DEBUG_tac) ||
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   395
  Args.parens (Args.$$$ no_asm_simpN) >> K (perm_asm_simp_tac_i NO_DEBUG_tac) ||
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   396
  Args.parens (Args.$$$ no_asm_useN) >> K (perm_full_simp_tac_i NO_DEBUG_tac) ||
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   397
  Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac) ||
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   398
  Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   399
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   400
val perm_simp_meth =
33554
4601372337e4 eliminated some unused/obsolete Args.bang_facts;
wenzelm
parents: 33244
diff changeset
   401
  Scan.lift perm_simp_options --| Method.sections (Simplifier.simp_modifiers') >>
4601372337e4 eliminated some unused/obsolete Args.bang_facts;
wenzelm
parents: 33244
diff changeset
   402
  (fn tac => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o tac (simpset_of ctxt)));
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   403
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   404
(* setup so that the simpset is used which is active at the moment when the tactic is called *)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   405
fun local_simp_meth_setup tac =
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   406
  Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32010
diff changeset
   407
  (K (SIMPLE_METHOD' o tac o simpset_of));
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   408
22595
293934e41dfd make fresh_guess fail if it does not solve the subgoal
narboux
parents: 22578
diff changeset
   409
(* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
293934e41dfd make fresh_guess fail if it does not solve the subgoal
narboux
parents: 22578
diff changeset
   410
22656
13302b2d0948 debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
narboux
parents: 22610
diff changeset
   411
fun basic_simp_meth_setup debug tac =
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   412
  Scan.depend (fn ctxt => Scan.succeed (Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt, ())) --
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   413
  Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
34885
6587c24ef6d8 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents: 33554
diff changeset
   414
  (K (SIMPLE_METHOD' o (if debug then tac else SOLVED' o tac) o simpset_of));
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22274
diff changeset
   415
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   416
val perm_simp_meth_debug        = local_simp_meth_setup dperm_simp_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   417
val perm_extend_simp_meth       = local_simp_meth_setup perm_extend_simp_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   418
val perm_extend_simp_meth_debug = local_simp_meth_setup dperm_extend_simp_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   419
val supports_meth               = local_simp_meth_setup supports_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   420
val supports_meth_debug         = local_simp_meth_setup dsupports_tac;
24571
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24519
diff changeset
   421
28322
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   422
val finite_guess_meth         = basic_simp_meth_setup false finite_guess_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   423
val finite_guess_meth_debug   = basic_simp_meth_setup true  dfinite_guess_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   424
val fresh_guess_meth          = basic_simp_meth_setup false fresh_guess_tac;
6f4cf302c798 made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents: 28262
diff changeset
   425
val fresh_guess_meth_debug    = basic_simp_meth_setup true  dfresh_guess_tac;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   426
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 19993
diff changeset
   427
end