author  nipkow 
Mon, 07 Aug 1995 15:23:59 +0200  
changeset 1221  19dde7bfcd07 
parent 1141  a94c0ab9a3ed 
child 1230  87e29e18e970 
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 

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

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

8 
sig 
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

9 
type thm_db_type 
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

10 

a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

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

12 
val store_thm_db: string * thm > thm 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

13 
val thms_containing: string list > (string * thm) list 
1221  14 
val findI: int > (string * thm)list 
15 
val findEs: int > (string * thm)list 

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

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

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

18 

1221  19 
functor ThmDBFun(): THMDB = 
20 
struct 

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

21 

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

24 

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

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

27 

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

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

30 
 _ => None); 

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

31 

1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

32 
type thm_db_type = (int * ((int * (string * thm)) list) Symtab.table) ref; 
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

33 

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

34 
(*Symtab which associates a constant with a list of theorems that contain the 
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

35 
constant (theorems are represented as numbers)*) 
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

36 
val thm_db = ref (0, 
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

37 
(Symtab.make ([] : (string * ((int * (string * thm)) list)) list))); 
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

38 
(*number of next theorem and symtab containing theorems*) 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

39 

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

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

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

42 
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

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

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

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

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

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

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

49 

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

50 
(*store a theorem in database*) 
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

51 
fun store_thm_db (named_thm as (name, t)) = 
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset

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

53 

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

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

55 

1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

56 
val (num, db) = !thm_db; 
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

57 

a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

58 
val tagged_thm = (num + 1, named_thm); 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

59 

1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

60 
fun update_db [] result = result 
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

61 
 update_db (c :: cs) result = 
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

62 
let val old_thms = Symtab.lookup_multi (result, c); 
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

63 
in update_db cs (Symtab.update ((c, tagged_thm :: old_thms), 
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

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

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

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

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

68 
\contains no or only ignored constants.") 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

69 
else (); 
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

70 
thm_db := (num+1, update_db consts db); 
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset

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

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

73 

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

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

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

76 
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

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

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

79 
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

80 
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

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

82 

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

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

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

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

86 
 collect (c :: cs) first result = 
1141
a94c0ab9a3ed
commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents:
1137
diff
changeset

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

88 
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

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

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

91 

1134  92 
val look_for = constants \\ ignore; 
93 
in if null look_for then 

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

94 
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

95 
\database search:\n " ^ commas (map quote ignore)) 
1134  96 
else (); 
97 
collect look_for true [] end; 

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

98 

1221  99 
val intro_const = top_const o concl_of; 
100 

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

102 

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

104 
functions 

105 

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

107 

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

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

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

111 
*) 

112 

113 
(* could be provided by thm db *) 

114 
fun index_intros c = 

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

116 
val named_thms = thms_containing [c] 

117 
in filter topc named_thms end; 

118 

119 
(* could be provided by thm db *) 

120 
fun index_elims c = 

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

122 
val named_thms = thms_containing [c] 

123 
in filter topc named_thms end; 

124 

125 
(*assume that parameters have unique names*) 

126 
fun goal_params i = 

127 
let val gi = getgoal i 

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

129 
in (gi,frees) end; 

130 

131 
fun concl_of_goal i = 

132 
let val (gi,frees) = goal_params i 

133 
val B = Logic.strip_assums_concl gi 

134 
in subst_bounds(frees,B) end; 

135 

136 
fun prems_of_goal i = 

137 
let val (gi,frees) = goal_params i 

138 
val As = Logic.strip_assums_hyp gi 

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

140 

141 
fun select_match(obj,signobj,named_thms,extract) = 

142 
let fun matches(prop,tsig) = 

143 
case extract prop of 

144 
None => false 

145 
 Some pat => Pattern.matches tsig (pat,obj); 

146 

147 
fun select((p as (_,thm))::named_thms,sels) = 

148 
let val {prop,sign,...} = rep_thm thm 

149 
in select(named_thms, 

150 
if Sign.subsig(sign,signobj) andalso 

151 
matches(prop,#tsig(Sign.rep_sg sign)) 

152 
then p::sels else sels) 

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

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

154 
 select([],sels) = sels 
1221  155 

156 
in select(named_thms,[]) end; 

157 

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

159 
(case top_const prop of 

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

161 
 _ => []); 

162 

163 
fun find_intros(prop,sign) = 

164 
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

165 

1221  166 
fun find_elims sign prop = 
167 
let fun major prop = case Logic.strip_imp_prems prop of 

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

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

170 

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

172 

173 
fun findEs i = 

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

175 
in flat(map (find_elims sign) (prems_of_goal i)) end; 

176 

177 
fun findE i j = 

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

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

180 

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

181 
end; 