author  blanchet 
Sat, 05 Jan 2013 11:24:09 +0100  
changeset 50736  07dfdf72ab75 
parent 50735  6b232d76cbc9 
child 50756  c96bb430ddb0 
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 
50511
8825c36cb1ce
don't query blacklisted theorems in evaluation driver
blanchet
parents:
50510
diff
changeset

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

28 
val clasimpset_rule_table_of : Proof.context > status Termtab.table 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

29 
val build_name_tables : 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

30 
(thm > string) > ('a * thm) list 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

31 
> string Symtab.table * string Symtab.table 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

32 
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

33 
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

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

35 
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

36 
val all_facts : 
50442
4f6a4d32522c
don't blacklist "case" theorems  this causes problems in MaSh later
blanchet
parents:
50239
diff
changeset

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

38 
> 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

39 
val nearly_all_facts : 
48299  40 
Proof.context > bool > fact_override > unit Symtab.table 
41 
> 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

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

43 

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

44 
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

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

46 

50495
bd9a0028b063
better tautology check  don't reject "prod_cases3" for example
blanchet
parents:
50490
diff
changeset

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

48 
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

49 
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

50 
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

51 

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

52 
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

53 

48292  54 
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

55 
{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

56 
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

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

58 

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

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

60 
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

61 
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

62 
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

63 
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

64 

48292  65 
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

66 

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

67 
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

68 
Symtab.defined reserved s orelse 
50239  69 
exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

70 

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

71 
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

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

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

74 

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

75 
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

76 
 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

77 
 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

78 

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

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

80 
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

81 

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

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

83 
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

84 

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

85 
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

86 
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

87 
 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

88 
 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

89 
 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

90 
 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

91 

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

92 
fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms 
48396  93 
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

94 

48396  95 
fun scope_of_thm global assms chained th = 
96 
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

97 
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

98 
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

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

100 

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

101 
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

102 
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

103 
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

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

105 

48396  106 
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

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

108 
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

109 
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

110 
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

111 
Induction 
48396  112 
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

113 
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

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

115 

48396  116 
fun stature_of_thm global assms chained css name th = 
117 
(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

118 

48396  119 
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

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

121 
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

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

123 
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

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

125 
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

126 
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

127 
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

128 
 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

129 
 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

130 
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

131 
 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

132 
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

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

134 
bracket 
48396  135 
fun add_nth th (j, rest) = 
136 
let val name = nth_name j in 

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

138 
:: rest) 

139 
end 

140 
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

141 

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

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

143 
"Accessible_Part.acc.defs", as these are definitions arising from packages. *) 
50736  144 
fun is_package_def s = 
145 
let val ss = Long_Name.explode s in 

146 
length ss > 2 andalso not (hd ss = "local") andalso 

147 
exists (fn suf => String.isSuffix suf s) 

148 
["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"] 

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

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

150 

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

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

152 
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

153 
["defs", "select_defs", "update_defs", "split", "splits", "split_asm", 
50442
4f6a4d32522c
don't blacklist "case" theorems  this causes problems in MaSh later
blanchet
parents:
50239
diff
changeset

154 
"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

155 
"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

156 
"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

157 
> 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

158 
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

159 
> 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

160 

50490
b977b727c7d5
really all facts means really all facts (well, almost)
blanchet
parents:
50485
diff
changeset

161 
val max_lambda_nesting = 5 (*only applies if not ho_atp*) 
48250
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 
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

164 
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

165 
 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

166 
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

167 
 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

168 

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

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

170 
quantifiers. *) 
48437  171 
fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) = 
172 
formula_has_too_many_lambdas (T :: Ts) t 

173 
 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

174 
if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then 
48437  175 
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

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

177 
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

178 

50523
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

179 
(* The maximum apply depth of any "metis" call in "Metis_Examples" (on 
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

180 
20071031) was 11. *) 
50490
b977b727c7d5
really all facts means really all facts (well, almost)
blanchet
parents:
50485
diff
changeset

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

182 

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

183 
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

184 
 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

185 
 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

186 

50512
c283bc0a8f1a
tweaked which facts are included for MaSh evaluations
blanchet
parents:
50511
diff
changeset

187 
fun is_too_complex ho_atp t = 
48437  188 
apply_depth t > max_apply_depth orelse 
189 
(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

190 

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

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

192 
val technical_prefixes = 
50736  193 
["ATP", "Code_Evaluation", "Datatype", "DSequence", "Enum", "Lazy_Sequence", 
194 
"Meson", "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence", 

195 
"Quickcheck", "Quickcheck_Exhaustive", "Quickcheck_Narrowing", 

196 
"Random_Sequence", "Sledgehammer", "SMT"] 

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

197 
> 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

198 

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

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

200 
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

201 
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

202 

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

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

204 
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

205 
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

206 
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

207 
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

208 

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

209 
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

210 
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

211 
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

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

213 

50523
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

214 
fun is_likely_tautology_too_meta_or_too_technical th = 
48406  215 
let 
50053
fea589c8583e
fixed detection of tautologies  things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
blanchet
parents:
50049
diff
changeset

216 
fun is_interesting_subterm (Const (s, _)) = 
fea589c8583e
fixed detection of tautologies  things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
blanchet
parents:
50049
diff
changeset

217 
not (member (op =) atp_widely_irrelevant_consts s) 
fea589c8583e
fixed detection of tautologies  things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
blanchet
parents:
50049
diff
changeset

218 
 is_interesting_subterm (Free _) = true 
fea589c8583e
fixed detection of tautologies  things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
blanchet
parents:
50049
diff
changeset

219 
 is_interesting_subterm _ = false 
48406  220 
fun is_boring_bool t = 
50053
fea589c8583e
fixed detection of tautologies  things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
blanchet
parents:
50049
diff
changeset

221 
not (exists_subterm is_interesting_subterm t) orelse 
48406  222 
exists_type (exists_subtype (curry (op =) @{typ prop})) t 
50495
bd9a0028b063
better tautology check  don't reject "prod_cases3" for example
blanchet
parents:
50490
diff
changeset

223 
fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t 
bd9a0028b063
better tautology check  don't reject "prod_cases3" for example
blanchet
parents:
50490
diff
changeset

224 
 is_boring_prop Ts (@{const "==>"} $ t $ u) = 
bd9a0028b063
better tautology check  don't reject "prod_cases3" for example
blanchet
parents:
50490
diff
changeset

225 
is_boring_prop Ts t andalso is_boring_prop Ts u 
50496
8665ec681e47
further fix related to bd9a0028b063  that change was per se right, but it exposed a bug in the pattern for "all"
blanchet
parents:
50495
diff
changeset

226 
 is_boring_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) = 
8665ec681e47
further fix related to bd9a0028b063  that change was per se right, but it exposed a bug in the pattern for "all"
blanchet
parents:
50495
diff
changeset

227 
is_boring_prop (T :: Ts) t 
50495
bd9a0028b063
better tautology check  don't reject "prod_cases3" for example
blanchet
parents:
50490
diff
changeset

228 
 is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) = 
bd9a0028b063
better tautology check  don't reject "prod_cases3" for example
blanchet
parents:
50490
diff
changeset

229 
is_boring_prop Ts (t $ eta_expand Ts u 1) 
bd9a0028b063
better tautology check  don't reject "prod_cases3" for example
blanchet
parents:
50490
diff
changeset

230 
 is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) = 
48406  231 
is_boring_bool t andalso is_boring_bool u 
50495
bd9a0028b063
better tautology check  don't reject "prod_cases3" for example
blanchet
parents:
50490
diff
changeset

232 
 is_boring_prop _ _ = true 
50523
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

233 
val t = prop_of th 
48406  234 
in 
50523
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

235 
(is_boring_prop [] (prop_of th) andalso 
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

236 
not (Thm.eq_thm_prop (@{thm ext}, th))) orelse 
48667
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

237 
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

238 
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

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

240 

50511
8825c36cb1ce
don't query blacklisted theorems in evaluation driver
blanchet
parents:
50510
diff
changeset

241 
fun is_blacklisted_or_something ctxt ho_atp name = 
50510  242 
(not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse 
243 
exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp) 

244 

50048  245 
fun hackish_string_for_term ctxt = 
50049
dd6a4655cd72
avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
blanchet
parents:
50048
diff
changeset

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

247 

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

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

249 
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

250 
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

251 
prefixes of all free variables. In the worse case scenario, where the fact 
49981  252 
won't be resolved correctly, the user can fix it manually, e.g., by giving a 
253 
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

254 
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

255 
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

256 

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

257 
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

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

259 
> 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

260 
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

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

262 
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

263 
$ 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

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

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

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

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

268 

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

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

271 
> hackish_string_for_term ctxt 
48400  272 
> backquote 
273 

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

274 
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

275 

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

276 
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

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

278 
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

279 
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

280 
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

281 
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

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

283 
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

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

285 
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

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

287 
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

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

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

290 
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

291 
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

292 
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

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

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

295 
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

296 
> 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

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

298 
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

299 
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

300 
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

301 
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

302 
> 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

303 
> 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

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

305 
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

306 
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

307 
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

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

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

310 
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

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

312 
> 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

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

314 
> 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

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

316 
> 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

317 
> 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

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

319 

50481
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

320 
fun normalize_eq (t as @{const Trueprop} 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

321 
$ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) = 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

322 
if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

323 
else HOLogic.mk_Trueprop (t0 $ t2 $ t1) 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

324 
 normalize_eq (t as @{const Trueprop} $ (@{const Not} 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

325 
$ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) = 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

326 
if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

327 
else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1)) 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

328 
 normalize_eq t = t 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

329 

50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

330 
val normalize_eq_etc = normalize_eq o Term_Subst.zero_var_indexes 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

331 

3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

332 
fun if_thm_before th th' = 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

333 
if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th' 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

334 

50734  335 
(* Hack: Conflate the facts about a class as seen from the outside with the 
336 
corresponding lowlevel facts, so that MaSh can learn from the lowlevel 

337 
proofs. *) 

338 
fun un_class_ify s = 

339 
case first_field "_class" s of 

340 
SOME (pref, suf) => [s, pref ^ suf] 

341 
 NONE => [s] 

342 

50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

343 
fun build_name_tables name_of facts = 
50733  344 
let 
345 
fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th) 

50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

346 
fun add_plain canon alias = 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

347 
Symtab.update (Thm.get_name_hint canon, 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

348 
name_of (if_thm_before canon alias)) 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

349 
fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

350 
fun add_inclass (name, target) = 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

351 
fold (fn s => Symtab.update (s, target)) (un_class_ify name) 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

352 
val prop_tab = fold_rev cons_thm facts Termtab.empty 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

353 
val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

354 
val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

355 
in (plain_name_tab, inclass_name_tab) end 
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

356 

3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

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

358 
Termtab.fold (cons o snd) 
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

359 
(fold (Termtab.default o `(normalize_eq_etc o prop_of o snd)) facts 
50481
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

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

361 

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

362 
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

363 
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

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

365 
$ ((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

366 
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

367 
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

368 
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

369 
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

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

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

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

373 

50586  374 
val instantiate_induct_timeout = seconds 0.01 
375 

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

376 
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

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

378 
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

379 
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

380 
 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

381 
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

382 
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

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

384 
> 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

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

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

387 
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

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

389 

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

390 
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

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

392 
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

393 

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

394 
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

395 
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

396 
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

397 
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

398 
stmt_xs > filter (fn (_, T) => type_match thy (T, ind_T)) 
50586  399 
> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout 
400 
(instantiate_induct_rule ctxt stmt p_name ax))) 

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

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

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

403 

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

404 
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

405 
[] > 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

406 

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

407 
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

408 
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

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

410 
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

411 
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

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

413 
> 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

414 
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

415 
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

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

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

418 

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

419 
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

420 
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

421 

50523
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

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

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

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

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

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

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

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

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

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

431 
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

432 
val unnamed_locals = 
48396  433 
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

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

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

436 
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

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

438 
foldx (fn (name0, ths) => 
50512
c283bc0a8f1a
tweaked which facts are included for MaSh evaluations
blanchet
parents:
50511
diff
changeset

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

440 
forall (not o member Thm.eq_thm_prop add_ths) ths andalso 
50511
8825c36cb1ce
don't query blacklisted theorems in evaluation driver
blanchet
parents:
50510
diff
changeset

441 
(Facts.is_concealed facts name0 orelse 
8825c36cb1ce
don't query blacklisted theorems in evaluation driver
blanchet
parents:
50510
diff
changeset

442 
not (can (Proof_Context.get_thms ctxt) name0) orelse 
50523
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

443 
(not generous andalso 
50512
c283bc0a8f1a
tweaked which facts are included for MaSh evaluations
blanchet
parents:
50511
diff
changeset

444 
is_blacklisted_or_something ctxt ho_atp name0)) then 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

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

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

447 
let 
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

448 
val n = length ths 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

449 
val multi = n > 1 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

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

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

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

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

454 
in 
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

455 
pair n 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

456 
#> fold_rev (fn th => fn (j, (multis, unis)) => 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

457 
(j  1, 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

458 
if not (member Thm.eq_thm_prop add_ths th) andalso 
50523
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

459 
(is_likely_tautology_too_meta_or_too_technical th orelse 
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

460 
(not generous andalso 
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

461 
is_too_complex ho_atp (prop_of th))) then 
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

462 
(multis, unis) 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

463 
else 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

464 
let 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

465 
val new = 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

466 
(((fn () => 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

467 
if name0 = "" then 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

468 
backquote_thm ctxt th 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

469 
else 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

470 
[Facts.extern ctxt facts name0, 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

471 
Name_Space.extern ctxt full_space name0] 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

472 
> find_first check_thms 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

473 
> the_default name0 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

474 
> make_name reserved multi j), 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

475 
stature_of_thm global assms chained css name0 th), 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

476 
th) 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

477 
in 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

478 
if multi then (new :: multis, unis) 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

479 
else (multis, new :: unis) 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

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

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

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

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

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

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

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

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

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

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

490 

48396  491 
fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts 
492 
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

493 
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

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

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

496 
let 
48396  497 
val chained = 
498 
chained 

48292  499 
> 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

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

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

502 
maps (map (fn ((name, stature), th) => ((K name, stature), th)) 
48396  503 
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

504 
else 
48292  505 
let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in 
50442
4f6a4d32522c
don't blacklist "case" theorems  this causes problems in MaSh later
blanchet
parents:
50239
diff
changeset

506 
all_facts ctxt false ho_atp reserved add chained css 
48292  507 
> filter_out (member Thm.eq_thm_prop del o snd) 
508 
> maybe_filter_no_atps ctxt 

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

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

511 
> 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

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

513 

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

514 
end; 