author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18501  915105af2e80 
child 18733  0508c8017839 
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 
18145  86 
val cprem_of: thm > int > cterm 
16656  87 
val transfer: theory > thm > thm 
16945  88 
val weaken: cterm > thm > thm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

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

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

95 
val axioms_of: theory > (string * thm) list 
1160  96 

97 
(*meta rules*) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

125 
val permute_prems: int > int > thm > thm 
1160  126 
val rename_params_rule: string list * int > thm > thm 
18501
915105af2e80
turned bicompose_no_flatten into compose_no_flatten, without elimination;
wenzelm
parents:
18486
diff
changeset

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

128 
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

129 
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

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

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

6089  134 
signature THM = 
135 
sig 

136 
include BASIC_THM 

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

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

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

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

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

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

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

143 
val no_prems: thm > bool 
17345  144 
val no_attributes: 'a > 'a * 'b list 
145 
val simple_fact: 'a > ('a * 'b list) list 

18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18184
diff
changeset

146 
val apply_attributes: 'a attribute list > 'a * thm > 'a * thm 
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18184
diff
changeset

147 
val applys_attributes: 'a attribute list > 'a * thm list > 'a * thm list 
16945  148 
val terms_of_tpairs: (term * term) list > term list 
149 
val full_prop_of: thm > term 

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

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

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

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

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

154 
val name_thm: string * thm > thm 
16945  155 
val compress: thm > thm 
156 
val adjust_maxidx_thm: thm > thm 

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

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

158 
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

159 
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

160 
val cterm_incr_indexes: int > cterm > cterm 
6089  161 
end; 
162 

3550  163 
structure Thm: THM = 
0  164 
struct 
250  165 

16656  166 

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

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

168 

16656  169 
(** collect occurrences of sorts  unless all sorts nonempty **) 
170 

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

16656  173 

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

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

176 
if Sign.all_sorts_nonempty thy then I 

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

178 

179 

180 

250  181 
(** certified types **) 
182 

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

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

186 
let val thy = Theory.deref thy_ref 
16656  187 
in {thy = thy, sign = thy, T = T, sorts = sorts} end; 
250  188 

16656  189 
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

190 

250  191 
fun typ_of (Ctyp {T, ...}) = T; 
192 

16656  193 
fun ctyp_of thy raw_T = 
194 
let val T = Sign.certify_typ thy raw_T 

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

250  196 

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

197 
fun read_ctyp thy s = 
16656  198 
let val T = Sign.read_typ (thy, K NONE) s 
199 
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

200 

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

16679  203 
 dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); 
15087  204 

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

205 

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

206 

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

208 

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

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

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

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

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

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

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

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

216 

16679  217 
exception CTERM of string; 
218 

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

219 
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

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

221 
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

222 

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

223 
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

224 
let val thy = Theory.deref thy_ref in 
16656  225 
{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

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

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

228 

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

229 
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

230 
val sign_of_cterm = theory_of_cterm; 
9461  231 

250  232 
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

233 

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

2671  236 

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

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

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

239 
val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm; 
16656  240 
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

241 
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

242 

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

245 

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

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

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

250 
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

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

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

253 

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

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

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

258 
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

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

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

261 

2147  262 
(*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

263 
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

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

265 
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

266 

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

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

268 
fun capply 
16656  269 
(cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...}) 
270 
(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

271 
if T = dty then 
16656  272 
Cterm {thy_ref = merge_thys0 cf cx, 
273 
t = f $ x, 

274 
T = rty, 

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

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

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

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

278 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  279 

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

280 
fun cabs 
16656  281 
(ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...}) 
282 
(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

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

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

287 
sorts = Sorts.union sorts1 sorts2} 

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

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

289 

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

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

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

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

294 
let 
16656  295 
val thy_ref = merge_thys0 ct1 ct2; 
18184  296 
val (Tinsts, tinsts) = match (Theory.deref thy_ref) (t1, t2) (Vartab.empty, Vartab.empty); 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

298 
val sorts = Sorts.union sorts1 sorts2; 
16656  299 
fun mk_cTinst (ixn, (S, T)) = 
300 
(Ctyp {T = TVar (ixn, S), thy_ref = thy_ref, sorts = sorts}, 

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

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

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

303 
let val T = Envir.typ_subst_TVars Tinsts T in 
16656  304 
(Cterm {t = Var (ixn, T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, 
305 
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

306 
end; 
16656  307 
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

308 

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

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

310 
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

311 

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

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

313 
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

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

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

316 
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

317 
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

318 

2509  319 

320 

574  321 
(** read cterms **) (*exception ERROR*) 
250  322 

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

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

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

326 
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

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

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

331 

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

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

333 
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

334 
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

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

336 

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

337 
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

338 

250  339 

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

342 

2509  343 

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

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

345 

11518  346 
structure Pt = Proofterm; 
347 

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

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

351 
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

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

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

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

355 
prop: term}; (*conclusion*) 
0  356 

16725  357 
(*errors involving theorems*) 
358 
exception THM of string * int * thm list; 

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

359 

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

360 
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

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

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

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

364 
end; 
0  365 

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

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

367 
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

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

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

370 
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

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

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

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

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

375 
prop = cterm maxidx prop} 
1517  376 
end; 
377 

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

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

381 
val union_tpairs = gen_merge_lists eq_tpairs; 

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

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

384 
fun attach_tpairs tpairs prop = 

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

386 

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

16945  388 

389 

390 
(* merge theories of cterms/thms; raise exception if incompatible *) 

391 

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

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

394 

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

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

397 

0  398 

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

399 
(*attributes subsume any kind of rules or context modifiers*) 
6089  400 
type 'a attribute = 'a * thm > 'a * thm; 
17708  401 

6089  402 
fun no_attributes x = (x, []); 
17345  403 
fun simple_fact x = [(x, [])]; 
18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18184
diff
changeset

404 
val apply_attributes = Library.apply; 
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18184
diff
changeset

405 
fun applys_attributes atts = foldl_map (Library.apply atts); 
6089  406 

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

407 

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

409 

16945  410 
val insert_hyps = OrdList.insert Term.fast_term_ord; 
16679  411 
val remove_hyps = OrdList.remove Term.fast_term_ord; 
412 
val union_hyps = OrdList.union Term.fast_term_ord; 

413 
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

414 

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

415 

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

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

417 

3994  418 
fun eq_thm (th1, th2) = 
419 
let 

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

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

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

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

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

427 
eq_set_hyps (hyps1, hyps2) andalso 
16656  428 
equal_lists eq_tpairs (tpairs1, tpairs2) andalso 
3994  429 
prop1 aconv prop2 
430 
end; 

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

431 

16135  432 
val eq_thms = Library.equal_lists eq_thm; 
433 

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

434 
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

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

436 

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

439 
fun tpairs_of (Thm {tpairs, ...}) = tpairs; 
0  440 

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

441 
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

442 
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

443 
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

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

445 

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

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

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

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

449 
 [] => 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

450 

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

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

452 
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

453 
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

454 

18145  455 
fun cprem_of (th as Thm {thy_ref, maxidx, shyps, prop, ...}) i = 
18035  456 
Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, sorts = shyps, 
18145  457 
t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])}; 
18035  458 

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

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

462 
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

463 
val thy = Theory.deref thy_ref; 
3895  464 
in 
16945  465 
if not (subthy (thy, thy')) then 
466 
raise THM ("transfer: not a super theory", 0, [thm]) 

467 
else if eq_thy (thy, thy') then thm 

468 
else 

469 
Thm {thy_ref = Theory.self_ref thy', 

470 
der = der, 

471 
maxidx = maxidx, 

472 
shyps = shyps, 

473 
hyps = hyps, 

474 
tpairs = tpairs, 

475 
prop = prop} 

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

477 

16945  478 
(*explicit weakening: maps  B to A  B*) 
479 
fun weaken raw_ct th = 

480 
let 

481 
val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx raw_ct; 

482 
val Thm {der, maxidx, shyps, hyps, tpairs, prop, ...} = th; 

483 
in 

484 
if T <> propT then 

485 
raise THM ("weaken: assumptions must have type prop", 0, []) 

486 
else if maxidxA <> ~1 then 

487 
raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, []) 

488 
else 

489 
Thm {thy_ref = merge_thys1 ct th, 

490 
der = der, 

491 
maxidx = maxidx, 

492 
shyps = Sorts.union sorts shyps, 

493 
hyps = insert_hyps A hyps, 

494 
tpairs = tpairs, 

495 
prop = prop} 

496 
end; 

16656  497 

498 

0  499 

1238  500 
(** sort contexts of theorems **) 
501 

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

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

1238  505 

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

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

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

510 
val thy = Theory.deref thy_ref; 
16656  511 
val shyps' = 
512 
if Sign.all_sorts_nonempty thy then [] 

513 
else 

514 
let 

515 
val present = present_sorts thm; 

516 
val extra = Sorts.subtract present shyps; 

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

518 
in Sorts.subtract witnessed shyps end; 

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

520 
Thm {thy_ref = thy_ref, der = der, maxidx = maxidx, 
16656  521 
shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop} 
7642  522 
end; 
1238  523 

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

526 

1238  527 

528 

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

530 

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

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

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

534 
fun get_ax thy = 
17412  535 
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

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

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

538 
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

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

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

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

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

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

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

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

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

549 

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

551 
get_axiom_i thy o NameSpace.intern (Theory.axiom_space thy); 
15672  552 

6368  553 
fun def_name name = name ^ "_def"; 
554 
fun get_def thy = get_axiom thy o def_name; 

4847  555 

1529  556 

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

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

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

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

561 

6089  562 

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

564 

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

4018  567 

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

568 
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

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

570 
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

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

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

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

575 
val name_of_thm = #1 o get_name_tags; 

576 
val tags_of_thm = #2 o get_name_tags; 

577 

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

0  579 

580 

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

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

583 
fun compress (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
16991  584 
let val thy = Theory.deref thy_ref in 
585 
Thm {thy_ref = thy_ref, 

586 
der = der, 

587 
maxidx = maxidx, 

588 
shyps = shyps, 

589 
hyps = map (Compress.term thy) hyps, 

590 
tpairs = map (pairself (Compress.term thy)) tpairs, 

591 
prop = Compress.term thy prop} 

592 
end; 

16945  593 

594 
fun adjust_maxidx_thm (Thm {thy_ref, der, shyps, hyps, tpairs, prop, ...}) = 

595 
Thm {thy_ref = thy_ref, 

596 
der = der, 

597 
maxidx = maxidx_tpairs tpairs (maxidx_of_term prop), 

598 
shyps = shyps, 

599 
hyps = hyps, 

600 
tpairs = tpairs, 

601 
prop = prop}; 

564  602 

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

603 

2509  604 

1529  605 
(*** Meta rules ***) 
0  606 

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

607 
(** primitive rules **) 
0  608 

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

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

611 
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

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

613 
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

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

615 
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

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

617 
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

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

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

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

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

622 
prop = prop} 
0  623 
end; 
624 

1220  625 
(*Implication introduction 
3529  626 
[A] 
627 
: 

628 
B 

1220  629 
 
630 
A ==> B 

631 
*) 

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

632 
fun implies_intr 
16679  633 
(ct as Cterm {t = A, T, maxidx = maxidxA, sorts, ...}) 
634 
(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

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

636 
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

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

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

639 
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

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

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

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

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

644 
prop = implies $ A $ prop}; 
0  645 

1529  646 

1220  647 
(*Implication elimination 
648 
A ==> B A 

649 
 

650 
B 

651 
*) 

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

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

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

654 
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

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

656 
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

657 
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

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

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

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

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

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

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

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

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

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

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

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

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

671 
end; 
250  672 

1220  673 
(*Forall introduction. The Free or Var x must not be free in the hypotheses. 
16656  674 
[x] 
675 
: 

676 
A 

677 
 

678 
!!x. A 

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

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

681 
(ct as Cterm {t = x, T, sorts, ...}) 
16679  682 
(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

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

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

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

686 
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

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

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

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

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

691 
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

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

693 
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

694 
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

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

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

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

698 
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

699 
 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

700 
 _ => raise THM ("forall_intr: not a variable", 0, [th]) 
0  701 
end; 
702 

1220  703 
(*Forall elimination 
16656  704 
!!x. A 
1220  705 
 
706 
A[t/x] 

707 
*) 

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

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

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

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

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

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

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

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

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

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

717 
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

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

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

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

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

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

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

725 

1220  726 
(* Equality *) 
0  727 

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

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

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

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

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

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

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

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

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

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

738 
prop = Logic.mk_equals (t, t)}; 
0  739 

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

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

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

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

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

745 
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

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

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

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

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

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

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

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

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

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

755 
 _ => raise THM ("symmetric", 0, [th])); 
0  756 

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

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

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

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

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

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

764 
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

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

766 
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

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

768 
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

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

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

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

772 
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

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

775 
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

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

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

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

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

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

781 
 _ => err "premises" 
0  782 
end; 
783 

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

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

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

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

788 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

803 

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

804 
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

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

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

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

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

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

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

811 
prop = Logic.mk_equals (t, Pattern.eta_contract t)}; 
0  812 

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

814 
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

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

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

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

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

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

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

822 
let 
17708  823 
val string_of = Sign.string_of_term (Theory.deref thy_ref); 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

825 
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

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

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

828 
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

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

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

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

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

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

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

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

836 
if exists (fn t => Logic.occs (x, t)) ts then 
17708  837 
raise THM ("abstract_rule: variable free in assumptions " ^ string_of x, 0, [th]) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

841 
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

842 
 Var _ => (check_occs x (terms_of_tpairs tpairs); result) 
17708  843 
 _ => raise THM ("abstract_rule: not a variable " ^ string_of x, 0, [th]) 
0  844 
end; 
845 

846 
(*The combination rule 

3529  847 
f == g t == u 
848 
 

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

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

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

853 
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

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

855 
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

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

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

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

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

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

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

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

863 
 _ => 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

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

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

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

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

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

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

870 
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

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

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

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

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

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

876 
 _ => raise THM ("combination: premises", 0, [th1, th2]) 
0  877 
end; 
878 

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

879 
(*Equality introduction 
3529  880 
A ==> B B ==> A 
881 
 

882 
A == B 

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

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

886 
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

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

888 
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

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

890 
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

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

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

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

894 
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

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

896 
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

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

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

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

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

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

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

903 
 _ => err "premises" 
1529  904 
end; 
905 

906 
(*The equal propositions rule 

3529  907 
A == B A 
1529  908 
 
909 
B 

910 
*) 

911 
fun equal_elim th1 th2 = 

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

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

913 
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

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

915 
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

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

917 
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

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

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

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

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

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

923 
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

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

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

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

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

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

929 
else err "not equal" 
1529  930 
 _ => err"major premise" 
931 
end; 

0  932 

1220  933 

934 

0  935 
(**** Derived rules ****) 
936 

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

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

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

941 
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

942 
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

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

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

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

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

947 
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

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

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

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

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

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

953 
der = Pt.infer_derivs' (Pt.norm_proof' env) der, 
16711  954 
maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'), 
16656  955 
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

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

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

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

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

960 

0  961 

962 
(*Instantiation of Vars 

16656  963 
A 
964 
 

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

1220  966 
*) 
0  967 

6928  968 
local 
969 

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

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

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

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

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

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

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

977 
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

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

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

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

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

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

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

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

985 
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

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

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

988 
Pretty.fbrk, Sign.pretty_term (Theory.deref thy_ref') t]), [], [t])) 
0  989 
end; 
990 

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

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

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

994 
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

995 
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

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

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

999 
(case T of TVar (v as (_, S)) => 
17203  1000 
if Sign.of_sort thy' (U, S) then ((v, U), (thy_ref', sorts')) 
16656  1001 
else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy' S, [U], []) 
1002 
 _ => raise TYPE (Pretty.string_of (Pretty.block 

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

0  1006 

6928  1007 
in 
1008 

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

1009 
(*Lefttoright replacements: ctpairs = [..., (vi, ti), ...]. 
0  1010 
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

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

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

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

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

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

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

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

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

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

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

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

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

1029 
maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'), 
16656  1030 
shyps = shyps', 
1031 
hyps = hyps, 

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

1032 
tpairs = tpairs', 
16656  1033 
prop = prop'} 
1034 
end 

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

6928  1036 

1037 
end; 

1038 

0  1039 

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

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

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

1042 
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

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

1044 
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

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

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

1047 
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

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

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

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

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

1052 
prop = implies $ A $ A}; 
0  1053 

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

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

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

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

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

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

1061 
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

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

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

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

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

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

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

1068 

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

1069 

6786  1070 
(* 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

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

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

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

1076 
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

1077 
in 
18127  1078 
(al, Thm {thy_ref = thy_ref, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1079 
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

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

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

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

1083 
tpairs = rev (map Logic.dest_equals ts), 
18127  1084 
prop = prop3}) 
0  1085 
end; 
1086 

18127  1087 
val varifyT = #2 o varifyT' []; 
6786  1088 

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

1090 
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

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

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

1094 
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

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

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

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

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

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

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

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

1102 
prop = prop3} 
1220  1103 
end; 
0  1104 

1105 

1106 
(*** Inference rules for tactics ***) 

1107 

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

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

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

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

1112 
 _ => raise THM("dest_state", i, [state])) 
0  1113 
handle TERM _ => raise THM("dest_state", i, [state]); 
1114 

309  1115 
(*Increment variables and parameters of orule as required for 
18035  1116 
resolution with a goal.*) 
1117 
fun lift_rule goal orule = 

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

1118 
let 
18035  1119 
val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal; 
1120 
val inc = gmax + 1; 

1121 
val lift_abs = Logic.lift_abs inc gprop; 

1122 
val lift_all = Logic.lift_all inc gprop; 

1123 
val Thm {der, maxidx, shyps, hyps, tpairs, prop, ...} = orule; 

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

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

1125 
in 
18035  1126 
if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, []) 
1127 
else 

1128 
Thm {thy_ref = merge_thys1 goal orule, 

1129 
der = Pt.infer_derivs' (Pt.lift_proof gprop inc prop) der, 

1130 
maxidx = maxidx + inc, 

1131 
shyps = Sorts.union shyps sorts, (*sic!*) 

1132 
hyps = hyps, 

1133 
tpairs = map (pairself lift_abs) tpairs, 

1134 
prop = Logic.list_implies (map lift_all As, lift_all B)} 

0  1135 
end; 
1136 

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

1137 
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

1138 
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

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

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

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

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

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

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

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

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

1147 
tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1148 
prop = Logic.incr_indexes ([], i) prop}; 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1149 

0  1150 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) 
1151 
fun assumption i state = 

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

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

1153 
val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = state; 
16656  1154 
val thy = Theory.deref thy_ref; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1155 
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

1156 
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

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

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

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

1160 
Pt.assumption_proof Bs Bi n) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1161 
maxidx = maxidx, 
16656  1162 
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

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

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

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

1166 
else map (pairself (Envir.norm_term env)) tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

1168 
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

1169 
Logic.list_implies (Bs, C) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1170 
else (*normalize the new rule fully*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1171 
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

1172 
fun addprfs [] _ = Seq.empty 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1173 
 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

1174 
(Seq.mapp (newth n) 
16656  1175 
(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

1176 
(addprfs apairs (n + 1)))) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1177 
in addprfs (Logic.assum_pairs (~1, Bi)) 1 end; 
0  1178 

250  1179 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. 
0  1180 
Checks if Bi's conclusion is alphaconvertible to one of its assumptions*) 
1181 
fun eq_assumption i state = 

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

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

1183 
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

1184 
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

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

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

1187 
~1 => raise THM ("eq_assumption", 0, [state]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

1190 
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

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

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

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

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

1195 
prop = Logic.list_implies (Bs, C)}) 
0  1196 
end; 
1197 

1198 

2671  1199 
(*For rotate_tac: fast rotation of assumptions of subgoal i*) 
1200 
fun rotate_rule k i state = 

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

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

1202 
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

1203 
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

1204 
val params = Term.strip_all_vars Bi 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1205 
and rest = Term.strip_all_body Bi; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1206 
val asms = Logic.strip_imp_prems rest 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1207 
and concl = Logic.strip_imp_concl rest; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1208 
val n = length asms; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1209 
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

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

1211 
if 0 = m orelse m = n then Bi 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1212 
else if 0 < m andalso m < n then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1213 
let val (ps, qs) = splitAt (m, asms) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1214 
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

1215 
else raise THM ("rotate_rule", k, [state]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

1218 
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

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

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

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

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

1223 
prop = Logic.list_implies (Bs @ [Bi'], C)} 
2671  1224 
end; 
1225 

1226 

7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

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

1228 
unchanged. Does nothing if k=0 or if k equals nj, where n is the 
16656  1229 
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

1230 
fun permute_prems j k rl = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

1232 
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

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

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

1235 
val moved_prems = List.drop (prems, j) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1236 
and fixed_prems = List.take (prems, j) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1237 
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

1238 
val n_j = length moved_prems; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1239 
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

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

1241 
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

1242 
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

1243 
let val (ps, qs) = splitAt (m, moved_prems) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1244 
in Logic.list_implies (fixed_prems @ qs @ ps, concl) end 
16725  1245 
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

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

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

1248 
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

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

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

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

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

1253 
prop = prop'} 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1254 
end; 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1255 

322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1256 

0  1257 
(** User renaming of parameters in a subgoal **) 
1258 

1259 
(*Calls error rather than raising an exception because it is intended 

1260 
for toplevel use  exception handling would not make sense here. 

1261 
The names in cs, if distinct, are used for the innermost parameters; 

17868  1262 
preceding parameters may be renamed to make all params distinct.*) 
0  1263 
fun rename_params_rule (cs, i) state = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

1265 
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

1266 
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

1267 
val iparams = map #1 (Logic.strip_params Bi); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1268 
val short = length iparams  length cs; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

1270 
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

1271 
else variantlist (Library.take (short, iparams), cs) @ cs; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1272 
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

1273 
val newBi = Logic.list_rename_params (newnames, Bi); 
250  1274 
in 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

1276 
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

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

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

1279 
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

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

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

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

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

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

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

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

1287 
prop = Logic.list_implies (Bs @ [newBi], C)}) 
0  1288 
end; 
1289 

12982  1290 

0  1291 
(*** Preservation of bound variable names ***) 
1292 

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

1293 
fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
12982  1294 
(case Term.rename_abs pat obj prop of 
15531  1295 
NONE => thm 
1296 
 SOME prop' => Thm 

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

1297 
{thy_ref = thy_ref, 
12982  1298 
der = der, 
1299 
maxidx = maxidx, 

1300 
hyps = hyps, 

1301 
shyps = shyps, 

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

1302 
tpairs = tpairs, 
12982  1303 
prop = prop'}); 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1304 

0  1305 

16656  1306 
(* strip_apply f (A, B) strips off all assumptions/parameters from A 
0  1307 
introduced by lifting over B, and applies f to remaining part of A*) 
1308 
fun strip_apply f = 

1309 
let fun strip(Const("==>",_)$ A1 $ B1, 

250  1310 
Const("==>",_)$ _ $ B2) = implies $ A1 $ strip(B1,B2) 
1311 
 strip((c as Const("all",_)) $ Abs(a,T,t1), 

1312 
Const("all",_) $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2)) 

1313 
 strip(A,_) = f A 

0  1314 
in strip end; 
1315 

1316 
(*Use the alist to rename all bound variables and some unknowns in a term 

1317 
dpairs = current disagreement pairs; tpairs = permanent ones (flexflex); 

1318 
Preserves unknowns in tpairs and on lhs of dpairs. *) 

1319 
fun rename_bvs([],_,_,_) = I 

1320 
 rename_bvs(al,dpairs,tpairs,B) = 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

1321 
let val vars = foldr add_term_vars [] 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

1322 
(map fst dpairs @ map fst tpairs @ map snd tpairs) 
250  1323 
(*unknowns appearing elsewhere be preserved!*) 
1324 
val vids = map (#1 o #1 o dest_Var) vars; 

1325 
fun rename(t as Var((x,i),T)) = 

17184  1326 
(case AList.lookup (op =) al x of 
15531  1327 
SOME(y) => if x mem_string vids orelse y mem_string vids then t 
250  1328 
else Var((y,i),T) 
15531  1329 
 NONE=> t) 
0  1330 
 rename(Abs(x,T,t)) = 
17184  1331 
Abs (if_none (AList.lookup (op =) al x) x, T, rename t) 
0  1332 
 rename(f$t) = rename f $ rename t 
1333 
 rename(t) = t; 

250  1334 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1335 
in strip_ren end; 
1336 

1337 
(*Function to rename bounds/unknowns in the argument, lifted over B*) 

1338 
fun rename_bvars(dpairs, tpairs, B) = 

15574 