author  wenzelm 
Thu, 20 Feb 2014 21:27:14 +0100  
changeset 55635  00e900057b38 
parent 55377  d79c057c68f0 
child 56245  84fc7dfa3cd4 
permissions  rwrr 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41227
diff
changeset

1 
(* Title: Pure/raw_simplifier.ML 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28839
diff
changeset

2 
Author: Tobias Nipkow and Stefan Berghofer, TU Muenchen 
10413  3 

41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41227
diff
changeset

4 
Higherorder Simplification. 
10413  5 
*) 
6 

15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

7 
infix 4 
45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45405
diff
changeset

8 
addsimps delsimps addsimprocs delsimprocs 
52037  9 
setloop addloop delloop 
45625
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45621
diff
changeset

10 
setSSolver addSSolver setSolver addSolver; 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

11 

41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41227
diff
changeset

12 
signature BASIC_RAW_SIMPLIFIER = 
11672  13 
sig 
41227  14 
val simp_depth_limit: int Config.T 
15 
val simp_trace_depth_limit: int Config.T 

40878
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
39163
diff
changeset

16 
val simp_debug: bool Config.T 
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
39163
diff
changeset

17 
val simp_trace: bool Config.T 
51590  18 
type cong_name = bool * string 
15023  19 
type rrule 
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55032
diff
changeset

20 
val mk_rrules: Proof.context > thm list > rrule list 
16807  21 
val eq_rrule: rrule * rrule > bool 
15023  22 
type proc 
17614  23 
type solver 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

24 
val mk_solver: string > (Proof.context > int > tactic) > solver 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

25 
type simpset 
15023  26 
val empty_ss: simpset 
27 
val merge_ss: simpset * simpset > simpset 

30356  28 
val dest_ss: simpset > 
29 
{simps: (string * thm) list, 

30 
procs: (string * cterm list) list, 

51590  31 
congs: (cong_name * thm) list, 
32 
weak_congs: cong_name list, 

30356  33 
loopers: string list, 
34 
unsafe_solvers: string list, 

35 
safe_solvers: string list} 

15023  36 
type simproc 
22234  37 
val eq_simproc: simproc * simproc > bool 
45290  38 
val transform_simproc: morphism > simproc > simproc 
22234  39 
val make_simproc: {name: string, lhss: cterm list, 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

40 
proc: morphism > Proof.context > cterm > thm option, identifier: thm list} > simproc 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

41 
val mk_simproc: string > cterm list > (Proof.context > term > thm option) > simproc 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

42 
val simpset_of: Proof.context > simpset 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

43 
val put_simpset: simpset > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

44 
val simpset_map: Proof.context > (Proof.context > Proof.context) > simpset > simpset 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

45 
val map_theory_simpset: (Proof.context > Proof.context) > theory > theory 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

46 
val empty_simpset: Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

47 
val clear_simpset: Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

48 
val addsimps: Proof.context * thm list > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

49 
val delsimps: Proof.context * thm list > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

50 
val addsimprocs: Proof.context * simproc list > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

51 
val delsimprocs: Proof.context * simproc list > Proof.context 
52037  52 
val setloop: Proof.context * (Proof.context > int > tactic) > Proof.context 
53 
val addloop: Proof.context * (string * (Proof.context > int > tactic)) > Proof.context 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

54 
val delloop: Proof.context * string > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

55 
val setSSolver: Proof.context * solver > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

56 
val addSSolver: Proof.context * solver > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

57 
val setSolver: Proof.context * solver > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

58 
val addSolver: Proof.context * solver > Proof.context 
21708  59 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54731
diff
changeset

60 
val rewrite_rule: Proof.context > thm list > thm > thm 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54731
diff
changeset

61 
val rewrite_goals_rule: Proof.context > thm list > thm > thm 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54731
diff
changeset

62 
val rewrite_goals_tac: Proof.context > thm list > tactic 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54731
diff
changeset

63 
val rewrite_goal_tac: Proof.context > thm list > int > tactic 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54731
diff
changeset

64 
val prune_params_tac: Proof.context > tactic 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54731
diff
changeset

65 
val fold_rule: Proof.context > thm list > thm > thm 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54731
diff
changeset

66 
val fold_goals_tac: Proof.context > thm list > tactic 
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

67 
val norm_hhf: Proof.context > thm > thm 
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

68 
val norm_hhf_protect: Proof.context > thm > thm 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

69 
end; 
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

70 

41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41227
diff
changeset

71 
signature RAW_SIMPLIFIER = 
10413  72 
sig 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41227
diff
changeset

73 
include BASIC_RAW_SIMPLIFIER 
54997  74 
exception SIMPLIFIER of string * thm list 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

75 
type trace_ops 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

76 
val set_trace_ops: trace_ops > theory > theory 
30336  77 
val internal_ss: simpset > 
51590  78 
{congs: (cong_name * thm) list * cong_name list, 
30336  79 
procs: proc Net.net, 
80 
mk_rews: 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

81 
{mk: Proof.context > thm > thm list, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

82 
mk_cong: Proof.context > thm > thm, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

83 
mk_sym: Proof.context > thm > thm option, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

84 
mk_eq_True: Proof.context > thm > thm option, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

85 
reorient: Proof.context > term list > term > term > bool}, 
30336  86 
termless: term * term > bool, 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

87 
subgoal_tac: Proof.context > int > tactic, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

88 
loop_tacs: (string * (Proof.context > int > tactic)) list, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

89 
solvers: solver list * solver list} 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

90 
val map_ss: (Proof.context > Proof.context) > Context.generic > Context.generic 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

91 
val prems_of: Proof.context > thm list 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

92 
val add_simp: thm > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

93 
val del_simp: thm > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

94 
val add_eqcong: thm > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

95 
val del_eqcong: thm > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

96 
val add_cong: thm > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

97 
val del_cong: thm > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

98 
val mksimps: Proof.context > thm > thm list 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

99 
val set_mksimps: (Proof.context > thm > thm list) > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

100 
val set_mkcong: (Proof.context > thm > thm) > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

101 
val set_mksym: (Proof.context > thm > thm option) > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

102 
val set_mkeqTrue: (Proof.context > thm > thm option) > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

103 
val set_termless: (term * term > bool) > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

104 
val set_subgoaler: (Proof.context > int > tactic) > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

105 
val solver: Proof.context > solver > int > tactic 
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset

106 
val simp_depth_limit_raw: Config.raw 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

107 
val default_mk_sym: Proof.context > thm > thm option 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

108 
val simproc_global_i: theory > string > term list > 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

109 
(Proof.context > term > thm option) > simproc 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

110 
val simproc_global: theory > string > string list > 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

111 
(Proof.context > term > thm option) > simproc 
41227  112 
val simp_trace_depth_limit_raw: Config.raw 
113 
val simp_trace_depth_limit_default: int Unsynchronized.ref 

114 
val simp_trace_default: bool Unsynchronized.ref 

115 
val simp_trace_raw: Config.raw 

116 
val simp_debug_raw: Config.raw 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

117 
val add_prems: thm list > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

118 
val set_reorient: (Proof.context > term list > term > term > bool) > 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

119 
Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

120 
val set_solvers: solver list > Proof.context > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

121 
val rewrite_cterm: bool * bool * bool > 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

122 
(Proof.context > thm > thm option) > Proof.context > conv 
16458  123 
val rewrite_term: theory > thm list > (term > term option) list > term > term 
15023  124 
val rewrite_thm: bool * bool * bool > 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

125 
(Proof.context > thm > thm option) > Proof.context > thm > thm 
46465  126 
val generic_rewrite_goal_tac: bool * bool * bool > 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

127 
(Proof.context > tactic) > Proof.context > int > tactic 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54731
diff
changeset

128 
val rewrite: Proof.context > bool > thm list > conv 
10413  129 
end; 
130 

41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41227
diff
changeset

131 
structure Raw_Simplifier: RAW_SIMPLIFIER = 
10413  132 
struct 
133 

15023  134 
(** datatype simpset **) 
135 

51590  136 
(* congruence rules *) 
137 

138 
type cong_name = bool * string; 

139 

140 
fun cong_name (Const (a, _)) = SOME (true, a) 

141 
 cong_name (Free (a, _)) = SOME (false, a) 

142 
 cong_name _ = NONE; 

143 

144 

15023  145 
(* rewrite rules *) 
10413  146 

20546
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

147 
type rrule = 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

148 
{thm: thm, (*the rewrite rule*) 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

149 
name: string, (*name of theorem from which rewrite rule was extracted*) 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

150 
lhs: term, (*the lefthand side*) 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

151 
elhs: cterm, (*the etaccontracted lhs*) 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

152 
extra: bool, (*extra variables outside of elhs*) 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

153 
fo: bool, (*use firstorder matching*) 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

154 
perm: bool}; (*the rewrite rule is permutative*) 
15023  155 

20546
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

156 
(* 
12603  157 
Remarks: 
10413  158 
 elhs is used for matching, 
15023  159 
lhs only for preservation of bound variable names; 
10413  160 
 fo is set iff 
161 
either elhs is firstorder (no Var is applied), 

15023  162 
in which case fomatching is complete, 
10413  163 
or elhs is not a pattern, 
20546
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

164 
in which case there is nothing better to do; 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

165 
*) 
10413  166 

167 
fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) = 

22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22254
diff
changeset

168 
Thm.eq_thm_prop (thm1, thm2); 
15023  169 

20546
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

170 
(* FIXME: it seems that the conditions on extra variables are too liberal if 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

171 
prems are nonempty: does solving the prems really guarantee instantiation of 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

172 
all its Vars? Better: a dynamic check each time a rule is applied. 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

173 
*) 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

174 
fun rewrite_rule_extra_vars prems elhs erhs = 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

175 
let 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

176 
val elhss = elhs :: prems; 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

177 
val tvars = fold Term.add_tvars elhss []; 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

178 
val vars = fold Term.add_vars elhss []; 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

179 
in 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

180 
erhs > Term.exists_type (Term.exists_subtype 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

181 
(fn TVar v => not (member (op =) tvars v)  _ => false)) orelse 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

182 
erhs > Term.exists_subterm 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

183 
(fn Var v => not (member (op =) vars v)  _ => false) 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

184 
end; 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

185 

8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

186 
fun rrule_extra_vars elhs thm = 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

187 
rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm); 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

188 

15023  189 
fun mk_rrule2 {thm, name, lhs, elhs, perm} = 
190 
let 

20546
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

191 
val t = term_of elhs; 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

192 
val fo = Pattern.first_order t orelse not (Pattern.pattern t); 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

193 
val extra = rrule_extra_vars elhs thm; 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

194 
in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end; 
10413  195 

15023  196 
(*simple test for looping rewrite rules and stupid orientations*) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

197 
fun default_reorient ctxt prems lhs rhs = 
15023  198 
rewrite_rule_extra_vars prems lhs rhs 
199 
orelse 

200 
is_Var (head_of lhs) 

201 
orelse 

16305  202 
(* turns t = x around, which causes a headache if x is a local variable  
203 
usually it is very useful :( 

204 
is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs)) 

205 
andalso not(exists_subterm is_Var lhs) 

206 
orelse 

207 
*) 

16842  208 
exists (fn t => Logic.occs (lhs, t)) (rhs :: prems) 
15023  209 
orelse 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

210 
null prems andalso Pattern.matches (Proof_Context.theory_of ctxt) (lhs, rhs) 
10413  211 
(*the condition "null prems" is necessary because conditional rewrites 
212 
with extra variables in the conditions may terminate although 

15023  213 
the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*) 
214 
orelse 

215 
is_Const lhs andalso not (is_Const rhs); 

10413  216 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

217 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

218 
(* simplification procedures *) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

219 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

220 
datatype proc = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

221 
Proc of 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

222 
{name: string, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

223 
lhs: cterm, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

224 
proc: Proof.context > cterm > thm option, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

225 
id: stamp * thm list}; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

226 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

227 
fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

228 
s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

229 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

230 
fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

231 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

232 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

233 
(* solvers *) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

234 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

235 
datatype solver = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

236 
Solver of 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

237 
{name: string, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

238 
solver: Proof.context > int > tactic, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

239 
id: stamp}; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

240 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

241 
fun mk_solver name solver = Solver {name = name, solver = solver, id = stamp ()}; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

242 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

243 
fun solver_name (Solver {name, ...}) = name; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

244 
fun solver ctxt (Solver {solver = tac, ...}) = tac ctxt; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

245 
fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

246 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

247 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

248 
(* simplification sets *) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

249 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

250 
(*A simpset contains data required during conversion: 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

251 
rules: discrimination net of rewrite rules; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

252 
prems: current premises; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

253 
depth: simp_depth and exceeded flag; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

254 
congs: association list of congruence rules and 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

255 
a list of `weak' congruence constants. 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

256 
A congruence is `weak' if it avoids normalization of some argument. 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

257 
procs: discrimination net of simplification procedures 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

258 
(functions that prove rewrite rules on the fly); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

259 
mk_rews: 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

260 
mk: turn simplification thms into rewrite rules; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

261 
mk_cong: prepare congruence rules; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

262 
mk_sym: turn == around; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

263 
mk_eq_True: turn P into P == True; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

264 
termless: relation for ordered rewriting;*) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

265 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

266 
datatype simpset = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

267 
Simpset of 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

268 
{rules: rrule Net.net, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

269 
prems: thm list, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

270 
depth: int * bool Unsynchronized.ref} * 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

271 
{congs: (cong_name * thm) list * cong_name list, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

272 
procs: proc Net.net, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

273 
mk_rews: 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

274 
{mk: Proof.context > thm > thm list, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

275 
mk_cong: Proof.context > thm > thm, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

276 
mk_sym: Proof.context > thm > thm option, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

277 
mk_eq_True: Proof.context > thm > thm option, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

278 
reorient: Proof.context > term list > term > term > bool}, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

279 
termless: term * term > bool, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

280 
subgoal_tac: Proof.context > int > tactic, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

281 
loop_tacs: (string * (Proof.context > int > tactic)) list, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

282 
solvers: solver list * solver list}; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

283 

54728  284 
fun internal_ss (Simpset (_, ss2)) = ss2; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

285 

55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

286 
fun make_ss1 (rules, prems, depth) = {rules = rules, prems = prems, depth = depth}; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

287 

55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

288 
fun map_ss1 f {rules, prems, depth} = make_ss1 (f (rules, prems, depth)); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

289 

54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

290 
fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

291 
{congs = congs, procs = procs, mk_rews = mk_rews, termless = termless, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

292 
subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers}; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

293 

54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

294 
fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} = 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

295 
make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

296 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

297 
fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

298 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

299 
fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

300 
{simps = Net.entries rules 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

301 
> map (fn {name, thm, ...} => (name, thm)), 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

302 
procs = Net.entries procs 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

303 
> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id)) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

304 
> partition_eq (eq_snd eq_procid) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

305 
> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)), 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

306 
congs = #1 congs, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

307 
weak_congs = #2 congs, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

308 
loopers = map fst loop_tacs, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

309 
unsafe_solvers = map solver_name (#1 solvers), 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

310 
safe_solvers = map solver_name (#2 solvers)}; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

311 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

312 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

313 
(* empty *) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

314 

55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

315 
fun init_ss depth mk_rews termless subgoal_tac solvers = 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

316 
make_simpset ((Net.empty, [], depth), 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

317 
(([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers)); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

318 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

319 
fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

320 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

321 
val empty_ss = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

322 
init_ss (0, Unsynchronized.ref false) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

323 
{mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

324 
mk_cong = K I, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

325 
mk_sym = default_mk_sym, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

326 
mk_eq_True = K (K NONE), 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

327 
reorient = default_reorient} 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

328 
Term_Ord.termless (K (K no_tac)) ([], []); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

329 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

330 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

331 
(* merge *) (*NOTE: ignores some fields of 2nd simpset*) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

332 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

333 
fun merge_ss (ss1, ss2) = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

334 
if pointer_eq (ss1, ss2) then ss1 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

335 
else 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

336 
let 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

337 
val Simpset ({rules = rules1, prems = prems1, depth = depth1}, 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

338 
{congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

339 
loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1; 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

340 
val Simpset ({rules = rules2, prems = prems2, depth = depth2}, 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

341 
{congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

342 
loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

343 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

344 
val rules' = Net.merge eq_rrule (rules1, rules2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

345 
val prems' = Thm.merge_thms (prems1, prems2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

346 
val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

347 
val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

348 
val weak' = merge (op =) (weak1, weak2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

349 
val procs' = Net.merge eq_proc (procs1, procs2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

350 
val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

351 
val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

352 
val solvers' = merge eq_solver (solvers1, solvers2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

353 
in 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

354 
make_simpset ((rules', prems', depth'), ((congs', weak'), procs', 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

355 
mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'))) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

356 
end; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

357 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

358 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

359 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

360 
(** context data **) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

361 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

362 
structure Simpset = Generic_Data 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

363 
( 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

364 
type T = simpset; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

365 
val empty = empty_ss; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

366 
val extend = I; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

367 
val merge = merge_ss; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

368 
); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

369 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

370 
val simpset_of = Simpset.get o Context.Proof; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

371 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

372 
fun map_simpset f = Context.proof_map (Simpset.map f); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

373 
fun map_simpset1 f = map_simpset (fn Simpset (ss1, ss2) => Simpset (map_ss1 f ss1, ss2)); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

374 
fun map_simpset2 f = map_simpset (fn Simpset (ss1, ss2) => Simpset (ss1, map_ss2 f ss2)); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

375 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

376 
fun simpset_map ctxt f ss = ctxt > map_simpset (K ss) > f > Context.Proof > Simpset.get; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

377 

55377
d79c057c68f0
more elementary put_simpset: exchange the simplifier configuration outright, which is particularly relevant concerning cumulative depth, e.g. for Product_Type.split_beta in the subsequent example:
wenzelm
parents:
55316
diff
changeset

378 
fun put_simpset ss = map_simpset (K ss); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

379 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

380 
val empty_simpset = put_simpset empty_ss; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

381 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

382 
fun map_theory_simpset f thy = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

383 
let 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

384 
val ctxt' = f (Proof_Context.init_global thy); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

385 
val thy' = Proof_Context.theory_of ctxt'; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

386 
in Context.theory_map (Simpset.map (K (simpset_of ctxt'))) thy' end; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

387 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

388 
fun map_ss f = Context.mapping (map_theory_simpset f) f; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

389 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

390 
val clear_simpset = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

391 
map_simpset (fn Simpset ({depth, ...}, {mk_rews, termless, subgoal_tac, solvers, ...}) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

392 
init_ss depth mk_rews termless subgoal_tac solvers); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

393 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

394 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

395 
(* simp depth *) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

396 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

397 
val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100)); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

398 
val simp_depth_limit = Config.int simp_depth_limit_raw; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

399 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

400 
val simp_trace_depth_limit_default = Unsynchronized.ref 1; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

401 
val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit" 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

402 
(fn _ => Config.Int (! simp_trace_depth_limit_default)); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

403 
val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

404 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

405 
fun inc_simp_depth ctxt = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

406 
ctxt > map_simpset1 (fn (rules, prems, (depth, exceeded)) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

407 
(rules, prems, 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

408 
(depth + 1, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

409 
if depth = Config.get ctxt simp_trace_depth_limit 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

410 
then Unsynchronized.ref false else exceeded))); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

411 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

412 
fun simp_depth ctxt = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

413 
let val Simpset ({depth = (depth, _), ...}, _) = simpset_of ctxt 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

414 
in depth end; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

415 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

416 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

417 
(* diagnostics *) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

418 

54997  419 
exception SIMPLIFIER of string * thm list; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

420 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

421 
val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false)); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

422 
val simp_debug = Config.bool simp_debug_raw; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

423 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

424 
val simp_trace_default = Unsynchronized.ref false; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

425 
val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default)); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

426 
val simp_trace = Config.bool simp_trace_raw; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

427 

55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

428 
fun cond_warning ctxt msg = 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

429 
if Context_Position.is_visible ctxt then warning (msg ()) else (); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

430 

55031  431 
fun cond_tracing' ctxt flag msg = 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

432 
if Config.get ctxt flag then 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

433 
let 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

434 
val Simpset ({depth = (depth, exceeded), ...}, _) = simpset_of ctxt; 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

435 
val depth_limit = Config.get ctxt simp_trace_depth_limit; 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

436 
in 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

437 
if depth > depth_limit then 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

438 
if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true) 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

439 
else (tracing (enclose "[" "]" (string_of_int depth) ^ msg ()); exceeded := false) 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

440 
end 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

441 
else (); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

442 

55031  443 
fun cond_tracing ctxt = cond_tracing' ctxt simp_trace; 
444 

55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

445 
fun print_term ctxt s t = 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

446 
s ^ "\n" ^ Syntax.string_of_term ctxt t; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

447 

55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

448 
fun print_thm ctxt s (name, th) = 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

449 
print_term ctxt (if name = "" then s else s ^ " " ^ quote name ^ ":") (Thm.full_prop_of th); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

450 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

451 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

452 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

453 
(** simpset operations **) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

454 

55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

455 
(* prems *) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

456 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

457 
fun prems_of ctxt = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

458 
let val Simpset ({prems, ...}, _) = simpset_of ctxt in prems end; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

459 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

460 
fun add_prems ths = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

461 
map_simpset1 (fn (rules, prems, depth) => (rules, ths @ prems, depth)); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

462 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

463 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

464 
(* maintain simp rules *) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

465 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

466 
fun del_rrule (rrule as {thm, elhs, ...}) ctxt = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

467 
ctxt > map_simpset1 (fn (rules, prems, depth) => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

468 
(Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, depth)) 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

469 
handle Net.DELETE => 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

470 
(cond_warning ctxt (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm)); ctxt); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

471 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

472 
fun insert_rrule (rrule as {thm, name, ...}) ctxt = 
55031  473 
(cond_tracing ctxt (fn () => print_thm ctxt "Adding rewrite rule" (name, thm)); 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

474 
ctxt > map_simpset1 (fn (rules, prems, depth) => 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

475 
let 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

476 
val rrule2 as {elhs, ...} = mk_rrule2 rrule; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

477 
val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules; 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

478 
in (rules', prems, depth) end) 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

479 
handle Net.INSERT => 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

480 
(cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm)); 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

481 
ctxt)); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

482 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

483 
local 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

484 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

485 
fun vperm (Var _, Var _) = true 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

486 
 vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

487 
 vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

488 
 vperm (t, u) = (t = u); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

489 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

490 
fun var_perm (t, u) = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

491 
vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

492 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

493 
in 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

494 

10413  495 
fun decomp_simp thm = 
15023  496 
let 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

497 
val prop = Thm.prop_of thm; 
15023  498 
val prems = Logic.strip_imp_prems prop; 
499 
val concl = Drule.strip_imp_concl (Thm.cprop_of thm); 

22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22892
diff
changeset

500 
val (lhs, rhs) = Thm.dest_equals concl handle TERM _ => 
54997  501 
raise SIMPLIFIER ("Rewrite rule not a metaequality", [thm]); 
20579  502 
val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs)); 
18929  503 
val erhs = Envir.eta_contract (term_of rhs); 
15023  504 
val perm = 
505 
var_perm (term_of elhs, erhs) andalso 

506 
not (term_of elhs aconv erhs) andalso 

507 
not (is_Var (term_of elhs)); 

52091  508 
in (prems, term_of lhs, elhs, term_of rhs, perm) end; 
10413  509 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

510 
end; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

511 

12783  512 
fun decomp_simp' thm = 
52091  513 
let val (_, lhs, _, rhs, _) = decomp_simp thm in 
54997  514 
if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", [thm]) 
12979
4c76bce4ce39
decomp_simp': use lhs instead of elhs (preserves more bound variable names);
wenzelm
parents:
12783
diff
changeset

515 
else (lhs, rhs) 
12783  516 
end; 
517 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

518 
fun mk_eq_True ctxt (thm, name) = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

519 
let val Simpset (_, {mk_rews = {mk_eq_True, ...}, ...}) = simpset_of ctxt in 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

520 
(case mk_eq_True ctxt thm of 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

521 
NONE => [] 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

522 
 SOME eq_True => 
52091  523 
let val (_, lhs, elhs, _, _) = decomp_simp eq_True; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

524 
in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

525 
end; 
10413  526 

15023  527 
(*create the rewrite rule and possibly also the eq_True variant, 
528 
in case there are extra vars on the rhs*) 

52082  529 
fun rrule_eq_True ctxt thm name lhs elhs rhs thm2 = 
15023  530 
let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in 
20546
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

531 
if rewrite_rule_extra_vars [] lhs rhs then 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

532 
mk_eq_True ctxt (thm2, name) @ [rrule] 
20546
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

533 
else [rrule] 
10413  534 
end; 
535 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

536 
fun mk_rrule ctxt (thm, name) = 
52091  537 
let val (prems, lhs, elhs, rhs, perm) = decomp_simp thm in 
15023  538 
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] 
539 
else 

540 
(*weak test for loops*) 

541 
if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs) 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

542 
then mk_eq_True ctxt (thm, name) 
52082  543 
else rrule_eq_True ctxt thm name lhs elhs rhs thm 
10413  544 
end; 
545 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

546 
fun orient_rrule ctxt (thm, name) = 
18208  547 
let 
52091  548 
val (prems, lhs, elhs, rhs, perm) = decomp_simp thm; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

549 
val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = simpset_of ctxt; 
18208  550 
in 
15023  551 
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

552 
else if reorient ctxt prems lhs rhs then 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

553 
if reorient ctxt prems rhs lhs 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

554 
then mk_eq_True ctxt (thm, name) 
15023  555 
else 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

556 
(case mk_sym ctxt thm of 
18208  557 
NONE => [] 
558 
 SOME thm' => 

52091  559 
let val (_, lhs', elhs', rhs', _) = decomp_simp thm' 
52082  560 
in rrule_eq_True ctxt thm' name lhs' elhs' rhs' thm end) 
561 
else rrule_eq_True ctxt thm name lhs elhs rhs thm 

10413  562 
end; 
563 

54982  564 
fun extract_rews ctxt thms = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

565 
let val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

566 
in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ctxt thm)) thms end; 
10413  567 

54982  568 
fun extract_safe_rrules ctxt thm = 
569 
maps (orient_rrule ctxt) (extract_rews ctxt [thm]); 

10413  570 

55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55032
diff
changeset

571 
fun mk_rrules ctxt thms = 
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55032
diff
changeset

572 
let 
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55032
diff
changeset

573 
val rews = extract_rews ctxt thms 
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55032
diff
changeset

574 
val raw_rrules = flat (map (mk_rrule ctxt) rews) 
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55032
diff
changeset

575 
in map mk_rrule2 raw_rrules end 
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55032
diff
changeset

576 

10413  577 

20028
b9752164ad92
add/del_simps: warning for inactive simpset (no context);
wenzelm
parents:
19798
diff
changeset

578 
(* add/del rules explicitly *) 
10413  579 

54982  580 
fun comb_simps ctxt comb mk_rrule thms = 
20028
b9752164ad92
add/del_simps: warning for inactive simpset (no context);
wenzelm
parents:
19798
diff
changeset

581 
let 
54982  582 
val rews = extract_rews ctxt thms; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

583 
in fold (fold comb o mk_rrule) rews ctxt end; 
10413  584 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

585 
fun ctxt addsimps thms = 
54982  586 
comb_simps ctxt insert_rrule (mk_rrule ctxt) thms; 
10413  587 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

588 
fun ctxt delsimps thms = 
54982  589 
comb_simps ctxt del_rrule (map mk_rrule2 o mk_rrule ctxt) thms; 
15023  590 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

591 
fun add_simp thm ctxt = ctxt addsimps [thm]; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

592 
fun del_simp thm ctxt = ctxt delsimps [thm]; 
15023  593 

594 
(* congs *) 

10413  595 

15023  596 
local 
597 

598 
fun is_full_cong_prems [] [] = true 

599 
 is_full_cong_prems [] _ = false 

600 
 is_full_cong_prems (p :: prems) varpairs = 

601 
(case Logic.strip_assums_concl p of 

602 
Const ("==", _) $ lhs $ rhs => 

603 
let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in 

604 
is_Var x andalso forall is_Bound xs andalso 

20972  605 
not (has_duplicates (op =) xs) andalso xs = ys andalso 
20671  606 
member (op =) varpairs (x, y) andalso 
19303  607 
is_full_cong_prems prems (remove (op =) (x, y) varpairs) 
15023  608 
end 
609 
 _ => false); 

610 

611 
fun is_full_cong thm = 

10413  612 
let 
43597  613 
val prems = Thm.prems_of thm and concl = Thm.concl_of thm; 
15023  614 
val (lhs, rhs) = Logic.dest_equals concl; 
615 
val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs; 

10413  616 
in 
20972  617 
f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso 
15023  618 
is_full_cong_prems prems (xs ~~ ys) 
10413  619 
end; 
620 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

621 
fun mk_cong ctxt = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

622 
let val Simpset (_, {mk_rews = {mk_cong = f, ...}, ...}) = simpset_of ctxt 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

623 
in f ctxt end; 
45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45405
diff
changeset

624 

f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45405
diff
changeset

625 
in 
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45405
diff
changeset

626 

54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

627 
fun add_eqcong thm ctxt = ctxt > map_simpset2 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

628 
(fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => 
15023  629 
let 
45621  630 
val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) 
54997  631 
handle TERM _ => raise SIMPLIFIER ("Congruence not a metaequality", [thm]); 
18929  632 
(*val lhs = Envir.eta_contract lhs;*) 
45621  633 
val a = the (cong_name (head_of lhs)) handle Option.Option => 
54997  634 
raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]); 
22221
8a8aa6114a89
changed cong alist  now using AList operations instead of overwrite_warn
haftmann
parents:
22008
diff
changeset

635 
val (xs, weak) = congs; 
38834
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

636 
val _ = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

637 
if AList.defined (op =) xs a then 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

638 
cond_warning ctxt (fn () => "Overwriting congruence rule for " ^ quote (#2 a)) 
22221
8a8aa6114a89
changed cong alist  now using AList operations instead of overwrite_warn
haftmann
parents:
22008
diff
changeset

639 
else (); 
30908
7ccf4a3d764c
replace type cong = {thm : thm, lhs : term} by plain thm  the other component has been unused for a long time.
krauss
parents:
30552
diff
changeset

640 
val xs' = AList.update (op =) (a, thm) xs; 
22221
8a8aa6114a89
changed cong alist  now using AList operations instead of overwrite_warn
haftmann
parents:
22008
diff
changeset

641 
val weak' = if is_full_cong thm then weak else a :: weak; 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

642 
in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); 
10413  643 

54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

644 
fun del_eqcong thm ctxt = ctxt > map_simpset2 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

645 
(fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => 
15023  646 
let 
45621  647 
val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) 
54997  648 
handle TERM _ => raise SIMPLIFIER ("Congruence not a metaequality", [thm]); 
18929  649 
(*val lhs = Envir.eta_contract lhs;*) 
20057  650 
val a = the (cong_name (head_of lhs)) handle Option.Option => 
54997  651 
raise SIMPLIFIER ("Congruence must start with a constant", [thm]); 
22221
8a8aa6114a89
changed cong alist  now using AList operations instead of overwrite_warn
haftmann
parents:
22008
diff
changeset

652 
val (xs, _) = congs; 
51590  653 
val xs' = filter_out (fn (x : cong_name, _) => x = a) xs; 
30908
7ccf4a3d764c
replace type cong = {thm : thm, lhs : term} by plain thm  the other component has been unused for a long time.
krauss
parents:
30552
diff
changeset

654 
val weak' = xs' > map_filter (fn (a, thm) => 
15531  655 
if is_full_cong thm then NONE else SOME a); 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

656 
in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); 
10413  657 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

658 
fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

659 
fun del_cong thm ctxt = del_eqcong (mk_cong ctxt thm) ctxt; 
15023  660 

661 
end; 

10413  662 

663 

15023  664 
(* simprocs *) 
665 

22234  666 
datatype simproc = 
667 
Simproc of 

668 
{name: string, 

669 
lhss: cterm list, 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

670 
proc: morphism > Proof.context > cterm > thm option, 
22234  671 
id: stamp * thm list}; 
672 

673 
fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2); 

22008  674 

45290  675 
fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) = 
22234  676 
Simproc 
677 
{name = name, 

678 
lhss = map (Morphism.cterm phi) lhss, 

22669  679 
proc = Morphism.transform phi proc, 
22234  680 
id = (s, Morphism.fact phi ths)}; 
681 

682 
fun make_simproc {name, lhss, proc, identifier} = 

683 
Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)}; 

22008  684 

685 
fun mk_simproc name lhss proc = 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

686 
make_simproc {name = name, lhss = lhss, proc = fn _ => fn ctxt => fn ct => 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

687 
proc ctxt (term_of ct), identifier = []}; 
22008  688 

35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35408
diff
changeset

689 
(* FIXME avoid global thy and Logic.varify_global *) 
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
36944
diff
changeset

690 
fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global); 
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
36944
diff
changeset

691 
fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy); 
22008  692 

693 

15023  694 
local 
10413  695 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

696 
fun add_proc (proc as Proc {name, lhs, ...}) ctxt = 
55031  697 
(cond_tracing ctxt (fn () => 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

698 
print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") (term_of lhs)); 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

699 
ctxt > map_simpset2 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

700 
(fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

701 
(congs, Net.insert_term eq_proc (term_of lhs, proc) procs, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

702 
mk_rews, termless, subgoal_tac, loop_tacs, solvers)) 
15023  703 
handle Net.INSERT => 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

704 
(cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name); 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

705 
ctxt)); 
10413  706 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

707 
fun del_proc (proc as Proc {name, lhs, ...}) ctxt = 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

708 
ctxt > map_simpset2 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

709 
(fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

710 
(congs, Net.delete_term eq_proc (term_of lhs, proc) procs, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

711 
mk_rews, termless, subgoal_tac, loop_tacs, solvers)) 
15023  712 
handle Net.DELETE => 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

713 
(cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset"); 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

714 
ctxt); 
10413  715 

22234  716 
fun prep_procs (Simproc {name, lhss, proc, id}) = 
22669  717 
lhss > map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id}); 
22234  718 

15023  719 
in 
10413  720 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

721 
fun ctxt addsimprocs ps = fold (fold add_proc o prep_procs) ps ctxt; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

722 
fun ctxt delsimprocs ps = fold (fold del_proc o prep_procs) ps ctxt; 
10413  723 

15023  724 
end; 
10413  725 

726 

727 
(* mk_rews *) 

728 

15023  729 
local 
730 

54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

731 
fun map_mk_rews f = 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

732 
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

733 
let 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

734 
val {mk, mk_cong, mk_sym, mk_eq_True, reorient} = mk_rews; 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

735 
val (mk', mk_cong', mk_sym', mk_eq_True', reorient') = 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

736 
f (mk, mk_cong, mk_sym, mk_eq_True, reorient); 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

737 
val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True', 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

738 
reorient = reorient'}; 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

739 
in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end); 
15023  740 

741 
in 

10413  742 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

743 
fun mksimps ctxt = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

744 
let val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

745 
in mk ctxt end; 
30318
3d03190d2864
replaced archaic use of rep_ss by Simplifier.mksimps;
wenzelm
parents:
29269
diff
changeset

746 

45625
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45621
diff
changeset

747 
fun set_mksimps mk = map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) => 
18208  748 
(mk, mk_cong, mk_sym, mk_eq_True, reorient)); 
15023  749 

45625
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45621
diff
changeset

750 
fun set_mkcong mk_cong = map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) => 
18208  751 
(mk, mk_cong, mk_sym, mk_eq_True, reorient)); 
10413  752 

45625
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45621
diff
changeset

753 
fun set_mksym mk_sym = map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) => 
18208  754 
(mk, mk_cong, mk_sym, mk_eq_True, reorient)); 
10413  755 

45625
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45621
diff
changeset

756 
fun set_mkeqTrue mk_eq_True = map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) => 
18208  757 
(mk, mk_cong, mk_sym, mk_eq_True, reorient)); 
758 

759 
fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) => 

760 
(mk, mk_cong, mk_sym, mk_eq_True, reorient)); 

15023  761 

762 
end; 

763 

14242
ec70653a02bf
Added access to the mk_rews field (and friends).
skalberg
parents:
14040
diff
changeset

764 

10413  765 
(* termless *) 
766 

45625
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45621
diff
changeset

767 
fun set_termless termless = 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

768 
map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) => 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

769 
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

770 

107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

771 

15023  772 
(* tactics *) 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

773 

45625
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45621
diff
changeset

774 
fun set_subgoaler subgoal_tac = 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

775 
map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) => 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

776 
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

777 

52037  778 
fun ctxt setloop tac = ctxt > 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

779 
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) => 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

780 
(congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers)); 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

781 

52037  782 
fun ctxt addloop (name, tac) = ctxt > 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

783 
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => 
15023  784 
(congs, procs, mk_rews, termless, subgoal_tac, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

785 
AList.update (op =) (name, tac) loop_tacs, solvers)); 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

786 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

787 
fun ctxt delloop name = ctxt > 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

788 
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => 
21286
b5e7b80caa6a
introduces canonical AList functions for loop_tacs
haftmann
parents:
20972
diff
changeset

789 
(congs, procs, mk_rews, termless, subgoal_tac, 
38834
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

790 
(if AList.defined (op =) loop_tacs name then () 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

791 
else cond_warning ctxt (fn () => "No such looper in simpset: " ^ quote name); 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

792 
AList.delete (op =) name loop_tacs), solvers)); 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

793 

54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

794 
fun ctxt setSSolver solver = ctxt > map_simpset2 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

795 
(fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, _)) => 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

796 
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]))); 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

797 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

798 
fun ctxt addSSolver solver = ctxt > map_simpset2 (fn (congs, procs, mk_rews, termless, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

799 
subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

800 
subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers))); 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

801 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

802 
fun ctxt setSolver solver = ctxt > map_simpset2 (fn (congs, procs, mk_rews, termless, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

803 
subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless, 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

804 
subgoal_tac, loop_tacs, ([solver], solvers))); 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

805 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

806 
fun ctxt addSolver solver = ctxt > map_simpset2 (fn (congs, procs, mk_rews, termless, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

807 
subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

808 
subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers))); 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

809 

15023  810 
fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless, 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

811 
subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless, 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

812 
subgoal_tac, loop_tacs, (solvers, solvers))); 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

813 

c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

814 

c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

815 
(* trace operations *) 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

816 

54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

817 
type trace_ops = 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

818 
{trace_invoke: {depth: int, term: term} > Proof.context > Proof.context, 
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55032
diff
changeset

819 
trace_apply: {unconditional: bool, term: term, thm: thm, rrule: rrule} > 
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

820 
Proof.context > (Proof.context > (thm * term) option) > (thm * term) option}; 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

821 

54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

822 
structure Trace_Ops = Theory_Data 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

823 
( 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

824 
type T = trace_ops; 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

825 
val empty: T = 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

826 
{trace_invoke = fn _ => fn ctxt => ctxt, 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

827 
trace_apply = fn _ => fn ctxt => fn cont => cont ctxt}; 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

828 
val extend = I; 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

829 
fun merge (trace_ops, _) = trace_ops; 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

830 
); 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

831 

384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

832 
val set_trace_ops = Trace_Ops.put; 
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

833 

384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54729
diff
changeset

834 
val trace_ops = Trace_Ops.get o Proof_Context.theory_of; 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

835 
fun trace_invoke args ctxt = #trace_invoke (trace_ops ctxt) args ctxt; 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

836 
fun trace_apply args ctxt = #trace_apply (trace_ops ctxt) args ctxt; 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

837 

107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

838 

107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
15001
diff
changeset

839 

10413  840 
(** rewriting **) 
841 

842 
(* 

843 
Uses conversions, see: 

844 
L C Paulson, A higherorder implementation of rewriting, 

845 
Science of Computer Programming 3 (1983), pages 119149. 

846 
*) 

847 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

848 
fun check_conv ctxt msg thm thm' = 
10413  849 
let 
36944  850 
val thm'' = Thm.transitive thm thm' handle THM _ => 
851 
Thm.transitive thm (Thm.transitive 

852 
(Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm') 

55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

853 
val _ = 
55031  854 
if msg then cond_tracing ctxt (fn () => print_thm ctxt "SUCCEEDED" ("", thm')) 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

855 
else (); 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

856 
in SOME thm'' end 
10413  857 
handle THM _ => 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

858 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

859 
val _ $ _ $ prop0 = Thm.prop_of thm; 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

860 
val _ = 
55032
b49366215417
back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;
wenzelm
parents:
55031
diff
changeset

861 
cond_tracing ctxt (fn () => 
b49366215417
back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;
wenzelm
parents:
55031
diff
changeset

862 
print_thm ctxt "Proved wrong theorem (bad subgoaler?)" ("", thm') ^ "\n" ^ 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

863 
print_term ctxt "Should have proved:" prop0); 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

864 
in NONE end; 
10413  865 

866 

867 
(* mk_procrule *) 

868 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

869 
fun mk_procrule ctxt thm = 
52091  870 
let val (prems, lhs, elhs, rhs, _) = decomp_simp thm in 
15023  871 
if rewrite_rule_extra_vars prems lhs rhs 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

872 
then (cond_warning ctxt (fn () => print_thm ctxt "Extra vars on rhs:" ("", thm)); []) 
15023  873 
else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}] 
10413  874 
end; 
875 

876 

15023  877 
(* rewritec: conversion to apply the meta simpset to a term *) 
10413  878 

15023  879 
(*Since the rewriting strategy is bottomup, we avoid renormalizing already 
880 
normalized terms by carrying around the rhs of the rewrite rule just 

881 
applied. This is called the `skeleton'. It is decomposed in parallel 

882 
with the term. Once a Var is encountered, the corresponding term is 

883 
already in normal form. 

884 
skel0 is a dummy skeleton that is to enforce complete normalization.*) 

885 

10413  886 
val skel0 = Bound 0; 
887 

15023  888 
(*Use rhs as skeleton only if the lhs does not contain unnormalized bits. 
889 
The latter may happen iff there are weak congruence rules for constants 

890 
in the lhs.*) 

10413  891 

15023  892 
fun uncond_skel ((_, weak), (lhs, rhs)) = 
893 
if null weak then rhs (*optimization*) 

51591
e4aeb102ad70
amended uncond_skel to observe notion of cong_name properly  may affect simplification with Free congs;
wenzelm
parents:
51590
diff
changeset

894 
else if exists_subterm 
e4aeb102ad70
amended uncond_skel to observe notion of cong_name properly  may affect simplification with Free congs;
wenzelm
parents:
51590
diff
changeset

895 
(fn Const (a, _) => member (op =) weak (true, a) 
e4aeb102ad70
amended uncond_skel to observe notion of cong_name properly  may affect simplification with Free congs;
wenzelm
parents:
51590
diff
changeset

896 
 Free (a, _) => member (op =) weak (false, a) 
e4aeb102ad70
amended uncond_skel to observe notion of cong_name properly  may affect simplification with Free congs;
wenzelm
parents:
51590
diff
changeset

897 
 _ => false) lhs then skel0 
15023  898 
else rhs; 
899 

900 
(*Behaves like unconditional rule if rhs does not contain vars not in the lhs. 

901 
Otherwise those vars may become instantiated with unnormalized terms 

902 
while the premises are solved.*) 

903 

32797  904 
fun cond_skel (args as (_, (lhs, rhs))) = 
33038  905 
if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args 
10413  906 
else skel0; 
907 

908 
(* 

15023  909 
Rewriting  we try in order: 
10413  910 
(1) beta reduction 
911 
(2) unconditional rewrite rules 

912 
(3) conditional rewrite rules 

913 
(4) simplification procedures 

914 

915 
IMPORTANT: rewrite rules must not introduce new Vars or TVars! 

916 
*) 

917 

52091  918 
fun rewritec (prover, maxt) ctxt t = 
10413  919 
let 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

920 
val Simpset ({rules, ...}, {congs, procs, termless, ...}) = simpset_of ctxt; 
10413  921 
val eta_thm = Thm.eta_conversion t; 
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22892
diff
changeset

922 
val eta_t' = Thm.rhs_of eta_thm; 
10413  923 
val eta_t = term_of eta_t'; 
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55032
diff
changeset

924 
fun rew rrule = 
10413  925 
let 
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55032
diff
changeset

926 
val {thm, name, lhs, elhs, extra, fo, perm} = rrule 
32797  927 
val prop = Thm.prop_of thm; 
20546
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

928 
val (rthm, elhs') = 
8923deb735ad
rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
wenzelm
parents:
20330
diff
changeset

929 
if maxt = ~1 orelse not extra then (thm, elhs) 
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22892
diff
changeset

930 
else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs); 
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22892
diff
changeset

931 
val insts = 
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22892
diff
changeset

932 
if fo then Thm.first_order_match (elhs', eta_t') 
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22892
diff
changeset

933 
else Thm.match (elhs', eta_t'); 
10413  934 
val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm); 
14643  935 
val prop' = Thm.prop_of thm'; 
21576  936 
val unconditional = (Logic.count_prems prop' = 0); 
54725  937 
val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop'); 
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55032
diff
changeset

938 
val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', rrule = rrule}; 
10413  939 
in 
11295  940 
if perm andalso not (termless (rhs', lhs')) 
54725  941 
then 
55031  942 
(cond_tracing ctxt (fn () => 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

943 
print_thm ctxt "Cannot apply permutative rewrite rule" (name, thm) ^ "\n" ^ 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

944 
print_thm ctxt "Term does not become smaller:" ("", thm')); 
54725  945 
NONE) 
946 
else 

55031  947 
(cond_tracing ctxt (fn () => 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

948 
print_thm ctxt "Applying instance of rewrite rule" (name, thm)); 
54725  949 
if unconditional 
950 
then 

55031  951 
(cond_tracing ctxt (fn () => print_thm ctxt "Rewriting:" ("", thm')); 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

952 
trace_apply trace_args ctxt (fn ctxt' => 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

953 
let 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

954 
val lr = Logic.dest_equals prop; 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

955 
val SOME thm'' = check_conv ctxt' false eta_thm thm'; 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

956 
in SOME (thm'', uncond_skel (congs, lr)) end)) 
54725  957 
else 
55031  958 
(cond_tracing ctxt (fn () => print_thm ctxt "Trying to rewrite:" ("", thm')); 
54725  959 
if simp_depth ctxt > Config.get ctxt simp_depth_limit 
55031  960 
then (cond_tracing ctxt (fn () => "simp_depth_limit exceeded  giving up"); NONE) 
54725  961 
else 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

962 
trace_apply trace_args ctxt (fn ctxt' => 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

963 
(case prover ctxt' thm' of 
55031  964 
NONE => (cond_tracing ctxt' (fn () => print_thm ctxt' "FAILED" ("", thm')); NONE) 
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

965 
 SOME thm2 => 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

966 
(case check_conv ctxt' true eta_thm thm2 of 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

967 
NONE => NONE 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

968 
 SOME thm2' => 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

969 
let 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

970 
val concl = Logic.strip_imp_concl prop; 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

971 
val lr = Logic.dest_equals concl; 
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset

972 
in SOME (thm2', cond_skel (congs, lr)) end))))) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

973 
end; 
10413  974 

15531  975 
fun rews [] = NONE 
10413  976 
 rews (rrule :: rrules) = 
15531  977 
let val opt = rew rrule handle Pattern.MATCH => NONE 
54725  978 
in (case opt of NONE => rews rrules  some => some) end; 
10413  979 

38834
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

980 
fun sort_rrules rrs = 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

981 
let 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

982 
fun is_simple ({thm, ...}: rrule) = 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

983 
(case Thm.prop_of thm of 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

984 
Const ("==", _) $ _ $ _ => true 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

985 
 _ => false); 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

986 
fun sort [] (re1, re2) = re1 @ re2 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

987 
 sort (rr :: rrs) (re1, re2) = 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

988 
if is_simple rr 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

989 
then sort rrs (rr :: re1, re2) 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

990 
else sort rrs (re1, rr :: re2); 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

991 
in sort rrs ([], []) end; 
10413  992 

15531  993 
fun proc_rews [] = NONE 
15023  994 
 proc_rews (Proc {name, proc, lhs, ...} :: ps) = 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

995 
if Pattern.matches (Proof_Context.theory_of ctxt) (term_of lhs, term_of t) then 
55031  996 
(cond_tracing' ctxt simp_debug (fn () => 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

997 
print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t); 
54725  998 
(case proc ctxt eta_t' of 
55031  999 
NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps) 
15531  1000 
 SOME raw_thm => 
55031  1001 
(cond_tracing ctxt (fn () => 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

1002 
print_thm ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:") 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

1003 
("", raw_thm)); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1004 
(case rews (mk_procrule ctxt raw_thm) of 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

1005 
NONE => 
55031  1006 
(cond_tracing ctxt (fn () => 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

1007 
print_term ctxt ("IGNORED result of simproc " ^ quote name ^ 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

1008 
"  does not match") (Thm.term_of t)); 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

1009 
proc_rews ps) 
54725  1010 
 some => some)))) 
10413  1011 
else proc_rews ps; 
38834
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1012 
in 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1013 
(case eta_t of 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1014 
Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0) 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1015 
 _ => 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1016 
(case rews (sort_rrules (Net.match_term rules eta_t)) of 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1017 
NONE => proc_rews (Net.match_term procs eta_t) 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1018 
 some => some)) 
10413  1019 
end; 
1020 

1021 

1022 
(* conversion to apply a congruence rule to a term *) 

1023 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1024 
fun congc prover ctxt maxt cong t = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1025 
let 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1026 
val rthm = Thm.incr_indexes (maxt + 1) cong; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1027 
val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm))); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1028 
val insts = Thm.match (rlhs, t) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1029 
(* Thm.match can raise Pattern.MATCH; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1030 
is handled when congc is called *) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1031 
val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm); 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

1032 
val _ = 
55031  1033 
cond_tracing ctxt (fn () => print_thm ctxt "Applying congruence rule:" ("", thm')); 
1034 
fun err (msg, thm) = (cond_tracing ctxt (fn () => print_thm ctxt msg ("", thm)); NONE); 

38834
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1035 
in 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1036 
(case prover thm' of 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1037 
NONE => err ("Congruence proof failed. Could not prove", thm') 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1038 
 SOME thm2 => 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1039 
(case check_conv ctxt true (Drule.beta_eta_conversion t) thm2 of 
15531  1040 
NONE => err ("Congruence proof failed. Should not have proved", thm2) 
1041 
 SOME thm2' => 

22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22892
diff
changeset

1042 
if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2'))) 
38834
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1043 
then NONE else SOME thm2')) 
10413  1044 
end; 
1045 

1046 
val (cA, (cB, cC)) = 

22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22892
diff
changeset

1047 
apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong))); 
10413  1048 

15531  1049 
fun transitive1 NONE NONE = NONE 
1050 
 transitive1 (SOME thm1) NONE = SOME thm1 

1051 
 transitive1 NONE (SOME thm2) = SOME thm2 

54725  1052 
 transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2); 
10413  1053 

15531  1054 
fun transitive2 thm = transitive1 (SOME thm); 
1055 
fun transitive3 thm = transitive1 thm o SOME; 

13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1056 

52091  1057 
fun bottomc ((simprem, useprem, mutsimp), prover, maxidx) = 
10413  1058 
let 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1059 
fun botc skel ctxt t = 
54725  1060 
if is_Var skel then NONE 
1061 
else 

1062 
(case subc skel ctxt t of 

1063 
some as SOME thm1 => 

1064 
(case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of 

1065 
SOME (thm2, skel2) => 

1066 
transitive2 (Thm.transitive thm1 thm2) 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1067 
(botc skel2 ctxt (Thm.rhs_of thm2)) 
54725  1068 
 NONE => some) 
1069 
 NONE => 

1070 
(case rewritec (prover, maxidx) ctxt t of 

1071 
SOME (thm2, skel2) => transitive2 thm2 

1072 
(botc skel2 ctxt (Thm.rhs_of thm2)) 

1073 
 NONE => NONE)) 

10413  1074 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1075 
and try_botc ctxt t = 
54725  1076 
(case botc skel0 ctxt t of 
1077 
SOME trec1 => trec1 

1078 
 NONE => Thm.reflexive t) 

10413  1079 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1080 
and subc skel ctxt t0 = 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
55000
diff
changeset

1081 
let val Simpset (_, {congs, ...}) = simpset_of ctxt in 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1082 
(case term_of t0 of 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1083 
Abs (a, T, _) => 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1084 
let 
55635  1085 
val (v, ctxt') = Variable.next_bound (a, T) ctxt; 
1086 
val b = #1 (Term.dest_Free v); 

1087 
val (v', t') = Thm.dest_abs (SOME b) t0; 

1088 
val b' = #1 (Term.dest_Free (term_of v')); 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1089 
val _ = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1090 
if b <> b' then 
55635  1091 
warning ("Bad Simplifier context: renamed bound variable " ^ 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1092 
quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ())) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1093 
else (); 
54725  1094 
val skel' = (case skel of Abs (_, _, sk) => sk  _ => skel0); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1095 
in 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1096 
(case botc skel' ctxt' t' of 
55635  1097 
SOME thm => SOME (Thm.abstract_rule a v' thm) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1098 
 NONE => NONE) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1099 
end 
54725  1100 
 t $ _ => 
1101 
(case t of 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1102 
Const ("==>", _) $ _ => impc t0 ctxt 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1103 
 Abs _ => 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1104 
let val thm = Thm.beta_conversion false t0 
54725  1105 
in 
1106 
(case subc skel0 ctxt (Thm.rhs_of thm) of 

1107 
NONE => SOME thm 

1108 
 SOME thm' => SOME (Thm.transitive thm thm')) 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1109 
end 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1110 
 _ => 
54727  1111 
let 
1112 
fun appc () = 

1113 
let 

1114 
val (tskel, uskel) = 

1115 
(case skel of 

1116 
tskel $ uskel => (tskel, uskel) 

1117 
 _ => (skel0, skel0)); 

1118 
val (ct, cu) = Thm.dest_comb t0; 

1119 
in 

1120 
(case botc tskel ctxt ct of 

1121 
SOME thm1 => 

1122 
(case botc uskel ctxt cu of 

1123 
SOME thm2 => SOME (Thm.combination thm1 thm2) 

1124 
 NONE => SOME (Thm.combination thm1 (Thm.reflexive cu))) 

1125 
 NONE => 

1126 
(case botc uskel ctxt cu of 

1127 
SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1) 

1128 
 NONE => NONE)) 

1129 
end; 

1130 
val (h, ts) = strip_comb t; 

54725  1131 
in 
1132 
(case cong_name h of 

1133 
SOME a => 

1134 
(case AList.lookup (op =) (fst congs) a of 

1135 
NONE => appc () 

1136 
 SOME cong => 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1137 
(*post processing: some partial applications h t1 ... tj, j <= length ts, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1138 
may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*) 
54725  1139 
(let 
1140 
val thm = congc (prover ctxt) ctxt maxidx cong t0; 

1141 
val t = the_default t0 (Option.map Thm.rhs_of thm); 

1142 
val (cl, cr) = Thm.dest_comb t 

1143 
val dVar = Var(("", 0), dummyT) 

1144 
val skel = 

1145 
list_comb (h, replicate (length ts) dVar) 

1146 
in 

1147 
(case botc skel ctxt cl of 

1148 
NONE => thm 

1149 
 SOME thm' => 

1150 
transitive3 thm (Thm.combination thm' (Thm.reflexive cr))) 

1151 
end handle Pattern.MATCH => appc ())) 

1152 
 _ => appc ()) 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1153 
end) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1154 
 _ => NONE) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1155 
end 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1156 
and impc ct ctxt = 
54725  1157 
if mutsimp then mut_impc0 [] ct [] [] ctxt 
1158 
else nonmut_impc ct ctxt 

10413  1159 

54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54982
diff
changeset

1160 
and rules_of_prem prem ctxt = 
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1161 
if maxidx_of_term (term_of prem) <> ~1 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

1162 
then 
55031  1163 
(cond_tracing ctxt (fn () => 
55028
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

1164 
print_term ctxt "Cannot add premise as rewrite rule because it contains (type) unknowns:" 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

1165 
(term_of prem)); 
00e849f5b397
clarified Simplifier diagnostics  simplified ML;
wenzelm
parents:
55014
diff
changeset

1166 
(([], NONE), ctxt)) 
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1167 
else 
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54982
diff
changeset

1168 
let val (asm, ctxt') = Thm.assume_hyps prem ctxt 
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54982
diff
changeset

1169 
in ((extract_safe_rrules ctxt' asm, SOME asm), ctxt') end 
10413  1170 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1171 
and add_rrules (rrss, asms) ctxt = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1172 
(fold o fold) insert_rrule rrss ctxt > add_prems (map_filter I asms) 
10413  1173 

23178  1174 
and disch r prem eq = 
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1175 
let 
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22892
diff
changeset

1176 
val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq); 
54727  1177 
val eq' = 
1178 
Thm.implies_elim 

1179 
(Thm.instantiate ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong) 

1180 
(Thm.implies_intr prem eq); 

54725  1181 
in 
1182 
if not r then eq' 

1183 
else 

1184 
let 

1185 
val (prem', concl) = Thm.dest_implies lhs; 

54727  1186 
val (prem'', _) = Thm.dest_implies rhs; 
1187 
in 

1188 
Thm.transitive 

1189 
(Thm.transitive 

1190 
(Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) Drule.swap_prems_eq) 

1191 
eq') 

1192 
(Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) Drule.swap_prems_eq) 

54725  1193 
end 
10413  1194 
end 
1195 

13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1196 
and rebuild [] _ _ _ _ eq = eq 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1197 
 rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ctxt eq = 
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1198 
let 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1199 
val ctxt' = add_rrules (rev rrss, rev asms) ctxt; 
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1200 
val concl' = 
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22892
diff
changeset

1201 
Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq)); 
54727  1202 
val dprem = Option.map (disch false prem); 
38834
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1203 
in 
52091  1204 
(case rewritec (prover, maxidx) ctxt' concl' of 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1205 
NONE => rebuild prems concl' rrss asms ctxt (dprem eq) 
54727  1206 
 SOME (eq', _) => 
1207 
transitive2 (fold (disch false) prems (the (transitive3 (dprem eq) eq'))) 

1208 
(mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ctxt)) 

13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1209 
end 
15023  1210 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1211 
and mut_impc0 prems concl rrss asms ctxt = 
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1212 
let 
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1213 
val prems' = strip_imp_prems concl; 
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54982
diff
changeset

1214 
val ((rrss', asms'), ctxt') = fold_map rules_of_prem prems' ctxt >> split_list; 
38834
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1215 
in 
658fcba35ed7
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38715
diff
changeset

1216 
mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss') 
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54982
diff
changeset

1217 
(asms @ asms') [] [] [] [] ctxt' ~1 ~1 
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1218 
end 
15023  1219 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1220 
and mut_impc [] concl [] [] prems' rrss' asms' eqns ctxt changed k = 
33245  1221 
transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1 
1222 
(Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE) 

13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1223 
(if changed > 0 then 
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1224 
mut_impc (rev prems') concl (rev rrss') (rev asms') 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1225 
[] [] [] [] ctxt ~1 changed 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1226 
else rebuild prems' concl rrss' asms' ctxt 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1227 
(botc skel0 (add_rrules (rev rrss', rev asms') ctxt) concl)) 
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1228 

6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1229 
 mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1230 
prems' rrss' asms' eqns ctxt changed k = 
54725  1231 
(case (if k = 0 then NONE else botc skel0 (add_rrules 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1232 
(rev rrss' @ rrss, rev asms' @ asms) ctxt) prem) of 
15531  1233 
NONE => mut_impc prems concl rrss asms (prem :: prems') 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51611
diff
changeset

1234 
(rrs :: rrss') (asm :: asms') (NONE :: eqns) ctxt changed 
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1235 
(if k = 0 then 0 else k  1) 
54725  1236 
 SOME eqn => 
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1237 
let 
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22892
diff
changeset

1238 
val prem' = Thm.rhs_of eqn; 
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset

1239 
val tprems = map term_of prems; 
33029  1240 
val i = 1 + fold Integer.max (map (fn p => 
44058  1241 
find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1; 
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54982
diff
changeset

1242 
val ((rrs', asm'), ctxt') = rules_of_prem prem' ctxt; 
54725  1243 
in 
1244 
mut_impc prems concl rrss asms (prem' :: 