src/HOL/Nominal/nominal_permeq.ML
author urbanc
Wed, 01 Mar 2006 18:26:20 +0100
changeset 19169 20a73345dd6e
parent 19163 b61039bf141f
child 19350 2e1c7ca05ee0
permissions -rw-r--r--
fixed a problem where a permutation is not analysed when the term is of the form (pi o f) x1...xn This was the case because the head of this term is the constant "nominal.perm". Now an applicability predicate decides the right behaviour of the simproc
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     1
(* $Id$ *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     2
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     3
(* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     4
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     5
local
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     6
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
     7
(* pulls out dynamically a thm via the simpset *)
18434
a31e52a3e6ef fixed a bug that occured when more than one atom-type
urbanc
parents: 18279
diff changeset
     8
fun dynamic_thms ss name = 
a31e52a3e6ef fixed a bug that occured when more than one atom-type
urbanc
parents: 18279
diff changeset
     9
    ProofContext.get_thms (Simplifier.the_context ss) (Name name);
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    10
fun dynamic_thm ss name = 
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    11
    ProofContext.get_thm (Simplifier.the_context ss) (Name name);
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    12
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    13
(* initial simplification step in the tactic *)
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    14
fun perm_eval_tac ss i =
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    15
    let
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    16
        fun perm_eval_simproc sg ss redex =
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    17
        let 
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    18
	   
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    19
           (* the "application" case below is only applicable when the head   *)
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    20
           (* 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
    21
           (* more arguments                                                  *)
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    22
           fun applicable t = 
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    23
	       (case (strip_comb t) of
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    24
		  (Const ("nominal.perm",_),ts) => (length ts) >= 2
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    25
		| (Const _,_) => false
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    26
		| _ => true)
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    27
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    28
	in
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    29
        (case redex of 
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    30
        (* 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
    31
        (* special treatment according to the head of f  *)
19144
9c8793c62d0c added support for arbitrary atoms in the simproc
urbanc
parents: 19139
diff changeset
    32
        (Const("nominal.perm",
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    33
          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
    34
	   (case (applicable f) of
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
    35
                false => NONE  
19163
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    36
              | _ => 
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    37
		let
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    38
		    val name = Sign.base_name n
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    39
		    val at_inst     = dynamic_thm ss ("at_"^name^"_inst")
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    40
		    val pt_inst     = dynamic_thm ss ("pt_"^name^"_inst")  
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    41
		    val perm_eq_app = thm "nominal.pt_fun_app_eq"	  
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    42
		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
    43
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    44
        (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
19144
9c8793c62d0c added support for arbitrary atoms in the simproc
urbanc
parents: 19139
diff changeset
    45
        | (Const("nominal.perm",_) $ pi $ (Abs _)) => 
9c8793c62d0c added support for arbitrary atoms in the simproc
urbanc
parents: 19139
diff changeset
    46
           let 
19163
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    47
               val perm_fun_def = thm "nominal.perm_fun_def"
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    48
           in SOME (perm_fun_def) end
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" 
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    55
	    ["nominal.perm pi x"] perm_eval_simproc;
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    56
18279
f7a18e2b10fc made some of the theorem look-ups static (by using
urbanc
parents: 18052
diff changeset
    57
        (* these lemmas are created dynamically according to the atom types *) 
19163
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    58
	val perm_swap     = dynamic_thms ss "perm_swap"
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    59
	val perm_fresh    = dynamic_thms ss "perm_fresh_fresh"
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    60
        val perm_bij      = dynamic_thms ss "perm_bij"
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    61
        val perm_compose' = dynamic_thms ss "perm_compose'"
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    62
        val perm_pi_simp  = dynamic_thms ss "perm_pi_simp"
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    63
        val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_compose'@perm_pi_simp)
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    64
    in
19163
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    65
      ("general simplification step", 
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
    66
        FIRST [rtac conjI i, asm_full_simp_tac (ss' addsimprocs [perm_eval]) i])
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    67
    end;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    68
18434
a31e52a3e6ef fixed a bug that occured when more than one atom-type
urbanc
parents: 18279
diff changeset
    69
(* applies the perm_compose rule - this rule would loop in the simplifier     *)
a31e52a3e6ef fixed a bug that occured when more than one atom-type
urbanc
parents: 18279
diff changeset
    70
(* in case there are more atom-types we have to check every possible instance *)
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
    71
(* of perm_compose                                                            *)
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    72
fun apply_perm_compose_tac ss i = 
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    73
    let
18434
a31e52a3e6ef fixed a bug that occured when more than one atom-type
urbanc
parents: 18279
diff changeset
    74
	val perm_compose = dynamic_thms ss "perm_compose"; 
a31e52a3e6ef fixed a bug that occured when more than one atom-type
urbanc
parents: 18279
diff changeset
    75
        val tacs = map (fn thm => (rtac (thm RS trans) i)) perm_compose
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    76
    in
18434
a31e52a3e6ef fixed a bug that occured when more than one atom-type
urbanc
parents: 18279
diff changeset
    77
	("analysing permutation compositions on the lhs",FIRST (tacs))
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    78
    end
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    79
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    80
(* applying Stefan's smart congruence tac *)
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    81
fun apply_cong_tac i = 
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    82
    ("application of congruence",
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    83
     (fn st => DatatypeAux.cong_tac  i st handle Subscript => no_tac st));
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    84
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    85
(* unfolds the definition of permutations applied to functions *)
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    86
fun unfold_perm_fun_def_tac i = 
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    87
    let
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    88
	val perm_fun_def = thm "nominal.perm_fun_def"
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    89
    in
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    90
	("unfolding of permutations on functions", 
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    91
	 simp_tac (HOL_basic_ss addsimps [perm_fun_def]) i)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    92
    end
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    93
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    94
(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    95
fun expand_fun_eq_tac i =    
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    96
    ("extensionality expansion of functions",
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
    97
    EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) i, REPEAT_DETERM (rtac allI i)]);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    98
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    99
(* debugging *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   100
fun DEBUG_tac (msg,tac) = 
19169
20a73345dd6e fixed a problem where a permutation is not analysed
urbanc
parents: 19163
diff changeset
   101
    CHANGED (EVERY [tac, print_tac ("after "^msg)]); 
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   102
fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   103
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   104
(* Main Tactic *)
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   105
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   106
fun perm_simp_tac tactical ss i = 
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
   107
    DETERM (tactical (perm_eval_tac ss i));
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
   108
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   109
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   110
(* perm_simp_tac plus additional tactics to decide            *)
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   111
(* support problems                                           *)
19163
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
   112
(* the "recursion"-depth is set to 10 - this seems sufficient *)
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   113
fun perm_supports_tac tactical ss n = 
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   114
    if n=0 then K all_tac
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   115
    else DETERM o 
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   116
         (FIRST'[fn i => tactical (perm_eval_tac ss i),
19163
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
   117
                 fn i => tactical (apply_perm_compose_tac ss i),
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
   118
		 fn i => tactical (apply_cong_tac i), 
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
   119
                 fn i => tactical (unfold_perm_fun_def_tac i),
b61039bf141f made some small tunings in the decision-procedure
urbanc
parents: 19151
diff changeset
   120
		 fn i => tactical (expand_fun_eq_tac i)]
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   121
         THEN_ALL_NEW (TRY o (perm_supports_tac tactical ss (n-1))));
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   122
19139
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
   123
(* tactic that first unfolds the support definition          *)
af69e41eab5d improved the decision-procedure for permutations;
urbanc
parents: 18434
diff changeset
   124
(* and strips off the intros, then applies perm_supports_tac *)
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   125
fun supports_tac tactical ss i =
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   126
  let 
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   127
      val supports_def = thm "nominal.op supports_def";
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   128
      val fresh_def    = thm "nominal.fresh_def";
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   129
      val fresh_prod   = thm "nominal.fresh_prod";
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   130
      val simps        = [supports_def,symmetric fresh_def,fresh_prod]
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   131
  in
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   132
      EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i),
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   133
             tactical ("stripping of foralls  ", REPEAT_DETERM (rtac allI i)),
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   134
             tactical ("geting rid of the imps", rtac impI i),
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   135
             tactical ("eliminating conjuncts ", REPEAT_DETERM (etac  conjE i)),
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   136
             tactical ("applying perm_simp    ", perm_supports_tac tactical ss 10 i)]
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   137
  end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   138
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   139
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   140
(* tactic that guesses the finite-support of a goal *)
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   141
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   142
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
   143
  | collect_vars i (v as Free _) vs = v ins vs
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   144
  | collect_vars i (v as Var _) vs = v ins vs
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   145
  | collect_vars i (Const _) vs = vs
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   146
  | 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
   147
  | 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
   148
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   149
val supports_rule = thm "supports_finite";
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   150
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   151
fun finite_guess_tac tactical ss i st =
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   152
    let val goal = List.nth(cprems_of st, i-1)
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   153
    in
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   154
      case Logic.strip_assums_concl (term_of goal) of
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   155
          _ $ (Const ("op :", _) $ (Const ("nominal.supp", T) $ x) $
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   156
            Const ("Finite_Set.Finites", _)) =>
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   157
          let
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   158
            val cert = Thm.cterm_of (sign_of_thm st);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   159
            val ps = Logic.strip_params (term_of goal);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   160
            val Ts = rev (map snd ps);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   161
            val vs = collect_vars 0 x [];
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   162
            val s = foldr (fn (v, s) =>
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   163
                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
   164
              HOLogic.unit vs;
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   165
            val s' = list_abs (ps,
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   166
              Const ("nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   167
            val supports_rule' = Thm.lift_rule goal supports_rule;
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   168
            val _ $ (_ $ S $ _) =
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   169
              Logic.strip_assums_concl (hd (prems_of supports_rule'));
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   170
            val supports_rule'' = Drule.cterm_instantiate
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   171
              [(cert (head_of S), cert s')] supports_rule'
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   172
          in
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   173
            (tactical ("guessing of the right supports-set",
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   174
                      EVERY [compose_tac (false, supports_rule'', 2) i,
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   175
                             asm_full_simp_tac ss (i+1),
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   176
                             supports_tac tactical ss i])) st
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   177
          end
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   178
        | _ => Seq.empty
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   179
    end
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   180
    handle Subscript => Seq.empty
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   181
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   182
in             
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   183
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   184
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   185
fun simp_meth_setup tac =
18046
b7389981170b Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
urbanc
parents: 18012
diff changeset
   186
  Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
18012
23e6cfda8c4b Added (optional) arguments to the tactics
urbanc
parents: 17870
diff changeset
   187
  (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   188
19151
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   189
val perm_eq_meth         = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   190
val perm_eq_meth_debug   = simp_meth_setup (perm_simp_tac DEBUG_tac);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   191
val supports_meth        = simp_meth_setup (supports_tac NO_DEBUG_tac);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   192
val supports_meth_debug  = simp_meth_setup (supports_tac DEBUG_tac);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   193
val finite_gs_meth       = simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
66e841b1001e added a finite_guess tactic, which solves
urbanc
parents: 19144
diff changeset
   194
val finite_gs_meth_debug = simp_meth_setup (finite_guess_tac DEBUG_tac);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   195
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   196
end
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   197
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   198
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   199