author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46219  426ed18eba43 
child 51717  9e7d1c139569 
permissions  rwrr 
19494  1 
(* Title: HOL/Nominal/nominal_permeq.ML 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

2 
Author: Christian Urban, TU Muenchen 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

3 
Author: Julien Narboux, TU Muenchen 
17870  4 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

5 
Methods for simplifying permutations and for analysing equations 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

6 
involving permutations. 
19494  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 
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

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

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

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

37 
val fresh_guess_tac : simpset > int > tactic 
17870  38 

30549  39 
val perm_simp_meth : (Proof.context > Proof.method) context_parser 
40 
val perm_simp_meth_debug : (Proof.context > Proof.method) context_parser 

41 
val perm_extend_simp_meth : (Proof.context > Proof.method) context_parser 

42 
val perm_extend_simp_meth_debug : (Proof.context > Proof.method) context_parser 

43 
val supports_meth : (Proof.context > Proof.method) context_parser 

44 
val supports_meth_debug : (Proof.context > Proof.method) context_parser 

45 
val finite_guess_meth : (Proof.context > Proof.method) context_parser 

46 
val finite_guess_meth_debug : (Proof.context > Proof.method) context_parser 

47 
val fresh_guess_meth : (Proof.context > Proof.method) context_parser 

48 
val fresh_guess_meth_debug : (Proof.context > Proof.method) context_parser 

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

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

50 

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

51 
structure NominalPermeq : NOMINAL_PERMEQ = 
b97607d4d9a5
 put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset

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

53 

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

54 
(* some lemmas needed below *) 
24519  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"} 

44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
43278
diff
changeset

59 
val perm_fun_def = Simpdata.mk_eq @{thm "Nominal.perm_fun_def"}; 
24519  60 
val perm_eq_app = @{thm "Nominal.pt_fun_app_eq"}; 
44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
43278
diff
changeset

61 
val supports_def = Simpdata.mk_eq @{thm "Nominal.supports_def"}; 
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
43278
diff
changeset

62 
val fresh_def = Simpdata.mk_eq @{thm "Nominal.fresh_def"}; 
24519  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 *) 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38715
diff
changeset

74 
fun dynamic_thms st name = Global_Theory.get_thms (theory_of_thm st) name; 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38715
diff
changeset

75 
fun dynamic_thm st name = Global_Theory.get_thm (theory_of_thm st) name; 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

76 

18012  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 

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

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

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

85 
CHANGED (EVERY [print_tac ("before "^msg), tac, print_tac ("after "^msg)]); 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

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

87 

19477  88 

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

89 
(* simproc that deals with instances of permutations in front *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

90 
(* of applications; just adding this rule to the simplifier *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

91 
(* would loop; it also needs careful tuning with the simproc *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

92 
(* for functions to avoid further possibilities for looping *) 
25997  93 
fun perm_simproc_app' sg ss redex = 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

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

95 
(* the "application" case is only applicable when the head of f is not a *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

96 
(* constant or when (f x) is a permuation with two or more arguments *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

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

98 
(case (strip_comb t) of 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

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

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

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

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

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

104 
(* case pi o (f x) == (pi o f) (pi o x) *) 
19494  105 
(Const("Nominal.perm", 
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset

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

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

108 
let 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

109 
val name = Long_Name.base_name n 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38715
diff
changeset

110 
val at_inst = Global_Theory.get_thm sg ("at_" ^ name ^ "_inst") 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38715
diff
changeset

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

112 
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

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

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

115 
end 
19139  116 

38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
37678
diff
changeset

117 
val perm_simproc_app = Simplifier.simproc_global @{theory} "perm_simproc_app" 
25997  118 
["Nominal.perm pi x"] perm_simproc_app'; 
119 

24519  120 
(* a simproc that deals with permutation instances in front of functions *) 
25997  121 
fun perm_simproc_fun' sg ss redex = 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

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

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

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

125 
(Abs _ ,[]) => true 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

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

127 
 (Const _, _) => true 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

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

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

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

131 
(* case pi o f == (%x. pi o (f ((rev pi)o x))) *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

132 
(Const("Nominal.perm",_) $ pi $ f) => 
44830  133 
(if applicable_fun f then SOME perm_fun_def else NONE) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

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

135 
end 
19139  136 

38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
37678
diff
changeset

137 
val perm_simproc_fun = Simplifier.simproc_global @{theory} "perm_simproc_fun" 
25997  138 
["Nominal.perm pi x"] perm_simproc_fun'; 
139 

28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

140 
(* function for simplyfying permutations *) 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

141 
(* stac contains the simplifiation tactic that is *) 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

142 
(* applied (see (no_asm) options below *) 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

143 
fun perm_simp_gen stac dyn_thms eqvt_thms ss i = 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

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

145 
let 
35232
f588e1169c8b
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents:
34885
diff
changeset

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

147 
addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms) 
25997  148 
addsimprocs [perm_simproc_fun, perm_simproc_app] 
45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
44830
diff
changeset

149 
> fold Simplifier.del_cong weak_congs 
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
44830
diff
changeset

150 
> fold Simplifier.add_cong strong_congs 
19477  151 
in 
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

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

153 
end); 
19477  154 

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

155 
(* general simplification of permutations and permutation that arose from eqvtproblems *) 
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

156 
fun perm_simp stac ss = 
22610  157 
let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"] 
158 
in 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

159 
perm_simp_gen stac simps [] ss 
22610  160 
end; 
161 

28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

162 
fun eqvt_simp stac ss = 
22610  163 
let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

164 
val eqvts_thms = NominalThmDecls.get_eqvt_thms (Simplifier.the_context ss); 
22610  165 
in 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

166 
perm_simp_gen stac simps eqvts_thms ss 
22610  167 
end; 
22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset

168 

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

169 

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

170 
(* main simplification tactics for permutations *) 
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

171 
fun perm_simp_tac_gen_i stac tactical ss i = DETERM (tactical (perm_simp stac ss i)); 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

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

173 

28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

174 
val perm_simp_tac_i = perm_simp_tac_gen_i simp_tac 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

175 
val perm_asm_simp_tac_i = perm_simp_tac_gen_i asm_simp_tac 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

176 
val perm_full_simp_tac_i = perm_simp_tac_gen_i full_simp_tac 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

177 
val perm_asm_lr_simp_tac_i = perm_simp_tac_gen_i asm_lr_simp_tac 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

178 
val perm_asm_full_simp_tac_i = perm_simp_tac_gen_i asm_full_simp_tac 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

179 
val eqvt_asm_full_simp_tac_i = eqvt_simp_tac_gen_i asm_full_simp_tac 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

180 

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

183 
(* is transformed to *) 

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

185 
(* *) 

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

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

188 
(* folding the definition *) 

25997  189 

190 
fun perm_compose_simproc' sg ss redex = 

191 
(case redex of 

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

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset

193 
[Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset

194 
Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ 
25997  195 
pi2 $ t)) => 
19477  196 
let 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

197 
val tname' = Long_Name.base_name tname 
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

198 
val uname' = Long_Name.base_name uname 
25997  199 
in 
200 
if pi1 <> pi2 then (* only apply the composition rule in this case *) 

201 
if T = U then 

202 
SOME (Drule.instantiate' 

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

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

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38715
diff
changeset

205 
(mk_meta_eq ([Global_Theory.get_thm sg ("pt_"^tname'^"_inst"), 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38715
diff
changeset

206 
Global_Theory.get_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux))) 
25997  207 
else 
208 
SOME (Drule.instantiate' 

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

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

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38715
diff
changeset

211 
(mk_meta_eq (Global_Theory.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS 
25997  212 
cp1_aux))) 
213 
else NONE 

214 
end 

215 
 _ => NONE); 

19477  216 

38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
37678
diff
changeset

217 
val perm_compose_simproc = Simplifier.simproc_global @{theory} "perm_compose" 
25997  218 
["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc'; 
19477  219 

25997  220 
fun perm_compose_tac ss i = 
221 
("analysing permutation compositions on the lhs", 

222 
fn st => EVERY 

223 
[rtac trans i, 

35232
f588e1169c8b
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents:
34885
diff
changeset

224 
asm_full_simp_tac (Simplifier.global_context (theory_of_thm st) empty_ss 
25997  225 
addsimprocs [perm_compose_simproc]) i, 
226 
asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i] st); 

18012  227 

32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32149
diff
changeset

228 
fun apply_cong_tac i = ("application of congruence", cong_tac i); 
17870  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 

28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

246 
(* perm_extend_simp_tac_i is perm_simp plus additional tactics *) 
19477  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 *) 

28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

250 
fun perm_extend_simp_tac_i tactical ss = 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

251 
let fun perm_extend_simp_tac_aux tactical ss n = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

252 
if n=0 then K all_tac 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

253 
else DETERM o 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

254 
(FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i), 
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

255 
fn i => tactical (perm_simp asm_full_simp_tac ss i), 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

256 
fn i => tactical (perm_compose_tac ss i), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

257 
fn i => tactical (apply_cong_tac i), 
19477  258 
fn i => tactical (unfold_perm_fun_def_tac i), 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

259 
fn i => tactical (ext_fun_tac i)] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32733
diff
changeset

260 
THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ss (n1)))) 
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

261 
in perm_extend_simp_tac_aux tactical ss 10 end; 
19151  262 

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

263 

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

264 
(* tactic that tries to solve "supports"goals; first it *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

265 
(* unfolds the support definition and strips off the *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

266 
(* intros, then applies eqvt_simp_tac *) 
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

267 
fun supports_tac_i tactical ss i = 
18012  268 
let 
36945  269 
val simps = [supports_def, Thm.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)), 

28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

275 
tactical ("applying eqvt_simp ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ss i )] 
17870  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 

43278  290 
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) 
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

291 
fun finite_guess_tac_i tactical ss i st = 
42364  292 
let val goal = nth (cprems_of st) (i  1) 
19151  293 
in 
26806  294 
case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of 
22274  295 
_ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) => 
19151  296 
let 
22578  297 
val cert = Thm.cterm_of (Thm.theory_of_thm st); 
19151  298 
val ps = Logic.strip_params (term_of goal); 
299 
val Ts = rev (map snd ps); 

300 
val vs = collect_vars 0 x []; 

33244  301 
val s = fold_rev (fn v => fn s => 
19151  302 
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) 
33244  303 
vs HOLogic.unit; 
46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset

304 
val s' = fold_rev Term.abs ps 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset

305 
(Const ("Nominal.supp", fastype_of1 (Ts, s) > 
44692
ccfc7c193d2b
modify nominal packages to better respect set/pred distinction
huffman
parents:
43278
diff
changeset

306 
Term.range_type T) $ s); 
19151  307 
val supports_rule' = Thm.lift_rule goal supports_rule; 
308 
val _ $ (_ $ S $ _) = 

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

310 
val supports_rule'' = Drule.cterm_instantiate 

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

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

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

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

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

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

317 
asm_full_simp_tac ss' (i+1), 
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

318 
supports_tac_i tactical ss i])) st 
19151  319 
end 
320 
 _ => Seq.empty 

321 
end 

43278  322 
handle General.Subscript => Seq.empty 
323 
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) 

19151  324 

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

325 

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

326 
(* tactic that guesses whether an atom is fresh for an expression *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

327 
(* it first collects all free variables and tries to show that the *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

328 
(* support of these free variables (op supports) the goal *) 
43278  329 
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) 
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

330 
fun fresh_guess_tac_i tactical ss i st = 
19857  331 
let 
42364  332 
val goal = nth (cprems_of st) (i  1) 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset

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

334 
val fresh_atm = dynamic_thms st ("fresh_atm") 
36945  335 
val ss1 = ss addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

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

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

340 
let 

22578  341 
val cert = Thm.cterm_of (Thm.theory_of_thm st); 
19857  342 
val ps = Logic.strip_params (term_of goal); 
343 
val Ts = rev (map snd ps); 

344 
val vs = collect_vars 0 t []; 

33244  345 
val s = fold_rev (fn v => fn s => 
19857  346 
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) 
33244  347 
vs HOLogic.unit; 
46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset

348 
val s' = 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset

349 
fold_rev Term.abs ps 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset

350 
(Const ("Nominal.supp", fastype_of1 (Ts, s) > HOLogic.mk_setT T) $ s); 
19857  351 
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule; 
352 
val _ $ (_ $ S $ _) = 

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

354 
val supports_fresh_rule'' = Drule.cterm_instantiate 

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

356 
in 

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

357 
(tactical ("guessing of the right set that supports the goal", 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

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

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

360 
asm_full_simp_tac ss2 (i+1), 
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

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

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

364 
(* in nominal_primrecs to try whether the goal can be solved by an hammer *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

365 
 _ => (tactical ("if it is not of the form _\<sharp>_, then try the simplifier", 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

366 
(asm_full_simp_tac (HOL_ss addsimps [fresh_prod]@fresh_atm) i))) st 
19857  367 
end 
43278  368 
handle General.Subscript => Seq.empty; 
369 
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) 

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

370 

28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

371 
val eqvt_simp_tac = eqvt_asm_full_simp_tac_i NO_DEBUG_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

372 

6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

373 
val perm_simp_tac = perm_asm_full_simp_tac_i NO_DEBUG_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

374 
val perm_extend_simp_tac = perm_extend_simp_tac_i NO_DEBUG_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

375 
val supports_tac = supports_tac_i NO_DEBUG_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

376 
val finite_guess_tac = finite_guess_tac_i NO_DEBUG_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

377 
val fresh_guess_tac = fresh_guess_tac_i NO_DEBUG_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

378 

6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

379 
val dperm_simp_tac = perm_asm_full_simp_tac_i DEBUG_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

380 
val dperm_extend_simp_tac = perm_extend_simp_tac_i DEBUG_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

381 
val dsupports_tac = supports_tac_i DEBUG_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

382 
val dfinite_guess_tac = finite_guess_tac_i DEBUG_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

383 
val dfresh_guess_tac = fresh_guess_tac_i DEBUG_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

384 

6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

385 
(* Code opied from the Simplifer for setting up the perm_simp method *) 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

386 
(* behaves nearly identical to the simpmethod, for example can handle *) 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

387 
(* options like (no_asm) etc. *) 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

388 
val no_asmN = "no_asm"; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

389 
val no_asm_useN = "no_asm_use"; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

390 
val no_asm_simpN = "no_asm_simp"; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

391 
val asm_lrN = "asm_lr"; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

392 

6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

393 
val perm_simp_options = 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

394 
(Args.parens (Args.$$$ no_asmN) >> K (perm_simp_tac_i NO_DEBUG_tac)  
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

395 
Args.parens (Args.$$$ no_asm_simpN) >> K (perm_asm_simp_tac_i NO_DEBUG_tac)  
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

396 
Args.parens (Args.$$$ no_asm_useN) >> K (perm_full_simp_tac_i NO_DEBUG_tac)  
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

397 
Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac)  
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

398 
Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac)); 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

399 

30549  400 
val perm_simp_meth = 
33554  401 
Scan.lift perm_simp_options  Method.sections (Simplifier.simp_modifiers') >> 
402 
(fn tac => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o tac (simpset_of ctxt))); 

28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

403 

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

404 
(* setup so that the simpset is used which is active at the moment when the tactic is called *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

405 
fun local_simp_meth_setup tac = 
30549  406 
Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >> 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32010
diff
changeset

407 
(K (SIMPLE_METHOD' o tac o simpset_of)); 
17870  408 

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

409 
(* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *) 
293934e41dfd
make fresh_guess fail if it does not solve the subgoal
narboux
parents:
22578
diff
changeset

410 

22656
13302b2d0948
debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
narboux
parents:
22610
diff
changeset

411 
fun basic_simp_meth_setup debug tac = 
30549  412 
Scan.depend (fn ctxt => Scan.succeed (Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt, ()))  
413 
Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >> 

34885
6587c24ef6d8
added SOLVED'  a more direct version of THEN_ALL_NEW (K no_tac)  strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents:
33554
diff
changeset

414 
(K (SIMPLE_METHOD' o (if debug then tac else SOLVED' o tac) o simpset_of)); 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset

415 

28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

416 
val perm_simp_meth_debug = local_simp_meth_setup dperm_simp_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

417 
val perm_extend_simp_meth = local_simp_meth_setup perm_extend_simp_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

418 
val perm_extend_simp_meth_debug = local_simp_meth_setup dperm_extend_simp_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

419 
val supports_meth = local_simp_meth_setup supports_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

420 
val supports_meth_debug = local_simp_meth_setup dsupports_tac; 
24571  421 

28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

422 
val finite_guess_meth = basic_simp_meth_setup false finite_guess_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

423 
val finite_guess_meth_debug = basic_simp_meth_setup true dfinite_guess_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

424 
val fresh_guess_meth = basic_simp_meth_setup false fresh_guess_tac; 
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset

425 
val fresh_guess_meth_debug = basic_simp_meth_setup true dfresh_guess_tac; 
17870  426 

20289  427 
end 