author  berghofe 
Fri, 15 Mar 1996 12:01:19 +0100  
changeset 1580  e3fd931e6095 
parent 1512  ce37c64244c0 
child 1654  faa643c33ee6 
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 = 
1512  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 

1512  26 
end; 
1132
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 

1272  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 

1272  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 
1308  83 
in if duplicate then None 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

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

85 
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

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

87 

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

88 
val const_idx' = update_db false consts const_idx; 
1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1512
diff
changeset

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

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

91 
\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

92 
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

93 
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

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

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

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

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

98 

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

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

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

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

103 

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

104 
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

105 

1272  106 
(*Remove theory from thy_idx and get the data associated with it*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

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

108 
 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

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

110 
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

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

112 
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

113 

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

114 
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

115 

1272  116 
(*Remove all theorems belonging to a theory*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset

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

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

119 
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

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

121 
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

122 
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

123 
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

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

125 

1272  126 
(*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

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

128 
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

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

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

131 
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

132 
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

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

134 

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

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

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

138 
 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

139 
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

140 

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

141 
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

142 
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

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

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

145 

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

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

148 
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

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

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

152 

1221  153 
val intro_const = top_const o concl_of; 
154 

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

156 

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

158 
functions 

159 

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

161 

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

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

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

165 
*) 

166 

167 
(* could be provided by thm db *) 

168 
fun index_intros c = 

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

170 
val named_thms = thms_containing [c] 

171 
in filter topc named_thms end; 

172 

173 
(* could be provided by thm db *) 

174 
fun index_elims c = 

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

176 
val named_thms = thms_containing [c] 

177 
in filter topc named_thms end; 

178 

179 
(*assume that parameters have unique names*) 

180 
fun goal_params i = 

181 
let val gi = getgoal i 

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

183 
in (gi,frees) end; 

184 

185 
fun concl_of_goal i = 

186 
let val (gi,frees) = goal_params i 

187 
val B = Logic.strip_assums_concl gi 

188 
in subst_bounds(frees,B) end; 

189 

190 
fun prems_of_goal i = 

191 
let val (gi,frees) = goal_params i 

192 
val As = Logic.strip_assums_hyp gi 

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

194 

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

195 
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

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

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

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

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

201 
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

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

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

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

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

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

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

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

213 
(case top_const prop of 

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

215 
 _ => []); 

216 

217 
fun find_intros(prop,sign) = 

218 
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

219 

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

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

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

224 

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

226 

227 
fun findEs i = 

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

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

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

1221  232 

233 
fun findE i j = 

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

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

236 

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

237 
end; 