author  paulson 
Tue, 22 Jul 1997 11:14:18 +0200  
changeset 3538  ed9de44032e0 
parent 2150  084218afaf4b 
child 3601  43c7912aac8d 
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 

1749  39 
 _ => None) 
40 
 top_const _ = None; 

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

41 

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

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

43 
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

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

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

46 
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

47 

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

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

50 
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

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

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

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

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

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

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

57 

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

59 
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

60 
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

61 

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

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

63 

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

64 
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

65 

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

66 
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

67 
 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

68 
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

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

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

71 

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

72 
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

73 

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

74 
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

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

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

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

78 

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

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

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

81 
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

82 
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

83 
 None => false 
1308  84 
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

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

86 
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

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

88 

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

89 
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

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

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

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

93 
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

94 
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

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

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

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

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

99 

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

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

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

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

104 

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

105 
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

106 

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

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

109 
 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

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

111 
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

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

113 
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

114 

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

115 
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

116 

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

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 

1272  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 

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

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 

1654
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

202 
fun substsize(prop, tsig) = 
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

203 
let val Some pat = extract prop 
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

204 
val (_,subst) = Pattern.match tsig (pat,obj) 
2150  205 
in foldl op+ 
206 
(0, map (fn (_,t) => size_of_term t) subst) 

207 
end 

1654
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

208 

faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

209 
fun thm_order ((p0:int,s0:int,_),(p1,s1,_)) = 
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

210 
(((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<=s1) 
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

211 
orelse (p0=0 andalso p1<>0) 
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

212 

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

213 
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

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

216 
if Sign.subsig(sign, signobj) andalso 
1230  217 
matches(prop,#tsig(Sign.rep_sg signobj)) 
1654
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

218 
then 
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

219 
(nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels 
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

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

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

222 
 select([],sels) = sels 
1221  223 

1654
faa643c33ee6
select_match now sorts list of matching theorems according to the
berghofe
parents:
1580
diff
changeset

224 
in map (fn (_,_,t) => t) (sort thm_order (select(named_thms, []))) end; 
1221  225 

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

227 
(case top_const prop of 

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

229 
 _ => []); 

230 

231 
fun find_intros(prop,sign) = 

232 
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

233 

1221  234 
fun find_elims sign prop = 
235 
let fun major prop = case Logic.strip_imp_prems prop of 

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

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

238 

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

240 

241 
fun findEs i = 

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

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

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

1221  246 

247 
fun findE i j = 

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

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

250 

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

251 
end; 