src/HOL/Nominal/nominal_permeq.ML
author berghofe
Mon, 12 Jun 2006 18:17:21 +0200
changeset 19857 a0c36e0fc897
parent 19494 2e909d5309f4
child 19858 d319e39a2e0e
permissions -rw-r--r--
Added fresh_guess_tac.
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
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
     2
    ID:         $Id$
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
     3
    Author:     Christian Urban, TU Muenchen
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     4
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
     5
Methods for simplifying permutations and
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
     6
for analysing equations involving permutations.
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
     7
*)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     8
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     9
local
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    10
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    11
(* pulls out dynamically a thm via the simpset *)
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    12
fun dynamic_thms ss name = ProofContext.get_thms (Simplifier.the_context ss) (Name name);
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    13
fun dynamic_thm ss name = ProofContext.get_thm (Simplifier.the_context ss) (Name name);
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    14
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    15
(* a tactic simplyfying permutations *)
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
    16
val perm_fun_def = thm "Nominal.perm_fun_def"
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
    17
val perm_eq_app = thm "Nominal.pt_fun_app_eq"
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    18
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    19
fun perm_eval_tac ss i =
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    20
    let
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    21
        fun perm_eval_simproc sg ss redex =
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    22
        let 
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    23
	   (* the "application" case below is only applicable when the head   *)
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    24
           (* of f is not a constant  or when it is a permuattion with two or *) 
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    25
           (* more arguments                                                  *)
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    26
           fun applicable t = 
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    27
	       (case (strip_comb t) of
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
    28
		  (Const ("Nominal.perm",_),ts) => (length ts) >= 2
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    29
		| (Const _,_) => false
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    30
		| _ => true)
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    31
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    32
	in
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    33
        (case redex of 
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    34
        (* case pi o (f x) == (pi o f) (pi o x)          *)
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    35
        (* special treatment according to the head of f  *)
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
    36
        (Const("Nominal.perm",
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    37
          Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    38
	   (case (applicable f) of
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    39
                false => NONE  
19163
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    40
              | _ => 
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    41
		let
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    42
		    val name = Sign.base_name n
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    43
		    val at_inst     = dynamic_thm ss ("at_"^name^"_inst")
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    44
		    val pt_inst     = dynamic_thm ss ("pt_"^name^"_inst")  
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    45
		in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end)
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    46
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    47
        (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
    48
        | (Const("Nominal.perm",_) $ pi $ (Abs _)) => SOME (perm_fun_def)
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    49
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    50
        (* no redex otherwise *) 
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    51
        | _ => NONE) end
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    52
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    53
	val perm_eval =
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    54
	    Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
    55
	    ["Nominal.perm pi x"] perm_eval_simproc;
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    56
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    57
      (* these lemmas are created dynamically according to the atom types *) 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    58
      val perm_swap        = dynamic_thms ss "perm_swap"
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    59
      val perm_fresh       = dynamic_thms ss "perm_fresh_fresh"
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    60
      val perm_bij         = dynamic_thms ss "perm_bij"
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    61
      val perm_pi_simp     = dynamic_thms ss "perm_pi_simp"
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    62
      val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    63
    in
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    64
	("general simplification step", asm_full_simp_tac (ss' addsimprocs [perm_eval]) i)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    65
    end;
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    66
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    67
(* applies the perm_compose rule such that                             *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    68
(*                                                                     *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    69
(*   pi o (pi' o lhs) = rhs                                            *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    70
(*                                                                     *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    71
(* is transformed to                                                   *) 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    72
(*                                                                     *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    73
(*  (pi o pi') o (pi' o lhs) = rhs                                     *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    74
(*                                                                     *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    75
(* this rule would loop in the simplifier, so some trick is used with  *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    76
(* generating perm_aux'es for the outermost permutation and then un-   *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    77
(* folding the definition                                              *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    78
val pt_perm_compose_aux = thm "pt_perm_compose_aux";
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    79
val cp1_aux             = thm "cp1_aux";
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    80
val perm_aux_fold       = thm "perm_aux_fold"; 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    81
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    82
fun perm_compose_tac ss i = 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    83
    let
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    84
	fun perm_compose_simproc sg ss redex =
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    85
	(case redex of
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
    86
           (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
    87
             [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    88
               Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    89
                pi2 $ t)) =>
19350
2e1c7ca05ee0 modified the perm_compose rule such that it
urbanc
parents: 19169
diff changeset
    90
        let
2e1c7ca05ee0 modified the perm_compose rule such that it
urbanc
parents: 19169
diff changeset
    91
	    val tname' = Sign.base_name tname
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    92
            val uname' = Sign.base_name uname
19350
2e1c7ca05ee0 modified the perm_compose rule such that it
urbanc
parents: 19169
diff changeset
    93
        in
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    94
            if pi1 <> pi2 then  (* only apply the composition rule in this case *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
    95
               if T = U then    
19350
2e1c7ca05ee0 modified the perm_compose rule such that it
urbanc
parents: 19169
diff changeset
    96
                SOME (Drule.instantiate'
2e1c7ca05ee0 modified the perm_compose rule such that it
urbanc
parents: 19169
diff changeset
    97
	              [SOME (ctyp_of sg (fastype_of t))]
2e1c7ca05ee0 modified the perm_compose rule such that it
urbanc
parents: 19169
diff changeset
    98
		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
2e1c7ca05ee0 modified the perm_compose rule such that it
urbanc
parents: 19169
diff changeset
    99
		      (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   100
	               PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose_aux)))
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   101
               else
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   102
                SOME (Drule.instantiate'
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   103
	              [SOME (ctyp_of sg (fastype_of t))]
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   104
		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   105
		      (mk_meta_eq (PureThy.get_thm sg (Name ("cp_"^tname'^"_"^uname'^"_inst")) RS 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   106
                       cp1_aux)))
19350
2e1c7ca05ee0 modified the perm_compose rule such that it
urbanc
parents: 19169
diff changeset
   107
            else NONE
2e1c7ca05ee0 modified the perm_compose rule such that it
urbanc
parents: 19169
diff changeset
   108
        end
2e1c7ca05ee0 modified the perm_compose rule such that it
urbanc
parents: 19169
diff changeset
   109
       | _ => NONE);
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   110
	  
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   111
      val perm_compose  =
19350
2e1c7ca05ee0 modified the perm_compose rule such that it
urbanc
parents: 19169
diff changeset
   112
	Simplifier.simproc (the_context()) "perm_compose" 
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
   113
	["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc;
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   114
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   115
      val ss' = Simplifier.theory_context (the_context ()) empty_ss	  
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   116
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   117
    in
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   118
	("analysing permutation compositions on the lhs",
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   119
         EVERY [rtac trans i,
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   120
                asm_full_simp_tac (ss' addsimprocs [perm_compose]) i,
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   121
                asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i])
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   122
    end
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   123
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   124
(* applying Stefan's smart congruence tac *)
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   125
fun apply_cong_tac i = 
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   126
    ("application of congruence",
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   127
     (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   128
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   129
(* unfolds the definition of permutations     *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   130
(* applied to functions such that             *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   131
(*                                            *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   132
(*   pi o f = rhs                             *)  
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   133
(*                                            *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   134
(* is transformed to                          *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   135
(*                                            *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   136
(*   %x. pi o (f ((rev pi) o x)) = rhs        *)
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   137
fun unfold_perm_fun_def_tac i = 
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   138
    let
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
   139
	val perm_fun_def = thm "Nominal.perm_fun_def"
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   140
    in
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   141
	("unfolding of permutations on functions", 
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   142
         rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   143
    end
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   144
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   145
(* applies the ext-rule such that      *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   146
(*                                     *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   147
(*    f = g    goes to /\x. f x = g x  *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   148
fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   149
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   150
(* FIXME FIXME FIXME *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   151
(* should be able to analyse pi o fresh_fun () = fresh_fun instances *) 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   152
fun fresh_fun_eqvt_tac i =
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   153
    let
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
   154
	val fresh_fun_equiv = thm "Nominal.fresh_fun_equiv_ineq"
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   155
    in
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   156
	("fresh_fun equivariance", rtac (fresh_fun_equiv RS trans) i)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   157
    end		       
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   158
		       
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   159
(* debugging *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   160
fun DEBUG_tac (msg,tac) = 
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
   161
    CHANGED (EVERY [tac, print_tac ("after "^msg)]); 
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   162
fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   163
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   164
(* Main Tactics *)
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   165
fun perm_simp_tac tactical ss i = 
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
   166
    DETERM (tactical (perm_eval_tac ss i));
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
   167
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   168
(* perm_full_simp_tac is perm_simp_tac plus additional tactics    *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   169
(* to decide equation that come from support problems             *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   170
(* since it contains looping rules the "recursion" - depth is set *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   171
(* to 10 - this seems to be sufficient in most cases              *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   172
fun perm_full_simp_tac tactical ss =
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   173
  let fun perm_full_simp_tac_aux tactical ss n = 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   174
	  if n=0 then K all_tac
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   175
	  else DETERM o 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   176
	       (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   177
                       fn i => tactical (perm_eval_tac ss i),
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   178
		       fn i => tactical (perm_compose_tac ss i),
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   179
		       fn i => tactical (apply_cong_tac i), 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   180
                       fn i => tactical (unfold_perm_fun_def_tac i),
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   181
                       fn i => tactical (ext_fun_tac i), 
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   182
                       fn i => tactical (fresh_fun_eqvt_tac i)]
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   183
		      THEN_ALL_NEW (TRY o (perm_full_simp_tac_aux tactical ss (n-1))))
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   184
  in perm_full_simp_tac_aux tactical ss 10 end;
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   185
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   186
(* tactic that first unfolds the support definition           *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   187
(* and strips off the intros, then applies perm_full_simp_tac *)
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   188
fun supports_tac tactical ss i =
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   189
  let 
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
   190
      val supports_def = thm "Nominal.op supports_def";
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
   191
      val fresh_def    = thm "Nominal.fresh_def";
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
   192
      val fresh_prod   = thm "Nominal.fresh_prod";
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   193
      val simps        = [supports_def,symmetric fresh_def,fresh_prod]
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   194
  in
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   195
      EVERY [tactical ("unfolding of supports   ", simp_tac (HOL_basic_ss addsimps simps) i),
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   196
             tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   197
             tactical ("geting rid of the imps  ", rtac impI i),
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   198
             tactical ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   199
             tactical ("applying perm_full_simp ", perm_full_simp_tac tactical ss i
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   200
                                                   (*perm_simp_tac tactical ss i*))]
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   201
  end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   202
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   203
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   204
(* tactic that guesses the finite-support of a goal       *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   205
(* it collects all free variables and tries to show       *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   206
(* that the support of these free variables (op supports) *)
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   207
(* the goal                                               *)
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   208
fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j - i) ins vs
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   209
  | collect_vars i (v as Free _) vs = v ins vs
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   210
  | collect_vars i (v as Var _) vs = v ins vs
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   211
  | collect_vars i (Const _) vs = vs
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   212
  | 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
   213
  | 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
   214
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   215
val supports_rule = thm "supports_finite";
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   216
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   217
fun finite_guess_tac tactical ss i st =
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   218
    let val goal = List.nth(cprems_of st, i-1)
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   219
    in
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   220
      case Logic.strip_assums_concl (term_of goal) of
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
   221
          _ $ (Const ("op :", _) $ (Const ("Nominal.supp", T) $ x) $
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   222
            Const ("Finite_Set.Finites", _)) =>
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   223
          let
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   224
            val cert = Thm.cterm_of (sign_of_thm st);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   225
            val ps = Logic.strip_params (term_of goal);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   226
            val Ts = rev (map snd ps);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   227
            val vs = collect_vars 0 x [];
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   228
            val s = foldr (fn (v, s) =>
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   229
                HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   230
              HOLogic.unit vs;
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   231
            val s' = list_abs (ps,
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
   232
              Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   233
            val supports_rule' = Thm.lift_rule goal supports_rule;
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   234
            val _ $ (_ $ S $ _) =
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   235
              Logic.strip_assums_concl (hd (prems_of supports_rule'));
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   236
            val supports_rule'' = Drule.cterm_instantiate
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   237
              [(cert (head_of S), cert s')] supports_rule'
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   238
          in
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   239
            (tactical ("guessing of the right supports-set",
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   240
                      EVERY [compose_tac (false, supports_rule'', 2) i,
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   241
                             asm_full_simp_tac ss (i+1),
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   242
                             supports_tac tactical ss i])) st
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   243
          end
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   244
        | _ => Seq.empty
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   245
    end
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   246
    handle Subscript => Seq.empty
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   247
19857
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   248
val supports_fresh_rule = thm "supports_fresh";
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   249
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   250
fun fresh_guess_tac tactical ss i st =
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   251
    let 
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   252
	val goal = List.nth(cprems_of st, i-1)
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   253
    in
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   254
      case Logic.strip_assums_concl (term_of goal) of
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   255
          _ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => 
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   256
          let
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   257
            val cert = Thm.cterm_of (sign_of_thm st);
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   258
            val ps = Logic.strip_params (term_of goal);
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   259
            val Ts = rev (map snd ps);
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   260
            val vs = collect_vars 0 t [];
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   261
            val s = foldr (fn (v, s) =>
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   262
                HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   263
              HOLogic.unit vs;
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   264
            val s' = list_abs (ps,
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   265
              Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   266
            val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   267
            val _ $ (_ $ S $ _) =
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   268
              Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   269
            val supports_fresh_rule'' = Drule.cterm_instantiate
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   270
              [(cert (head_of S), cert s')] supports_fresh_rule'
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   271
          in
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   272
            (tactical ("guessing of the right set that supports the goal",
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   273
                      EVERY [compose_tac (false, supports_fresh_rule'', 3) i(*,
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   274
                             asm_full_simp_tac ss (i+1),
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   275
                             supports_tac tactical ss i*)])) st
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   276
          end
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   277
        | _ => Seq.empty
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   278
    end
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   279
    handle Subscript => Seq.empty
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   280
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   281
in             
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   282
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   283
fun simp_meth_setup tac =
18046
b7389981170b Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
urbanc
parents: 18012
diff changeset
   284
  Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   285
  (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   286
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   287
val perm_eq_meth            = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   288
val perm_eq_meth_debug      = simp_meth_setup (perm_simp_tac DEBUG_tac);
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   289
val perm_full_eq_meth       = simp_meth_setup (perm_full_simp_tac NO_DEBUG_tac);
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   290
val perm_full_eq_meth_debug = simp_meth_setup (perm_full_simp_tac DEBUG_tac);
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   291
val supports_meth           = simp_meth_setup (supports_tac NO_DEBUG_tac);
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   292
val supports_meth_debug     = simp_meth_setup (supports_tac DEBUG_tac);
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   293
val finite_gs_meth          = simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
a95176d0f0dd isar-keywords.el
urbanc
parents: 19350
diff changeset
   294
val finite_gs_meth_debug    = simp_meth_setup (finite_guess_tac DEBUG_tac);
19857
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   295
val fresh_gs_meth           = simp_meth_setup (fresh_guess_tac NO_DEBUG_tac);
a0c36e0fc897 Added fresh_guess_tac.
berghofe
parents: 19494
diff changeset
   296
val fresh_gs_meth_debug     = simp_meth_setup (fresh_guess_tac DEBUG_tac);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   297
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   298
end
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   299
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   300
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   301