author  wenzelm 
Fri, 03 Aug 2007 16:28:22 +0200  
changeset 24143  90a9a6fe0d01 
parent 23781  ab793a6ddf9f 
child 24313  5a6342236a32 
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 
T: typ, 

20512  17 
maxidx: int, 
16656  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 
1160  22 

23 
(*certified terms*) 

24 
type cterm 

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

26 
val rep_cterm: cterm > 
16656  27 
{thy: theory, 
28 
t: term, 

29 
T: typ, 

30 
maxidx: int, 

31 
sorts: sort list} 

22596  32 
val crep_cterm: cterm > {thy: 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

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

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

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

36 
val ctyp_of_term: cterm > ctyp 
1160  37 

38 
(*meta theorems*) 

39 
type thm 

23601  40 
type conv = cterm > thm 
41 
type attribute = Context.generic * thm > Context.generic * thm 

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

42 
val rep_thm: thm > 
16656  43 
{thy: theory, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

44 
der: bool * Proofterm.proof, 
23657  45 
tags: Markup.property list, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

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

51 
val crep_thm: thm > 
16656  52 
{thy: theory, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

53 
der: bool * Proofterm.proof, 
23657  54 
tags: Markup.property list, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

68 
val cprop_of: thm > cterm 
18145  69 
val cprem_of: thm > int > cterm 
16656  70 
val transfer: theory > thm > thm 
16945  71 
val weaken: cterm > thm > thm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

76 
val def_name: string > string 
20884  77 
val def_name_optional: string > string > string 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

79 
val axioms_of: theory > (string * thm) list 
1160  80 

81 
(*meta rules*) 

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

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

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

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

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

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

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

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

89 
val transitive: thm > thm > thm 
23601  90 
val beta_conversion: bool > conv 
91 
val eta_conversion: conv 

92 
val eta_long_conversion: conv 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

110 
val permute_prems: int > int > thm > thm 
1160  111 
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

112 
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

113 
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

114 
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

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

116 
val invoke_oracle_i: theory > string > theory * Object.T > thm 
250  117 
end; 
0  118 

6089  119 
signature THM = 
120 
sig 

121 
include BASIC_THM 

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

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

123 
val dest_comb: cterm > cterm * cterm 
22909  124 
val dest_fun: cterm > cterm 
20580
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

125 
val dest_arg: cterm > cterm 
22909  126 
val dest_fun2: cterm > cterm 
127 
val dest_arg1: cterm > cterm 

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

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

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

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

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

133 
val no_prems: thm > bool 
16945  134 
val terms_of_tpairs: (term * term) list > term list 
19881  135 
val maxidx_of: thm > int 
19910  136 
val maxidx_thm: thm > int > int 
19881  137 
val hyps_of: thm > term list 
16945  138 
val full_prop_of: thm > term 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

139 
val get_name: thm > string 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

140 
val put_name: string > thm > thm 
23657  141 
val get_tags: thm > Markup.property list 
142 
val map_tags: (Markup.property list > Markup.property list) > thm > thm 

16945  143 
val compress: thm > thm 
23781
ab793a6ddf9f
Added function norm_proof for normalizing the proof term
berghofe
parents:
23657
diff
changeset

144 
val norm_proof: thm > thm 
20261  145 
val adjust_maxidx_thm: int > thm > thm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

146 
val rename_boundvars: term > term > thm > thm 
22909  147 
val match: cterm * cterm > (ctyp * ctyp) list * (cterm * cterm) list 
148 
val first_order_match: cterm * cterm > (ctyp * ctyp) list * (cterm * cterm) list 

149 
val incr_indexes_cterm: int > cterm > cterm 

20002  150 
val varifyT: thm > thm 
151 
val varifyT': (string * sort) list > thm > ((string * sort) * indexname) list * thm 

19881  152 
val freezeT: thm > thm 
6089  153 
end; 
154 

3550  155 
structure Thm: THM = 
0  156 
struct 
250  157 

22237
bb9b1c8a8a95
oldfashioned abstype ctyp/cterm/thm prevents accidental equality tests;
wenzelm
parents:
21975
diff
changeset

158 
structure Pt = Proofterm; 
bb9b1c8a8a95
oldfashioned abstype ctyp/cterm/thm prevents accidental equality tests;
wenzelm
parents:
21975
diff
changeset

159 

16656  160 

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

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

162 

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

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

16656  167 

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

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

170 
if Sign.all_sorts_nonempty thy then I 

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

172 

173 

174 

250  175 
(** certified types **) 
176 

22237
bb9b1c8a8a95
oldfashioned abstype ctyp/cterm/thm prevents accidental equality tests;
wenzelm
parents:
21975
diff
changeset

177 
abstype ctyp = Ctyp of 
20512  178 
{thy_ref: theory_ref, 
179 
T: typ, 

180 
maxidx: int, 

22237
bb9b1c8a8a95
oldfashioned abstype ctyp/cterm/thm prevents accidental equality tests;
wenzelm
parents:
21975
diff
changeset

181 
sorts: sort list} 
bb9b1c8a8a95
oldfashioned abstype ctyp/cterm/thm prevents accidental equality tests;
wenzelm
parents:
21975
diff
changeset

182 
with 
250  183 

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

185 
let val thy = Theory.deref thy_ref 
22596  186 
in {thy = thy, T = T, maxidx = maxidx, sorts = sorts} end; 
250  187 

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

189 

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

16656  192 
fun ctyp_of thy raw_T = 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

193 
let 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

194 
val T = Sign.certify_typ thy raw_T; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

195 
val maxidx = Term.maxidx_of_typ T; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

196 
val sorts = may_insert_typ_sorts thy T []; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

197 
in Ctyp {thy_ref = Theory.check_thy thy, T = T, maxidx = maxidx, sorts = sorts} end; 
250  198 

20512  199 
fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts), maxidx, sorts}) = 
200 
map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts 

16679  201 
 dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); 
15087  202 

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

203 

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

204 

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

206 

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

207 
(*certified terms with checked typ, maxidx, and sorts*) 
22237
bb9b1c8a8a95
oldfashioned abstype ctyp/cterm/thm prevents accidental equality tests;
wenzelm
parents:
21975
diff
changeset

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

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

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

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

212 
maxidx: int, 
22237
bb9b1c8a8a95
oldfashioned abstype ctyp/cterm/thm prevents accidental equality tests;
wenzelm
parents:
21975
diff
changeset

213 
sorts: sort list} 
bb9b1c8a8a95
oldfashioned abstype ctyp/cterm/thm prevents accidental equality tests;
wenzelm
parents:
21975
diff
changeset

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

215 

22584  216 
exception CTERM of string * cterm list; 
16679  217 

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

218 
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

219 
let val thy = Theory.deref thy_ref 
22596  220 
in {thy = 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

221 

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

222 
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

223 
let val thy = Theory.deref thy_ref in 
22596  224 
{thy = thy, t = t, 
20512  225 
T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

228 

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

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

231 

20512  232 
fun ctyp_of_term (Cterm {thy_ref, T, maxidx, sorts, ...}) = 
233 
Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}; 

2671  234 

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

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

236 
let 
18969  237 
val (t, T, maxidx) = Sign.certify_term thy tm; 
16656  238 
val sorts = may_insert_term_sorts thy t []; 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

239 
in Cterm {thy_ref = Theory.check_thy 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

240 

20057  241 
fun merge_thys0 (Cterm {thy_ref = r1, t = t1, ...}) (Cterm {thy_ref = r2, t = t2, ...}) = 
23601  242 
Theory.merge_refs (r1, r2); 
16656  243 

20580
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

244 

22909  245 
(* destructors *) 
246 

247 
fun dest_comb (ct as Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) = 

248 
let val A = Term.argument_type_of c 0 in 

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

250 
Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) 

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

251 
end 
22584  252 
 dest_comb ct = raise CTERM ("dest_comb", [ct]); 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

253 

22909  254 
fun dest_fun (ct as Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) = 
255 
let val A = Term.argument_type_of c 0 

256 
in Cterm {t = c, T = A > T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end 

257 
 dest_fun ct = raise CTERM ("dest_fun", [ct]); 

258 

259 
fun dest_arg (ct as Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) = 

260 
let val A = Term.argument_type_of c 0 

261 
in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end 

22584  262 
 dest_arg ct = raise CTERM ("dest_arg", [ct]); 
20580
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

263 

22909  264 

265 
fun dest_fun2 (Cterm {t = c $ a $ b, T, thy_ref, maxidx, sorts}) = 

266 
let 

267 
val A = Term.argument_type_of c 0; 

268 
val B = Term.argument_type_of c 1; 

269 
in Cterm {t = c, T = A > B > T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end 

270 
 dest_fun2 ct = raise CTERM ("dest_fun2", [ct]); 

271 

272 
fun dest_arg1 (Cterm {t = c $ a $ _, T = _, thy_ref, maxidx, sorts}) = 

273 
let val A = Term.argument_type_of c 0 

274 
in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end 

275 
 dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); 

20673  276 

22584  277 
fun dest_abs a (ct as 
278 
Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) = 

18944  279 
let val (y', t') = Term.dest_abs (the_default x a, T, t) in 
16679  280 
(Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, 
281 
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

282 
end 
22584  283 
 dest_abs _ ct = raise CTERM ("dest_abs", [ct]); 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

284 

22909  285 

286 
(* constructors *) 

287 

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

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

291 
if T = dty then 
16656  292 
Cterm {thy_ref = merge_thys0 cf cx, 
293 
t = f $ x, 

294 
T = rty, 

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

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

296 
sorts = Sorts.union sorts1 sorts2} 
22584  297 
else raise CTERM ("capply: types don't agree", [cf, cx]) 
298 
 capply cf cx = raise CTERM ("capply: first arg is not a function", [cf, cx]); 

250  299 

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

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

21975
1152dc45d591
Term.lambda: abstract over arbitrary closed terms;
wenzelm
parents:
21798
diff
changeset

303 
let val t = Term.lambda t1 t2 in 
16656  304 
Cterm {thy_ref = merge_thys0 ct1 ct2, 
305 
t = t, T = T1 > T2, 

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

307 
sorts = Sorts.union sorts1 sorts2} 

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

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

309 

20580
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

310 

22909  311 
(* indexes *) 
312 

20580
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

313 
fun adjust_maxidx_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

314 
if maxidx = i then ct 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

315 
else if maxidx < i then 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

316 
Cterm {maxidx = i, thy_ref = thy_ref, t = t, T = T, sorts = sorts} 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

317 
else 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

318 
Cterm {maxidx = Int.max (maxidx_of_term t, i), thy_ref = thy_ref, t = t, T = T, sorts = sorts}; 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

319 

22909  320 
fun incr_indexes_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = 
321 
if i < 0 then raise CTERM ("negative increment", [ct]) 

322 
else if i = 0 then ct 

323 
else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t, 

324 
T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts}; 

325 

326 

327 
(* matching *) 

328 

329 
local 

330 

331 
fun gen_match match 

20512  332 
(ct1 as Cterm {t = t1, sorts = sorts1, ...}, 
20815  333 
ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

334 
let 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

335 
val thy = Theory.deref (merge_thys0 ct1 ct2); 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

336 
val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

337 
val sorts = Sorts.union sorts1 sorts2; 
20512  338 
fun mk_cTinst ((a, i), (S, T)) = 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

339 
(Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts}, 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

340 
Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}); 
20512  341 
fun mk_ctinst ((x, i), (T, t)) = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

342 
let val T = Envir.typ_subst_TVars Tinsts T in 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

343 
(Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy, 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

344 
maxidx = i, sorts = sorts}, 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

345 
Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}) 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

346 
end; 
16656  347 
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

348 

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

350 

22909  351 
val match = gen_match Pattern.match; 
352 
val first_order_match = gen_match Pattern.first_order_match; 

353 

354 
end; 

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

355 

2509  356 

357 

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

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

359 

22237
bb9b1c8a8a95
oldfashioned abstype ctyp/cterm/thm prevents accidental equality tests;
wenzelm
parents:
21975
diff
changeset

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

361 
{thy_ref: theory_ref, (*dynamic reference to theory*) 
11518  362 
der: bool * Pt.proof, (*derivation*) 
23657  363 
tags: Markup.property list, (*additional annotations/comments*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

364 
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

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

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

367 
tpairs: (term * term) list, (*flexflex pairs*) 
22237
bb9b1c8a8a95
oldfashioned abstype ctyp/cterm/thm prevents accidental equality tests;
wenzelm
parents:
21975
diff
changeset

368 
prop: term} (*conclusion*) 
bb9b1c8a8a95
oldfashioned abstype ctyp/cterm/thm prevents accidental equality tests;
wenzelm
parents:
21975
diff
changeset

369 
with 
0  370 

23601  371 
type conv = cterm > thm; 
372 

22365  373 
(*attributes subsume any kind of rules or context modifiers*) 
374 
type attribute = Context.generic * thm > Context.generic * thm; 

375 

16725  376 
(*errors involving theorems*) 
377 
exception THM of string * int * thm list; 

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

378 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

380 
let val thy = Theory.deref thy_ref in 
22596  381 
{thy = thy, der = der, tags = tags, maxidx = maxidx, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

383 
end; 
0  384 

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

385 
(*version of rep_thm returning cterms instead of terms*) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

389 
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

390 
in 
22596  391 
{thy = thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

394 
prop = cterm maxidx prop} 
1517  395 
end; 
396 

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

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

18944  400 
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

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

403 
fun attach_tpairs tpairs prop = 

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

405 

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

16945  407 

22365  408 
val union_hyps = OrdList.union Term.fast_term_ord; 
409 

16945  410 

24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

411 
(* merge theories of cterms/thms  trivial absorption only *) 
16945  412 

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

23601  414 
Theory.merge_refs (r1, r2); 
16945  415 

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

23601  417 
Theory.merge_refs (r1, r2); 
16945  418 

0  419 

22365  420 
(* basic components *) 
16135  421 

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

422 
fun theory_of_thm (Thm {thy_ref, ...}) = Theory.deref thy_ref; 
19429  423 
fun maxidx_of (Thm {maxidx, ...}) = maxidx; 
19910  424 
fun maxidx_thm th i = Int.max (maxidx_of th, i); 
19881  425 
fun hyps_of (Thm {hyps, ...}) = hyps; 
12803  426 
fun prop_of (Thm {prop, ...}) = prop; 
13528  427 
fun proof_of (Thm {der = (_, proof), ...}) = proof; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

428 
fun tpairs_of (Thm {tpairs, ...}) = tpairs; 
0  429 

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

430 
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

431 
val prems_of = Logic.strip_imp_prems o prop_of; 
21576  432 
val nprems_of = Logic.count_prems o prop_of; 
19305  433 
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

434 

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

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

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

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

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

439 

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

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

441 
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

442 
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

443 

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

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

449 
fun transfer thy' thm = 
3895  450 
let 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

452 
val thy = Theory.deref thy_ref; 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

453 
val _ = subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]); 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

454 
val is_eq = eq_thy (thy, thy'); 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

455 
val _ = Theory.check_thy thy; 
3895  456 
in 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

457 
if is_eq then thm 
16945  458 
else 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

459 
Thm {thy_ref = Theory.check_thy thy', 
16945  460 
der = der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

461 
tags = tags, 
16945  462 
maxidx = maxidx, 
463 
shyps = shyps, 

464 
hyps = hyps, 

465 
tpairs = tpairs, 

466 
prop = prop} 

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

468 

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

471 
let 

20261  472 
val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct; 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

473 
val Thm {der, tags, maxidx, shyps, hyps, tpairs, prop, ...} = th; 
16945  474 
in 
475 
if T <> propT then 

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

477 
else if maxidxA <> ~1 then 

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

479 
else 

480 
Thm {thy_ref = merge_thys1 ct th, 

481 
der = der, 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

482 
tags = tags, 
16945  483 
maxidx = maxidx, 
484 
shyps = Sorts.union sorts shyps, 

22365  485 
hyps = OrdList.insert Term.fast_term_ord A hyps, 
16945  486 
tpairs = tpairs, 
487 
prop = prop} 

488 
end; 

16656  489 

490 

0  491 

1238  492 
(** sort contexts of theorems **) 
493 

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

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

1238  497 

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

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

502 
val thy = Theory.deref thy_ref; 
16656  503 
val shyps' = 
504 
if Sign.all_sorts_nonempty thy then [] 

505 
else 

506 
let 

507 
val present = present_sorts thm; 

508 
val extra = Sorts.subtract present shyps; 

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

510 
in Sorts.subtract witnessed shyps end; 

7642  511 
in 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

512 
Thm {thy_ref = Theory.check_thy thy, der = der, tags = tags, maxidx = maxidx, 
16656  513 
shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop} 
7642  514 
end; 
1238  515 

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

518 

1238  519 

520 

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

522 

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

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

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

526 
fun get_ax thy = 
22685  527 
Symtab.lookup (Theory.axiom_table thy) name 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

528 
> Option.map (fn prop => 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

529 
let 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

530 
val der = Pt.infer_derivs' I (false, Pt.axm_proof name prop); 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

531 
val maxidx = maxidx_of_term prop; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

532 
val shyps = may_insert_term_sorts thy prop []; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

533 
in 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

534 
Thm {thy_ref = Theory.check_thy thy, der = der, tags = [], 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

535 
maxidx = maxidx, shyps = shyps, hyps = [], tpairs = [], prop = prop} 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

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

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

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

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

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

542 

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

544 
get_axiom_i thy o NameSpace.intern (Theory.axiom_space thy); 
15672  545 

20884  546 
fun def_name c = c ^ "_def"; 
547 

548 
fun def_name_optional c "" = def_name c 

549 
 def_name_optional _ name = name; 

550 

6368  551 
fun get_def thy = get_axiom thy o def_name; 
4847  552 

1529  553 

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

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

555 
fun axioms_of thy = 
22685  556 
map (fn s => (s, get_axiom_i thy s)) (Symtab.keys (Theory.axiom_table thy)); 
776
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

557 

6089  558 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

559 
(* official name and additional tags *) 
6089  560 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

561 
fun get_name (Thm {hyps, prop, der = (_, prf), ...}) = 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

562 
Pt.get_name hyps prop prf; 
4018  563 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

564 
fun put_name name (Thm {thy_ref, der = (ora, prf), tags, maxidx, shyps, hyps, tpairs = [], prop}) = 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

565 
let 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

566 
val thy = Theory.deref thy_ref; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

567 
val der = (ora, Pt.thm_proof thy name hyps prop prf); 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

568 
in 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

569 
Thm {thy_ref = Theory.check_thy thy, der = der, tags = tags, maxidx = maxidx, 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

570 
shyps = shyps, hyps = hyps, tpairs = [], prop = prop} 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

571 
end 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

572 
 put_name _ thm = raise THM ("name_thm: unsolved flexflex constraints", 0, [thm]); 
6089  573 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

574 
val get_tags = #tags o rep_thm; 
6089  575 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

576 
fun map_tags f (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) = 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

577 
Thm {thy_ref = thy_ref, der = der, tags = f tags, maxidx = maxidx, 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

578 
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}; 
0  579 

580 

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

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

586 
der = der, 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

587 
tags = tags, 
16991  588 
maxidx = maxidx, 
589 
shyps = shyps, 

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

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

592 
prop = Compress.term thy prop} 

593 
end; 

16945  594 

23781
ab793a6ddf9f
Added function norm_proof for normalizing the proof term
berghofe
parents:
23657
diff
changeset

595 
fun norm_proof (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) = 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

596 
let 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

597 
val thy = Theory.deref thy_ref; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

598 
val der = Pt.infer_derivs' (Pt.rew_proof thy) der; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

599 
in 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

600 
Thm {thy_ref = Theory.check_thy thy, der = der, tags = tags, maxidx = maxidx, 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

601 
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop} 
23781
ab793a6ddf9f
Added function norm_proof for normalizing the proof term
berghofe
parents:
23657
diff
changeset

602 
end; 
ab793a6ddf9f
Added function norm_proof for normalizing the proof term
berghofe
parents:
23657
diff
changeset

603 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

604 
fun adjust_maxidx_thm i (th as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) = 
20261  605 
if maxidx = i then th 
606 
else if maxidx < i then 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

607 
Thm {maxidx = i, thy_ref = thy_ref, der = der, tags = tags, shyps = shyps, 
20261  608 
hyps = hyps, tpairs = tpairs, prop = prop} 
609 
else 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

610 
Thm {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), thy_ref = thy_ref, 
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

611 
der = der, tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}; 
564  612 

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

613 

2509  614 

1529  615 
(*** Meta rules ***) 
0  616 

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

617 
(** primitive rules **) 
0  618 

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

620 
fun assume raw_ct = 
20261  621 
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

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

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

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

627 
der = Pt.infer_derivs' I (false, Pt.Hyp prop), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

633 
prop = prop} 
0  634 
end; 
635 

1220  636 
(*Implication introduction 
3529  637 
[A] 
638 
: 

639 
B 

1220  640 
 
641 
A ==> B 

642 
*) 

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

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

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

647 
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

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

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

650 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

653 
shyps = Sorts.union sorts shyps, 
22365  654 
hyps = OrdList.remove Term.fast_term_ord A hyps, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

656 
prop = implies $ A $ prop}; 
0  657 

1529  658 

1220  659 
(*Implication elimination 
660 
A ==> B A 

661 
 

662 
B 

663 
*) 

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

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

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

666 
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

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

668 
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

669 
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

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

671 
case prop of 
20512  672 
Const ("==>", _) $ A $ B => 
673 
if A aconv propA then 

16656  674 
Thm {thy_ref = merge_thys2 thAB thA, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

675 
der = Pt.infer_derivs (curry Pt.%%) der derA, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

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

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

684 
end; 
250  685 

1220  686 
(*Forall introduction. The Free or Var x must not be free in the hypotheses. 
16656  687 
[x] 
688 
: 

689 
A 

690 
 

691 
!!x. A 

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

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

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

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

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

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

699 
der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

705 
prop = all T $ Abs (a, T, abstract_over (x, prop))}; 
21798  706 
fun check_occs a x ts = 
16847
8fc160b12e73
invoke_oracle: do not keep theory value, but theory_ref;
wenzelm
parents:
16725
diff
changeset

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

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

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

711 
case x of 
21798  712 
Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a) 
713 
 Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a) 

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

714 
 _ => raise THM ("forall_intr: not a variable", 0, [th]) 
0  715 
end; 
716 

1220  717 
(*Forall elimination 
16656  718 
!!x. A 
1220  719 
 
720 
A[t/x] 

721 
*) 

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

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

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

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

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

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

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

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

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

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

731 
der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

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

740 

1220  741 
(* Equality *) 
0  742 

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

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

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

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

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

748 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

754 
prop = Logic.mk_equals (t, t)}; 
0  755 

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

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

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

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

759 
u == t 
1220  760 
*) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

761 
fun symmetric (th 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

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

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

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

765 
der = Pt.infer_derivs' Pt.symmetric der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

772 
 _ => raise THM ("symmetric", 0, [th])); 
0  773 

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

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

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

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

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

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

781 
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

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

783 
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

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

785 
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

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

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

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

789 
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

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

792 
der = Pt.infer_derivs (Pt.transitive u T) der1 der2, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

806 
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

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

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

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

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

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

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

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

814 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

815 
tags = [], 
16601
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), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

23493  833 
fun eta_long_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) = 
834 
Thm {thy_ref = thy_ref, 

835 
der = Pt.infer_derivs' I (false, Pt.reflexive), 

836 
tags = [], 

837 
maxidx = maxidx, 

838 
shyps = sorts, 

839 
hyps = [], 

840 
tpairs = [], 

841 
prop = Logic.mk_equals (t, Pattern.eta_long [] t)}; 

842 

0  843 
(*The abstraction rule. The Free or Var x must not be free in the hypotheses. 
844 
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

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

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

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

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

850 
(Cterm {t = x, T, sorts, ...}) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

854 
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

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

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

857 
der = Pt.infer_derivs' (Pt.abstract_rule x a) der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

864 
(Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))}; 
21798  865 
fun check_occs a x ts = 
16847
8fc160b12e73
invoke_oracle: do not keep theory value, but theory_ref;
wenzelm
parents:
16725
diff
changeset

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

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

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

870 
case x of 
21798  871 
Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result) 
872 
 Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result) 

873 
 _ => raise THM ("abstract_rule: not a variable", 0, [th]) 

0  874 
end; 
875 

876 
(*The combination rule 

3529  877 
f == g t == u 
878 
 

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

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

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

883 
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

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

885 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

900 
der = Pt.infer_derivs (Pt.combination f g t u fT) der1 der2, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

907 
 _ => raise THM ("combination: premises", 0, [th1, th2]) 
0  908 
end; 
909 

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

910 
(*Equality introduction 
3529  911 
A ==> B B ==> A 
912 
 

913 
A == B 

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

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

917 
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

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

919 
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

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

921 
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

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

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

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

925 
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

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

927 
der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

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

935 
 _ => err "premises" 
1529  936 
end; 
937 

938 
(*The equal propositions rule 

3529  939 
A == B A 
1529  940 
 
941 
B 

942 
*) 

943 
fun equal_elim th1 th2 = 

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

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

945 
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

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

947 
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

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

949 
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

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

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

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

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

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

955 
der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

962 
else err "not equal" 
1529  963 
 _ => err"major premise" 
964 
end; 

0  965 

1220  966 

967 

0  968 
(**** Derived rules ****) 
969 

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

970 
(*Smash unifies the list of term pairs leaving no flexflex pairs. 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

971 
Instantiates the theorem and deletes trivial tpairs. Resulting 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

972 
sequence may contain multiple elements if the tpairs are not all 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

973 
flexflex.*) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

974 
fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) = 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

975 
let val thy = Theory.deref thy_ref in 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

976 
Unify.smash_unifiers thy tpairs (Envir.empty maxidx) 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

977 
> Seq.map (fn env => 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

978 
if Envir.is_empty env then th 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

979 
else 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

980 
let 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

981 
val tpairs' = tpairs > map (pairself (Envir.norm_term env)) 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

982 
(*remove trivial tpairs, of the form t==t*) 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

983 
> filter_out (op aconv); 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

984 
val der = Pt.infer_derivs' (Pt.norm_proof' env) der; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

985 
val prop' = Envir.norm_term env prop; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

986 
val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

987 
val shyps = may_insert_env_sorts thy env shyps; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

988 
in 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

989 
Thm {thy_ref = Theory.check_thy thy, der = der, tags = [], maxidx = maxidx, 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

990 
shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'} 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

991 
end) 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

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

993 

0  994 

19910  995 
(*Generalization of fixed variables 
996 
A 

997 
 

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

999 
*) 

1000 

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

1002 
 generalize (tfrees, frees) idx th = 

1003 
let 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1004 
val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...} = th; 
19910  1005 
val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); 
1006 

1007 
val bad_type = if null tfrees then K false else 

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

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

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

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

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

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

1014 
 bad_term (Bound _) = false; 

1015 
val _ = exists bad_term hyps andalso 

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

1017 

20512  1018 
val gen = TermSubst.generalize (tfrees, frees) idx; 
19910  1019 
val prop' = gen prop; 
1020 
val tpairs' = map (pairself gen) tpairs; 

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

1022 
in 

1023 
Thm { 

1024 
thy_ref = thy_ref, 

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

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1026 
tags = [], 
19910  1027 
maxidx = maxidx', 
1028 
shyps = shyps, 

1029 
hyps = hyps, 

1030 
tpairs = tpairs', 

1031 
prop = prop'} 

1032 
end; 

1033 

1034 

22584  1035 
(*Instantiation of schematic variables 
16656  1036 
A 
1037 
 

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

1220  1039 
*) 
0  1040 

6928  1041 
local 
1042 

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

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

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

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

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

1048 
val Cterm {t = t, T = T, ...} = ct 
20512  1049 
and Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1050 
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

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

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

1053 
(case t of Var v => 
20512  1054 
if T = U then ((v, (u, maxidx_u)), (thy_ref', sorts')) 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

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

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

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

1058 
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

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

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

1061 
Pretty.fbrk, Sign.pretty_term (Theory.deref thy_ref') t]), [], [t])) 
0  1062 
end; 
1063 

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

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

1066 
val Ctyp {T, thy_ref = thy_ref1, ...} = cT 
20512  1067 
and Ctyp {T = U, thy_ref = thy_ref2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

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

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

1071 
(case T of TVar (v as (_, S)) => 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1072 
if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (Theory.check_thy thy', sorts')) 
16656  1073 
else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy' S, [U], []) 
1074 
 _ => raise TYPE (Pretty.string_of (Pretty.block 

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

0  1078 

6928  1079 
in 
1080 

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

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

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

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

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

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

1089 
(thy_ref, shyps) > fold_map add_inst inst > fold_map add_instT instT; 
20512  1090 
val subst = TermSubst.instantiate_maxidx (instT', inst'); 
1091 
val (prop', maxidx1) = subst prop ~1; 

1092 
val (tpairs', maxidx') = 

1093 
fold_map (fn (t, u) => fn i => subst t i >> subst u) tpairs maxidx1; 

16656  1094 
in 
20545
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1095 
Thm {thy_ref = thy_ref', 
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1096 
der = Pt.infer_derivs' (fn d => 
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1097 
Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1098 
tags = [], 
20545
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1099 
maxidx = maxidx', 
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1100 
shyps = shyps', 
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1101 
hyps = hyps, 
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1102 
tpairs = tpairs', 
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1103 
prop = prop'} 
16656  1104 
end 
1105 
handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); 

6928  1106 

22584  1107 
fun instantiate_cterm ([], []) ct = ct 
1108 
 instantiate_cterm (instT, inst) ct = 

1109 
let 

1110 
val Cterm {thy_ref, t, T, sorts, ...} = ct; 

1111 
val (inst', (instT', (thy_ref', sorts'))) = 

1112 
(thy_ref, sorts) > fold_map add_inst inst > fold_map add_instT instT; 

1113 
val subst = TermSubst.instantiate_maxidx (instT', inst'); 

1114 
val substT = TermSubst.instantiateT_maxidx instT'; 

1115 
val (t', maxidx1) = subst t ~1; 

1116 
val (T', maxidx') = substT T maxidx1; 

1117 
in Cterm {thy_ref = thy_ref', t = t', T = T', sorts = sorts', maxidx = maxidx'} end 

1118 
handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); 

1119 

6928  1120 
end; 
1121 

0  1122 

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

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

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

1125 
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

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

1127 
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

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

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

1130 
der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

1136 
prop = implies $ A $ A}; 
0  1137 

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

1139 
fun class_triv thy c = 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1140 
let 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1141 
val Cterm {t, maxidx, sorts, ...} = 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1142 
cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), Sign.certify_class thy c)) 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1143 
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1144 
val der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])); 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

1145 
in 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1146 
Thm {thy_ref = Theory.check_thy thy, der = der, tags = [], maxidx = maxidx, 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1147 
shyps = sorts, hyps = [], tpairs = [], prop = t} 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

1149 

19505  1150 
(*Internalize sort constraints of type variable*) 
1151 
fun unconstrainT 

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

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1153 
(th as Thm {thy_ref = thy_ref2, der, maxidx, shyps, hyps, tpairs, prop, ...}) = 
19505  1154 
let 
1155 
val ((x, i), S) = Term.dest_TVar T handle TYPE _ => 

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

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

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20545
diff
changeset

1158 
val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U)); 
19505  1159 
val constraints = map (curry Logic.mk_inclass T') S; 
1160 
in 

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

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

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1163 
tags = [], 
19505  1164 
maxidx = Int.max (maxidx, i), 
1165 
shyps = Sorts.remove_sort S shyps, 

1166 
hyps = hyps, 

1167 
tpairs = map (pairself unconstrain) tpairs, 

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

1169 
end; 

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

1170 

6786  1171 
(* Replace all TFrees not fixed or in the hyps by new TVars *) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

1177 
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

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

1180 
der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

1185 
tpairs = rev (map Logic.dest_equals ts), 
18127  1186 
prop = prop3}) 
0  1187 
end; 
1188 

18127  1189 
val varifyT = #2 o varifyT' []; 
6786  1190 

0  1191 
(* Replace all TVars by new TFrees *) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1192 
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

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

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

1196 
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

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

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

1199 
der = Pt.infer_derivs' (Pt.freezeT prop1) der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

1205 
prop = prop3} 
1220  1206 
end; 
0  1207 

1208 

1209 
(*** Inference rules for tactics ***) 

1210 

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

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

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

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

1215 
 _ => raise THM("dest_state", i, [state])) 
0  1216 
handle TERM _ => raise THM("dest_state", i, [state]); 
1217 

309  1218 
(*Increment variables and parameters of orule as required for 
18035  1219 
resolution with a goal.*) 
1220 
fun lift_rule goal orule = 

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

1221 
let 
18035  1222 
val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal; 
1223 
val inc = gmax + 1; 

1224 
val lift_abs = Logic.lift_abs inc gprop; 

1225 
val lift_all = Logic.lift_all inc gprop; 

1226 
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

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

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

1231 
Thm {thy_ref = merge_thys1 goal orule, 

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

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1233 
tags = [], 
18035  1234 
maxidx = maxidx + inc, 
1235 
shyps = Sorts.union shyps sorts, (*sic!*) 

1236 
hyps = hyps, 

1237 
tpairs = map (pairself lift_abs) tpairs, 

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

0  1239 
end; 
1240 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1241 
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

1242 
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

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

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

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

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

1247 
(Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

1254 

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

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

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

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

1260 
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

1261 
fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) = 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

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

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

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

1265 
Pt.assumption_proof Bs Bi n) der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

1267 
maxidx = maxidx, 
16656  1268 
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

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

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

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

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

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

1274 
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

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

1276 
else (*normalize the new rule fully*) 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1277 
Envir.norm_term env (Logic.list_implies (Bs, C)), 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

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

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

1280 
 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

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

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

1284 
in addprfs (Logic.assum_pairs (~1, Bi)) 1 end; 
0  1285 

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

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

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

1290 
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

1291 
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

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

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

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

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

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

1297 
der = Pt.infer_derivs' (Pt.assumption_proof Bs Bi (n + 1)) der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

1303 
prop = Logic.list_implies (Bs, C)}) 
0  1304 
end; 
1305 

1306 

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

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

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

1310 
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

1311 
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

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

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

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

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

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

1317 
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

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

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

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

1322 
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

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

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

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

1326 
der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1327 