author  wenzelm 
Thu, 20 Mar 2008 00:20:44 +0100  
changeset 26343  0dd2eab7b296 
parent 26338  f8ed02f22433 
child 26806  40b411ec05aa 
permissions  rwrr 
19494  1 
(* Title: HOL/Nominal/nominal_permeq.ML 
2 
ID: $Id$ 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

3 
Authors: Christian Urban, Julien Narboux, TU Muenchen 
17870  4 

19494  5 
Methods for simplifying permutations and 
6 
for analysing equations involving permutations. 

7 
*) 

17870  8 

20431  9 
(* 
10 
FIXMES: 

11 

12 
 allow the user to give an explicit set S in the 

13 
fresh_guess tactic which is then verified 

14 

15 
 the perm_compose tactic does not do an "outermost 

16 
rewriting" and can therefore not deal with goals 

17 
like 

18 

19 
[(a,b)] o pi1 o pi2 = .... 

20 

21 
rather it tries to permute pi1 over pi2, which 

22 
results in a failure when used with the 

23 
perm_(full)_simp tactics 

24 

25 
*) 

26 

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  30 
val perm_simproc_fun : simproc 
31 
val perm_simproc_app : simproc 

32 

19987
b97607d4d9a5
 put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset

33 
val perm_simp_tac : simpset > int > tactic 
b97607d4d9a5
 put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset

34 
val perm_full_simp_tac : simpset > int > tactic 
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  38 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

39 
val perm_simp_meth : Method.src > Proof.context > Proof.method 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

40 
val perm_simp_meth_debug : Method.src > Proof.context > Proof.method 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

41 
val perm_full_simp_meth : Method.src > Proof.context > Proof.method 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

42 
val perm_full_simp_meth_debug : Method.src > Proof.context > Proof.method 
20289  43 
val supports_meth : Method.src > Proof.context > Proof.method 
44 
val supports_meth_debug : Method.src > Proof.context > Proof.method 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

45 
val finite_guess_meth : Method.src > Proof.context > Proof.method 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

46 
val finite_guess_meth_debug : Method.src > Proof.context > Proof.method 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

47 
val fresh_guess_meth : Method.src > Proof.context > Proof.method 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

48 
val fresh_guess_meth_debug : Method.src > Proof.context > Proof.method 
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  55 
val finite_emptyI = @{thm "finite.emptyI"}; 
56 
val finite_Un = @{thm "finite_Un"}; 

57 
val conj_absorb = @{thm "conj_absorb"}; 

58 
val not_false = @{thm "not_False_eq_True"} 

59 
val perm_fun_def = @{thm "Nominal.perm_fun_def"}; 

60 
val perm_eq_app = @{thm "Nominal.pt_fun_app_eq"}; 

61 
val supports_def = @{thm "Nominal.supports_def"}; 

62 
val fresh_def = @{thm "Nominal.fresh_def"}; 

63 
val fresh_prod = @{thm "Nominal.fresh_prod"}; 

64 
val fresh_unit = @{thm "Nominal.fresh_unit"}; 

65 
val supports_rule = @{thm "supports_finite"}; 

66 
val supp_prod = @{thm "supp_prod"}; 

67 
val supp_unit = @{thm "supp_unit"}; 

68 
val pt_perm_compose_aux = @{thm "pt_perm_compose_aux"}; 

69 
val cp1_aux = @{thm "cp1_aux"}; 

70 
val perm_aux_fold = @{thm "perm_aux_fold"}; 

71 
val supports_fresh_rule = @{thm "supports_fresh"}; 

21669  72 

19987
b97607d4d9a5
 put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset

73 
(* pulls out dynamically a thm via the proof state *) 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

74 
fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) name; 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

75 
fun dynamic_thm st name = PureThy.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  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  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  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 

24519  83 
(* FIXME comment *) 
22595
293934e41dfd
make fresh_guess fail if it does not solve the subgoal
narboux
parents:
22578
diff
changeset

84 
(* a tactical which fails if the tactic taken as an argument generates does not solve the sub goal i *) 
293934e41dfd
make fresh_guess fail if it does not solve the subgoal
narboux
parents:
22578
diff
changeset

85 
fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac); 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

86 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

87 
(* debugging *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

88 
fun DEBUG_tac (msg,tac) = 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

89 
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

90 
fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

91 

19477  92 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

93 
(* 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

94 
(* 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

95 
(* 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

96 
(* for functions to avoid further possibilities for looping *) 
25997  97 
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

98 
let 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

99 
(* 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

100 
(* 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

101 
fun applicable_app t = 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

102 
(case (strip_comb t) of 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

103 
(Const ("Nominal.perm",_),ts) => (length ts) >= 2 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

104 
 (Const _,_) => false 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

105 
 _ => true) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

106 
in 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

107 
case redex of 
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset

108 
(* case pi o (f x) == (pi o f) (pi o x) *) 
19494  109 
(Const("Nominal.perm", 
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset

110 
Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

111 
(if (applicable_app f) then 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

112 
let 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

113 
val name = Sign.base_name n 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

114 
val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst") 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

115 
val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst") 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

116 
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

117 
else NONE) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

118 
 _ => NONE 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

119 
end 
19139  120 

25997  121 
val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app" 
122 
["Nominal.perm pi x"] perm_simproc_app'; 

123 

24519  124 
(* a simproc that deals with permutation instances in front of functions *) 
25997  125 
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

126 
let 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

127 
fun applicable_fun t = 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

128 
(case (strip_comb t) of 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

129 
(Abs _ ,[]) => true 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

130 
 (Const ("Nominal.perm",_),_) => false 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

131 
 (Const _, _) => true 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

132 
 _ => false) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

133 
in 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

134 
case redex of 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

135 
(* 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

136 
(Const("Nominal.perm",_) $ pi $ f) => 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

137 
(if (applicable_fun f) then SOME (perm_fun_def) else NONE) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

138 
 _ => NONE 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

139 
end 
19139  140 

25997  141 
val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun" 
142 
["Nominal.perm pi x"] perm_simproc_fun'; 

143 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

144 
(* function for simplyfying permutations *) 
24571  145 
fun perm_simp_gen dyn_thms eqvt_thms ss i = 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

146 
("general simplification of permutations", fn st => 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

147 
let 
25997  148 
val ss' = Simplifier.theory_context (theory_of_thm st) ss 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

149 
addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms) 
25997  150 
delcongs weak_congs 
151 
addcongs strong_congs 

152 
addsimprocs [perm_simproc_fun, perm_simproc_app] 

19477  153 
in 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

154 
asm_full_simp_tac ss' i st 
19987
b97607d4d9a5
 put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset

155 
end); 
19477  156 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

157 
(* general simplification of permutations and permutation that arose from eqvtproblems *) 
24571  158 
fun perm_simp ss = 
22610  159 
let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"] 
160 
in 

24571  161 
perm_simp_gen simps [] ss 
22610  162 
end; 
163 

24571  164 
fun eqvt_simp ss = 
22610  165 
let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"] 
24571  166 
val eqvts_thms = NominalThmDecls.get_eqvt_thms (Simplifier.the_context ss); 
22610  167 
in 
24571  168 
perm_simp_gen simps eqvts_thms ss 
22610  169 
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

170 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

171 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

172 
(* main simplification tactics for permutations *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

173 
fun perm_simp_tac tactical ss i = DETERM (tactical (perm_simp ss i)); 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

174 
fun eqvt_simp_tac tactical ss i = DETERM (tactical (eqvt_simp ss i)); 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

175 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

176 

19477  177 
(* applies the perm_compose rule such that *) 
178 
(* pi o (pi' o lhs) = rhs *) 

179 
(* is transformed to *) 

180 
(* (pi o pi') o (pi' o lhs) = rhs *) 

181 
(* *) 

182 
(* this rule would loop in the simplifier, so some trick is used with *) 

183 
(* generating perm_aux'es for the outermost permutation and then un *) 

184 
(* folding the definition *) 

25997  185 

186 
fun perm_compose_simproc' sg ss redex = 

187 
(case redex of 

188 
(Const ("Nominal.perm", Type ("fun", [Type ("List.list", 

189 
[Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 

190 
Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 

191 
pi2 $ t)) => 

19477  192 
let 
25997  193 
val tname' = Sign.base_name tname 
194 
val uname' = Sign.base_name uname 

195 
in 

196 
if pi1 <> pi2 then (* only apply the composition rule in this case *) 

197 
if T = U then 

198 
SOME (Drule.instantiate' 

199 
[SOME (ctyp_of sg (fastype_of t))] 

200 
[SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)] 

26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

201 
(mk_meta_eq ([PureThy.get_thm sg ("pt_"^tname'^"_inst"), 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

202 
PureThy.get_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux))) 
25997  203 
else 
204 
SOME (Drule.instantiate' 

205 
[SOME (ctyp_of sg (fastype_of t))] 

206 
[SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)] 

26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

207 
(mk_meta_eq (PureThy.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS 
25997  208 
cp1_aux))) 
209 
else NONE 

210 
end 

211 
 _ => NONE); 

19477  212 

25997  213 
val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose" 
214 
["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc'; 

19477  215 

25997  216 
fun perm_compose_tac ss i = 
217 
("analysing permutation compositions on the lhs", 

218 
fn st => EVERY 

219 
[rtac trans i, 

220 
asm_full_simp_tac (Simplifier.theory_context (theory_of_thm st) empty_ss 

221 
addsimprocs [perm_compose_simproc]) i, 

222 
asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i] st); 

18012  223 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

224 

18012  225 
(* applying Stefan's smart congruence tac *) 
226 
fun apply_cong_tac i = 

227 
("application of congruence", 

19477  228 
(fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st)); 
17870  229 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

230 

19477  231 
(* unfolds the definition of permutations *) 
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  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  236 
fun unfold_perm_fun_def_tac i = 
237 
("unfolding of permutations on functions", 

238 
rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i) 

17870  239 

19477  240 
(* applies the extrule such that *) 
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  243 
fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i); 
17870  244 

245 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

246 
(* perm_full_simp_tac is perm_simp plus additional tactics *) 
19477  247 
(* to decide equation that come from support problems *) 
248 
(* since it contains looping rules the "recursion"  depth is set *) 

249 
(* to 10  this seems to be sufficient in most cases *) 

250 
fun perm_full_simp_tac tactical ss = 

251 
let fun perm_full_simp_tac_aux tactical ss n = 

252 
if n=0 then K all_tac 

253 
else DETERM o 

254 
(FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i), 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

255 
fn i => tactical (perm_simp ss i), 
19477  256 
fn i => tactical (perm_compose_tac ss i), 
257 
fn i => tactical (apply_cong_tac i), 

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)] 
19477  260 
THEN_ALL_NEW (TRY o (perm_full_simp_tac_aux tactical ss (n1)))) 
261 
in perm_full_simp_tac_aux tactical ss 10 end; 

19151  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 *) 
18012  267 
fun supports_tac tactical ss i = 
268 
let 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

269 
val simps = [supports_def,symmetric fresh_def,fresh_prod] 
17870  270 
in 
19477  271 
EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i), 
272 
tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)), 

273 
tactical ("geting rid of the imps ", rtac impI i), 

274 
tactical ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)), 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

275 
tactical ("applying eqvt_simp ", eqvt_simp_tac tactical ss i )] 
17870  276 
end; 
277 

19151  278 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

279 
(* tactic that guesses the finitesupport 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  283 
fun collect_vars i (Bound j) vs = if j < i then vs else insert (op =) (Bound (j  i)) vs 
284 
 collect_vars i (v as Free _) vs = insert (op =) v vs 

285 
 collect_vars i (v as Var _) vs = insert (op =) v vs 

19151  286 
 collect_vars i (Const _) vs = vs 
287 
 collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs 

288 
 collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs); 

289 

290 
fun finite_guess_tac tactical ss i st = 

291 
let val goal = List.nth(cprems_of st, i1) 

292 
in 

293 
case Logic.strip_assums_concl (term_of goal) of 

22274  294 
_ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) => 
19151  295 
let 
22578  296 
val cert = Thm.cterm_of (Thm.theory_of_thm st); 
19151  297 
val ps = Logic.strip_params (term_of goal); 
298 
val Ts = rev (map snd ps); 

299 
val vs = collect_vars 0 x []; 

21078  300 
val s = Library.foldr (fn (v, s) => 
19151  301 
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) 
21078  302 
(vs, HOLogic.unit); 
19151  303 
val s' = list_abs (ps, 
19494  304 
Const ("Nominal.supp", fastype_of1 (Ts, s) > body_type T) $ s); 
19151  305 
val supports_rule' = Thm.lift_rule goal supports_rule; 
306 
val _ $ (_ $ S $ _) = 

307 
Logic.strip_assums_concl (hd (prems_of supports_rule')); 

308 
val supports_rule'' = Drule.cterm_instantiate 

309 
[(cert (head_of S), cert s')] supports_rule' 

26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

310 
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

311 
val ss' = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp 
19151  312 
in 
313 
(tactical ("guessing of the right supportsset", 

314 
EVERY [compose_tac (false, supports_rule'', 2) i, 

19987
b97607d4d9a5
 put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset

315 
asm_full_simp_tac ss' (i+1), 
19151  316 
supports_tac tactical ss i])) st 
317 
end 

318 
 _ => Seq.empty 

319 
end 

320 
handle Subscript => Seq.empty 

321 

22595
293934e41dfd
make fresh_guess fail if it does not solve the subgoal
narboux
parents:
22578
diff
changeset

322 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

323 
(* 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

324 
(* 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

325 
(* support of these free variables (op supports) the goal *) 
19857  326 
fun fresh_guess_tac tactical ss i st = 
327 
let 

328 
val goal = List.nth(cprems_of st, i1) 

26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

329 
val fin_supp = dynamic_thms st ("fin_supp") 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

330 
val fresh_atm = dynamic_thms st ("fresh_atm") 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

331 
val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

332 
val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp 
19857  333 
in 
334 
case Logic.strip_assums_concl (term_of goal) of 

335 
_ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => 

336 
let 

22578  337 
val cert = Thm.cterm_of (Thm.theory_of_thm st); 
19857  338 
val ps = Logic.strip_params (term_of goal); 
339 
val Ts = rev (map snd ps); 

340 
val vs = collect_vars 0 t []; 

21078  341 
val s = Library.foldr (fn (v, s) => 
19857  342 
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) 
21078  343 
(vs, HOLogic.unit); 
19857  344 
val s' = list_abs (ps, 
345 
Const ("Nominal.supp", fastype_of1 (Ts, s) > (HOLogic.mk_setT T)) $ s); 

346 
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule; 

347 
val _ $ (_ $ S $ _) = 

348 
Logic.strip_assums_concl (hd (prems_of supports_fresh_rule')); 

349 
val supports_fresh_rule'' = Drule.cterm_instantiate 

350 
[(cert (head_of S), cert s')] supports_fresh_rule' 

351 
in 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

352 
(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

353 
(EVERY [compose_tac (false, supports_fresh_rule'', 3) i, 
19993
e0a5783d708f
added simplification rules to the fresh_guess tactic
urbanc
parents:
19987
diff
changeset

354 
asm_full_simp_tac ss1 (i+2), 
e0a5783d708f
added simplification rules to the fresh_guess tactic
urbanc
parents:
19987
diff
changeset

355 
asm_full_simp_tac ss2 (i+1), 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

356 
supports_tac tactical ss i]))) st 
19857  357 
end 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

358 
(* when a termconstructor 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

359 
(* 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

360 
 _ => (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

361 
(asm_full_simp_tac (HOL_ss addsimps [fresh_prod]@fresh_atm) i))) st 
19857  362 
end 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

363 
handle Subscript => Seq.empty; 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

364 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

365 
(* 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

366 
fun local_simp_meth_setup tac = 
18046
b7389981170b
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
urbanc
parents:
18012
diff
changeset

367 
Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

368 
(Method.SIMPLE_METHOD' o tac o local_simpset_of) ; 
17870  369 

22595
293934e41dfd
make fresh_guess fail if it does not solve the subgoal
narboux
parents:
22578
diff
changeset

370 
(* 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

371 

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

372 
fun basic_simp_meth_setup debug tac = 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

373 
Method.sectioned_args 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

374 
(fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l))) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

375 
(Simplifier.simp_modifiers' @ Splitter.split_modifiers) 
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

376 
(fn _ => Method.SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of); 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

377 

17870  378 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

379 
val perm_simp_meth = local_simp_meth_setup (perm_simp_tac NO_DEBUG_tac); 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

380 
val perm_simp_meth_debug = local_simp_meth_setup (perm_simp_tac DEBUG_tac); 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

381 
val perm_full_simp_meth = local_simp_meth_setup (perm_full_simp_tac NO_DEBUG_tac); 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

382 
val perm_full_simp_meth_debug = local_simp_meth_setup (perm_full_simp_tac DEBUG_tac); 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

383 
val supports_meth = local_simp_meth_setup (supports_tac NO_DEBUG_tac); 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

384 
val supports_meth_debug = local_simp_meth_setup (supports_tac DEBUG_tac); 
24571  385 

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

386 
val finite_guess_meth = basic_simp_meth_setup false (finite_guess_tac NO_DEBUG_tac); 
13302b2d0948
debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
narboux
parents:
22610
diff
changeset

387 
val finite_guess_meth_debug = basic_simp_meth_setup true (finite_guess_tac DEBUG_tac); 
13302b2d0948
debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
narboux
parents:
22610
diff
changeset

388 
val fresh_guess_meth = basic_simp_meth_setup false (fresh_guess_tac NO_DEBUG_tac); 
13302b2d0948
debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
narboux
parents:
22610
diff
changeset

389 
val fresh_guess_meth_debug = basic_simp_meth_setup true (fresh_guess_tac DEBUG_tac); 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

390 

19987
b97607d4d9a5
 put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset

391 
val perm_simp_tac = perm_simp_tac NO_DEBUG_tac; 
b97607d4d9a5
 put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset

392 
val perm_full_simp_tac = perm_full_simp_tac NO_DEBUG_tac; 
b97607d4d9a5
 put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset

393 
val supports_tac = supports_tac NO_DEBUG_tac; 
b97607d4d9a5
 put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset

394 
val finite_guess_tac = finite_guess_tac NO_DEBUG_tac; 
b97607d4d9a5
 put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset

395 
val fresh_guess_tac = fresh_guess_tac NO_DEBUG_tac; 
17870  396 

20289  397 
end 