author  urbanc 
Wed, 01 Mar 2006 18:26:20 +0100  
changeset 19169  20a73345dd6e 
parent 19163  b61039bf141f 
child 19350  2e1c7ca05ee0 
permissions  rwrr 
17870  1 
(* $Id$ *) 
2 

3 
(* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *) 

4 

5 
local 

6 

18012  7 
(* pulls out dynamically a thm via the simpset *) 
18434
a31e52a3e6ef
fixed a bug that occured when more than one atomtype
urbanc
parents:
18279
diff
changeset

8 
fun dynamic_thms ss name = 
a31e52a3e6ef
fixed a bug that occured when more than one atomtype
urbanc
parents:
18279
diff
changeset

9 
ProofContext.get_thms (Simplifier.the_context ss) (Name name); 
19139  10 
fun dynamic_thm ss name = 
11 
ProofContext.get_thm (Simplifier.the_context ss) (Name name); 

18012  12 

13 
(* initial simplification step in the tactic *) 

19139  14 
fun perm_eval_tac ss i = 
18012  15 
let 
19139  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  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  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  36 
 _ => 
37 
let 

38 
val name = Sign.base_name n 

39 
val at_inst = dynamic_thm ss ("at_"^name^"_inst") 

40 
val pt_inst = dynamic_thm ss ("pt_"^name^"_inst") 

41 
val perm_eq_app = thm "nominal.pt_fun_app_eq" 

42 
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end) 

19139  43 

44 
(* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *) 

19144  45 
 (Const("nominal.perm",_) $ pi $ (Abs _)) => 
46 
let 

19163  47 
val perm_fun_def = thm "nominal.perm_fun_def" 
19139  48 
in SOME (perm_fun_def) end 
49 

50 
(* no redex otherwise *) 

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

51 
 _ => NONE) end 
19139  52 

53 
val perm_eval = 

54 
Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 

55 
["nominal.perm pi x"] perm_eval_simproc; 

56 

18279
f7a18e2b10fc
made some of the theorem lookups static (by using
urbanc
parents:
18052
diff
changeset

57 
(* these lemmas are created dynamically according to the atom types *) 
19163  58 
val perm_swap = dynamic_thms ss "perm_swap" 
59 
val perm_fresh = dynamic_thms ss "perm_fresh_fresh" 

60 
val perm_bij = dynamic_thms ss "perm_bij" 

61 
val perm_compose' = dynamic_thms ss "perm_compose'" 

62 
val perm_pi_simp = dynamic_thms ss "perm_pi_simp" 

19139  63 
val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_compose'@perm_pi_simp) 
18012  64 
in 
19163  65 
("general simplification step", 
66 
FIRST [rtac conjI i, asm_full_simp_tac (ss' addsimprocs [perm_eval]) i]) 

18012  67 
end; 
17870  68 

18434
a31e52a3e6ef
fixed a bug that occured when more than one atomtype
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 atomtype
urbanc
parents:
18279
diff
changeset

70 
(* in case there are more atomtypes we have to check every possible instance *) 
19139  71 
(* of perm_compose *) 
18012  72 
fun apply_perm_compose_tac ss i = 
73 
let 

18434
a31e52a3e6ef
fixed a bug that occured when more than one atomtype
urbanc
parents:
18279
diff
changeset

74 
val perm_compose = dynamic_thms ss "perm_compose"; 
a31e52a3e6ef
fixed a bug that occured when more than one atomtype
urbanc
parents:
18279
diff
changeset

75 
val tacs = map (fn thm => (rtac (thm RS trans) i)) perm_compose 
18012  76 
in 
18434
a31e52a3e6ef
fixed a bug that occured when more than one atomtype
urbanc
parents:
18279
diff
changeset

77 
("analysing permutation compositions on the lhs",FIRST (tacs)) 
18012  78 
end 
79 

80 
(* applying Stefan's smart congruence tac *) 

81 
fun apply_cong_tac i = 

82 
("application of congruence", 

83 
(fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st)); 

17870  84 

85 
(* unfolds the definition of permutations applied to functions *) 

18012  86 
fun unfold_perm_fun_def_tac i = 
87 
let 

88 
val perm_fun_def = thm "nominal.perm_fun_def" 

89 
in 

90 
("unfolding of permutations on functions", 

91 
simp_tac (HOL_basic_ss addsimps [perm_fun_def]) i) 

17870  92 
end 
93 

18012  94 
(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *) 
95 
fun expand_fun_eq_tac i = 

96 
("extensionality expansion of functions", 

97 
EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) i, REPEAT_DETERM (rtac allI i)]); 

17870  98 

99 
(* debugging *) 

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  102 
fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
103 

104 
(* Main Tactic *) 

18012  105 

106 
fun perm_simp_tac tactical ss i = 

19139  107 
DETERM (tactical (perm_eval_tac ss i)); 
108 

19151  109 

110 
(* perm_simp_tac plus additional tactics to decide *) 

111 
(* support problems *) 

19163  112 
(* the "recursion"depth is set to 10  this seems sufficient *) 
19151  113 
fun perm_supports_tac tactical ss n = 
114 
if n=0 then K all_tac 

115 
else DETERM o 

116 
(FIRST'[fn i => tactical (perm_eval_tac ss i), 

19163  117 
fn i => tactical (apply_perm_compose_tac ss i), 
118 
fn i => tactical (apply_cong_tac i), 

119 
fn i => tactical (unfold_perm_fun_def_tac i), 

120 
fn i => tactical (expand_fun_eq_tac i)] 

19151  121 
THEN_ALL_NEW (TRY o (perm_supports_tac tactical ss (n1)))); 
17870  122 

19139  123 
(* tactic that first unfolds the support definition *) 
124 
(* and strips off the intros, then applies perm_supports_tac *) 

18012  125 
fun supports_tac tactical ss i = 
126 
let 

127 
val supports_def = thm "nominal.op supports_def"; 

128 
val fresh_def = thm "nominal.fresh_def"; 

129 
val fresh_prod = thm "nominal.fresh_prod"; 

130 
val simps = [supports_def,symmetric fresh_def,fresh_prod] 

17870  131 
in 
19151  132 
EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i), 
133 
tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)), 

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

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

136 
tactical ("applying perm_simp ", perm_supports_tac tactical ss 10 i)] 

17870  137 
end; 
138 

19151  139 

140 
(* tactic that guesses the finitesupport of a goal *) 

141 

142 
fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j  i) ins vs 

143 
 collect_vars i (v as Free _) vs = v ins vs 

144 
 collect_vars i (v as Var _) vs = v ins vs 

145 
 collect_vars i (Const _) vs = vs 

146 
 collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs 

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

148 

149 
val supports_rule = thm "supports_finite"; 

150 

151 
fun finite_guess_tac tactical ss i st = 

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

153 
in 

154 
case Logic.strip_assums_concl (term_of goal) of 

155 
_ $ (Const ("op :", _) $ (Const ("nominal.supp", T) $ x) $ 

156 
Const ("Finite_Set.Finites", _)) => 

157 
let 

158 
val cert = Thm.cterm_of (sign_of_thm st); 

159 
val ps = Logic.strip_params (term_of goal); 

160 
val Ts = rev (map snd ps); 

161 
val vs = collect_vars 0 x []; 

162 
val s = foldr (fn (v, s) => 

163 
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) 

164 
HOLogic.unit vs; 

165 
val s' = list_abs (ps, 

166 
Const ("nominal.supp", fastype_of1 (Ts, s) > body_type T) $ s); 

167 
val supports_rule' = Thm.lift_rule goal supports_rule; 

168 
val _ $ (_ $ S $ _) = 

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

170 
val supports_rule'' = Drule.cterm_instantiate 

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

172 
in 

173 
(tactical ("guessing of the right supportsset", 

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

175 
asm_full_simp_tac ss (i+1), 

176 
supports_tac tactical ss i])) st 

177 
end 

178 
 _ => Seq.empty 

179 
end 

180 
handle Subscript => Seq.empty 

181 

17870  182 
in 
183 

184 

18012  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  187 
(Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of); 
17870  188 

19151  189 
val perm_eq_meth = simp_meth_setup (perm_simp_tac NO_DEBUG_tac); 
190 
val perm_eq_meth_debug = simp_meth_setup (perm_simp_tac DEBUG_tac); 

191 
val supports_meth = simp_meth_setup (supports_tac NO_DEBUG_tac); 

192 
val supports_meth_debug = simp_meth_setup (supports_tac DEBUG_tac); 

193 
val finite_gs_meth = simp_meth_setup (finite_guess_tac NO_DEBUG_tac); 

194 
val finite_gs_meth_debug = simp_meth_setup (finite_guess_tac DEBUG_tac); 

17870  195 

196 
end 

197 

198 

199 