author  wenzelm 
Tue, 19 Jul 2005 17:21:56 +0200  
changeset 16884  1678a796b6b2 
parent 16847  8fc160b12e73 
child 16945  5d3ae25673a8 
permissions  rwrr 
250  1 
(* Title: Pure/thm.ML 
0  2 
ID: $Id$ 
250  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

4 
Copyright 1994 University of Cambridge 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

5 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

6 
The very core of Isabelle's Meta Logic: certified types and terms, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

7 
meta theorems, meta rules (including lifting and resolution). 
0  8 
*) 
9 

6089  10 
signature BASIC_THM = 
1503  11 
sig 
1160  12 
(*certified types*) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

13 
type ctyp 
16656  14 
val rep_ctyp: ctyp > 
15 
{thy: theory, 

16 
sign: theory, (*obsolete*) 

17 
T: typ, 

18 
sorts: sort list} 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

19 
val theory_of_ctyp: ctyp > theory 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

20 
val typ_of: ctyp > typ 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

21 
val ctyp_of: theory > typ > ctyp 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

22 
val read_ctyp: theory > string > ctyp 
1160  23 

24 
(*certified terms*) 

25 
type cterm 

1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

26 
exception CTERM of string 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

27 
val rep_cterm: cterm > 
16656  28 
{thy: theory, 
29 
sign: theory, (*obsolete*) 

30 
t: term, 

31 
T: typ, 

32 
maxidx: int, 

33 
sorts: sort list} 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

34 
val crep_cterm: cterm > 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

35 
{thy: theory, sign: theory, t: term, T: ctyp, maxidx: int, sorts: sort list} 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

36 
val theory_of_cterm: cterm > theory 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

37 
val sign_of_cterm: cterm > theory (*obsolete*) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

38 
val term_of: cterm > term 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

39 
val cterm_of: theory > term > cterm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

40 
val ctyp_of_term: cterm > ctyp 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

41 
val read_cterm: theory > string * typ > cterm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

42 
val adjust_maxidx: cterm > cterm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

43 
val read_def_cterm: 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

44 
theory * (indexname > typ option) * (indexname > sort option) > 
1160  45 
string list > bool > string * typ > cterm * (indexname * typ) list 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

46 
val read_def_cterms: 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

47 
theory * (indexname > typ option) * (indexname > sort option) > 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

48 
string list > bool > (string * typ)list 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

49 
> cterm list * (indexname * typ)list 
1160  50 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

51 
type tag (* = string * string list *) 
1529  52 

1160  53 
(*meta theorems*) 
54 
type thm 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

55 
val rep_thm: thm > 
16656  56 
{thy: theory, 
57 
sign: theory, (*obsolete*) 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

58 
der: bool * Proofterm.proof, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

59 
maxidx: int, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

60 
shyps: sort list, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

61 
hyps: term list, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

62 
tpairs: (term * term) list, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

63 
prop: term} 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

64 
val crep_thm: thm > 
16656  65 
{thy: theory, 
66 
sign: theory, (*obsolete*) 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

67 
der: bool * Proofterm.proof, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

68 
maxidx: int, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

69 
shyps: sort list, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

70 
hyps: cterm list, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

71 
tpairs: (cterm * cterm) list, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

72 
prop: cterm} 
6089  73 
exception THM of string * int * thm list 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

74 
type 'a attribute (* = 'a * thm > 'a * thm *) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

75 
val eq_thm: thm * thm > bool 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

76 
val eq_thms: thm list * thm list > bool 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

77 
val theory_of_thm: thm > theory 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

78 
val sign_of_thm: thm > theory (*obsolete*) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

79 
val prop_of: thm > term 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

80 
val proof_of: thm > Proofterm.proof 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

81 
val tpairs_of: thm > (term * term) list 
16656  82 
val concl_of: thm > term 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

83 
val prems_of: thm > term list 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

84 
val nprems_of: thm > int 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

85 
val cprop_of: thm > cterm 
16656  86 
val transfer: theory > thm > thm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

87 
val extra_shyps: thm > sort list 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

88 
val strip_shyps: thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

89 
val get_axiom_i: theory > string > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

90 
val get_axiom: theory > xstring > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

91 
val def_name: string > string 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

92 
val get_def: theory > xstring > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

93 
val axioms_of: theory > (string * thm) list 
1160  94 

95 
(*meta rules*) 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

96 
val assume: cterm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

97 
val compress: thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

98 
val implies_intr: cterm > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

99 
val implies_elim: thm > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

100 
val forall_intr: cterm > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

101 
val forall_elim: cterm > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

102 
val reflexive: cterm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

103 
val symmetric: thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

104 
val transitive: thm > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

105 
val beta_conversion: bool > cterm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

106 
val eta_conversion: cterm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

107 
val abstract_rule: string > cterm > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

108 
val combination: thm > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

109 
val equal_intr: thm > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

110 
val equal_elim: thm > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

111 
val flexflex_rule: thm > thm Seq.seq 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

112 
val instantiate: (ctyp * ctyp) list * (cterm * cterm) list > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

113 
val trivial: cterm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

114 
val class_triv: theory > class > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

115 
val varifyT: thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

116 
val varifyT': (string * sort) list > thm > thm * ((string * sort) * indexname) list 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

117 
val freezeT: thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

118 
val dest_state: thm * int > (term * term) list * term list * term * term 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

119 
val lift_rule: (thm * int) > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

120 
val incr_indexes: int > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

121 
val assumption: int > thm > thm Seq.seq 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

122 
val eq_assumption: int > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

123 
val rotate_rule: int > int > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

124 
val permute_prems: int > int > thm > thm 
1160  125 
val rename_params_rule: string list * int > thm > thm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

126 
val bicompose: bool > bool * thm * int > int > thm > thm Seq.seq 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

127 
val biresolution: bool > (bool * thm) list > int > thm > thm Seq.seq 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

128 
val invoke_oracle: theory > xstring > theory * Object.T > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

129 
val invoke_oracle_i: theory > string > theory * Object.T > thm 
250  130 
end; 
0  131 

6089  132 
signature THM = 
133 
sig 

134 
include BASIC_THM 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

135 
val dest_ctyp: ctyp > ctyp list 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

136 
val dest_comb: cterm > cterm * cterm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

137 
val dest_abs: string option > cterm > cterm * cterm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

138 
val capply: cterm > cterm > cterm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

139 
val cabs: cterm > cterm > cterm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

140 
val major_prem_of: thm > term 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

141 
val no_prems: thm > bool 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

142 
val no_attributes: 'a > 'a * 'b attribute list 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

143 
val apply_attributes: ('a * thm) * 'a attribute list > ('a * thm) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

144 
val applys_attributes: ('a * thm list) * 'a attribute list > ('a * thm list) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

145 
val get_name_tags: thm > string * tag list 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

146 
val put_name_tags: string * tag list > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

147 
val name_of_thm: thm > string 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

148 
val tags_of_thm: thm > tag list 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

149 
val name_thm: string * thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

150 
val rename_boundvars: term > term > thm > thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

151 
val cterm_match: cterm * cterm > (ctyp * ctyp) list * (cterm * cterm) list 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

152 
val cterm_first_order_match: cterm * cterm > (ctyp * ctyp) list * (cterm * cterm) list 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

153 
val cterm_incr_indexes: int > cterm > cterm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

154 
val terms_of_tpairs: (term * term) list > term list 
16725  155 
val full_prop_of: thm > term 
6089  156 
end; 
157 

3550  158 
structure Thm: THM = 
0  159 
struct 
250  160 

16656  161 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

162 
(*** Certified terms and types ***) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

163 

16656  164 
(** collect occurrences of sorts  unless all sorts nonempty **) 
165 

16679  166 
fun may_insert_typ_sorts thy T = if Sign.all_sorts_nonempty thy then I else Sorts.insert_typ T; 
167 
fun may_insert_term_sorts thy t = if Sign.all_sorts_nonempty thy then I else Sorts.insert_term t; 

16656  168 

169 
(*NB: type unification may invent new sorts*) 

170 
fun may_insert_env_sorts thy (env as Envir.Envir {iTs, ...}) = 

171 
if Sign.all_sorts_nonempty thy then I 

172 
else Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) iTs; 

173 

174 

175 

250  176 
(** certified types **) 
177 

16656  178 
datatype ctyp = Ctyp of {thy_ref: theory_ref, T: typ, sorts: sort list}; 
250  179 

16656  180 
fun rep_ctyp (Ctyp {thy_ref, T, sorts}) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

181 
let val thy = Theory.deref thy_ref 
16656  182 
in {thy = thy, sign = thy, T = T, sorts = sorts} end; 
250  183 

16656  184 
fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

185 

250  186 
fun typ_of (Ctyp {T, ...}) = T; 
187 

16656  188 
fun ctyp_of thy raw_T = 
189 
let val T = Sign.certify_typ thy raw_T 

190 
in Ctyp {thy_ref = Theory.self_ref thy, T = T, sorts = may_insert_typ_sorts thy T []} end; 

250  191 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

192 
fun read_ctyp thy s = 
16656  193 
let val T = Sign.read_typ (thy, K NONE) s 
194 
in Ctyp {thy_ref = Theory.self_ref thy, T = T, sorts = may_insert_typ_sorts thy T []} end; 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

195 

16656  196 
fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts), sorts}) = 
197 
map (fn T => Ctyp {thy_ref = thy_ref, T = T, sorts = sorts}) Ts 

16679  198 
 dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); 
15087  199 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

200 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

201 

250  202 
(** certified terms **) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

203 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

204 
(*certified terms with checked typ, maxidx, and sorts*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

205 
datatype cterm = Cterm of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

206 
{thy_ref: theory_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

207 
t: term, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

208 
T: typ, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

209 
maxidx: int, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

210 
sorts: sort list}; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

211 

16679  212 
exception CTERM of string; 
213 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

214 
fun rep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

215 
let val thy = Theory.deref thy_ref 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

216 
in {thy = thy, sign = thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

217 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

218 
fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

219 
let val thy = Theory.deref thy_ref in 
16656  220 
{thy = thy, sign = thy, t = t, T = Ctyp {thy_ref = thy_ref, T = T, sorts = sorts}, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

221 
maxidx = maxidx, sorts = sorts} 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

222 
end; 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

223 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

224 
fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref; 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

225 
val sign_of_cterm = theory_of_cterm; 
9461  226 

250  227 
fun term_of (Cterm {t, ...}) = t; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

228 

16656  229 
fun ctyp_of_term (Cterm {thy_ref, T, sorts, ...}) = 
230 
Ctyp {thy_ref = thy_ref, T = T, sorts = sorts}; 

2671  231 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

232 
fun cterm_of thy tm = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

233 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

234 
val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm; 
16656  235 
val sorts = may_insert_term_sorts thy t []; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

236 
in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

237 

16656  238 
fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) = 
239 
Theory.merge_refs (r1, r2); 

240 

1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

241 
(*Destruct application in cterms*) 
16679  242 
fun dest_comb (Cterm {t = t $ u, T, thy_ref, maxidx, sorts}) = 
243 
let val A = Term.argument_type_of t in 

244 
(Cterm {t = t, T = A > T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, 

245 
Cterm {t = u, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) 

1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

246 
end 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

247 
 dest_comb _ = raise CTERM "dest_comb"; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

248 

e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

249 
(*Destruct abstraction in cterms*) 
16679  250 
fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) = 
251 
let val (y', t') = Term.dest_abs (if_none a x, T, t) in 

252 
(Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, 

253 
Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) 

1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

254 
end 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

255 
 dest_abs _ _ = raise CTERM "dest_abs"; 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

256 

2147  257 
(*Makes maxidx precise: it is often too big*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

258 
fun adjust_maxidx (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

259 
if maxidx = ~1 then ct 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

260 
else Cterm {thy_ref = thy_ref, t = t, T = T, maxidx = maxidx_of_term t, sorts = sorts}; 
1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

261 

1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

262 
(*Form cterm out of a function and an argument*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

263 
fun capply 
16656  264 
(cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...}) 
265 
(cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

266 
if T = dty then 
16656  267 
Cterm {thy_ref = merge_thys0 cf cx, 
268 
t = f $ x, 

269 
T = rty, 

270 
maxidx = Int.max (maxidx1, maxidx2), 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

271 
sorts = Sorts.union sorts1 sorts2} 
1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

272 
else raise CTERM "capply: types don't agree" 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

273 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  274 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

275 
fun cabs 
16656  276 
(ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...}) 
277 
(ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

278 
let val t = lambda t1 t2 handle TERM _ => raise CTERM "cabs: first arg is not a variable" in 
16656  279 
Cterm {thy_ref = merge_thys0 ct1 ct2, 
280 
t = t, T = T1 > T2, 

281 
maxidx = Int.max (maxidx1, maxidx2), 

282 
sorts = Sorts.union sorts1 sorts2} 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

283 
end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

284 

10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

285 
(*Matching of cterms*) 
16656  286 
fun gen_cterm_match match 
287 
(ct1 as Cterm {t = t1, maxidx = maxidx1, sorts = sorts1, ...}, 

288 
ct2 as Cterm {t = t2, maxidx = maxidx2, sorts = sorts2, ...}) = 

10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

289 
let 
16656  290 
val thy_ref = merge_thys0 ct1 ct2; 
291 
val (Tinsts, tinsts) = match (Sign.tsig_of (Theory.deref thy_ref)) (t1, t2); 

10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

292 
val maxidx = Int.max (maxidx1, maxidx2); 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

293 
val sorts = Sorts.union sorts1 sorts2; 
16656  294 
fun mk_cTinst (ixn, (S, T)) = 
295 
(Ctyp {T = TVar (ixn, S), thy_ref = thy_ref, sorts = sorts}, 

296 
Ctyp {T = T, thy_ref = thy_ref, sorts = sorts}); 

297 
fun mk_ctinst (ixn, (T, t)) = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

298 
let val T = Envir.typ_subst_TVars Tinsts T in 
16656  299 
(Cterm {t = Var (ixn, T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, 
300 
Cterm {t = t, T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) 

10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

301 
end; 
16656  302 
in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

303 

5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

304 
val cterm_match = gen_cterm_match Pattern.match; 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

305 
val cterm_first_order_match = gen_cterm_match Pattern.first_order_match; 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

306 

5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

307 
(*Incrementing indexes*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

308 
fun cterm_incr_indexes i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

309 
if i < 0 then raise CTERM "negative increment" 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

310 
else if i = 0 then ct 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

311 
else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t, 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

312 
T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts}; 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

313 

2509  314 

315 

574  316 
(** read cterms **) (*exception ERROR*) 
250  317 

4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

318 
(*read terms, infer types, certify terms*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

319 
fun read_def_cterms (thy, types, sorts) used freeze sTs = 
250  320 
let 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

321 
val (ts', tye) = Sign.read_def_terms (thy, types, sorts) used freeze sTs; 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

322 
val cts = map (cterm_of thy) ts' 
2979  323 
handle TYPE (msg, _, _) => error msg 
2386  324 
 TERM (msg, _) => error msg; 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

325 
in (cts, tye) end; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

326 

6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

327 
(*read term, infer types, certify term*) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

328 
fun read_def_cterm args used freeze aT = 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

329 
let val ([ct],tye) = read_def_cterms args used freeze [aT] 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

330 
in (ct,tye) end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

331 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

332 
fun read_cterm thy = #1 o read_def_cterm (thy, K NONE, K NONE) [] true; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

333 

250  334 

6089  335 
(*tags provide additional comment, apart from the axiom/theorem name*) 
336 
type tag = string * string list; 

337 

2509  338 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

339 
(*** Meta theorems ***) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

340 

11518  341 
structure Pt = Proofterm; 
342 

0  343 
datatype thm = Thm of 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

344 
{thy_ref: theory_ref, (*dynamic reference to theory*) 
11518  345 
der: bool * Pt.proof, (*derivation*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

346 
maxidx: int, (*maximum index of any Var or TVar*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

347 
shyps: sort list, (*sort hypotheses as ordered list*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

348 
hyps: term list, (*hypotheses as ordered list*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

349 
tpairs: (term * term) list, (*flexflex pairs*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

350 
prop: term}; (*conclusion*) 
0  351 

16725  352 
(*errors involving theorems*) 
353 
exception THM of string * int * thm list; 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

354 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

355 
fun rep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

356 
let val thy = Theory.deref thy_ref in 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

357 
{thy = thy, sign = thy, der = der, maxidx = maxidx, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

358 
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop} 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

359 
end; 
0  360 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

361 
(*version of rep_thm returning cterms instead of terms*) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

362 
fun crep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

363 
let 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

364 
val thy = Theory.deref thy_ref; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

365 
fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps}; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

366 
in 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

367 
{thy = thy, sign = thy, der = der, maxidx = maxidx, shyps = shyps, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

368 
hyps = map (cterm ~1) hyps, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

369 
tpairs = map (pairself (cterm maxidx)) tpairs, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

370 
prop = cterm maxidx prop} 
1517  371 
end; 
372 

16725  373 
fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs []; 
374 

375 
fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u'; 

376 
val union_tpairs = gen_merge_lists eq_tpairs; 

16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

377 
val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u); 
16725  378 

379 
fun attach_tpairs tpairs prop = 

380 
Logic.list_implies (map Logic.mk_equals tpairs, prop); 

381 

382 
fun full_prop_of (Thm {tpairs, prop, ...}) = attach_tpairs tpairs prop; 

383 

0  384 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

385 
(*attributes subsume any kind of rules or context modifiers*) 
6089  386 
type 'a attribute = 'a * thm > 'a * thm; 
387 

388 
fun no_attributes x = (x, []); 

389 
fun apply_attributes (x_th, atts) = Library.apply atts x_th; 

390 
fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths; 

391 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

392 

16656  393 
(* hyps *) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

394 

16679  395 
val remove_hyps = OrdList.remove Term.fast_term_ord; 
396 
val union_hyps = OrdList.union Term.fast_term_ord; 

397 
val eq_set_hyps = OrdList.eq_set Term.fast_term_ord; 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

398 

ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

399 

ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

400 
(* eq_thm(s) *) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

401 

3994  402 
fun eq_thm (th1, th2) = 
403 
let 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

404 
val {thy = thy1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = 
9031  405 
rep_thm th1; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

406 
val {thy = thy2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = 
9031  407 
rep_thm th2; 
3994  408 
in 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

409 
Context.joinable (thy1, thy2) andalso 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

410 
Sorts.eq_set (shyps1, shyps2) andalso 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

411 
eq_set_hyps (hyps1, hyps2) andalso 
16656  412 
equal_lists eq_tpairs (tpairs1, tpairs2) andalso 
3994  413 
prop1 aconv prop2 
414 
end; 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

415 

16135  416 
val eq_thms = Library.equal_lists eq_thm; 
417 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

418 
fun theory_of_thm (Thm {thy_ref, ...}) = Theory.deref thy_ref; 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

419 
val sign_of_thm = theory_of_thm; 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

420 

12803  421 
fun prop_of (Thm {prop, ...}) = prop; 
13528  422 
fun proof_of (Thm {der = (_, proof), ...}) = proof; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

423 
fun tpairs_of (Thm {tpairs, ...}) = tpairs; 
0  424 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

425 
val concl_of = Logic.strip_imp_concl o prop_of; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

426 
val prems_of = Logic.strip_imp_prems o prop_of; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

427 
fun nprems_of th = Logic.count_prems (prop_of th, 0); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

428 
val no_prems = equal 0 o nprems_of; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

429 

ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

430 
fun major_prem_of th = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

431 
(case prems_of th of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

432 
prem :: _ => Logic.strip_assums_concl prem 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

433 
 [] => raise THM ("major_prem_of: rule with no premises", 0, [th])); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

434 

ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

435 
(*the statement of any thm is a cterm*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

436 
fun cprop_of (Thm {thy_ref, maxidx, shyps, prop, ...}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

437 
Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop, sorts = shyps}; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

438 

16656  439 
(*explicit transfer to a super theory*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

440 
fun transfer thy' thm = 
3895  441 
let 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

442 
val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm; 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

443 
val thy = Theory.deref thy_ref; 
3895  444 
in 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

445 
if eq_thy (thy, thy') then thm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

446 
else if subthy (thy, thy') then 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

447 
Thm {thy_ref = Theory.self_ref thy', der = der, maxidx = maxidx, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

448 
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop} 
3895  449 
else raise THM ("transfer: not a super theory", 0, [thm]) 
450 
end; 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

451 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

452 

16656  453 
(* merge theories of cterms/thms; raise exception if incompatible *) 
454 

455 
fun merge_thys1 (Cterm {thy_ref = r1, ...}) (th as Thm {thy_ref = r2, ...}) = 

456 
Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th]); 

457 

458 
fun merge_thys2 (th1 as Thm {thy_ref = r1, ...}) (th2 as Thm {thy_ref = r2, ...}) = 

459 
Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]); 

460 

461 

0  462 

1238  463 
(** sort contexts of theorems **) 
464 

16656  465 
fun present_sorts (Thm {hyps, tpairs, prop, ...}) = 
466 
fold (fn (t, u) => Sorts.insert_term t o Sorts.insert_term u) tpairs 

467 
(Sorts.insert_terms hyps (Sorts.insert_term prop [])); 

1238  468 

7642  469 
(*remove extra sorts that are nonempty by virtue of type signature information*) 
470 
fun strip_shyps (thm as Thm {shyps = [], ...}) = thm 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

471 
 strip_shyps (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
7642  472 
let 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

473 
val thy = Theory.deref thy_ref; 
16656  474 
val shyps' = 
475 
if Sign.all_sorts_nonempty thy then [] 

476 
else 

477 
let 

478 
val present = present_sorts thm; 

479 
val extra = Sorts.subtract present shyps; 

480 
val witnessed = map #2 (Sign.witness_sorts thy present extra); 

481 
in Sorts.subtract witnessed shyps end; 

7642  482 
in 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

483 
Thm {thy_ref = thy_ref, der = der, maxidx = maxidx, 
16656  484 
shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop} 
7642  485 
end; 
1238  486 

16656  487 
(*dangling sort constraints of a thm*) 
488 
fun extra_shyps (th as Thm {shyps, ...}) = Sorts.subtract (present_sorts th) shyps; 

489 

1238  490 

491 

1529  492 
(** Axioms **) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

493 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

494 
(*look up the named axiom in the theory or its ancestors*) 
15672  495 
fun get_axiom_i theory name = 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

496 
let 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

497 
fun get_ax thy = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

498 
Symtab.lookup (#2 (#axioms (Theory.rep_theory thy)), name) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

499 
> Option.map (fn prop => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

500 
Thm {thy_ref = Theory.self_ref thy, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

501 
der = Pt.infer_derivs' I (false, Pt.axm_proof name prop), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

502 
maxidx = maxidx_of_term prop, 
16656  503 
shyps = may_insert_term_sorts thy prop [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

504 
hyps = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

505 
tpairs = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

506 
prop = prop}); 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

507 
in 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

508 
(case get_first get_ax (theory :: Theory.ancestors_of theory) of 
15531  509 
SOME thm => thm 
510 
 NONE => raise THEORY ("No axiom " ^ quote name, [theory])) 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

511 
end; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

512 

16352  513 
fun get_axiom thy = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

514 
get_axiom_i thy o NameSpace.intern (Theory.axiom_space thy); 
15672  515 

6368  516 
fun def_name name = name ^ "_def"; 
517 
fun get_def thy = get_axiom thy o def_name; 

4847  518 

1529  519 

776
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

520 
(*return additional axioms of this theory node*) 
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

521 
fun axioms_of thy = 
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

522 
map (fn (s, _) => (s, get_axiom thy s)) 
16352  523 
(Symtab.dest (#2 (#axioms (Theory.rep_theory thy)))); 
776
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

524 

6089  525 

526 
(* name and tags  make proof objects more readable *) 

527 

12923  528 
fun get_name_tags (Thm {hyps, prop, der = (_, prf), ...}) = 
529 
Pt.get_name_tags hyps prop prf; 

4018  530 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

531 
fun put_name_tags x (Thm {thy_ref, der = (ora, prf), maxidx, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

532 
shyps, hyps, tpairs = [], prop}) = Thm {thy_ref = thy_ref, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

533 
der = (ora, Pt.thm_proof (Theory.deref thy_ref) x hyps prop prf), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

534 
maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = [], prop = prop} 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

535 
 put_name_tags _ thm = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

536 
raise THM ("put_name_tags: unsolved flexflex constraints", 0, [thm]); 
6089  537 

538 
val name_of_thm = #1 o get_name_tags; 

539 
val tags_of_thm = #2 o get_name_tags; 

540 

541 
fun name_thm (name, thm) = put_name_tags (name, tags_of_thm thm) thm; 

0  542 

543 

1529  544 
(*Compression of theorems  a separate rule, not integrated with the others, 
545 
as it could be slow.*) 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

546 
fun compress (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

547 
Thm {thy_ref = thy_ref, 
2386  548 
der = der, (*No derivation recorded!*) 
549 
maxidx = maxidx, 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

550 
shyps = shyps, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

551 
hyps = map Term.compress_term hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

552 
tpairs = map (pairself Term.compress_term) tpairs, 
2386  553 
prop = Term.compress_term prop}; 
564  554 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

555 

2509  556 

1529  557 
(*** Meta rules ***) 
0  558 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

559 
(** primitive rules **) 
0  560 

16656  561 
(*The assumption rule A  A*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

562 
fun assume raw_ct = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

563 
let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx raw_ct in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

564 
if T <> propT then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

565 
raise THM ("assume: assumptions must have type prop", 0, []) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

566 
else if maxidx <> ~1 then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

567 
raise THM ("assume: assumptions may not contain schematic variables", maxidx, []) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

568 
else Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

569 
der = Pt.infer_derivs' I (false, Pt.Hyp prop), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

570 
maxidx = ~1, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

571 
shyps = sorts, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

572 
hyps = [prop], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

573 
tpairs = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

574 
prop = prop} 
0  575 
end; 
576 

1220  577 
(*Implication introduction 
3529  578 
[A] 
579 
: 

580 
B 

1220  581 
 
582 
A ==> B 

583 
*) 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

584 
fun implies_intr 
16679  585 
(ct as Cterm {t = A, T, maxidx = maxidxA, sorts, ...}) 
586 
(th as Thm {der, maxidx, hyps, shyps, tpairs, prop, ...}) = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

587 
if T <> propT then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

588 
raise THM ("implies_intr: assumptions must have type prop", 0, [th]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

589 
else 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

590 
Thm {thy_ref = merge_thys1 ct th, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

591 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

592 
maxidx = Int.max (maxidxA, maxidx), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

593 
shyps = Sorts.union sorts shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

594 
hyps = remove_hyps A hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

595 
tpairs = tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

596 
prop = implies $ A $ prop}; 
0  597 

1529  598 

1220  599 
(*Implication elimination 
600 
A ==> B A 

601 
 

602 
B 

603 
*) 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

604 
fun implies_elim thAB thA = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

605 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

606 
val Thm {maxidx = maxA, der = derA, hyps = hypsA, shyps = shypsA, tpairs = tpairsA, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

607 
prop = propA, ...} = thA 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

608 
and Thm {der, maxidx, hyps, shyps, tpairs, prop, ...} = thAB; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

609 
fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

610 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

611 
case prop of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

612 
imp $ A $ B => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

613 
if imp = Term.implies andalso A aconv propA then 
16656  614 
Thm {thy_ref = merge_thys2 thAB thA, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

615 
der = Pt.infer_derivs (curry Pt.%%) der derA, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

616 
maxidx = Int.max (maxA, maxidx), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

617 
shyps = Sorts.union shypsA shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

618 
hyps = union_hyps hypsA hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

619 
tpairs = union_tpairs tpairsA tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

620 
prop = B} 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

621 
else err () 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

622 
 _ => err () 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

623 
end; 
250  624 

1220  625 
(*Forall introduction. The Free or Var x must not be free in the hypotheses. 
16656  626 
[x] 
627 
: 

628 
A 

629 
 

630 
!!x. A 

1220  631 
*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

632 
fun forall_intr 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

633 
(ct as Cterm {t = x, T, sorts, ...}) 
16679  634 
(th as Thm {der, maxidx, shyps, hyps, tpairs, prop, ...}) = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

635 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

636 
fun result a = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

637 
Thm {thy_ref = merge_thys1 ct th, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

638 
der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

639 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

640 
shyps = Sorts.union sorts shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

641 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

642 
tpairs = tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

643 
prop = all T $ Abs (a, T, abstract_over (x, prop))}; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

644 
fun check_occs x ts = 
16847
8fc160b12e73
invoke_oracle: do not keep theory value, but theory_ref;
wenzelm
parents:
16725
diff
changeset

645 
if exists (fn t => Logic.occs (x, t)) ts then 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

646 
raise THM("forall_intr: variable free in assumptions", 0, [th]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

647 
else (); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

648 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

649 
case x of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

650 
Free (a, _) => (check_occs x hyps; check_occs x (terms_of_tpairs tpairs); result a) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

651 
 Var ((a, _), _) => (check_occs x (terms_of_tpairs tpairs); result a) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

652 
 _ => raise THM ("forall_intr: not a variable", 0, [th]) 
0  653 
end; 
654 

1220  655 
(*Forall elimination 
16656  656 
!!x. A 
1220  657 
 
658 
A[t/x] 

659 
*) 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

660 
fun forall_elim 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

661 
(ct as Cterm {t, T, maxidx = maxt, sorts, ...}) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

662 
(th as Thm {der, maxidx, shyps, hyps, tpairs, prop, ...}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

663 
(case prop of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

664 
Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

665 
if T <> qary then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

666 
raise THM ("forall_elim: type mismatch", 0, [th]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

667 
else 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

668 
Thm {thy_ref = merge_thys1 ct th, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

669 
der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

670 
maxidx = Int.max (maxidx, maxt), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

671 
shyps = Sorts.union sorts shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

672 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

673 
tpairs = tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

674 
prop = Term.betapply (A, t)} 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

675 
 _ => raise THM ("forall_elim: not quantified", 0, [th])); 
0  676 

677 

1220  678 
(* Equality *) 
0  679 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

680 
(*Reflexivity 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

681 
t == t 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

682 
*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

683 
fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = 
16656  684 
Thm {thy_ref = thy_ref, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

685 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

686 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

687 
shyps = sorts, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

688 
hyps = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

689 
tpairs = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

690 
prop = Logic.mk_equals (t, t)}; 
0  691 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

692 
(*Symmetry 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

693 
t == u 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

694 
 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

695 
u == t 
1220  696 
*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

697 
fun symmetric (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

698 
(case prop of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

699 
(eq as Const ("==", Type (_, [T, _]))) $ t $ u => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

700 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

701 
der = Pt.infer_derivs' Pt.symmetric der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

702 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

703 
shyps = shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

704 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

705 
tpairs = tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

706 
prop = eq $ u $ t} 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

707 
 _ => raise THM ("symmetric", 0, [th])); 
0  708 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

709 
(*Transitivity 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

710 
t1 == u u == t2 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

711 
 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

712 
t1 == t2 
1220  713 
*) 
0  714 
fun transitive th1 th2 = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

715 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

716 
val Thm {der = der1, maxidx = max1, hyps = hyps1, shyps = shyps1, tpairs = tpairs1, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

717 
prop = prop1, ...} = th1 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

718 
and Thm {der = der2, maxidx = max2, hyps = hyps2, shyps = shyps2, tpairs = tpairs2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

719 
prop = prop2, ...} = th2; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

720 
fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

721 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

722 
case (prop1, prop2) of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

723 
((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

724 
if not (u aconv u') then err "middle term" 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

725 
else 
16656  726 
Thm {thy_ref = merge_thys2 th1 th2, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

727 
der = Pt.infer_derivs (Pt.transitive u T) der1 der2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

728 
maxidx = Int.max (max1, max2), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

729 
shyps = Sorts.union shyps1 shyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

730 
hyps = union_hyps hyps1 hyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

731 
tpairs = union_tpairs tpairs1 tpairs2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

732 
prop = eq $ t1 $ t2} 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

733 
 _ => err "premises" 
0  734 
end; 
735 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

736 
(*Betaconversion 
16656  737 
(%x. t)(u) == t[u/x] 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

738 
fully betareduces the term if full = true 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

739 
*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

740 
fun beta_conversion full (Cterm {thy_ref, t, T, maxidx, sorts}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

741 
let val t' = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

742 
if full then Envir.beta_norm t 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

743 
else 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

744 
(case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

745 
 _ => raise THM ("beta_conversion: not a redex", 0, [])); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

746 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

747 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

748 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

749 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

750 
shyps = sorts, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

751 
hyps = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

752 
tpairs = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

753 
prop = Logic.mk_equals (t, t')} 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

754 
end; 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

755 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

756 
fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

757 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

758 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

759 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

760 
shyps = sorts, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

761 
hyps = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

762 
tpairs = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

763 
prop = Logic.mk_equals (t, Pattern.eta_contract t)}; 
0  764 

765 
(*The abstraction rule. The Free or Var x must not be free in the hypotheses. 

766 
The bound variable will be named "a" (since x will be something like x320) 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

767 
t == u 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

768 
 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

769 
%x. t == %x. u 
1220  770 
*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

771 
fun abstract_rule a 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

772 
(Cterm {t = x, T, sorts, ...}) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

773 
(th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

774 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

775 
val (t, u) = Logic.dest_equals prop 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

776 
handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

777 
val result = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

778 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

779 
der = Pt.infer_derivs' (Pt.abstract_rule x a) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

780 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

781 
shyps = Sorts.union sorts shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

782 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

783 
tpairs = tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

784 
prop = Logic.mk_equals 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

785 
(Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))}; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

786 
fun check_occs x ts = 
16847
8fc160b12e73
invoke_oracle: do not keep theory value, but theory_ref;
wenzelm
parents:
16725
diff
changeset

787 
if exists (fn t => Logic.occs (x, t)) ts then 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

788 
raise THM ("abstract_rule: variable free in assumptions", 0, [th]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

789 
else (); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

790 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

791 
case x of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

792 
Free _ => (check_occs x hyps; check_occs x (terms_of_tpairs tpairs); result) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

793 
 Var _ => (check_occs x (terms_of_tpairs tpairs); result) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

794 
 _ => raise THM ("abstract_rule: not a variable", 0, [th]) 
0  795 
end; 
796 

797 
(*The combination rule 

3529  798 
f == g t == u 
799 
 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

800 
f t == g u 
1220  801 
*) 
0  802 
fun combination th1 th2 = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

803 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

804 
val Thm {der = der1, maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

805 
prop = prop1, ...} = th1 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

806 
and Thm {der = der2, maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

807 
prop = prop2, ...} = th2; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

808 
fun chktypes fT tT = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

809 
(case fT of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

810 
Type ("fun", [T1, T2]) => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

811 
if T1 <> tT then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

812 
raise THM ("combination: types", 0, [th1, th2]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

813 
else () 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

814 
 _ => raise THM ("combination: not function type", 0, [th1, th2])); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

815 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

816 
case (prop1, prop2) of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

817 
(Const ("==", Type ("fun", [fT, _])) $ f $ g, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

818 
Const ("==", Type ("fun", [tT, _])) $ t $ u) => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

819 
(chktypes fT tT; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

820 
Thm {thy_ref = merge_thys2 th1 th2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

821 
der = Pt.infer_derivs (Pt.combination f g t u fT) der1 der2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

822 
maxidx = Int.max (max1, max2), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

823 
shyps = Sorts.union shyps1 shyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

824 
hyps = union_hyps hyps1 hyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

825 
tpairs = union_tpairs tpairs1 tpairs2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

826 
prop = Logic.mk_equals (f $ t, g $ u)}) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

827 
 _ => raise THM ("combination: premises", 0, [th1, th2]) 
0  828 
end; 
829 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

830 
(*Equality introduction 
3529  831 
A ==> B B ==> A 
832 
 

833 
A == B 

1220  834 
*) 
0  835 
fun equal_intr th1 th2 = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

836 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

837 
val Thm {der = der1, maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

838 
prop = prop1, ...} = th1 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

839 
and Thm {der = der2, maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

840 
prop = prop2, ...} = th2; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

841 
fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

842 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

843 
case (prop1, prop2) of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

844 
(Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

845 
if A aconv A' andalso B aconv B' then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

846 
Thm {thy_ref = merge_thys2 th1 th2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

847 
der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

848 
maxidx = Int.max (max1, max2), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

849 
shyps = Sorts.union shyps1 shyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

850 
hyps = union_hyps hyps1 hyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

851 
tpairs = union_tpairs tpairs1 tpairs2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

852 
prop = Logic.mk_equals (A, B)} 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

853 
else err "not equal" 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

854 
 _ => err "premises" 
1529  855 
end; 
856 

857 
(*The equal propositions rule 

3529  858 
A == B A 
1529  859 
 
860 
B 

861 
*) 

862 
fun equal_elim th1 th2 = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

863 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

864 
val Thm {der = der1, maxidx = max1, shyps = shyps1, hyps = hyps1, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

865 
tpairs = tpairs1, prop = prop1, ...} = th1 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

866 
and Thm {der = der2, maxidx = max2, shyps = shyps2, hyps = hyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

867 
tpairs = tpairs2, prop = prop2, ...} = th2; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

868 
fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

869 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

870 
case prop1 of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

871 
Const ("==", _) $ A $ B => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

872 
if prop2 aconv A then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

873 
Thm {thy_ref = merge_thys2 th1 th2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

874 
der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

875 
maxidx = Int.max (max1, max2), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

876 
shyps = Sorts.union shyps1 shyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

877 
hyps = union_hyps hyps1 hyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

878 
tpairs = union_tpairs tpairs1 tpairs2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

879 
prop = B} 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

880 
else err "not equal" 
1529  881 
 _ => err"major premise" 
882 
end; 

0  883 

1220  884 

885 

0  886 
(**** Derived rules ****) 
887 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

888 
(*Smash unifies the list of term pairs leaving no flexflex pairs. 
250  889 
Instantiates the theorem and deletes trivial tpairs. 
0  890 
Resulting sequence may contain multiple elements if the tpairs are 
891 
not all flexflex. *) 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

892 
fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

893 
Unify.smash_unifiers (Theory.deref thy_ref, Envir.empty maxidx, tpairs) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

894 
> Seq.map (fn env => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

895 
if Envir.is_empty env then th 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

896 
else 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

897 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

898 
val tpairs' = tpairs > map (pairself (Envir.norm_term env)) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

899 
(*remove trivial tpairs, of the form t==t*) 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

900 
> filter_out (op aconv); 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

901 
val prop' = Envir.norm_term env prop; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

902 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

903 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

904 
der = Pt.infer_derivs' (Pt.norm_proof' env) der, 
16711  905 
maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'), 
16656  906 
shyps = may_insert_env_sorts (Theory.deref thy_ref) env shyps, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

907 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

908 
tpairs = tpairs', 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

909 
prop = prop'} 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

910 
end); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

911 

0  912 

913 
(*Instantiation of Vars 

16656  914 
A 
915 
 

916 
A[t1/v1, ..., tn/vn] 

1220  917 
*) 
0  918 

6928  919 
local 
920 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

921 
fun pretty_typing thy t T = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

922 
Pretty.block [Sign.pretty_term thy t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ thy T]; 
15797  923 

16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

924 
fun add_inst (ct, cu) (thy_ref, sorts) = 
6928  925 
let 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

926 
val Cterm {t = t, T = T, ...} = ct 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

927 
and Cterm {t = u, T = U, sorts = sorts_u, ...} = cu; 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

928 
val thy_ref' = Theory.merge_refs (thy_ref, merge_thys0 ct cu); 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

929 
val sorts' = Sorts.union sorts_u sorts; 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

930 
in 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

931 
(case t of Var v => 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

932 
if T = U then ((v, u), (thy_ref', sorts')) 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

933 
else raise TYPE (Pretty.string_of (Pretty.block 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

934 
[Pretty.str "instantiate: type conflict", 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

935 
Pretty.fbrk, pretty_typing (Theory.deref thy_ref') t T, 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

936 
Pretty.fbrk, pretty_typing (Theory.deref thy_ref') u U]), [T, U], [t, u]) 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

937 
 _ => raise TYPE (Pretty.string_of (Pretty.block 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

938 
[Pretty.str "instantiate: not a variable", 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

939 
Pretty.fbrk, Sign.pretty_term (Theory.deref thy_ref') t]), [], [t])) 
0  940 
end; 
941 

16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

942 
fun add_instT (cT, cU) (thy_ref, sorts) = 
16656  943 
let 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

944 
val Ctyp {T, thy_ref = thy_ref1, ...} = cT 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

945 
and Ctyp {T = U, thy_ref = thy_ref2, sorts = sorts_U, ...} = cU; 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

946 
val thy_ref' = Theory.merge_refs (thy_ref, Theory.merge_refs (thy_ref1, thy_ref2)); 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

947 
val thy' = Theory.deref thy_ref'; 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

948 
val sorts' = Sorts.union sorts_U sorts; 
16656  949 
in 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

950 
(case T of TVar (v as (_, S)) => 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

951 
if Type.of_sort (Sign.tsig_of thy') (U, S) then ((v, U), (thy_ref', sorts')) 
16656  952 
else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy' S, [U], []) 
953 
 _ => raise TYPE (Pretty.string_of (Pretty.block 

15797  954 
[Pretty.str "instantiate: not a type variable", 
16656  955 
Pretty.fbrk, Sign.pretty_typ thy' T]), [T], [])) 
956 
end; 

0  957 

6928  958 
in 
959 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

960 
(*Lefttoright replacements: ctpairs = [..., (vi, ti), ...]. 
0  961 
Instantiates distinct Vars by terms of same type. 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

962 
Does NOT normalize the resulting theorem!*) 
1529  963 
fun instantiate ([], []) th = th 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

964 
 instantiate (instT, inst) th = 
16656  965 
let 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

966 
val Thm {thy_ref, der, hyps, shyps, tpairs, prop, ...} = th; 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

967 
val (inst', (instT', (thy_ref', shyps'))) = 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

968 
(thy_ref, shyps) > fold_map add_inst inst > fold_map add_instT instT; 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

969 
val subst = Term.instantiate (instT', inst'); 
16656  970 
val prop' = subst prop; 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

971 
val tpairs' = map (pairself subst) tpairs; 
16656  972 
in 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

973 
if has_duplicates (fn ((v, _), (v', _)) => Term.eq_var (v, v')) inst' then 
16656  974 
raise THM ("instantiate: variables not distinct", 0, [th]) 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

975 
else if has_duplicates (fn ((v, _), (v', _)) => Term.eq_tvar (v, v')) instT' then 
16656  976 
raise THM ("instantiate: type variables not distinct", 0, [th]) 
977 
else 

16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

978 
Thm {thy_ref = thy_ref', 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

979 
der = Pt.infer_derivs' (Pt.instantiate (instT', inst')) der, 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

980 
maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'), 
16656  981 
shyps = shyps', 
982 
hyps = hyps, 

16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

983 
tpairs = tpairs', 
16656  984 
prop = prop'} 
985 
end 

986 
handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); 

6928  987 

988 
end; 

989 

0  990 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

991 
(*The trivial implication A ==> A, justified by assume and forall rules. 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

992 
A can contain Vars, not so for assume!*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

993 
fun trivial (Cterm {thy_ref, t =A, T, maxidx, sorts}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

994 
if T <> propT then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

995 
raise THM ("trivial: the term must have type prop", 0, []) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

996 
else 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

997 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

998 
der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

999 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1000 
shyps = sorts, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1001 
hyps = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1002 
tpairs = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1003 
prop = implies $ A $ A}; 
0  1004 

1503  1005 
(*Axiomscheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1006 
fun class_triv thy c = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1007 
let val Cterm {thy_ref, t, maxidx, sorts, ...} = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1008 
cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) 
6368  1009 
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

1010 
in 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1011 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1012 
der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1013 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1014 
shyps = sorts, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1015 
hyps = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1016 
tpairs = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1017 
prop = t} 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

1018 
end; 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

1019 

86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

1020 

6786  1021 
(* Replace all TFrees not fixed or in the hyps by new TVars *) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1022 
fun varifyT' fixed (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
12500  1023 
let 
15797  1024 
val tfrees = foldr add_term_tfrees fixed hyps; 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1025 
val prop1 = attach_tpairs tpairs prop; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1026 
val (prop2, al) = Type.varify (prop1, tfrees); 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1027 
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1028 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1029 
(Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1030 
der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1031 
maxidx = Int.max (0, maxidx), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1032 
shyps = shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1033 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1034 
tpairs = rev (map Logic.dest_equals ts), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1035 
prop = prop3}, al) 
0  1036 
end; 
1037 

12500  1038 
val varifyT = #1 o varifyT' []; 
6786  1039 

0  1040 
(* Replace all TVars by new TFrees *) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1041 
fun freezeT (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1042 
let 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1043 
val prop1 = attach_tpairs tpairs prop; 
16287  1044 
val prop2 = Type.freeze prop1; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1045 
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1046 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1047 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1048 
der = Pt.infer_derivs' (Pt.freezeT prop1) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1049 
maxidx = maxidx_of_term prop2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1050 
shyps = shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1051 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1052 
tpairs = rev (map Logic.dest_equals ts), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1053 
prop = prop3} 
1220  1054 
end; 
0  1055 

1056 

1057 
(*** Inference rules for tactics ***) 

1058 

1059 
(*Destruct proof state into constraints, other goals, goal(i), rest *) 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1060 
fun dest_state (state as Thm{prop,tpairs,...}, i) = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1061 
(case Logic.strip_prems(i, [], prop) of 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1062 
(B::rBs, C) => (tpairs, rev rBs, B, C) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1063 
 _ => raise THM("dest_state", i, [state])) 
0  1064 
handle TERM _ => raise THM("dest_state", i, [state]); 
1065 

309  1066 
(*Increment variables and parameters of orule as required for 
0  1067 
resolution with goal i of state. *) 
1068 
fun lift_rule (state, i) orule = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1069 
let 
16679  1070 
val Thm {shyps = sshyps, prop = sprop, maxidx = smax, ...} = state; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1071 
val (Bi :: _, _) = Logic.strip_prems (i, [], sprop) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1072 
handle TERM _ => raise THM ("lift_rule", i, [orule, state]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1073 
val (lift_abs, lift_all) = Logic.lift_fns (Bi, smax + 1); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1074 
val (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = orule; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1075 
val (As, B) = Logic.strip_horn prop; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1076 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1077 
Thm {thy_ref = merge_thys2 state orule, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1078 
der = Pt.infer_derivs' (Pt.lift_proof Bi (smax + 1) prop) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1079 
maxidx = maxidx + smax + 1, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1080 
shyps = Sorts.union sshyps shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1081 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1082 
tpairs = map (pairself lift_abs) tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1083 
prop = Logic.list_implies (map lift_all As, lift_all B)} 
0  1084 
end; 
1085 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1086 
fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1087 
if i < 0 then raise THM ("negative increment", 0, [thm]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1088 
else if i = 0 then thm 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1089 
else 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1090 
Thm {thy_ref = thy_ref, 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1091 
der = Pt.infer_derivs' 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1092 
(Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1093 
maxidx = maxidx + i, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1094 
shyps = shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1095 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1096 
tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1097 
prop = Logic.incr_indexes ([], i) prop}; 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1098 

0  1099 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) 
1100 
fun assumption i state = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1101 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1102 
val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = state; 
16656  1103 
val thy = Theory.deref thy_ref; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1104 
val (tpairs, Bs, Bi, C) = dest_state (state, i); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1105 
fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1106 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1107 
der = Pt.infer_derivs' 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1108 
((if Envir.is_empty env then I else (Pt.norm_proof' env)) o 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1109 
Pt.assumption_proof Bs Bi n) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1110 
maxidx = maxidx, 
16656  1111 
shyps = may_insert_env_sorts thy env shyps, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1112 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1113 
tpairs = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1114 
if Envir.is_empty env then tpairs 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1115 
else map (pairself (Envir.norm_term env)) tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1116 
prop = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1117 
if Envir.is_empty env then (*avoid wasted normalizations*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1118 
Logic.list_implies (Bs, C) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1119 
else (*normalize the new rule fully*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1120 
Envir.norm_term env (Logic.list_implies (Bs, C))}; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1121 
fun addprfs [] _ = Seq.empty 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1122 
 addprfs ((t, u) :: apairs) n = Seq.make (fn () => Seq.pull 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1123 
(Seq.mapp (newth n) 
16656  1124 
(Unify.unifiers (thy, Envir.empty maxidx, (t, u) :: tpairs)) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1125 
(addprfs apairs (n + 1)))) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1126 
in addprfs (Logic.assum_pairs (~1, Bi)) 1 end; 
0  1127 

250  1128 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. 
0  1129 
Checks if Bi's conclusion is alphaconvertible to one of its assumptions*) 
1130 
fun eq_assumption i state = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1131 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1132 
val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = state; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1133 
val (tpairs, Bs, Bi, C) = dest_state (state, i); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1134 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1135 
(case find_index (op aconv) (Logic.assum_pairs (~1, Bi)) of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1136 
~1 => raise THM ("eq_assumption", 0, [state]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1137 
 n => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1138 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1139 
der = Pt.infer_derivs' (Pt.assumption_proof Bs Bi (n + 1)) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1140 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1141 
shyps = shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1142 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1143 
tpairs = tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1144 
prop = Logic.list_implies (Bs, C)}) 
0  1145 
end; 
1146 

1147 

2671  1148 
(*For rotate_tac: fast rotation of assumptions of subgoal i*) 
1149 
fun rotate_rule k i state = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1150 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1151 
val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = state; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1152 
val (tpairs, Bs, Bi, C) = dest_state (state, i); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1153 
val params = Term.strip_all_vars Bi 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1154 
and rest = Term.strip_all_body Bi; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1155 
val asms = Logic.strip_imp_prems rest 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1156 
and concl = Logic.strip_imp_concl rest; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1157 
val n = length asms; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1158 
val m = if k < 0 then n + k else k; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1159 
val Bi' = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1160 
if 0 = m orelse m = n then Bi 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1161 
else if 0 < m andalso m < n then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1162 
let val (ps, qs) = splitAt (m, asms) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1163 
in list_all (params, Logic.list_implies (qs @ ps, concl)) end 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1164 
else raise THM ("rotate_rule", k, [state]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1165 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1166 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1167 
der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1168 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1169 
shyps = shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1170 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1171 
tpairs = tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1172 
prop = Logic.list_implies (Bs @ [Bi'], C)} 
2671  1173 
end; 
1174 

1175 

7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1176 
(*Rotates a rule's premises to the left by k, leaving the first j premises 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1177 
unchanged. Does nothing if k=0 or if k equals nj, where n is the 
16656  1178 
number of premises. Useful with etac and underlies defer_tac*) 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1179 
fun permute_prems j k rl = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1180 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1181 
val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = rl; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1182 
val prems = Logic.strip_imp_prems prop 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1183 
and concl = Logic.strip_imp_concl prop; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1184 
val moved_prems = List.drop (prems, j) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1185 
and fixed_prems = List.take (prems, j) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1186 
handle Subscript => raise THM ("permute_prems: j", j, [rl]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1187 
val n_j = length moved_prems; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1188 
val m = if k < 0 then n_j + k else k; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1189 
val prop' = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1190 
if 0 = m orelse m = n_j then prop 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1191 
else if 0 < m andalso m < n_j then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1192 
let val (ps, qs) = splitAt (m, moved_prems) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1193 
in Logic.list_implies (fixed_prems @ qs @ ps, concl) end 
16725  1194 
else raise THM ("permute_prems: k", k, [rl]); 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1195 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1196 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1197 
der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1198 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1199 
shyps = shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1200 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1201 
tpairs = tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1202 
prop = prop'} 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1203 
end; 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1204 

322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1205 

0  1206 
(** User renaming of parameters in a subgoal **) 
1207 

1208 
(*Calls error rather than raising an exception because it is intended 

1209 
for toplevel use  exception handling would not make sense here. 

1210 
The names in cs, if distinct, are used for the innermost parameters; 

1211 
preceding parameters may be renamed to make all params distinct.*) 

1212 
fun rename_params_rule (cs, i) state = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1213 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1214 
val Thm {thy_ref, der, maxidx, shyps, hyps, ...} = state; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1215 
val (tpairs, Bs, Bi, C) = dest_state (state, i); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1216 
val iparams = map #1 (Logic.strip_params Bi); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1217 
val short = length iparams  length cs; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1218 
val newnames = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1219 
if short < 0 then error "More names than abstractions!" 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1220 
else variantlist (Library.take (short, iparams), cs) @ cs; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1221 
val freenames = map (#1 o dest_Free) (term_frees Bi); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1222 
val newBi = Logic.list_rename_params (newnames, Bi); 
250  1223 
in 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1224 
case findrep cs of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1225 
c :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ c); state) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1226 
 [] => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1227 
(case cs inter_string freenames of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1228 
a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); state) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1229 
 [] => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1230 
Thm {thy_ref = thy_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1231 
der = der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1232 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1233 
shyps = shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1234 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1235 
tpairs = tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1236 
prop = Logic.list_implies (Bs @ [newBi], C)}) 
0  1237 
end; 
1238 

12982  1239 

0  1240 
(*** Preservation of bound variable names ***) 
1241 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1242 
fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
12982  1243 
(case Term.rename_abs pat obj prop of 
15531  1244 
NONE => thm 
1245 
 SOME prop' => Thm 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1246 
{thy_ref = thy_ref, 
12982  1247 
der = der, 
1248 
maxidx = maxidx, 

1249 
hyps = hyps, 

1250 
shyps = shyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1251 
tpairs = tpairs, 
12982  1252 
prop = prop'}); 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1253 

0  1254 

16656  1255 
(* strip_apply f (A, B) strips off all assumptions/parameters from A 
0  1256 
introduced by lifting over B, and applies f to remaining part of A*) 
1257 
fun strip_apply f = 

1258 
let fun strip(Const("==>",_)$ A1 $ B1, 

250  1259 
Const("==>",_)$ _ $ B2) = implies $ A1 $ strip(B1,B2) 
1260 
 strip((c as Const("all",_)) $ Abs(a,T,t1), 

1261 
Const("all",_) $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2)) 

1262 
 strip(A,_) = f A 

0  1263 
in strip end; 
1264 

1265 
(*Use the alist to rename all bound variables and some unknowns in a term 

1266 
dpairs = current disagreement pairs; tpairs = permanent ones (flexflex); 

1267 
Preserves unknowns in tpairs and on lhs of dpairs. *) 

1268 
fun rename_bvs([],_,_,_) = I 

1269 
 rename_bvs(al,dpairs,tpairs,B) = 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

1270 
let val vars = foldr add_term_vars [] 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

1271 
(map fst dpairs @ map fst tpairs @ map snd tpairs) 
250  1272 
(*unknowns appearing elsewhere be preserved!*) 
1273 
val vids = map (#1 o #1 o dest_Var) vars; 

1274 
fun rename(t as Var((x,i),T)) = 

1275 
(case assoc(al,x) of 

15531  1276 
SOME(y) => if x mem_string vids orelse y mem_string vids then t 
250  1277 
else Var((y,i),T) 
15531  1278 
 NONE=> t) 
0  1279 
 rename(Abs(x,T,t)) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1280 
Abs (if_none (assoc_string (al, x)) x, T, rename t) 
0  1281 
 rename(f$t) = rename f $ rename t 
1282 
 rename(t) = t; 

250  1283 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1284 
in strip_ren end; 
1285 

1286 
(*Function to rename bounds/unknowns in the argument, lifted over B*) 

1287 
fun rename_bvars(dpairs, tpairs, B) = 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

1288 
rename_bvs(foldr Term.match_bvars [] dpairs, dpairs, tpairs, B); 
0  1289 

1290 

1291 
(*** RESOLUTION ***) 

1292 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1293 
(** Lifting optimizations **) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1294 

0  1295 
(*strip off pairs of assumptions/parameters in parallel  they are 
1296 
identical because of lifting*) 

250  1297 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1298 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1299 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1300 
Const("all",_)$Abs(_,_,t2)) = 
0  1301 
let val (B1,B2) = strip_assums2 (t1,t2) 
1302 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1303 
 strip_assums2 BB = BB; 

1304 

1305 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1306 
(*Faster normalization: skip assumptions that were lifted over*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1307 
fun norm_term_skip env 0 t = Envir.norm_term env t 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1308 
 norm_term_skip env n (Const("all",_)$Abs(a,T,t)) = 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1309 
let val Envir.Envir{iTs, ...} = env 
15797  1310 
val T' = Envir.typ_subst_TVars iTs T 
1238  1311 
(*Must instantiate types of parameters because they are flattened; 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1312 
this could be a NEW parameter*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1313 
in all T' $ Abs(a, T', norm_term_skip env n t) end 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1314 
 norm_term_skip env n (Const("==>", _) $ A $ B) = 
1238  1315 
implies $ A $ norm_term_skip env (n1) B 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1316 
 norm_term_skip env n t = error"norm_term_skip: too few assumptions??"; 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1317 

479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1318 

0  1319 
(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) 
250  1320 
Unifies B with Bi, replacing subgoal i (1 <= i <= n) 
0  1321 
If match then forbid instantiations in proof state 
1322 
If lifted then shorten the dpair using strip_assums2. 

1323 
If eres_flg then simultaneously proves A1 by assumption. 

250  1324 
nsubgoal is the number of new subgoals (written m above). 
0  1325 
Curried so that resolution calls dest_state only once. 
1326 
*) 

4270  1327 
local exception COMPOSE 
0  1328 
in 
250  1329 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1330 
(eres_flg, orule, nsubgoal) = 
1529  1331 
let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1332 
and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1333 
tpairs=rtpairs, prop=rprop,...} = orule 
1529  1334 
(*How many hyps to skip over during normalization*) 
1238  1335 
and nlift = Logic.count_prems(strip_all_body Bi, 
1336 
if eres_flg then ~1 else 0) 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1337 
val thy_ref = merge_thys2 state orule; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1338 
val thy = Theory.deref thy_ref; 
0 