author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18708  4b3dadb4fe33 
child 18874  05585eee8d74 
permissions  rwrr 
12350  1 
(* Title: Pure/Isar/context_rules.ML 
2 
ID: $Id$ 

3 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 

4 

18728  5 
Declarations of intro/elim/dest rules in Pure (see also 
6 
Provers/classical.ML for a more specialized version of the same idea). 

12350  7 
*) 
8 

9 
signature CONTEXT_RULES = 

10 
sig 

11 
type netpair 

12 
type T 

13372
18790d503fe0
module now right after ProofContext (for locales);
wenzelm
parents:
13105
diff
changeset

13 
val netpair_bang: ProofContext.context > netpair 
18790d503fe0
module now right after ProofContext (for locales);
wenzelm
parents:
13105
diff
changeset

14 
val netpair: ProofContext.context > netpair 
12350  15 
val orderlist: ((int * int) * 'a) list > 'a list 
12399  16 
val find_rules_netpair: bool > thm list > term > netpair > thm list 
13372
18790d503fe0
module now right after ProofContext (for locales);
wenzelm
parents:
13105
diff
changeset

17 
val find_rules: bool > thm list > term > ProofContext.context > thm list list 
18637  18 
val print_rules: Context.generic > unit 
12350  19 
val addSWrapper: ((int > tactic) > int > tactic) > theory > theory 
20 
val addWrapper: ((int > tactic) > int > tactic) > theory > theory 

13372
18790d503fe0
module now right after ProofContext (for locales);
wenzelm
parents:
13105
diff
changeset

21 
val Swrap: ProofContext.context > (int > tactic) > int > tactic 
18790d503fe0
module now right after ProofContext (for locales);
wenzelm
parents:
13105
diff
changeset

22 
val wrap: ProofContext.context > (int > tactic) > int > tactic 
18728  23 
val intro_bang: int option > attribute 
24 
val elim_bang: int option > attribute 

25 
val dest_bang: int option > attribute 

26 
val intro: int option > attribute 

27 
val elim: int option > attribute 

28 
val dest: int option > attribute 

29 
val intro_query: int option > attribute 

30 
val elim_query: int option > attribute 

31 
val dest_query: int option > attribute 

32 
val rule_del: attribute 

33 
val add_args: 

34 
(int option > attribute) > (int option > attribute) > (int option > attribute) > 

35 
Attrib.src > attribute 

12350  36 
end; 
37 

38 
structure ContextRules: CONTEXT_RULES = 

39 
struct 

40 

41 

42 
(** rule declaration contexts **) 

43 

44 
(* rule kinds *) 

45 

46 
val intro_bangK = (0, false); 

47 
val elim_bangK = (0, true); 

48 
val introK = (1, false); 

49 
val elimK = (1, true); 

50 
val intro_queryK = (2, false); 

51 
val elim_queryK = (2, true); 

52 

53 
val kind_names = 

54 
[(intro_bangK, "safe introduction rules (intro!)"), 

55 
(elim_bangK, "safe elimination rules (elim!)"), 

56 
(introK, "introduction rules (intro)"), 

57 
(elimK, "elimination rules (elim)"), 

58 
(intro_queryK, "extra introduction rules (intro?)"), 

59 
(elim_queryK, "extra elimination rules (elim?)")]; 

60 

61 
val rule_kinds = map #1 kind_names; 

62 
val rule_indexes = distinct (map #1 rule_kinds); 

63 

64 

18637  65 
(* context data *) 
12350  66 

67 
type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net; 

68 
val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty); 

69 

70 
datatype T = Rules of 

71 
{next: int, 

72 
rules: (int * ((int * bool) * thm)) list, 

73 
netpairs: netpair list, 

74 
wrappers: (((int > tactic) > int > tactic) * stamp) list * 

75 
(((int > tactic) > int > tactic) * stamp) list}; 

76 

77 
fun make_rules next rules netpairs wrappers = 

78 
Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers}; 

79 

80 
fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) = 

15531  81 
let val w = (case opt_w of SOME w => w  NONE => Tactic.subgoals_of_brl (b, th)) in 
12350  82 
make_rules (next  1) ((w, ((i, b), th)) :: rules) 
18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17511
diff
changeset

83 
(nth_map i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers 
12350  84 
end; 
85 

86 
fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) = 

87 
let 

13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12805
diff
changeset

88 
fun eq_th (_, (_, th')) = Drule.eq_thm_prop (th, th'); 
12350  89 
fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair; 
90 
in 

91 
if not (exists eq_th rules) then rs 

92 
else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers 

93 
end; 

94 

18637  95 
structure Rules = GenericDataFun 
96 
( 

17511  97 
val name = "Isar/rules"; 
12350  98 
type T = T; 
99 

100 
val empty = make_rules ~1 [] empty_netpairs ([], []); 

16424  101 
val extend = I; 
12350  102 

16424  103 
fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...}, 
12350  104 
Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) = 
105 
let 

18637  106 
val wrappers = 
107 
(gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2'); 

12350  108 
val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) => 
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12805
diff
changeset

109 
k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2; 
12350  110 
val next = ~ (length rules); 
15570  111 
val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) => 
18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17511
diff
changeset

112 
nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps) 
12350  113 
(empty_netpairs, next upto ~1 ~~ rules); 
18637  114 
in make_rules (next  1) rules netpairs wrappers end 
12350  115 

18637  116 
fun print generic (Rules {rules, ...}) = 
117 
let 

118 
val ctxt = Context.proof_of generic; 

119 
fun prt_kind (i, b) = 

120 
Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":") 

121 
(List.mapPartial (fn (_, (k, th)) => 

122 
if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE) 

123 
(sort (int_ord o pairself fst) rules)); 

124 
in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end; 

125 
); 

12350  126 

18708  127 
val _ = Context.add_setup Rules.init; 
18637  128 
val print_rules = Rules.print; 
12350  129 

130 

131 
(* access data *) 

132 

18637  133 
fun netpairs ctxt = let val Rules {netpairs, ...} = Rules.get (Context.Proof ctxt) in netpairs end; 
12350  134 
val netpair_bang = hd o netpairs; 
135 
val netpair = hd o tl o netpairs; 

136 

137 

12399  138 
(* retrieving rules *) 
139 

12350  140 
fun untaglist [] = [] 
141 
 untaglist [(k : int * int, x)] = [x] 

142 
 untaglist ((k, x) :: (rest as (k', x') :: _)) = 

143 
if k = k' then untaglist rest 

144 
else x :: untaglist rest; 

145 

16424  146 
fun orderlist brls = 
16512  147 
untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls); 
16424  148 

149 
fun orderlist_no_weight brls = 

16512  150 
untaglist (sort (int_ord o pairself (snd o fst)) brls); 
12399  151 

152 
fun may_unify weighted t net = 

153 
map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t)); 

154 

155 
fun find_erules _ [] = K [] 

12805  156 
 find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (Thm.prop_of fact)); 
16424  157 

12399  158 
fun find_irules w goal = may_unify w (Logic.strip_assums_concl goal); 
12380  159 

12399  160 
fun find_rules_netpair weighted facts goal (inet, enet) = 
161 
find_erules weighted facts enet @ find_irules weighted goal inet; 

12380  162 

16424  163 
fun find_rules weighted facts goals = 
164 
map (find_rules_netpair weighted facts goals) o netpairs; 

12350  165 

166 

12399  167 
(* wrappers *) 
168 

18667  169 
fun gen_add_wrapper upd w = 
18728  170 
Context.theory_map (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) => 
18667  171 
make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers))); 
12350  172 

173 
val addSWrapper = gen_add_wrapper Library.apfst; 

174 
val addWrapper = gen_add_wrapper Library.apsnd; 

175 

176 

177 
fun gen_wrap which ctxt = 

18637  178 
let val Rules {wrappers, ...} = Rules.get (Context.Proof ctxt) 
17351  179 
in fold_rev fst (which wrappers) end; 
12350  180 

181 
val Swrap = gen_wrap #1; 

182 
val wrap = gen_wrap #2; 

183 

184 

185 

186 
(** attributes **) 

187 

188 
(* add and del rules *) 

189 

18637  190 
fun rule_del (x, th) = 
191 
(Rules.map (del_rule th o del_rule (Tactic.make_elim th)) x, th); 

12350  192 

18637  193 
fun rule_add k view opt_w = 
194 
(fn (x, th) => (Rules.map (add_rule k opt_w (view th)) x, th)) o rule_del; 

12350  195 

18637  196 
val intro_bang = rule_add intro_bangK I; 
197 
val elim_bang = rule_add elim_bangK I; 

198 
val dest_bang = rule_add elim_bangK Tactic.make_elim; 

199 
val intro = rule_add introK I; 

200 
val elim = rule_add elimK I; 

201 
val dest = rule_add elimK Tactic.make_elim; 

202 
val intro_query = rule_add intro_queryK I; 

203 
val elim_query = rule_add elim_queryK I; 

204 
val dest_query = rule_add elim_queryK Tactic.make_elim; 

12350  205 

18637  206 
val _ = Context.add_setup 
18728  207 
(snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]); 
18637  208 

12350  209 

18637  210 
(* concrete syntax *) 
211 

212 
fun add_args a b c x = Attrib.syntax 

18692  213 
(Scan.lift ((Args.bang >> K a  Args.query >> K c  Scan.succeed b)  Scan.option Args.nat) 
18637  214 
>> (fn (f, n) => f n)) x; 
215 

216 
val rule_atts = 

18728  217 
[("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"), 
218 
("elim", add_args elim_bang elim elim_query, "declaration of elimination rule"), 

219 
("dest", add_args dest_bang dest dest_query, "declaration of destruction rule"), 

220 
("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del), 

18637  221 
"remove declaration of intro/elim/dest rule")]; 
222 

18708  223 
val _ = Context.add_setup (Attrib.add_attributes rule_atts); 
12350  224 

225 
end; 