author  huffman 
Fri, 27 Apr 2012 14:07:31 +0200  
changeset 47789  71a526ee569a 
parent 47658  7631f6f7873d 
child 47803  2e3821e13d67 
permissions  rwrr 
47325  1 
(* Title: HOL/Tools/transfer.ML 
2 
Author: Brian Huffman, TU Muenchen 

3 

4 
Generic theorem transfer method. 

5 
*) 

6 

7 
signature TRANSFER = 

8 
sig 

9 
val prep_conv: conv 

47503  10 
val get_relator_eq: Proof.context > thm list 
47325  11 
val transfer_add: attribute 
12 
val transfer_del: attribute 

47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47635
diff
changeset

13 
val transfer_tac: bool > Proof.context > int > tactic 
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47618
diff
changeset

14 
val transfer_prover_tac: Proof.context > int > tactic 
47325  15 
val setup: theory > theory 
16 
end 

17 

18 
structure Transfer : TRANSFER = 

19 
struct 

20 

21 
structure Data = Named_Thms 

22 
( 

23 
val name = @{binding transfer_raw} 

47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47618
diff
changeset

24 
val description = "raw transfer rule for transfer method" 
47325  25 
) 
26 

47503  27 
structure Relator_Eq = Named_Thms 
28 
( 

29 
val name = @{binding relator_eq} 

30 
val description = "relator equality rule (used by transfer method)" 

31 
) 

32 

33 
fun get_relator_eq ctxt = 

34 
map (Thm.symmetric o mk_meta_eq) (Relator_Eq.get ctxt) 

35 

47325  36 
(** Conversions **) 
37 

38 
val Rel_rule = Thm.symmetric @{thm Rel_def} 

39 

40 
fun dest_funcT cT = 

41 
(case Thm.dest_ctyp cT of [T, U] => (T, U) 

42 
 _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], [])) 

43 

44 
fun Rel_conv ct = 

45 
let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct) 

46 
val (cU, _) = dest_funcT cT' 

47 
in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end 

48 

49 
fun Trueprop_conv cv ct = 

50 
(case Thm.term_of ct of 

51 
Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct 

52 
 _ => raise CTERM ("Trueprop_conv", [ct])) 

53 

47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47618
diff
changeset

54 
(* Conversion to preprocess a transfer rule *) 
47325  55 
fun prep_conv ct = ( 
56 
Conv.implies_conv Conv.all_conv prep_conv 

57 
else_conv 

58 
Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) 

59 
else_conv 

60 
Conv.all_conv) ct 

61 

62 
(** Transfer proof method **) 

63 

64 
fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y 

47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

65 
 RelT t = raise TERM ("RelT", [t]) 
47325  66 

67 
(* Tactic to correspond a value to itself *) 

68 
fun eq_tac ctxt = SUBGOAL (fn (t, i) => 

69 
let 

70 
val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t)) 

71 
val cT = ctyp_of (Proof_Context.theory_of ctxt) T 

47503  72 
val rews = get_relator_eq ctxt 
47325  73 
val thm1 = Drule.instantiate' [SOME cT] [] @{thm Rel_eq_refl} 
74 
val thm2 = Raw_Simplifier.rewrite_rule rews thm1 

75 
in 

76 
rtac thm2 i 

77 
end handle Match => no_tac  TERM _ => no_tac) 

78 

47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47327
diff
changeset

79 
val post_simps = 
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

80 
@{thms transfer_forall_eq [symmetric] 
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47327
diff
changeset

81 
transfer_implies_eq [symmetric] transfer_bforall_unfold} 
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47327
diff
changeset

82 

47356
19fb95255ec9
transfer method generalizes over free variables in goal
huffman
parents:
47355
diff
changeset

83 
fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) => 
19fb95255ec9
transfer method generalizes over free variables in goal
huffman
parents:
47355
diff
changeset

84 
let 
19fb95255ec9
transfer method generalizes over free variables in goal
huffman
parents:
47355
diff
changeset

85 
val vs = rev (Term.add_frees t []) 
47568
98c8b7542b72
add option to transfer method for specifying variables not to generalize over
huffman
parents:
47523
diff
changeset

86 
val vs' = filter_out (member (op =) keepers) vs 
47356
19fb95255ec9
transfer method generalizes over free variables in goal
huffman
parents:
47355
diff
changeset

87 
in 
19fb95255ec9
transfer method generalizes over free variables in goal
huffman
parents:
47355
diff
changeset

88 
Induct.arbitrary_tac ctxt 0 vs' i 
19fb95255ec9
transfer method generalizes over free variables in goal
huffman
parents:
47355
diff
changeset

89 
end) 
19fb95255ec9
transfer method generalizes over free variables in goal
huffman
parents:
47355
diff
changeset

90 

47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

91 
(* create a lambda term of the same shape as the given term *) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

92 
fun skeleton (Bound i) ctxt = (Bound i, ctxt) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

93 
 skeleton (Abs (x, _, t)) ctxt = 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

94 
let 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

95 
val (t', ctxt) = skeleton t ctxt 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

96 
in 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

97 
(Abs (x, dummyT, t'), ctxt) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

98 
end 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

99 
 skeleton (t $ u) ctxt = 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

100 
let 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

101 
val (t', ctxt) = skeleton t ctxt 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

102 
val (u', ctxt) = skeleton u ctxt 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

103 
in 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

104 
(t' $ u', ctxt) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

105 
end 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

106 
 skeleton _ ctxt = 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

107 
let 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

108 
val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

109 
in 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

110 
(Free (c, dummyT), ctxt) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

111 
end 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

112 

71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

113 
fun mk_relT (T, U) = T > U > HOLogic.boolT 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

114 

71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

115 
fun mk_Rel t = 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

116 
let val T = fastype_of t 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

117 
in Const (@{const_name Transfer.Rel}, T > T) $ t end 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

118 

71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

119 
fun transfer_rule_of_terms ctxt tab t u = 
47580
d99c883cdf2c
use simpler method for preserving bound variable names in transfer tactic
huffman
parents:
47568
diff
changeset

120 
let 
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

121 
val thy = Proof_Context.theory_of ctxt 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

122 
(* precondition: T must consist of only TFrees and function space *) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

123 
fun rel (T as TFree (a, _)) U = 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

124 
Free (the (AList.lookup (op =) tab a), mk_relT (T, U)) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

125 
 rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) = 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

126 
let 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

127 
val r1 = rel T1 U1 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

128 
val r2 = rel T2 U2 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

129 
val rT = fastype_of r1 > fastype_of r2 > mk_relT (T, U) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

130 
in 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

131 
Const (@{const_name fun_rel}, rT) $ r1 $ r2 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

132 
end 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

133 
 rel T U = raise TYPE ("rel", [T, U], []) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

134 
fun zip _ thms (Bound i) (Bound _) = (nth thms i, []) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

135 
 zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) = 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

136 
let 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

137 
val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

138 
val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

139 
val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

140 
val thm0 = Thm.assume cprop 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

141 
val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

142 
val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop)) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

143 
val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1)) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

144 
val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1)) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

145 
val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2)) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

146 
val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2] 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

147 
val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)] 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

148 
val rule = Drule.instantiate' tinsts insts @{thm Rel_abs} 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

149 
val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1)) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

150 
in 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

151 
(thm2 COMP rule, hyps) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

152 
end 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

153 
 zip ctxt thms (f $ t) (g $ u) = 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

154 
let 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

155 
val (thm1, hyps1) = zip ctxt thms f g 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

156 
val (thm2, hyps2) = zip ctxt thms t u 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

157 
in 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

158 
(thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

159 
end 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

160 
 zip _ _ (t as Free (_, T)) u = 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

161 
let 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

162 
val U = fastype_of u 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

163 
val prop = mk_Rel (rel T U) $ t $ u 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

164 
val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

165 
in 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

166 
(Thm.assume cprop, [cprop]) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

167 
end 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

168 
 zip _ _ t u = raise TERM ("zip_relterm", [t, u]) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

169 
val r = mk_Rel (rel (fastype_of t) (fastype_of u)) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

170 
val goal = HOLogic.mk_Trueprop (r $ t $ u) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

171 
val rename = Thm.trivial (cterm_of thy goal) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

172 
val (thm, hyps) = zip ctxt [] t u 
47580
d99c883cdf2c
use simpler method for preserving bound variable names in transfer tactic
huffman
parents:
47568
diff
changeset

173 
in 
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

174 
Drule.implies_intr_list hyps (thm RS rename) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

175 
end 
47580
d99c883cdf2c
use simpler method for preserving bound variable names in transfer tactic
huffman
parents:
47568
diff
changeset

176 

47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

177 
fun transfer_rule_of_term ctxt t = 
47325  178 
let 
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

179 
val s = skeleton t ctxt > fst > Syntax.check_term ctxt > 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

180 
map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS))) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

181 
val frees = map fst (Term.add_frees s []) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

182 
val tfrees = map fst (Term.add_tfrees s []) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

183 
fun prep a = "R" ^ Library.unprefix "'" a 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

184 
val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

185 
val thm = transfer_rule_of_terms ctxt' (tfrees ~~ rnames) s t 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

186 
in 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

187 
Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

188 
end 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

189 

71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

190 
fun transfer_tac equiv ctxt i = 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

191 
let 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

192 
val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

193 
val start_rule = 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

194 
if equiv then @{thm transfer_start} else @{thm transfer_start'} 
47325  195 
val rules = Data.get ctxt 
196 
in 

197 
EVERY 

47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

198 
[rewrite_goal_tac pre_simps i THEN 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

199 
SUBGOAL (fn (t, i) => 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

200 
rtac start_rule i THEN 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

201 
(rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t)) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

202 
THEN_ALL_NEW 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

203 
(SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

204 
ORELSE' eq_tac ctxt)) (i + 1)) i, 
47325  205 
(* FIXME: rewrite_goal_tac does unwanted etacontraction *) 
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47327
diff
changeset

206 
rewrite_goal_tac post_simps i, 
47325  207 
rtac @{thm _} i] 
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

208 
end 
47325  209 

47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

210 
fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) => 
47325  211 
let 
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

212 
val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

213 
val rule1 = transfer_rule_of_term ctxt rhs 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

214 
val rules = Data.get ctxt 
47325  215 
in 
216 
EVERY 

47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

217 
[CONVERSION prep_conv i, 
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47618
diff
changeset

218 
rtac @{thm transfer_prover_start} i, 
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

219 
(rtac rule1 THEN_ALL_NEW 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

220 
REPEAT_ALL_NEW 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

221 
(resolve_tac rules ORELSE' eq_tac ctxt)) (i+1), 
47618
1568dadd598a
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents:
47580
diff
changeset

222 
rtac @{thm refl} i] 
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

223 
end) 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

224 

71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47658
diff
changeset

225 
(** Methods and attributes **) 
47325  226 

47568
98c8b7542b72
add option to transfer method for specifying variables not to generalize over
huffman
parents:
47523
diff
changeset

227 
val free = Args.context  Args.term >> (fn (_, Free v) => v  (ctxt, t) => 
98c8b7542b72
add option to transfer method for specifying variables not to generalize over
huffman
parents:
47523
diff
changeset

228 
error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)) 
98c8b7542b72
add option to transfer method for specifying variables not to generalize over
huffman
parents:
47523
diff
changeset

229 

98c8b7542b72
add option to transfer method for specifying variables not to generalize over
huffman
parents:
47523
diff
changeset

230 
val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing"  Args.colon) 
98c8b7542b72
add option to transfer method for specifying variables not to generalize over
huffman
parents:
47523
diff
changeset

231 
 Scan.repeat free) [] 
98c8b7542b72
add option to transfer method for specifying variables not to generalize over
huffman
parents:
47523
diff
changeset

232 

47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47635
diff
changeset

233 
fun transfer_method equiv : (Proof.context > Method.method) context_parser = 
47568
98c8b7542b72
add option to transfer method for specifying variables not to generalize over
huffman
parents:
47523
diff
changeset

234 
fixing >> (fn vs => fn ctxt => 
47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47635
diff
changeset

235 
SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt)) 
47325  236 

47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47618
diff
changeset

237 
val transfer_prover_method : (Proof.context > Method.method) context_parser = 
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47618
diff
changeset

238 
Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt)) 
47325  239 

47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47618
diff
changeset

240 
(* Attribute for transfer rules *) 
47325  241 

242 
val prep_rule = Conv.fconv_rule prep_conv 

243 

244 
val transfer_add = 

245 
Thm.declaration_attribute (Data.add_thm o prep_rule) 

246 

247 
val transfer_del = 

248 
Thm.declaration_attribute (Data.del_thm o prep_rule) 

249 

250 
val transfer_attribute = 

251 
Attrib.add_del transfer_add transfer_del 

252 

253 
(* Theory setup *) 

254 

255 
val setup = 

256 
Data.setup 

47503  257 
#> Relator_Eq.setup 
47325  258 
#> Attrib.setup @{binding transfer_rule} transfer_attribute 
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47618
diff
changeset

259 
"transfer rule for transfer method" 
47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47635
diff
changeset

260 
#> Method.setup @{binding transfer} (transfer_method true) 
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47635
diff
changeset

261 
"generic theorem transfer method" 
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47635
diff
changeset

262 
#> Method.setup @{binding transfer'} (transfer_method false) 
47325  263 
"generic theorem transfer method" 
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47618
diff
changeset

264 
#> Method.setup @{binding transfer_prover} transfer_prover_method 
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47618
diff
changeset

265 
"for proving transfer rules" 
47325  266 

267 
end 