author  blanchet 
Mon, 12 Nov 2012 11:32:22 +0100  
changeset 50047  45684acf0b94 
parent 49981  e12b4e9794fd 
child 50048  fb024bbf4b65 
permissions  rwrr 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact.ML 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

2 
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

4 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

5 
Sledgehammer fact handling. 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

6 
*) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

7 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

8 
signature SLEDGEHAMMER_FACT = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

9 
sig 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

10 
type status = ATP_Problem_Generate.status 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

11 
type stature = ATP_Problem_Generate.stature 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

12 

48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48292
diff
changeset

13 
type fact = ((unit > string) * stature) * thm 
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48292
diff
changeset

14 

48292  15 
type fact_override = 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

16 
{add : (Facts.ref * Attrib.src list) list, 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

17 
del : (Facts.ref * Attrib.src list) list, 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

18 
only : bool} 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

19 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

20 
val ignore_no_atp : bool Config.T 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

21 
val instantiate_inducts : bool Config.T 
48292  22 
val no_fact_override : fact_override 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

23 
val fact_from_ref : 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

24 
Proof.context > unit Symtab.table > thm list > status Termtab.table 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

25 
> Facts.ref * Attrib.src list > ((string * stature) * thm) list 
50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49981
diff
changeset

26 
val backquote_thm : Proof.context > thm > string 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

27 
val clasimpset_rule_table_of : Proof.context > status Termtab.table 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

28 
val maybe_instantiate_inducts : 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

29 
Proof.context > term list > term > (((unit > string) * 'a) * thm) list 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

30 
> (((unit > string) * 'a) * thm) list 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

31 
val maybe_filter_no_atps : Proof.context > ('a * thm) list > ('a * thm) list 
48530
d443166f9520
repaired accessibility chains generated by MaSh exporter + tuned one function out
blanchet
parents:
48440
diff
changeset

32 
val all_facts : 
d443166f9520
repaired accessibility chains generated by MaSh exporter + tuned one function out
blanchet
parents:
48440
diff
changeset

33 
Proof.context > bool > unit Symtab.table > thm list > thm list 
d443166f9520
repaired accessibility chains generated by MaSh exporter + tuned one function out
blanchet
parents:
48440
diff
changeset

34 
> status Termtab.table > fact list 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

35 
val nearly_all_facts : 
48299  36 
Proof.context > bool > fact_override > unit Symtab.table 
37 
> status Termtab.table > thm list > term list > term > fact list 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

38 
end; 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

39 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

40 
structure Sledgehammer_Fact : SLEDGEHAMMER_FACT = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

41 
struct 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

42 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

43 
open ATP_Problem_Generate 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

44 
open Metis_Tactic 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

45 
open Sledgehammer_Util 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

46 

48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48292
diff
changeset

47 
type fact = ((unit > string) * stature) * thm 
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48292
diff
changeset

48 

48292  49 
type fact_override = 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

50 
{add : (Facts.ref * Attrib.src list) list, 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

51 
del : (Facts.ref * Attrib.src list) list, 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

52 
only : bool} 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

53 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

54 
(* experimental features *) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

55 
val ignore_no_atp = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

56 
Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

57 
val instantiate_inducts = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

58 
Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

59 

48292  60 
val no_fact_override = {add = [], del = [], only = false} 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

61 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

62 
fun needs_quoting reserved s = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

63 
Symtab.defined reserved s orelse 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

64 
exists (not o Lexicon.is_identifier) (Long_Name.explode s) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

65 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

66 
fun make_name reserved multi j name = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

67 
(name > needs_quoting reserved name ? quote) ^ 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

68 
(if multi then "(" ^ string_of_int j ^ ")" else "") 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

69 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

70 
fun explode_interval _ (Facts.FromTo (i, j)) = i upto j 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

71 
 explode_interval max (Facts.From i) = i upto i + max  1 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

72 
 explode_interval _ (Facts.Single i) = [i] 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

73 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

74 
val backquote = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

75 
raw_explode #> map (fn "`" => "\\`"  s => s) #> implode #> enclose "`" "`" 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

76 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

77 
(* unfolding these can yield really huge terms *) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

78 
val risky_defs = @{thms Bit0_def Bit1_def} 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

79 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

80 
fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs)) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

81 
fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

82 
 is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

83 
 is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

84 
 is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

85 
 is_rec_def _ = false 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

86 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

87 
fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms 
48396  88 
fun is_chained chained = member Thm.eq_thm_prop chained 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

89 

48396  90 
fun scope_of_thm global assms chained th = 
91 
if is_chained chained th then Chained 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

92 
else if global then Global 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

93 
else if is_assum assms th then Assum 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

94 
else Local 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

95 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

96 
val may_be_induction = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

97 
exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

98 
body_type T = @{typ bool} 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

99 
 _ => false) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

100 

48396  101 
fun status_of_thm css name th = 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

102 
(* FIXME: use structured name *) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

103 
if (String.isSubstring ".induct" name orelse 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

104 
String.isSubstring ".inducts" name) andalso 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

105 
may_be_induction (prop_of th) then 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

106 
Induction 
48396  107 
else case Termtab.lookup css (prop_of th) of 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

108 
SOME status => status 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

109 
 NONE => General 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

110 

48396  111 
fun stature_of_thm global assms chained css name th = 
112 
(scope_of_thm global assms chained th, status_of_thm css name th) 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

113 

48396  114 
fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) = 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

115 
let 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

116 
val ths = Attrib.eval_thms ctxt [xthm] 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

117 
val bracket = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

118 
map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

119 
> implode 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

120 
fun nth_name j = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

121 
case xref of 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

122 
Facts.Fact s => backquote s ^ bracket 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

123 
 Facts.Named (("", _), _) => "[" ^ bracket ^ "]" 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

124 
 Facts.Named ((name, _), NONE) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

125 
make_name reserved (length ths > 1) (j + 1) name ^ bracket 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

126 
 Facts.Named ((name, _), SOME intervals) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

127 
make_name reserved true 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

128 
(nth (maps (explode_interval (length ths)) intervals) j) name ^ 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

129 
bracket 
48396  130 
fun add_nth th (j, rest) = 
131 
let val name = nth_name j in 

132 
(j + 1, ((name, stature_of_thm false [] chained css name th), th) 

133 
:: rest) 

134 
end 

135 
in (0, []) > fold add_nth ths > snd end 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

136 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

137 
(* Reject theorems with names like "List.filter.filter_list_def" or 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

138 
"Accessible_Part.acc.defs", as these are definitions arising from packages. *) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

139 
fun is_package_def a = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

140 
let val names = Long_Name.explode a in 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

141 
(length names > 2 andalso not (hd names = "local") andalso 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

142 
String.isSuffix "_def" a) orelse String.isSuffix "_defs" a 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

143 
end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

144 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

145 
(* FIXME: put other record thms here, or declare as "no_atp" *) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

146 
fun multi_base_blacklist ctxt ho_atp = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

147 
["defs", "select_defs", "update_defs", "split", "splits", "split_asm", 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

148 
"cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", 
48440
159e320ef851
identified "evil" theories for MaSh  this is rather ad hoc, but so is MaSh anyway
blanchet
parents:
48438
diff
changeset

149 
"weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps", 
159e320ef851
identified "evil" theories for MaSh  this is rather ad hoc, but so is MaSh anyway
blanchet
parents:
48438
diff
changeset

150 
"nibble.distinct"] 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

151 
> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

152 
append ["induct", "inducts"] 
48440
159e320ef851
identified "evil" theories for MaSh  this is rather ad hoc, but so is MaSh anyway
blanchet
parents:
48438
diff
changeset

153 
> map (prefix Long_Name.separator) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

154 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

155 
val max_lambda_nesting = 3 (*only applies if not ho_atp*) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

156 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

157 
fun term_has_too_many_lambdas max (t1 $ t2) = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

158 
exists (term_has_too_many_lambdas max) [t1, t2] 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

159 
 term_has_too_many_lambdas max (Abs (_, _, t)) = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

160 
max = 0 orelse term_has_too_many_lambdas (max  1) t 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

161 
 term_has_too_many_lambdas _ _ = false 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

162 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

163 
(* Don't count nested lambdas at the level of formulas, since they are 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

164 
quantifiers. *) 
48437  165 
fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) = 
166 
formula_has_too_many_lambdas (T :: Ts) t 

167 
 formula_has_too_many_lambdas Ts t = 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

168 
if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then 
48437  169 
exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t)) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

170 
else 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

171 
term_has_too_many_lambdas max_lambda_nesting t 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

172 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

173 
(* The max apply depth of any "metis" call in "Metis_Examples" (on 20071031) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

174 
was 11. *) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

175 
val max_apply_depth = 15 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

176 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

177 
fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

178 
 apply_depth (Abs (_, _, t)) = apply_depth t 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

179 
 apply_depth _ = 0 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

180 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

181 
fun is_formula_too_complex ho_atp t = 
48437  182 
apply_depth t > max_apply_depth orelse 
183 
(not ho_atp andalso formula_has_too_many_lambdas [] t) 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

184 

48667
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

185 
(* FIXME: Ad hoc list *) 
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

186 
val technical_prefixes = 
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

187 
["ATP", "Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Meson", 
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

188 
"Metis", "Nitpick", "New_DSequence", "New_Random_Sequence", "Quickcheck", 
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

189 
"Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", 
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

190 
"Sledgehammer", "SMT"] 
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

191 
> map (suffix Long_Name.separator) 
48440
159e320ef851
identified "evil" theories for MaSh  this is rather ad hoc, but so is MaSh anyway
blanchet
parents:
48438
diff
changeset

192 

48667
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

193 
fun has_technical_prefix s = 
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

194 
exists (fn pref => String.isPrefix pref s) technical_prefixes 
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

195 
val exists_technical_const = exists_Const (has_technical_prefix o fst) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

196 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

197 
(* FIXME: make more reliable *) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

198 
val exists_low_level_class_const = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

199 
exists_Const (fn (s, _) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

200 
s = @{const_name equal_class.equal} orelse 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

201 
String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

202 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

203 
fun is_that_fact th = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

204 
String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

205 
andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

206 
 _ => false) (prop_of th) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

207 

48406  208 
fun is_likely_tautology_or_too_meta th = 
209 
let 

210 
val is_boring_const = member (op =) atp_widely_irrelevant_consts 

211 
fun is_boring_bool t = 

212 
not (exists_Const (not o is_boring_const o fst) t) orelse 

213 
exists_type (exists_subtype (curry (op =) @{typ prop})) t 

214 
fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t 

215 
 is_boring_prop (@{const "==>"} $ t $ u) = 

216 
is_boring_prop t andalso is_boring_prop u 

217 
 is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) = 

218 
is_boring_prop t andalso is_boring_prop u 

219 
 is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) = 

220 
is_boring_bool t andalso is_boring_bool u 

221 
 is_boring_prop _ = true 

222 
in 

223 
is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) 

224 
end 

225 

48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48437
diff
changeset

226 
fun is_theorem_bad_for_atps ho_atp th = 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48437
diff
changeset

227 
is_likely_tautology_or_too_meta th orelse 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48437
diff
changeset

228 
let val t = prop_of th in 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48437
diff
changeset

229 
is_formula_too_complex ho_atp t orelse 
48667
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

230 
exists_type type_has_top_sort t orelse exists_technical_const t orelse 
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

231 
exists_low_level_class_const t orelse is_that_fact th 
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48437
diff
changeset

232 
end 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48437
diff
changeset

233 

50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49981
diff
changeset

234 
fun hackish_string_for_term ctxt t = 
49981  235 
Print_Mode.setmp 
236 
(filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) 

50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49981
diff
changeset

237 
(Syntax.string_of_term ctxt) t 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

238 
> String.translate (fn c => if Char.isPrint c then str c else "") 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

239 
> simplify_spaces 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

240 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

241 
(* This is a terrible hack. Free variables are sometimes coded as "M__" when 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

242 
they are displayed as "M" and we want to avoid clashes with these. But 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

243 
sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

244 
prefixes of all free variables. In the worse case scenario, where the fact 
49981  245 
won't be resolved correctly, the user can fix it manually, e.g., by giving a 
246 
name to the offending fact. *) 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

247 
fun all_prefixes_of s = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

248 
map (fn i => String.extract (s, 0, SOME i)) (1 upto size s  1) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

249 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

250 
fun close_form t = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

251 
(t, [] > Term.add_free_names t > maps all_prefixes_of) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

252 
> fold (fn ((s, i), T) => fn (t', taken) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

253 
let val s' = singleton (Name.variant_list taken) s in 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

254 
((if fastype_of t' = HOLogic.boolT then HOLogic.all_const 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

255 
else Logic.all_const) T 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

256 
$ Abs (s', T, abstract_over (Var ((s, i), T), t')), 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

257 
s' :: taken) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

258 
end) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

259 
(Term.add_vars t [] > sort_wrt (fst o fst)) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

260 
> fst 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

261 

50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49981
diff
changeset

262 
fun backquote_term ctxt t = 
48400  263 
t > close_form 
50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49981
diff
changeset

264 
> hackish_string_for_term ctxt 
48400  265 
> backquote 
266 

50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49981
diff
changeset

267 
fun backquote_thm ctxt th = backquote_term ctxt (prop_of th) 
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48332
diff
changeset

268 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

269 
fun clasimpset_rule_table_of ctxt = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

270 
let 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

271 
val thy = Proof_Context.theory_of ctxt 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

272 
val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

273 
fun add stature normalizers get_th = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

274 
fold (fn rule => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

275 
let 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

276 
val th = rule > get_th 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

277 
val t = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

278 
th > Thm.maxidx_of th > 0 ? zero_var_indexes > prop_of 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

279 
in 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

280 
fold (fn normalize => Termtab.update (normalize t, stature)) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

281 
(I :: normalizers) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

282 
end) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

283 
val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

284 
ctxt > claset_of > Classical.rep_cs 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

285 
val intros = Item_Net.content safeIs @ Item_Net.content hazIs 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

286 
(* Add once it is used: 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

287 
val elims = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

288 
Item_Net.content safeEs @ Item_Net.content hazEs 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

289 
> map Classical.classical_rule 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

290 
*) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

291 
val simps = ctxt > simpset_of > dest_ss > #simps 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

292 
val specs = ctxt > Spec_Rules.get 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

293 
val (rec_defs, nonrec_defs) = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

294 
specs > filter (curry (op =) Spec_Rules.Equational o fst) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

295 
> maps (snd o snd) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

296 
> filter_out (member Thm.eq_thm_prop risky_defs) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

297 
> List.partition (is_rec_def o prop_of) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

298 
val spec_intros = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

299 
specs > filter (member (op =) [Spec_Rules.Inductive, 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

300 
Spec_Rules.Co_Inductive] o fst) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

301 
> maps (snd o snd) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

302 
in 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

303 
Termtab.empty > add Simp [atomize] snd simps 
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48437
diff
changeset

304 
> add Rec_Def [] I rec_defs 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48437
diff
changeset

305 
> add Non_Rec_Def [] I nonrec_defs 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

306 
(* Add once it is used: 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

307 
> add Elim [] I elims 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

308 
*) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

309 
> add Intro [] I intros 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

310 
> add Inductive [] I spec_intros 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

311 
end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

312 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

313 
fun uniquify xs = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

314 
Termtab.fold (cons o snd) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

315 
(fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) [] 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

316 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

317 
fun struct_induct_rule_on th = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

318 
case Logic.strip_horn (prop_of th) of 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

319 
(prems, @{const Trueprop} 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

320 
$ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

321 
if not (is_TVar ind_T) andalso length prems > 1 andalso 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

322 
exists (exists_subterm (curry (op aconv) p)) prems andalso 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

323 
not (exists (exists_subterm (curry (op aconv) a)) prems) then 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

324 
SOME (p_name, ind_T) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

325 
else 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

326 
NONE 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

327 
 _ => NONE 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

328 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

329 
fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

330 
let 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

331 
fun varify_noninducts (t as Free (s, T)) = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

332 
if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

333 
 varify_noninducts t = t 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

334 
val p_inst = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

335 
concl_prop > map_aterms varify_noninducts > close_form 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

336 
> lambda (Free ind_x) 
50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49981
diff
changeset

337 
> hackish_string_for_term ctxt 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

338 
in 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

339 
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

340 
stature), th > read_instantiate ctxt [((p_name, 0), p_inst)]) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

341 
end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

342 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

343 
fun type_match thy (T1, T2) = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

344 
(Sign.typ_match thy (T2, T1) Vartab.empty; true) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

345 
handle Type.TYPE_MATCH => false 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

346 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

347 
fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

348 
case struct_induct_rule_on th of 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

349 
SOME (p_name, ind_T) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

350 
let val thy = Proof_Context.theory_of ctxt in 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

351 
stmt_xs > filter (fn (_, T) => type_match thy (T, ind_T)) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

352 
> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax)) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

353 
end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

354 
 NONE => [ax] 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

355 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

356 
fun external_frees t = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

357 
[] > Term.add_frees t > filter_out (can Name.dest_internal o fst) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

358 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

359 
fun maybe_instantiate_inducts ctxt hyp_ts concl_t = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

360 
if Config.get ctxt instantiate_inducts then 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

361 
let 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

362 
val thy = Proof_Context.theory_of ctxt 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

363 
val ind_stmt = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

364 
(hyp_ts > filter_out (null o external_frees), concl_t) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

365 
> Logic.list_implies > Object_Logic.atomize_term thy 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

366 
val ind_stmt_xs = external_frees ind_stmt 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

367 
in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

368 
else 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

369 
I 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

370 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

371 
fun maybe_filter_no_atps ctxt = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

372 
not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

373 

48396  374 
fun all_facts ctxt ho_atp reserved add_ths chained css = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

375 
let 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

376 
val thy = Proof_Context.theory_of ctxt 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

377 
val global_facts = Global_Theory.facts_of thy 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

378 
val local_facts = Proof_Context.facts_of ctxt 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

379 
val named_locals = local_facts > Facts.dest_static [] 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

380 
val assms = Assumption.all_assms_of ctxt 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

381 
fun is_good_unnamed_local th = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

382 
not (Thm.has_name_hint th) andalso 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

383 
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

384 
val unnamed_locals = 
48396  385 
union Thm.eq_thm_prop (Facts.props local_facts) chained 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

386 
> filter is_good_unnamed_local > map (pair "" o single) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

387 
val full_space = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

388 
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

389 
fun add_facts global foldx facts = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

390 
foldx (fn (name0, ths) => 
48327
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48299
diff
changeset

391 
if name0 <> "" andalso 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

392 
forall (not o member Thm.eq_thm_prop add_ths) ths andalso 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

393 
(Facts.is_concealed facts name0 orelse 
48327
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48299
diff
changeset

394 
not (can (Proof_Context.get_thms ctxt) name0) orelse 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

395 
(not (Config.get ctxt ignore_no_atp) andalso 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

396 
is_package_def name0) orelse 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

397 
exists (fn s => String.isSuffix s name0) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

398 
(multi_base_blacklist ctxt ho_atp)) then 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

399 
I 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

400 
else 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

401 
let 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

402 
val multi = length ths > 1 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

403 
fun check_thms a = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

404 
case try (Proof_Context.get_thms ctxt) a of 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

405 
NONE => false 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

406 
 SOME ths' => eq_list Thm.eq_thm_prop (ths, ths') 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

407 
in 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

408 
pair 1 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

409 
#> fold (fn th => fn (j, (multis, unis)) => 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

410 
(j + 1, 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

411 
if not (member Thm.eq_thm_prop add_ths th) andalso 
48327
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48299
diff
changeset

412 
is_theorem_bad_for_atps ho_atp th then 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

413 
(multis, unis) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

414 
else 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

415 
let 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

416 
val new = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

417 
(((fn () => 
48327
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48299
diff
changeset

418 
if name0 = "" then 
50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49981
diff
changeset

419 
backquote_thm ctxt th 
48327
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48299
diff
changeset

420 
else 
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48299
diff
changeset

421 
[Facts.extern ctxt facts name0, 
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48299
diff
changeset

422 
Name_Space.extern ctxt full_space name0] 
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48299
diff
changeset

423 
> find_first check_thms 
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48299
diff
changeset

424 
> the_default name0 
568b3193e53e
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents:
48299
diff
changeset

425 
> make_name reserved multi j), 
48396  426 
stature_of_thm global assms chained css name0 
427 
th), th) 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

428 
in 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

429 
if multi then (new :: multis, unis) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

430 
else (multis, new :: unis) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

431 
end)) ths 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

432 
#> snd 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

433 
end) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

434 
in 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

435 
(* The singlename theorems go after the multiplename ones, so that single 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

436 
names are preferred when both are available. *) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

437 
([], []) > add_facts false fold local_facts (unnamed_locals @ named_locals) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

438 
> add_facts true Facts.fold_static global_facts global_facts 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

439 
> op @ 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

440 
end 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

441 

48396  442 
fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts 
443 
concl_t = 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

444 
if only andalso null add then 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

445 
[] 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

446 
else 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

447 
let 
48396  448 
val chained = 
449 
chained 

48292  450 
> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th]) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

451 
in 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

452 
(if only then 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

453 
maps (map (fn ((name, stature), th) => ((K name, stature), th)) 
48396  454 
o fact_from_ref ctxt reserved chained css) add 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

455 
else 
48292  456 
let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in 
48396  457 
all_facts ctxt ho_atp reserved add chained css 
48292  458 
> filter_out (member Thm.eq_thm_prop del o snd) 
459 
> maybe_filter_no_atps ctxt 

48332
271a4a6af734
optimize parent computation in MaSh + remove temporary files
blanchet
parents:
48327
diff
changeset

460 
> uniquify 
48292  461 
end) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

462 
> maybe_instantiate_inducts ctxt hyp_ts concl_t 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

463 
end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

464 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

465 
end; 