author  wenzelm 
Wed, 29 May 2013 18:25:11 +0200  
changeset 52223  5bb6ae8acb87 
parent 46476  dac966e4e51d 
child 52732  b4da1f2ec73f 
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 
Author: Makarius 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

3 

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

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

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

6 

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

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

8 
sig 
27236  9 
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

10 
val instantiate_tac: Proof.context > (indexname * string) list > tactic 
27120  11 
val res_inst_tac: Proof.context > (indexname * string) list > thm > int > tactic 
12 
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

13 
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

14 
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

15 
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

16 
val thin_tac: Proof.context > string > int > tactic 
27219  17 
val subgoal_tac: Proof.context > string > int > tactic 
30545  18 
val method: (Proof.context > (indexname * string) list > thm > int > tactic) > 
30551  19 
(Proof.context > thm list > int > tactic) > (Proof.context > Proof.method) context_parser 
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 

42806  28 
structure Rule_Insts: RULE_INSTS = 
20336
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 

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

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

32 

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

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

34 

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

36 

45611  37 
fun the_sort tvars (xi: indexname) = 
38 
(case AList.lookup (op =) tvars xi of 

39 
SOME S => S 

40 
 NONE => error_var "No such type variable in theorem: " xi); 

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

41 

45611  42 
fun the_type vars (xi: indexname) = 
43 
(case AList.lookup (op =) vars xi of 

44 
SOME T => T 

45 
 NONE => error_var "No such variable in theorem: " xi); 

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

46 

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

47 
fun instantiate inst = 
31977  48 
Term_Subst.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

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

50 

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

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

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

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

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

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

56 

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

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

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

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

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

61 
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

62 

27282  63 
val add_used = 
64 
(Thm.fold_terms o fold_types o fold_atyps) 

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

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

67 
 _ => I); 

68 

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

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

70 

25333  71 
fun read_termTs ctxt schematic ss Ts = 
25329  72 
let 
73 
fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt; 

74 
val ts = map2 parse Ts ss; 

75 
val ts' = 

39288  76 
map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts 
42360  77 
> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt) 
25329  78 
> Variable.polymorphic ctxt; 
79 
val Ts' = map Term.fastype_of ts'; 

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

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

82 

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

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

84 
let 
42360  85 
val thy = Proof_Context.theory_of ctxt; 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

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

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

88 

45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

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

90 

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

91 

45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

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

93 

45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

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

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

96 
val S = the_sort tvars xi; 
45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

97 
val T = Syntax.read_typ ctxt s; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

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

99 
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

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

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

102 

45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

103 
val instT1 = Term_Subst.instantiateT (map readT type_insts); 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

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

105 

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

106 

45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

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

108 

45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

109 
val (xs, ss) = split_list term_insts; 
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

110 
val Ts = map (the_type vars1) xs; 
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

111 
val (ts, inferred) = read_termTs ctxt false ss Ts; 
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

112 

70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

113 
val instT2 = Term.typ_subst_TVars inferred; 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

114 
val vars2 = map (apsnd instT2) vars1; 
45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

115 
val inst2 = instantiate (xs ~~ ts); 
20336
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 

45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

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

119 

45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

120 
val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars; 
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

121 
val inst_vars = map_filter (make_inst inst2) vars2; 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

122 
in 
45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

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

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

125 

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

127 
let 
45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

128 
val ctxt' = ctxt 
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

129 
> Variable.declare_thm thm 
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

130 
> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []); (* FIXME !? *) 
22692  131 
val tvars = Thm.fold_terms Term.add_tvars thm []; 
132 
val vars = Thm.fold_terms Term.add_vars thm []; 

45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

133 
val insts = read_insts ctxt' mixed_insts (tvars, vars); 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

134 
in 
45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

135 
Drule.instantiate_normalize insts thm 
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

136 
> Rule_Cases.save thm 
20343
e093a54bf25e
reworked read_instantiate  separate read_insts;
wenzelm
parents:
20336
diff
changeset

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

138 

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

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

141 
fun zip_vars _ [] = [] 
45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

142 
 zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest 
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

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

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

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

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

147 
zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args; 
27236  148 
in read_instantiate_mixed ctxt insts thm end; 
149 

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

150 
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

151 

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

152 

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

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

154 

45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

155 
fun read_instantiate ctxt = 
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

156 
read_instantiate_mixed (ctxt > Proof_Context.set_mode Proof_Context.mode_schematic); (* FIXME !? *) 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

157 

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

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

159 

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

160 

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

161 

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

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

163 

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

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

165 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30551
diff
changeset

166 
val _ = Context.>> (Context.map_theory 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30551
diff
changeset

167 
(Attrib.setup (Binding.name "where") 
45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

168 
(Scan.lift (Parse.and_list (Args.var  (Args.$$$ "="  Args.name_source))) >> 
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

169 
(fn args => 
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

170 
Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) 
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30551
diff
changeset

171 
"named instantiation of theorem")); 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

172 

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

173 

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

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

175 

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

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

177 

45613
70e5b43535cd
simplified read_instantiate  no longer need to assign values, since rule attributes are now static;
wenzelm
parents:
45611
diff
changeset

178 
val inst = Args.maybe Args.name_source; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

179 
val concl = Args.$$$ "concl"  Args.colon; 
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 
val insts = 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

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

183 
Scan.optional (concl  Scan.repeat inst) []; 
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 
in 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

186 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30551
diff
changeset

187 
val _ = Context.>> (Context.map_theory 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30551
diff
changeset

188 
(Attrib.setup (Binding.name "of") 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30551
diff
changeset

189 
(Scan.lift insts >> (fn args => 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30551
diff
changeset

190 
Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30551
diff
changeset

191 
"positional instantiation of theorem")); 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

192 

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

193 
end; 
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 

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

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

198 

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

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

200 

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

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

202 

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

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

204 
let 
42360  205 
val thy = Proof_Context.theory_of ctxt; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

206 
(* Separate type and term insts *) 
32784  207 
fun has_type_var ((x, _), _) = 
208 
(case Symbol.explode x of "'" :: _ => true  _ => false); 

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

210 
val tinsts = filter_out has_type_var insts; 
25333  211 

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

212 
(* Tactic *) 
46474
7e6be8270ddb
more conventional tactic setup  avoid lowlevel Thm.dest_state and spurious warnings about it;
wenzelm
parents:
46461
diff
changeset

213 
fun tac i st = CSUBGOAL (fn (cgoal, _) => 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

214 
let 
46474
7e6be8270ddb
more conventional tactic setup  avoid lowlevel Thm.dest_state and spurious warnings about it;
wenzelm
parents:
46461
diff
changeset

215 
val goal = term_of cgoal; 
7e6be8270ddb
more conventional tactic setup  avoid lowlevel Thm.dest_state and spurious warnings about it;
wenzelm
parents:
46461
diff
changeset

216 
val params = Logic.strip_params goal; (*params of subgoal i as string typ pairs*) 
7e6be8270ddb
more conventional tactic setup  avoid lowlevel Thm.dest_state and spurious warnings about it;
wenzelm
parents:
46461
diff
changeset

217 
val params = rev (Term.rename_wrt_term goal params) 
25333  218 
(*as they are printed: bound variables with*) 
219 
(*the same name are renamed during printing*) 

220 

221 
val (param_names, ctxt') = ctxt 

222 
> Variable.declare_thm thm 

223 
> Thm.fold_terms Variable.declare_constraints st 

42360  224 
> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params); 
25333  225 

226 
(* Process type insts: Tinsts_env *) 

227 
fun absent xi = error 

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

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

230 
fun readT (xi, s) = 

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

232 
val T = Syntax.read_typ ctxt' s; 

233 
val U = TVar (xi, S); 

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

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

236 
end; 

237 
val Tinsts_env = map readT Tinsts; 

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

239 
fun get_typ xi = 

240 
(case rtypes xi of 

241 
SOME T => typ_subst_atomic Tinsts_env T 

242 
 NONE => absent xi); 

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

244 
val Ts = map get_typ xis; 

245 

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

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

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

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

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

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

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

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

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

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

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

256 
(* Lift and instantiate rule *) 
44058  257 
val maxidx = Thm.maxidx_of st; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

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

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

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

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

262 
 liftvar t = raise TERM("Variable expected", [t]); 
44241  263 
fun liftterm t = 
264 
fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t); 

265 
fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct); 

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

266 
val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc); 
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
42806
diff
changeset

267 
val rule = Drule.instantiate_normalize 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

268 
(map lifttvar envT', map liftpair cenv) 
46474
7e6be8270ddb
more conventional tactic setup  avoid lowlevel Thm.dest_state and spurious warnings about it;
wenzelm
parents:
46461
diff
changeset

269 
(Thm.lift_rule cgoal thm) 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

270 
in 
46474
7e6be8270ddb
more conventional tactic setup  avoid lowlevel Thm.dest_state and spurious warnings about it;
wenzelm
parents:
46461
diff
changeset

271 
compose_tac (bires_flag, rule, nprems_of thm) i 
46476
dac966e4e51d
clarified bires_inst_tac: retain internal exceptions;
wenzelm
parents:
46474
diff
changeset

272 
end) i st; 
20336
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

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

274 

27120  275 
val res_inst_tac = bires_inst_tac false; 
276 
val eres_inst_tac = bires_inst_tac true; 

277 

278 

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

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

280 

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

281 
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

282 
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

283 
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

284 
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

285 
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

286 
val revcut_rl' = 
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
42806
diff
changeset

287 
Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)), 
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

288 
(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

289 
in 
52223
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
46476
diff
changeset

290 
(case Seq.list_of 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
46476
diff
changeset

291 
(Thm.bicompose {flatten = true, match = false, incremented = false} 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
46476
diff
changeset

292 
(false, rl, Thm.nprems_of rl) 1 revcut_rl') 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
46476
diff
changeset

293 
of 
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

294 
[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

295 
 _ => 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

296 
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

297 

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

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

299 
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

300 

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

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

302 
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

303 

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

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

305 
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

306 

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

307 

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

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

309 

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

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

311 
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

312 

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

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

314 
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

315 

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

316 

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

317 

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

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

319 

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

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

321 

30545  322 
fun method inst_tac tac = 
30515  323 
Args.goal_spec  
324 
Scan.optional (Scan.lift 

36950  325 
(Parse.and_list1 (Args.var  (Args.$$$ "="  Parse.!!! Args.name_source))  
326 
Args.$$$ "in")) []  

30515  327 
Attrib.thms >> 
328 
(fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts => 

30551  329 
if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms) 
30515  330 
else 
331 
(case thms of 

332 
[thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm) 

333 
 _ => error "Cannot have instantiations with multiple rules"))); 

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

334 

30551  335 
val res_inst_meth = method res_inst_tac (K Tactic.resolve_tac); 
336 
val eres_inst_meth = method eres_inst_tac (K Tactic.eresolve_tac); 

337 
val cut_inst_meth = method cut_inst_tac (K Tactic.cut_rules_tac); 

338 
val dres_inst_meth = method dres_inst_tac (K Tactic.dresolve_tac); 

339 
val forw_inst_meth = method forw_inst_tac (K Tactic.forward_tac); 

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

340 

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 
(* setup *) 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

343 

26463  344 
val _ = Context.>> (Context.map_theory 
30515  345 
(Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #> 
346 
Method.setup (Binding.name "erule_tac") eres_inst_meth 

347 
"apply rule in elimination manner (dynamic instantiation)" #> 

348 
Method.setup (Binding.name "drule_tac") dres_inst_meth 

349 
"apply rule in destruct manner (dynamic instantiation)" #> 

350 
Method.setup (Binding.name "frule_tac") forw_inst_meth 

351 
"apply rule in forward manner (dynamic instantiation)" #> 

352 
Method.setup (Binding.name "cut_tac") cut_inst_meth "cut rule (dynamic instantiation)" #> 

353 
Method.setup (Binding.name "subgoal_tac") 

354 
(Args.goal_spec  Scan.lift (Scan.repeat1 Args.name_source) >> 

46461  355 
(fn (quant, props) => fn ctxt => 
356 
SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props)))) 

30515  357 
"insert subgoal (dynamic instantiation)" #> 
358 
Method.setup (Binding.name "thin_tac") 

359 
(Args.goal_spec  Scan.lift Args.name_source >> 

360 
(fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop))) 

361 
"remove premise (dynamic instantiation)")); 

20336
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; 
aac494583949
Rule instantiations  operations within a rule/subgoal context.
wenzelm
parents:
diff
changeset

364 

42806  365 
structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts; 
36950  366 
open Basic_Rule_Insts; 