author  wenzelm 
Sat, 09 Aug 2008 22:43:46 +0200  
changeset 27809  a1e409db516b 
parent 27378  0968c0d0b969 
child 27882  eaa9fef9f4c1 
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 

27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

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

9 
sig 
27236  10 
val read_instantiate: Proof.context > (indexname * string) list > thm > thm 
27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

11 
val instantiate_tac: Proof.context > (indexname * string) list > tactic 
27120  12 
val res_inst_tac: Proof.context > (indexname * string) list > thm > int > tactic 
13 
val eres_inst_tac: Proof.context > (indexname * string) list > thm > int > tactic 

27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

14 
val cut_inst_tac: Proof.context > (indexname * string) list > thm > int > tactic 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

15 
val forw_inst_tac: Proof.context > (indexname * string) list > thm > int > tactic 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

16 
val dres_inst_tac: Proof.context > (indexname * string) list > thm > int > tactic 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

17 
val thin_tac: Proof.context > string > int > tactic 
27219  18 
val subgoal_tac: Proof.context > string > int > tactic 
19 
val subgoals_tac: Proof.context > string list > int > tactic 

27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

20 
end; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

21 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

22 
signature RULE_INSTS = 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

23 
sig 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

24 
include BASIC_RULE_INSTS 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

25 
val make_elim_preserve: thm > thm 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

26 
end; 
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 
structure RuleInsts: RULE_INSTS = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

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

30 

27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

31 
structure T = OuterLex; 
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

32 
structure P = OuterParse; 
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

33 

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

34 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

35 
(** reading instantiations **) 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

36 

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

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

38 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

39 
fun is_tvar (x, _) = String.isPrefix "'" x; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

40 

22681
9d42e5365ad1
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
21879
diff
changeset

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

42 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

43 
fun the_sort tvars xi = the (AList.lookup (op =) tvars xi) 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

44 
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

45 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

46 
fun the_type vars xi = the (AList.lookup (op =) vars xi) 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

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

48 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

49 
fun unify_vartypes thy vars (xi, u) (unifier, maxidx) = 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

50 
let 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

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

52 
val U = Term.fastype_of u; 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

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

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

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

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

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

58 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

59 
fun instantiate inst = 
20509  60 
TermSubst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #> 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

61 
Envir.beta_norm; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

62 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

63 
fun make_instT f v = 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

64 
let 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

65 
val T = TVar v; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

66 
val T' = f T; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

67 
in if T = T' then NONE else SOME (T, T') end; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

68 

e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

69 
fun make_inst f v = 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

70 
let 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

71 
val t = Var v; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

72 
val t' = f t; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

73 
in if t aconv t' then NONE else SOME (t, t') end; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

74 

27282  75 
val add_used = 
76 
(Thm.fold_terms o fold_types o fold_atyps) 

77 
(fn TFree (a, _) => insert (op =) a 

78 
 TVar ((a, _), _) => insert (op =) a 

79 
 _ => I); 

80 

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

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

82 

25333  83 
fun read_termTs ctxt schematic ss Ts = 
25329  84 
let 
85 
fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt; 

86 
val ts = map2 parse Ts ss; 

87 
val ts' = 

88 
map2 (TypeInfer.constrain o TypeInfer.paramify_vars) Ts ts 

25333  89 
> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt) 
25329  90 
> Variable.polymorphic ctxt; 
91 
val Ts' = map Term.fastype_of ts'; 

92 
val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty; 

93 
in (ts', map (apsnd snd) (Vartab.dest tyenv)) end; 

94 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

95 
fun read_insts ctxt mixed_insts (tvars, vars) = 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

96 
let 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

97 
val thy = ProofContext.theory_of ctxt; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

98 
val cert = Thm.cterm_of thy; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

99 
val certT = Thm.ctyp_of thy; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

100 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

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

102 
val internal_insts = term_insts > map_filter 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

103 
(fn (xi, T.Term t) => SOME (xi, t) 
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

104 
 (_, T.Text _) => NONE 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

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

106 
val external_insts = term_insts > map_filter 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

107 
(fn (xi, T.Text s) => SOME (xi, s)  _ => NONE); 
20336
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 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

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

111 

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

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

113 
let 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

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

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

116 
(case arg of 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

117 
T.Text s => Syntax.read_typ ctxt s 
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

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

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

120 
in 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

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

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

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

124 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

125 
val type_insts1 = map readT type_insts; 
20509  126 
val instT1 = TermSubst.instantiateT type_insts1; 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

127 
val vars1 = map (apsnd instT1) vars; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

128 

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

129 

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

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

131 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

132 
val instT2 = Envir.norm_type 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

133 
(#1 (fold (unify_vartypes thy vars1) internal_insts (Vartab.empty, 0))); 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

134 
val vars2 = map (apsnd instT2) vars1; 
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20509
diff
changeset

135 
val internal_insts2 = map (apsnd (map_types instT2)) internal_insts; 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

136 
val inst2 = instantiate internal_insts2; 
20336
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 

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

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

140 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

141 
val (xs, strs) = split_list external_insts; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

142 
val Ts = map (the_type vars2) xs; 
25354  143 
val (ts, inferred) = read_termTs ctxt false strs Ts; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

144 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

145 
val instT3 = Term.typ_subst_TVars inferred; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

146 
val vars3 = map (apsnd instT3) vars2; 
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20509
diff
changeset

147 
val internal_insts3 = map (apsnd (map_types instT3)) internal_insts2; 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

148 
val external_insts3 = xs ~~ ts; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

149 
val inst3 = instantiate external_insts3; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

150 

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

151 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

152 
(* results *) 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

153 

e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

154 
val type_insts3 = map (fn ((a, _), T) => (a, instT3 (instT2 T))) type_insts1; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

155 
val term_insts3 = internal_insts3 @ external_insts3; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

156 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

157 
val inst_tvars = map_filter (make_instT (instT3 o instT2 o instT1)) tvars; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

158 
val inst_vars = map_filter (make_inst (inst3 o inst2)) vars3; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

159 
in 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

160 
((type_insts3, term_insts3), 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

161 
(map (pairself certT) inst_tvars, map (pairself cert) inst_vars)) 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

162 
end; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

163 

27236  164 
fun read_instantiate_mixed ctxt mixed_insts thm = 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

165 
let 
20487
6ac7a4fc32a0
read_instantiate: declare names of TVars as well (temporary workaround for nofreeze feature of type inference);
wenzelm
parents:
20343
diff
changeset

166 
val ctxt' = ctxt > Variable.declare_thm thm 
27282  167 
> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []); (* FIXME tmp *) 
22692  168 
val tvars = Thm.fold_terms Term.add_tvars thm []; 
169 
val vars = Thm.fold_terms Term.add_vars thm []; 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

170 
val ((type_insts, term_insts), insts) = read_insts ctxt' (map snd mixed_insts) (tvars, vars); 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

171 

e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

172 
val _ = (*assign internalized values*) 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

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

174 
if is_tvar xi then 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

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

176 
else 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

177 
T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg); 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

178 
in 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

179 
Drule.instantiate insts thm > RuleCases.save thm 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

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

181 

27236  182 
fun read_instantiate_mixed' ctxt (args, concl_args) thm = 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

183 
let 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

184 
fun zip_vars _ [] = [] 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

185 
 zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

186 
 zip_vars ((x, _) :: xs) ((arg, SOME t) :: rest) = (arg, (x, t)) :: zip_vars xs rest 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

187 
 zip_vars [] _ = error "More instantiations than variables in theorem"; 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

188 
val insts = 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

189 
zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @ 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

190 
zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args; 
27236  191 
in read_instantiate_mixed ctxt insts thm end; 
192 

27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

193 
end; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

194 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

195 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

196 
(* instantiation of rule or goal state *) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

197 

27236  198 
fun read_instantiate ctxt args thm = 
199 
read_instantiate_mixed (ctxt > ProofContext.set_mode ProofContext.mode_schematic) (* FIXME !? *) 

27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

200 
(map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

201 

27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

202 
fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args); 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

203 

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

204 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

205 

e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

206 
(** attributes **) 
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

207 

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

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

209 

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

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

211 

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

212 
val value = 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

213 
Args.internal_typ >> T.Typ  
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

214 
Args.internal_term >> T.Term  
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

215 
Args.name >> T.Text; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

216 

27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

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

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

219 

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

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

221 

27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

222 
val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args => 
27236  223 
Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))); 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

224 

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

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

226 

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

227 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

228 
(* of: positional instantiation (terms only) *) 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

229 

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

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

231 

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

232 
val value = 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

233 
Args.internal_term >> T.Term  
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

234 
Args.name >> T.Text; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

235 

27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

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

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

238 

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

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

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

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

242 

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

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

244 

20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

245 
val of_att = Attrib.syntax (Scan.lift insts >> (fn args => 
27236  246 
Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))); 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

247 

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

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

249 

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

250 

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

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

252 

26463  253 
val _ = Context.>> (Context.map_theory 
254 
(Attrib.add_attributes 

255 
[("where", where_att, "named instantiation of theorem"), 

256 
("of", of_att, "positional instantiation of theorem")])); 

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

257 

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

258 

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

259 

27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

260 
(** tactics **) 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

261 

27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

262 
(* resolution after lifting and instantation; may refer to parameters of the subgoal *) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

263 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

264 
(* FIXME cleanup this mess!!! *) 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

265 

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

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

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

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

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

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

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

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

273 
val tinsts = filter_out has_type_var insts; 
25333  274 

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

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

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

277 
let 
25333  278 
val (_, _, Bi, _) = Thm.dest_state (st, i); 
279 
val params = Logic.strip_params Bi; (*params of subgoal i as string typ pairs*) 

280 
val params = rev (Term.rename_wrt_term Bi params) 

281 
(*as they are printed: bound variables with*) 

282 
(*the same name are renamed during printing*) 

283 

284 
val (param_names, ctxt') = ctxt 

285 
> Variable.declare_thm thm 

286 
> Thm.fold_terms Variable.declare_constraints st 

287 
> ProofContext.add_fixes_i (map (fn (x, T) => (x, SOME T, NoSyn)) params); 

288 

289 
(* Process type insts: Tinsts_env *) 

290 
fun absent xi = error 

291 
("No such variable in theorem: " ^ Term.string_of_vname xi); 

292 
val (rtypes, rsorts) = Drule.types_sorts thm; 

293 
fun readT (xi, s) = 

294 
let val S = case rsorts xi of SOME S => S  NONE => absent xi; 

295 
val T = Syntax.read_typ ctxt' s; 

296 
val U = TVar (xi, S); 

297 
in if Sign.typ_instance thy (T, U) then (U, T) 

298 
else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails") 

299 
end; 

300 
val Tinsts_env = map readT Tinsts; 

301 
(* Preprocess rule: extract vars and their types, apply Tinsts *) 

302 
fun get_typ xi = 

303 
(case rtypes xi of 

304 
SOME T => typ_subst_atomic Tinsts_env T 

305 
 NONE => absent xi); 

306 
val (xis, ss) = Library.split_list tinsts; 

307 
val Ts = map get_typ xis; 

308 

309 
val (ts, envT) = read_termTs ctxt' true ss Ts; 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

326 
fun liftterm t = list_abs_free 
25333  327 
(param_names ~~ paramTs, Logic.incr_indexes(paramTs,inc) t) 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

342 

27120  343 
val res_inst_tac = bires_inst_tac false; 
344 
val eres_inst_tac = bires_inst_tac true; 

345 

346 

27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

347 
(* forward resolution *) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

348 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

349 
fun make_elim_preserve rl = 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

350 
let 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

351 
val cert = Thm.cterm_of (Thm.theory_of_thm rl); 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

352 
val maxidx = Thm.maxidx_of rl; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

353 
fun cvar xi = cert (Var (xi, propT)); 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

354 
val revcut_rl' = 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

355 
instantiate ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)), 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

356 
(cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

357 
in 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

358 
(case Seq.list_of (bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

359 
[th] => th 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

360 
 _ => raise THM ("make_elim_preserve", 1, [rl])) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

361 
end; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

362 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

363 
(*instantiate and cut  for atomic fact*) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

364 
fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve rule); 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

365 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

366 
(*forward tactic applies a rule to an assumption without deleting it*) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

367 
fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

368 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

369 
(*dresolve tactic applies a rule to replace an assumption*) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

370 
fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve rule); 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

371 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

372 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

373 
(* derived tactics *) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

374 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

375 
(*deletion of an assumption*) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

376 
fun thin_tac ctxt s = eres_inst_tac ctxt [(("V", 0), s)] Drule.thin_rl; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

377 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

378 
(*Introduce the given proposition as lemma and subgoal*) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

379 
fun subgoal_tac ctxt A = DETERM o res_inst_tac ctxt [(("psi", 0), A)] cut_rl; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

380 
fun subgoals_tac ctxt As = EVERY' (map (subgoal_tac ctxt) As); 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

381 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

382 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

383 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

384 
(** methods **) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

385 

817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

386 
(* rule_tac etc.  refer to dynamic goal state! *) 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

387 

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

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

389 

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

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

391 
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

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

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

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

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

396 

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

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

398 

27120  399 
val res_inst_meth = gen_inst res_inst_tac Tactic.resolve_tac; 
400 
val eres_inst_meth = gen_inst eres_inst_tac Tactic.eresolve_tac; 

27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

401 
val cut_inst_meth = gen_inst cut_inst_tac Tactic.cut_rules_tac; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

402 
val dres_inst_meth = gen_inst dres_inst_tac Tactic.dresolve_tac; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

403 
val forw_inst_meth = gen_inst forw_inst_tac Tactic.forward_tac; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

404 

27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

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

406 

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

407 

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

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

409 

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

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

411 
Scan.optional 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

412 
(Scan.lift (P.and_list1 (Args.name  (Args.$$$ "="  P.!!! Args.name))  Args.$$$ "in")) [] 
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

413 
 Attrib.thms; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

414 

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

415 
fun inst_args f src ctxt = 
21879  416 
f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL  insts) src ctxt)); 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

417 

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

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

419 
Scan.optional 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

420 
(Scan.lift (P.and_list1 (Args.var  (Args.$$$ "="  P.!!! Args.name))  Args.$$$ "in")) [] 
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset

421 
 Attrib.thms; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

422 

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

423 
fun inst_args_var f src ctxt = 
21879  424 
f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL  insts_var) src ctxt)); 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

425 

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

426 

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

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

428 

26463  429 
val _ = Context.>> (Context.map_theory 
430 
(Method.add_methods 

431 
[("rule_tac", inst_args_var res_inst_meth, 

432 
"apply rule (dynamic instantiation)"), 

433 
("erule_tac", inst_args_var eres_inst_meth, 

434 
"apply rule in elimination manner (dynamic instantiation)"), 

435 
("drule_tac", inst_args_var dres_inst_meth, 

436 
"apply rule in destruct manner (dynamic instantiation)"), 

437 
("frule_tac", inst_args_var forw_inst_meth, 

438 
"apply rule in forward manner (dynamic instantiation)"), 

439 
("cut_tac", inst_args_var cut_inst_meth, 

440 
"cut rule (dynamic instantiation)"), 

441 
("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac, 

442 
"insert subgoal (dynamic instantiation)"), 

443 
("thin_tac", Method.goal_args_ctxt Args.name thin_tac, 

444 
"remove premise (dynamic instantiation)")])); 

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

445 

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

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

447 

27245
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

448 
structure BasicRuleInsts: BASIC_RULE_INSTS = RuleInsts; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

449 
open BasicRuleInsts; 
817d34377170
added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
wenzelm
parents:
27236
diff
changeset

450 