author  clasohm 
Wed, 04 Oct 1995 12:59:52 +0100  
changeset 1262  8f40ff1299d8 
parent 1245  934183dfc786 
child 1272  dd877dc7c1f4 
permissions  rwrr 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

1 
(* Title: Pure/Thy/thm_database.ML 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

2 
ID: $Id$ 
1221  3 
Author: Carsten Clasohm and Tobias Nipkow 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

4 
Copyright 1995 TU Muenchen 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

5 
*) 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

6 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

7 
datatype thm_db_type = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

8 
ThmDB of {count: int, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

9 
thy_idx: (Sign.sg * (string list * int list)) list, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

10 
const_idx: ((int * (string * thm)) list) Symtab.table}; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

11 
(*count: number of theorems in database (used as unique ID for next thm) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

12 
thy_idx: constants and IDs of theorems 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

13 
indexed by the theory's signature they belong to 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

14 
const_idx: named theorems tagged by numbers and 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

15 
indexed by the constants they contain*) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

16 

1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

17 
signature THMDB = 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

18 
sig 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

19 
val thm_db: thm_db_type ref 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

20 
val store_thm_db: string * thm > thm 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

21 
val delete_thm_db: theory > unit 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

22 
val thms_containing: string list > (string * thm) list 
1221  23 
val findI: int > (string * thm)list 
24 
val findEs: int > (string * thm)list 

25 
val findE: int > int > (string * thm)list 

1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

26 
end; 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

27 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

28 
functor ThmDBFun(): THMDB = 
1221  29 
struct 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

30 

1221  31 
(*** ignore and top_const could be turned into functorparameters, but are 
32 
currently identical for all object logics ***) 

33 

34 
(* Constants not to be used for theorem indexing *) 

35 
val ignore = ["Trueprop", "all", "==>", "=="]; 

36 

37 
(* top_const: main constant, ignoring Trueprop *) 

38 
fun top_const (_ $ t) = (case head_of t of Const(c,_) => Some c 

39 
 _ => None); 

1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

40 

dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

41 
(*Symtab which associates a constant with a list of theorems that contain the 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

42 
constant (theorems are tagged with numbers)*) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

43 
val thm_db = ref (ThmDB 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

44 
{count = 0, thy_idx = []:(Sign.sg * (string list * int list)) list, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

45 
const_idx = Symtab.make ([]:(string * ((int * (string * thm)) list)) list)}); 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

46 

1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

47 
(*list all relevant constants a term contains*) 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

48 
fun list_consts t = 
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

49 
let fun consts (Const (c, _)) = if c mem ignore then [] else [c] 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

50 
 consts (Free _) = [] 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

51 
 consts (Var _) = [] 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

52 
 consts (Bound _) = [] 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

53 
 consts (Abs (_, _, t)) = consts t 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

54 
 consts (t1$t2) = (consts t1) union (consts t2); 
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

55 
in distinct (consts t) end; 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

56 

dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

57 
(*store a theorem in database*) 
1236
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1230
diff
changeset

58 
fun store_thm_db (named_thm as (name, thm)) = 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

59 
let val {prop, hyps, sign, ...} = rep_thm thm; 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

60 

1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

61 
val consts = distinct (flat (map list_consts (prop :: hyps))); 
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

62 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

63 
val ThmDB {count, thy_idx, const_idx} = !thm_db; 
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

64 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

65 
fun update_thys [] = [(sign, (consts, [count]))] 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

66 
 update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

67 
if Sign.eq_sg (sign, thy_sign) then 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

68 
(thy_sign, (thy_consts union consts, count :: thy_nums)) :: ts 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

69 
else thy :: update_thys ts; 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

70 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

71 
val tagged_thm = (count, named_thm); 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

72 

8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

73 
fun update_db _ [] result = Some result 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

74 
 update_db checked (c :: cs) result = 
1236
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1230
diff
changeset

75 
let 
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1230
diff
changeset

76 
val old_thms = Symtab.lookup_multi (result, c); 
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1230
diff
changeset

77 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

78 
val duplicate = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

79 
if checked then false 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

80 
else case find_first (fn (_, (n, _)) => n = name) old_thms of 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

81 
Some (_, (_, t)) => eq_thm (t, thm) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

82 
 None => false 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

83 
in if duplicate then 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

84 
(writeln ("Warning: Theorem database already contains copy of\ 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

85 
\ theorem " ^ quote name); 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

86 
None) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

87 
else update_db true 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

88 
cs (Symtab.update ((c, tagged_thm :: old_thms), result)) 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

89 
end; 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

90 

8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

91 
val const_idx' = update_db false consts const_idx; 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

92 
in if consts = [] then writeln ("Warning: Theorem " ^ name ^ 
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

93 
" cannot be stored in ThmDB\n\t because it \ 
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

94 
\contains no or only ignored constants.") 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

95 
else if is_some const_idx' then 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

96 
thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

97 
const_idx = the const_idx'} 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

98 
else (); 
1236
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1230
diff
changeset

99 
thm 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

100 
end; 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

101 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

102 
(*remove all theorems with given signature from database*) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

103 
fun delete_thm_db thy = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

104 
let 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

105 
val sign = sign_of thy; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

106 

8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

107 
val ThmDB {count, thy_idx, const_idx} = !thm_db; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

108 

8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

109 
fun update_thys [] result = (result, [], []) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

110 
 update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

111 
result = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

112 
if Sign.eq_sg (sign, thy_sign) then 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

113 
(result @ ts, thy_consts, thy_nums) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

114 
else update_thys ts (thy :: result); 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

115 

8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

116 
val (thy_idx', thy_consts, thy_nums) = update_thys thy_idx []; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

117 

8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

118 
fun update_db [] result = result 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

119 
 update_db (c :: cs) result = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

120 
let val thms' = filter_out (fn (num, _) => num mem thy_nums) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

121 
(Symtab.lookup_multi (result, c)); 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

122 
in update_db cs (Symtab.update ((c, thms'), result)) end; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

123 
in thm_db := ThmDB {count = count, thy_idx = thy_idx', 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

124 
const_idx = update_db thy_consts const_idx} 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

125 
end; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

126 

8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

127 
(*intersection of two theorem lists with descending tags*) 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

128 
infix desc_inter; 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

129 
fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = [] 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

130 
 xs desc_inter [] = [] 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

131 
 (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) = 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

132 
if xi = yi then x :: (xs desc_inter ys) 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

133 
else if xi > yi then xs desc_inter yss 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

134 
else xss desc_inter ys; 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

135 

dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

136 
(*get all theorems from database that contain a list of constants*) 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

137 
fun thms_containing constants = 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

138 
let fun collect [] _ result = map snd result 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

139 
 collect (c :: cs) first result = 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

140 
let val ThmDB {const_idx, ...} = !thm_db; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

141 

8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

142 
val new_thms = Symtab.lookup_multi (const_idx, c); 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

143 
in collect cs false (if first then new_thms 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

144 
else (result desc_inter new_thms)) 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

145 
end; 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

146 

1134  147 
val look_for = constants \\ ignore; 
148 
in if null look_for then 

1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

149 
error ("No or only ignored constants were specified for theorem \ 
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

150 
\database search:\n " ^ commas (map quote ignore)) 
1134  151 
else (); 
152 
collect look_for true [] end; 

1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

153 

1221  154 
val intro_const = top_const o concl_of; 
155 

156 
fun elim_const thm = case prems_of thm of [] => None  p::_ => top_const(p); 

157 

158 
(* In case faster access is necessary, the thm db should provide special 

159 
functions 

160 

161 
index_intros, index_elims: string > (string * thm) list 

162 

163 
where thm [ A1 ; ...; An ] ==> B is returned by 

164 
 index_intros c if B is of the form c t1 ... tn 

165 
 index_elims c if A1 is of the form c t1 ... tn 

166 
*) 

167 

168 
(* could be provided by thm db *) 

169 
fun index_intros c = 

170 
let fun topc(_,thm) = intro_const thm = Some(c); 

171 
val named_thms = thms_containing [c] 

172 
in filter topc named_thms end; 

173 

174 
(* could be provided by thm db *) 

175 
fun index_elims c = 

176 
let fun topc(_,thm) = elim_const thm = Some(c); 

177 
val named_thms = thms_containing [c] 

178 
in filter topc named_thms end; 

179 

180 
(*assume that parameters have unique names*) 

181 
fun goal_params i = 

182 
let val gi = getgoal i 

183 
val frees = map Free (Logic.strip_params gi) 

184 
in (gi,frees) end; 

185 

186 
fun concl_of_goal i = 

187 
let val (gi,frees) = goal_params i 

188 
val B = Logic.strip_assums_concl gi 

189 
in subst_bounds(frees,B) end; 

190 

191 
fun prems_of_goal i = 

192 
let val (gi,frees) = goal_params i 

193 
val As = Logic.strip_assums_hyp gi 

194 
in map (fn A => subst_bounds(frees,A)) As end; 

195 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

196 
fun select_match(obj, signobj, named_thms, extract) = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

197 
let fun matches(prop, tsig) = 
1221  198 
case extract prop of 
199 
None => false 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

200 
 Some pat => Pattern.matches tsig (pat, obj); 
1221  201 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

202 
fun select((p as (_,thm))::named_thms, sels) = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

203 
let val {prop, sign, ...} = rep_thm thm 
1221  204 
in select(named_thms, 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

205 
if Sign.subsig(sign, signobj) andalso 
1230  206 
matches(prop,#tsig(Sign.rep_sg signobj)) 
1221  207 
then p::sels else sels) 
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

208 
end 
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

209 
 select([],sels) = sels 
1221  210 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

211 
in select(named_thms, []) end; 
1221  212 

213 
fun find_matching(prop,sign,index,extract) = 

214 
(case top_const prop of 

215 
Some c => select_match(prop,sign,index c,extract) 

216 
 _ => []); 

217 

218 
fun find_intros(prop,sign) = 

219 
find_matching(prop,sign,index_intros,Some o Logic.strip_imp_concl); 

1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

220 

1221  221 
fun find_elims sign prop = 
222 
let fun major prop = case Logic.strip_imp_prems prop of 

223 
[] => None  p::_ => Some p 

224 
in find_matching(prop,sign,index_elims,major) end; 

225 

226 
fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm()))); 

227 

228 
fun findEs i = 

1230  229 
let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2); 
230 
val sign = #sign(rep_thm(topthm())) 

231 
val thmss = map (find_elims sign) (prems_of_goal i) 

232 
in foldl (gen_union eq_nth) ([],thmss) end; 

1221  233 

234 
fun findE i j = 

235 
let val sign = #sign(rep_thm(topthm())) 

236 
in find_elims sign (nth_elem(j1, prems_of_goal i)) end; 

237 

1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

238 
end; 