author  wenzelm 
Thu, 03 Aug 2006 17:30:38 +0200  
changeset 20330  6192478fdba5 
parent 20289  ba7a7c56bed5 
child 20348  d59364649bcc 
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 term_of: cterm > term 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

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

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

45 
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

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

47 
> cterm list * (indexname * typ)list 
1160  48 

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

49 
type tag (* = string * string list *) 
1529  50 

1160  51 
(*meta theorems*) 
52 
type thm 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

70 
prop: cterm} 
6089  71 
exception THM of string * int * thm list 
18733  72 
type attribute (* = Context.generic * thm > Context.generic * thm *) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

95 
(*meta rules*) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

110 
val flexflex_rule: thm > thm Seq.seq 
19910  111 
val generalize: string list * string list > int > thm > thm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

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

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

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

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

122 
val permute_prems: int > int > thm > thm 
1160  123 
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

124 
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

125 
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

126 
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

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

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

6089  131 
signature THM = 
132 
sig 

133 
include BASIC_THM 

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

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

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

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

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

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

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

141 
val no_prems: thm > bool 
18733  142 
val rule_attribute: (Context.generic > thm > thm) > attribute 
143 
val declaration_attribute: (thm > Context.generic > Context.generic) > attribute 

144 
val theory_attributes: attribute list > theory * thm > theory * thm 

20289  145 
val proof_attributes: attribute list > Proof.context * thm > Proof.context * thm 
17345  146 
val no_attributes: 'a > 'a * 'b list 
147 
val simple_fact: 'a > ('a * 'b list) list 

16945  148 
val terms_of_tpairs: (term * term) list > term list 
19881  149 
val maxidx_of: thm > int 
19910  150 
val maxidx_thm: thm > int > int 
19881  151 
val hyps_of: thm > term list 
16945  152 
val full_prop_of: thm > term 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

157 
val name_thm: string * thm > thm 
16945  158 
val compress: thm > thm 
20261  159 
val adjust_maxidx_thm: int > thm > thm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

161 
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

162 
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

163 
val cterm_incr_indexes: int > cterm > cterm 
20002  164 
val varifyT: thm > thm 
165 
val varifyT': (string * sort) list > thm > ((string * sort) * indexname) list * thm 

19881  166 
val freezeT: thm > thm 
6089  167 
end; 
168 

3550  169 
structure Thm: THM = 
0  170 
struct 
250  171 

16656  172 

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

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

174 

16656  175 
(** collect occurrences of sorts  unless all sorts nonempty **) 
176 

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

16656  179 

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

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

182 
if Sign.all_sorts_nonempty thy then I 

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

184 

185 

186 

250  187 
(** certified types **) 
188 

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

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

192 
let val thy = Theory.deref thy_ref 
16656  193 
in {thy = thy, sign = thy, T = T, sorts = sorts} end; 
250  194 

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

196 

250  197 
fun typ_of (Ctyp {T, ...}) = T; 
198 

16656  199 
fun ctyp_of thy raw_T = 
200 
let val T = Sign.certify_typ thy raw_T 

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

250  202 

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

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

206 

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

16679  209 
 dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); 
15087  210 

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

211 

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

212 

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

214 

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

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

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

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

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

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

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

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

222 

16679  223 
exception CTERM of string; 
224 

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

225 
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

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

227 
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

228 

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

229 
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

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

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

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

234 

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

235 
fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref; 
250  236 
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

237 

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

2671  240 

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

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

242 
let 
18969  243 
val (t, T, maxidx) = Sign.certify_term thy tm; 
16656  244 
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

245 
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

246 

20057  247 
fun merge_thys0 (Cterm {thy_ref = r1, t = t1, ...}) (Cterm {thy_ref = r2, t = t2, ...}) = 
248 
Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise TERM (msg, [t1, t2]); 

16656  249 

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

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

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

254 
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

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

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

257 

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

258 
(*Destruct abstraction in cterms*) 
16679  259 
fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) = 
18944  260 
let val (y', t') = Term.dest_abs (the_default x a, T, t) in 
16679  261 
(Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, 
262 
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

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

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

265 

20261  266 
fun adjust_maxidx_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = 
267 
if maxidx = i then ct 

268 
else if maxidx < i then 

269 
Cterm {maxidx = i, thy_ref = thy_ref, t = t, T = T, sorts = sorts} 

270 
else 

271 
Cterm {maxidx = Int.max (maxidx_of_term t, i), thy_ref = thy_ref, t = t, T = T, sorts = sorts}; 

1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

272 

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

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

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

277 
if T = dty then 
16656  278 
Cterm {thy_ref = merge_thys0 cf cx, 
279 
t = f $ x, 

280 
T = rty, 

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

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

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

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

284 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  285 

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

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

18944  289 
let val t = lambda t1 t2 handle TERM _ => raise CTERM "cabs: malformed first argument" in 
16656  290 
Cterm {thy_ref = merge_thys0 ct1 ct2, 
291 
t = t, T = T1 > T2, 

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

293 
sorts = Sorts.union sorts1 sorts2} 

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

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

295 

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

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

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

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

300 
let 
16656  301 
val thy_ref = merge_thys0 ct1 ct2; 
18184  302 
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

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

304 
val sorts = Sorts.union sorts1 sorts2; 
16656  305 
fun mk_cTinst (ixn, (S, T)) = 
306 
(Ctyp {T = TVar (ixn, S), thy_ref = thy_ref, sorts = sorts}, 

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

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

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

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

312 
end; 
16656  313 
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

314 

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

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

316 
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

317 

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

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

319 
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

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

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

322 
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

323 
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

324 

2509  325 

326 

574  327 
(** read cterms **) (*exception ERROR*) 
250  328 

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

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

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

332 
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

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

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

337 

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

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

339 
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

340 
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

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

342 

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

343 
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

344 

250  345 

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

348 

2509  349 

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

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

351 

11518  352 
structure Pt = Proofterm; 
353 

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

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

357 
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

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

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

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

361 
prop: term}; (*conclusion*) 
0  362 

16725  363 
(*errors involving theorems*) 
364 
exception THM of string * int * thm list; 

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

365 

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

366 
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

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

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

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

370 
end; 
0  371 

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

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

373 
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

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

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

376 
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

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

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

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

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

381 
prop = cterm maxidx prop} 
1517  382 
end; 
383 

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

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

18944  387 
fun union_tpairs ts us = Library.merge eq_tpairs (ts, us); 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

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

390 
fun attach_tpairs tpairs prop = 

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

392 

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

16945  394 

395 

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

397 

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

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

400 

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

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

403 

0  404 

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

405 
(*attributes subsume any kind of rules or context modifiers*) 
18733  406 
type attribute = Context.generic * thm > Context.generic * thm; 
407 

408 
fun rule_attribute f (x, th) = (x, f x th); 

409 
fun declaration_attribute f (x, th) = (f th x, th); 

410 

411 
fun apply_attributes mk dest = 

412 
let 

413 
fun app [] = I 

414 
 app ((f: attribute) :: fs) = fn (x, th) => f (mk x, th) >> dest > app fs; 

415 
in app end; 

416 

417 
val theory_attributes = apply_attributes Context.Theory Context.the_theory; 

418 
val proof_attributes = apply_attributes Context.Proof Context.the_proof; 

17708  419 

6089  420 
fun no_attributes x = (x, []); 
17345  421 
fun simple_fact x = [(x, [])]; 
6089  422 

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

423 

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

425 

16945  426 
val insert_hyps = OrdList.insert Term.fast_term_ord; 
16679  427 
val remove_hyps = OrdList.remove Term.fast_term_ord; 
428 
val union_hyps = OrdList.union Term.fast_term_ord; 

429 
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

430 

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

431 

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

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

433 

3994  434 
fun eq_thm (th1, th2) = 
435 
let 

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

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

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

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

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

443 
eq_set_hyps (hyps1, hyps2) andalso 
16656  444 
equal_lists eq_tpairs (tpairs1, tpairs2) andalso 
3994  445 
prop1 aconv prop2 
446 
end; 

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

447 

16135  448 
val eq_thms = Library.equal_lists eq_thm; 
449 

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

450 
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

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

452 

19429  453 
fun maxidx_of (Thm {maxidx, ...}) = maxidx; 
19910  454 
fun maxidx_thm th i = Int.max (maxidx_of th, i); 
19881  455 
fun hyps_of (Thm {hyps, ...}) = hyps; 
12803  456 
fun prop_of (Thm {prop, ...}) = prop; 
13528  457 
fun proof_of (Thm {der = (_, proof), ...}) = proof; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

458 
fun tpairs_of (Thm {tpairs, ...}) = tpairs; 
0  459 

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

460 
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

461 
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

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

464 

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

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

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

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

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

469 

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

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

471 
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

472 
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

473 

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

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

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

481 
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

482 
val thy = Theory.deref thy_ref; 
3895  483 
in 
16945  484 
if not (subthy (thy, thy')) then 
485 
raise THM ("transfer: not a super theory", 0, [thm]) 

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

487 
else 

488 
Thm {thy_ref = Theory.self_ref thy', 

489 
der = der, 

490 
maxidx = maxidx, 

491 
shyps = shyps, 

492 
hyps = hyps, 

493 
tpairs = tpairs, 

494 
prop = prop} 

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

496 

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

499 
let 

20261  500 
val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct; 
16945  501 
val Thm {der, maxidx, shyps, hyps, tpairs, prop, ...} = th; 
502 
in 

503 
if T <> propT then 

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

505 
else if maxidxA <> ~1 then 

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

507 
else 

508 
Thm {thy_ref = merge_thys1 ct th, 

509 
der = der, 

510 
maxidx = maxidx, 

511 
shyps = Sorts.union sorts shyps, 

512 
hyps = insert_hyps A hyps, 

513 
tpairs = tpairs, 

514 
prop = prop} 

515 
end; 

16656  516 

517 

0  518 

1238  519 
(** sort contexts of theorems **) 
520 

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

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

1238  524 

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

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

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

529 
val thy = Theory.deref thy_ref; 
16656  530 
val shyps' = 
531 
if Sign.all_sorts_nonempty thy then [] 

532 
else 

533 
let 

534 
val present = present_sorts thm; 

535 
val extra = Sorts.subtract present shyps; 

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

537 
in Sorts.subtract witnessed shyps end; 

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

539 
Thm {thy_ref = thy_ref, der = der, maxidx = maxidx, 
16656  540 
shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop} 
7642  541 
end; 
1238  542 

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

545 

1238  546 

547 

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

549 

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

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

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

553 
fun get_ax thy = 
17412  554 
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

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

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

557 
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

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

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

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

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

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

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

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

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

568 

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

570 
get_axiom_i thy o NameSpace.intern (Theory.axiom_space thy); 
15672  571 

6368  572 
fun def_name name = name ^ "_def"; 
573 
fun get_def thy = get_axiom thy o def_name; 

4847  574 

1529  575 

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

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

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

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

580 

6089  581 

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

583 

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

4018  586 

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

587 
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

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

589 
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

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

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

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

594 
val name_of_thm = #1 o get_name_tags; 

595 
val tags_of_thm = #2 o get_name_tags; 

596 

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

0  598 

599 

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

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

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

605 
der = der, 

606 
maxidx = maxidx, 

607 
shyps = shyps, 

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

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

610 
prop = Compress.term thy prop} 

611 
end; 

16945  612 

20261  613 
fun adjust_maxidx_thm i (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
614 
if maxidx = i then th 

615 
else if maxidx < i then 

616 
Thm {maxidx = i, thy_ref = thy_ref, der = der, shyps = shyps, 

617 
hyps = hyps, tpairs = tpairs, prop = prop} 

618 
else 

619 
Thm {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), 

620 
thy_ref = thy_ref, der = der, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}; 

564  621 

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

622 

2509  623 

1529  624 
(*** Meta rules ***) 
0  625 

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

626 
(** primitive rules **) 
0  627 

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

629 
fun assume raw_ct = 
20261  630 
let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

631 
if T <> propT then 
19230  632 
raise THM ("assume: prop", 0, []) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

633 
else if maxidx <> ~1 then 
19230  634 
raise THM ("assume: variables", maxidx, []) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

636 
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

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

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

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

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

641 
prop = prop} 
0  642 
end; 
643 

1220  644 
(*Implication introduction 
3529  645 
[A] 
646 
: 

647 
B 

1220  648 
 
649 
A ==> B 

650 
*) 

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

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

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

655 
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

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

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

658 
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

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

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

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

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

663 
prop = implies $ A $ prop}; 
0  664 

1529  665 

1220  666 
(*Implication elimination 
667 
A ==> B A 

668 
 

669 
B 

670 
*) 

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

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

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

673 
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

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

675 
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

676 
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

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

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

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

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

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

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

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

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

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

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

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

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

690 
end; 
250  691 

1220  692 
(*Forall introduction. The Free or Var x must not be free in the hypotheses. 
16656  693 
[x] 
694 
: 

695 
A 

696 
 

697 
!!x. A 

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

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

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

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

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

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

705 
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

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

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

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

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

710 
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

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

712 
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

713 
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

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

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

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

717 
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

718 
 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

719 
 _ => raise THM ("forall_intr: not a variable", 0, [th]) 
0  720 
end; 
721 

1220  722 
(*Forall elimination 
16656  723 
!!x. A 
1220  724 
 
725 
A[t/x] 

726 
*) 

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

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

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

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

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

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

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

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

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

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

736 
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

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

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

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

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

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

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

744 

1220  745 
(* Equality *) 
0  746 

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

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

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

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

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

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

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

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

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

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

757 
prop = Logic.mk_equals (t, t)}; 
0  758 

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

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

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

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

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

764 
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

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

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

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

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

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

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

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

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

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

774 
 _ => raise THM ("symmetric", 0, [th])); 
0  775 

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

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

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

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

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

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

783 
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

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

785 
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

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

787 
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

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

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

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

791 
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

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

794 
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

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

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

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

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

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

800 
 _ => err "premises" 
0  801 
end; 
802 

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

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

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

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

807 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

822 

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

823 
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

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

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

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

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

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

829 
tpairs = [], 
18944  830 
prop = Logic.mk_equals (t, Envir.eta_contract t)}; 
0  831 

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

833 
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

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

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

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

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

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

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

841 
let 
17708  842 
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

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

844 
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

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

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

847 
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

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

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

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

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

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

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

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

855 
if exists (fn t => Logic.occs (x, t)) ts then 
17708  856 
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

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

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

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

860 
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

861 
 Var _ => (check_occs x (terms_of_tpairs tpairs); result) 
17708  862 
 _ => raise THM ("abstract_rule: not a variable " ^ string_of x, 0, [th]) 
0  863 
end; 
864 

865 
(*The combination rule 

3529  866 
f == g t == u 
867 
 

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

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

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

872 
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

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

874 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

889 
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

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

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

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

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

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

895 
 _ => raise THM ("combination: premises", 0, [th1, th2]) 
0  896 
end; 
897 

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

898 
(*Equality introduction 
3529  899 
A ==> B B ==> A 
900 
 

901 
A == B 

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

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

905 
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

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

907 
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

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

909 
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

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

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

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

913 
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

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

915 
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

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

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

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

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

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

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

922 
 _ => err "premises" 
1529  923 
end; 
924 

925 
(*The equal propositions rule 

3529  926 
A == B A 
1529  927 
 
928 
B 

929 
*) 

930 
fun equal_elim th1 th2 = 

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

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

932 
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

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

934 
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

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

936 
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

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

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

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

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

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

942 
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

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

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

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

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

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

948 
else err "not equal" 
1529  949 
 _ => err"major premise" 
950 
end; 

0  951 

1220  952 

953 

0  954 
(**** Derived rules ****) 
955 

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

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

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

960 
fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
19861  961 
Unify.smash_unifiers (Theory.deref thy_ref) tpairs (Envir.empty maxidx) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

966 
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

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

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

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

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

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

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

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

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

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

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

979 

0  980 

19910  981 
(*Generalization of fixed variables 
982 
A 

983 
 

984 
A[?'a/'a, ?x/x, ...] 

985 
*) 

986 

987 
fun generalize ([], []) _ th = th 

988 
 generalize (tfrees, frees) idx th = 

989 
let 

990 
val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = th; 

991 
val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); 

992 

993 
val bad_type = if null tfrees then K false else 

994 
Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a  _ => false); 

995 
fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x 

996 
 bad_term (Var (_, T)) = bad_type T 

997 
 bad_term (Const (_, T)) = bad_type T 

998 
 bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t 

999 
 bad_term (t $ u) = bad_term t orelse bad_term u 

1000 
 bad_term (Bound _) = false; 

1001 
val _ = exists bad_term hyps andalso 

1002 
raise THM ("generalize: variable free in assumptions", 0, [th]); 

1003 

1004 
val gen = Term.generalize (tfrees, frees) idx; 

1005 
val prop' = gen prop; 

1006 
val tpairs' = map (pairself gen) tpairs; 

1007 
val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); 

1008 
in 

1009 
Thm { 

1010 
thy_ref = thy_ref, 

1011 
der = Pt.infer_derivs' (Pt.generalize (tfrees, frees) idx) der, 

1012 
maxidx = maxidx', 

1013 
shyps = shyps, 

1014 
hyps = hyps, 

1015 
tpairs = tpairs', 

1016 
prop = prop'} 

1017 
end; 

1018 

1019 

0  1020 
(*Instantiation of Vars 
16656  1021 
A 
1022 
 

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

1220  1024 
*) 
0  1025 

6928  1026 
local 
1027 

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

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

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

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

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

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

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

1035 
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

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

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

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

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

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

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

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

1043 
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

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

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

1046 
Pretty.fbrk, Sign.pretty_term (Theory.deref thy_ref') t]), [], [t])) 
0  1047 
end; 
1048 

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

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

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

1052 
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

1053 
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

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

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

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

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

0  1064 

6928  1065 
in 
1066 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1087 
maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'), 
16656  1088 
shyps = shyps', 
1089 
hyps = hyps, 

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

1090 
tpairs = tpairs', 
16656  1091 
prop = prop'} 
1092 
end 

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

6928  1094 

1095 
end; 

1096 

0  1097 

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

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

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

1100 
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

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

1102 
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

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

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

1105 
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

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

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

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

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

1110 
prop = implies $ A $ A}; 
0  1111 

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

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

1114 
let val Cterm {thy_ref, t, maxidx, sorts, ...} = 
19525  1115 
cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), Sign.certify_class thy c)) 
6368  1116 
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

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

1119 
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

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

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

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

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

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

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

1126 

19505  1127 
(*Internalize sort constraints of type variable*) 
1128 
fun unconstrainT 

1129 
(Ctyp {thy_ref = thy_ref1, T, ...}) 

1130 
(th as Thm {thy_ref = thy_ref2, der, maxidx, shyps, hyps, tpairs, prop}) = 

1131 
let 

1132 
val ((x, i), S) = Term.dest_TVar T handle TYPE _ => 

1133 
raise THM ("unconstrainT: not a type variable", 0, [th]); 

1134 
val T' = TVar ((x, i), []); 

1135 
val unconstrain = Term.map_term_types (Term.map_atyps (fn U => if U = T then T' else U)); 

1136 
val constraints = map (curry Logic.mk_inclass T') S; 

1137 
in 

1138 
Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), 

1139 
der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.unconstrainT", prop, SOME [])), 

1140 
maxidx = Int.max (maxidx, i), 

1141 
shyps = Sorts.remove_sort S shyps, 

1142 
hyps = hyps, 

1143 
tpairs = map (pairself unconstrain) tpairs, 

1144 
prop = Logic.list_implies (constraints, unconstrain prop)} 

1145 
end; 

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

1146 

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

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

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

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

1153 
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

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

1156 
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

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

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

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

1160 
tpairs = rev (map Logic.dest_equals ts), 
18127  1161 
prop = prop3}) 
0  1162 
end; 
1163 

18127  1164 
val varifyT = #2 o varifyT' []; 
6786  1165 

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

1167 
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

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

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

1171 
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

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

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

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

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

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

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

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

1179 
prop = prop3} 
1220  1180 
end; 
0  1181 

1182 

1183 
(*** Inference rules for tactics ***) 

1184 

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

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

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

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

1189 
 _ => raise THM("dest_state", i, [state])) 
0  1190 
handle TERM _ => raise THM("dest_state", i, [state]); 
1191 

309  1192 
(*Increment variables and parameters of orule as required for 
18035  1193 
resolution with a goal.*) 
1194 
fun lift_rule goal orule = 

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

1195 
let 
18035  1196 
val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal; 
1197 
val inc = gmax + 1; 

1198 
val lift_abs = Logic.lift_abs inc gprop; 

1199 
val lift_all = Logic.lift_all inc gprop; 

1200 
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

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

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

1205 
Thm {thy_ref = merge_thys1 goal orule, 

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

1207 
maxidx = maxidx + inc, 

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

1209 
hyps = hyps, 

1210 
tpairs = map (pairself lift_abs) tpairs, 

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

0  1212 
end; 
1213 

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

1214 
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

1215 
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

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

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

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

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

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

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

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

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

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

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

1226 

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

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

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

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

1232 
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

1233 
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

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

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

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

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

1238 
maxidx = maxidx, 
16656  1239 
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

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

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

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

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

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

1245 
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

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

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

1248 
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

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

1250 
 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

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

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

1254 
in addprfs (Logic.assum_pairs (~1, Bi)) 1 end; 
0  1255 

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

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

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

1260 
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

1261 
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

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

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

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

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

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

1267 
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

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

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

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

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

1272 
prop = Logic.list_implies (Bs, C)}) 
0  1273 
end; 
1274 

1275 

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

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

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

1279 
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

1280 
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

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

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

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

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

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

1286 
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

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

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

1289 
else if 0 < m andalso m < n then 
19012  1290 
let val (ps, qs) = chop m asms 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1291 
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

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

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

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

1295 
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

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

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

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

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

1300 
prop = Logic.list_implies (Bs @ [Bi'], C)} 
2671  1301 
end; 
1302 

1303 

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

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

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

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

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

1309 
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

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

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

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

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

1314 
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

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

1316 
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

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

1318 
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

1319 
else if 0 < m andalso m < n_j then 
19012  1320 
let val (ps, qs) = chop m moved_prems 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

1325 
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

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

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

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

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

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

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

1332 

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

1333 

0  1334 
(** User renaming of parameters in a subgoal **) 
1335 

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

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

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

17868 