author  wenzelm 
Thu, 03 Aug 2006 17:30:44 +0200  
changeset 20336  aac494583949 
child 20343  e093a54bf25e 
permissions  rwrr 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/Isar/rule_insts.ML 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

3 
Author: Makarius 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

4 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

5 
Rule instantiations  operations within a rule/subgoal context. 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

6 
*) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

7 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

8 
signature RULE_INSTS = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

9 
sig 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

10 
val bires_inst_tac: bool > Proof.context > (indexname * string) list > 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

11 
thm > int > tactic 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

12 
end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

13 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

14 
structure RuleInsts: RULE_INSTS = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

15 
struct 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

16 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

17 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

18 
(** attributes **) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

19 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

20 
(* read_instantiate: named instantiation of type and term variables *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

21 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

22 
local 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

23 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

24 
fun is_tvar (x, _) = (case Symbol.explode x of "'" :: _ => true  _ => false); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

25 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

26 
fun error_var msg xi = error (msg ^ Syntax.string_of_vname xi); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

27 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

28 
fun the_sort sorts xi = the (sorts xi) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

29 
handle Option.Option => error_var "No such type variable in theorem: " xi; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

30 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

31 
fun the_type types xi = the (types xi) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

32 
handle Option.Option => error_var "No such variable in theorem: " xi; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

33 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

34 
fun unify_types thy types (xi, u) (unifier, maxidx) = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

35 
let 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

36 
val T = the_type types xi; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

37 
val U = Term.fastype_of u; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

38 
val maxidx' = Int.max (maxidx, Int.max (#2 xi, Term.maxidx_of_term u)); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

39 
in 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

40 
Sign.typ_unify thy (T, U) (unifier, maxidx') 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

41 
handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

42 
end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

43 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

44 
fun typ_subst env = apsnd (Term.typ_subst_TVars env); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

45 
fun subst env = apsnd (Term.subst_TVars env); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

46 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

47 
fun instantiate thy envT env thm = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

48 
let 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

49 
val (_, sorts) = Drule.types_sorts thm; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

50 
fun prepT (a, T) = (Thm.ctyp_of thy (TVar (a, the_sort sorts a)), Thm.ctyp_of thy T); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

51 
fun prep (xi, t) = pairself (Thm.cterm_of thy) (Var (xi, Term.fastype_of t), t); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

52 
in 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

53 
Drule.instantiate (map prepT (distinct (op =) envT), 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

54 
map prep (distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

55 
end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

56 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

57 
in 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

58 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

59 
fun read_instantiate mixed_insts (context, thm) = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

60 
let 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

61 
val thy = Context.theory_of context; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

62 
val ctxt = Context.proof_of context; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

63 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

64 
val (type_insts, term_insts) = List.partition (is_tvar o fst) (map snd mixed_insts); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

65 
val internal_insts = term_insts > map_filter 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

66 
(fn (xi, Args.Term t) => SOME (xi, t) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

67 
 (_, Args.Name _) => NONE 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

68 
 (xi, _) => error_var "Term argument expected for " xi); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

69 
val external_insts = term_insts > map_filter 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

70 
(fn (xi, Args.Name s) => SOME (xi, s)  _ => NONE); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

71 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

72 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

73 
(* type instantiations *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

74 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

75 
val sorts = #2 (Drule.types_sorts thm); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

76 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

77 
fun readT (xi, arg) = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

78 
let 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

79 
val S = the_sort sorts xi; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

80 
val T = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

81 
(case arg of 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

82 
Args.Name s => ProofContext.read_typ ctxt s 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

83 
 Args.Typ T => T 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

84 
 _ => error_var "Type argument expected for " xi); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

85 
in 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

86 
if Sign.of_sort thy (T, S) then (xi, T) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

87 
else error_var "Incompatible sort for typ instantiation of " xi 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

88 
end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

89 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

90 
val type_insts' = map readT type_insts; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

91 
val thm' = instantiate thy type_insts' [] thm; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

92 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

93 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

94 
(* internal term instantiations *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

95 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

96 
val types' = #1 (Drule.types_sorts thm'); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

97 
val unifier = map (apsnd snd) (Vartab.dest (#1 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

98 
(fold (unify_types thy types') internal_insts (Vartab.empty, 0)))); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

99 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

100 
val type_insts'' = map (typ_subst unifier) type_insts'; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

101 
val internal_insts'' = map (subst unifier) internal_insts; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

102 
val thm'' = instantiate thy unifier internal_insts'' thm'; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

103 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

104 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

105 
(* external term instantiations *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

106 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

107 
val types'' = #1 (Drule.types_sorts thm''); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

108 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

109 
val (xs, ss) = split_list external_insts; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

110 
val Ts = map (the_type types'') xs; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

111 
val (ts, inferred) = ProofContext.read_termTs ctxt (K false) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

112 
(K NONE) (K NONE) (Drule.add_used thm'' []) (ss ~~ Ts); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

113 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

114 
val type_insts''' = map (typ_subst inferred) type_insts''; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

115 
val internal_insts''' = map (subst inferred) internal_insts''; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

116 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

117 
val external_insts''' = xs ~~ ts; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

118 
val term_insts''' = internal_insts''' @ external_insts'''; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

119 
val thm''' = instantiate thy inferred external_insts''' thm''; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

120 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

121 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

122 
(* assign internalized values *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

123 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

124 
val _ = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

125 
mixed_insts > List.app (fn (arg, (xi, _)) => 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

126 
if is_tvar xi then 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

127 
Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts''' xi)))) arg 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

128 
else 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

129 
Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts''' xi)))) arg); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

130 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

131 
in (context, thm''' > RuleCases.save thm) end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

132 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

133 
end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

134 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

135 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

136 
(* where: named instantiation *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

137 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

138 
local 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

139 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

140 
val value = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

141 
Args.internal_typ >> Args.Typ  
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

142 
Args.internal_term >> Args.Term  
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

143 
Args.name >> Args.Name; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

144 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

145 
val inst = Args.var  (Args.$$$ "="  Args.ahead  value) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

146 
>> (fn (xi, (a, v)) => (a, (xi, v))); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

147 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

148 
in 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

149 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

150 
val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> read_instantiate); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

151 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

152 
end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

153 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

154 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

155 
(* of: positional instantiation (term arguments only) *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

156 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

157 
local 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

158 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

159 
fun read_instantiate' (args, concl_args) (context, thm) = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

160 
let 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

161 
fun zip_vars _ [] = [] 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

162 
 zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

163 
 zip_vars ((x, _) :: xs) ((arg, SOME t) :: rest) = (arg, (x, t)) :: zip_vars xs rest 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

164 
 zip_vars [] _ = error "More instantiations than variables in theorem"; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

165 
val insts = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

166 
zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @ 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

167 
zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

168 
in read_instantiate insts (context, thm) end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

169 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

170 
val value = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

171 
Args.internal_term >> Args.Term  
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

172 
Args.name >> Args.Name; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

173 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

174 
val inst = Args.ahead  Args.maybe value; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

175 
val concl = Args.$$$ "concl"  Args.colon; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

176 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

177 
val insts = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

178 
Scan.repeat (Scan.unless concl inst)  
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

179 
Scan.optional (concl  Scan.repeat inst) []; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

180 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

181 
in 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

182 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

183 
val of_att = Attrib.syntax (Scan.lift insts >> read_instantiate'); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

184 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

185 
end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

186 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

187 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

188 
(* setup *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

189 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

190 
val _ = Context.add_setup (Attrib.add_attributes 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

191 
[("where", where_att, "named instantiation of theorem"), 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

192 
("of", of_att, "rule applied to terms")]); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

193 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

194 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

195 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

196 
(** methods **) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

197 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

198 
(* rule_tac etc.  refer to dynamic goal state!! *) (* FIXME cleanup!! *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

199 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

200 
fun bires_inst_tac bires_flag ctxt insts thm = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

201 
let 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

202 
val thy = ProofContext.theory_of ctxt; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

203 
(* Separate type and term insts *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

204 
fun has_type_var ((x, _), _) = (case Symbol.explode x of 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

205 
"'"::cs => true  cs => false); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

206 
val Tinsts = List.filter has_type_var insts; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

207 
val tinsts = filter_out has_type_var insts; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

208 
(* Tactic *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

209 
fun tac i st = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

210 
let 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

211 
(* Preprocess state: extract environment information: 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

212 
 variables and their types 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

213 
 type variables and their sorts 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

214 
 parameters and their types *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

215 
val (types, sorts) = types_sorts st; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

216 
(* Process type insts: Tinsts_env *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

217 
fun absent xi = error 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

218 
("No such variable in theorem: " ^ Syntax.string_of_vname xi); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

219 
val (rtypes, rsorts) = types_sorts thm; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

220 
fun readT (xi, s) = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

221 
let val S = case rsorts xi of SOME S => S  NONE => absent xi; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

222 
val T = Sign.read_typ (thy, sorts) s; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

223 
val U = TVar (xi, S); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

224 
in if Sign.typ_instance thy (T, U) then (U, T) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

225 
else error 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

226 
("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails") 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

227 
end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

228 
val Tinsts_env = map readT Tinsts; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

229 
(* Preprocess rule: extract vars and their types, apply Tinsts *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

230 
fun get_typ xi = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

231 
(case rtypes xi of 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

232 
SOME T => typ_subst_atomic Tinsts_env T 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

233 
 NONE => absent xi); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

234 
val (xis, ss) = Library.split_list tinsts; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

235 
val Ts = map get_typ xis; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

236 
val (_, _, Bi, _) = dest_state(st,i) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

237 
val params = Logic.strip_params Bi 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

238 
(* params of subgoal i as string typ pairs *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

239 
val params = rev(Term.rename_wrt_term Bi params) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

240 
(* as they are printed: bound variables with *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

241 
(* the same name are renamed during printing *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

242 
fun types' (a, ~1) = (case AList.lookup (op =) params a of 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

243 
NONE => types (a, ~1) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

244 
 some => some) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

245 
 types' xi = types xi; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

246 
fun internal x = is_some (types' (x, ~1)); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

247 
val used = Drule.add_used thm (Drule.add_used st []); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

248 
val (ts, envT) = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

249 
ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

250 
val envT' = map (fn (ixn, T) => 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

251 
(TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

252 
val cenv = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

253 
map 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

254 
(fn (xi, t) => 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

255 
pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t)) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

256 
(distinct 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

257 
(fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

258 
(xis ~~ ts)); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

259 
(* Lift and instantiate rule *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

260 
val {maxidx, ...} = rep_thm st; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

261 
val paramTs = map #2 params 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

262 
and inc = maxidx+1 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

263 
fun liftvar (Var ((a,j), T)) = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

264 
Var((a, j+inc), paramTs > Logic.incr_tvar inc T) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

265 
 liftvar t = raise TERM("Variable expected", [t]); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

266 
fun liftterm t = list_abs_free 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

267 
(params, Logic.incr_indexes(paramTs,inc) t) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

268 
fun liftpair (cv,ct) = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

269 
(cterm_fun liftvar cv, cterm_fun liftterm ct) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

270 
val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

271 
val rule = Drule.instantiate 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

272 
(map lifttvar envT', map liftpair cenv) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

273 
(Thm.lift_rule (Thm.cprem_of st i) thm) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

274 
in 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

275 
if i > nprems_of st then no_tac st 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

276 
else st > 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

277 
compose_tac (bires_flag, rule, nprems_of thm) i 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

278 
end 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

279 
handle TERM (msg,_) => (warning msg; no_tac st) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

280 
 THM (msg,_,_) => (warning msg; no_tac st); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

281 
in tac end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

282 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

283 
local 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

284 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

285 
fun gen_inst _ tac _ (quant, ([], thms)) = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

286 
Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms)) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

287 
 gen_inst inst_tac _ ctxt (quant, (insts, [thm])) = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

288 
Method.METHOD (fn facts => 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

289 
quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

290 
 gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules"; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

291 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

292 
in 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

293 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

294 
val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

295 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

296 
val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

297 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

298 
val cut_inst_meth = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

299 
gen_inst 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

300 
(fn ctxt => fn insts => bires_inst_tac false ctxt insts o Tactic.make_elim_preserve) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

301 
Tactic.cut_rules_tac; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

302 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

303 
val dres_inst_meth = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

304 
gen_inst 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

305 
(fn ctxt => fn insts => bires_inst_tac true ctxt insts o Tactic.make_elim_preserve) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

306 
Tactic.dresolve_tac; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

307 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

308 
val forw_inst_meth = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

309 
gen_inst 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

310 
(fn ctxt => fn insts => fn rule => 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

311 
bires_inst_tac false ctxt insts (Tactic.make_elim_preserve rule) THEN' 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

312 
assume_tac) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

313 
Tactic.forward_tac; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

314 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

315 
fun subgoal_tac ctxt sprop = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

316 
DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

317 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

318 
fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

319 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

320 
fun thin_tac ctxt s = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

321 
bires_inst_tac true ctxt [(("V", 0), s)] thin_rl; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

322 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

323 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

324 
(* method syntax *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

325 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

326 
val insts = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

327 
Scan.optional 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

328 
(Args.enum1 "and" (Scan.lift (Args.name  (Args.$$$ "="  Args.!!! Args.name)))  
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

329 
Scan.lift (Args.$$$ "in")) []  Attrib.thms; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

330 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

331 
fun inst_args f src ctxt = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

332 
f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL  insts) src ctxt)); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

333 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

334 
val insts_var = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

335 
Scan.optional 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

336 
(Args.enum1 "and" (Scan.lift (Args.var  (Args.$$$ "="  Args.!!! Args.name)))  
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

337 
Scan.lift (Args.$$$ "in")) []  Attrib.thms; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

338 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

339 
fun inst_args_var f src ctxt = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

340 
f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL  insts_var) src ctxt)); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

341 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

342 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

343 
(* setup *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

344 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

345 
val _ = Context.add_setup (Method.add_methods 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

346 
[("rule_tac", inst_args_var res_inst_meth, 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

347 
"apply rule (dynamic instantiation)"), 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

348 
("erule_tac", inst_args_var eres_inst_meth, 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

349 
"apply rule in elimination manner (dynamic instantiation)"), 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

350 
("drule_tac", inst_args_var dres_inst_meth, 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

351 
"apply rule in destruct manner (dynamic instantiation)"), 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

352 
("frule_tac", inst_args_var forw_inst_meth, 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

353 
"apply rule in forward manner (dynamic instantiation)"), 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

354 
("cut_tac", inst_args_var cut_inst_meth, 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

355 
"cut rule (dynamic instantiation)"), 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

356 
("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac, 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

357 
"insert subgoal (dynamic instantiation)"), 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

358 
("thin_tac", Method.goal_args_ctxt Args.name thin_tac, 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

359 
"remove premise (dynamic instantiation)")]); 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

360 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

361 
end; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

362 

aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

363 
end; 