author  wenzelm 
Wed, 29 Jun 2005 15:13:31 +0200  
changeset 16601  ee8eefade568 
parent 16425  2427be27cc60 
child 16656  18b0cb22057d 
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 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

14 
val rep_ctyp: ctyp > {thy: theory, sign: theory, T: typ} 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

18 
val read_ctyp: theory > string > ctyp 
1160  19 

20 
(*certified terms*) 

21 
type cterm 

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

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

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

24 
{thy: theory, sign: theory, t: term, T: typ, maxidx: int, sorts: sort list} 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

40 
> cterm list * (indexname * typ)list 
1160  41 

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

42 
type tag (* = string * string list *) 
1529  43 

1160  44 
(*meta theorems*) 
45 
type thm 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

82 
val axioms_of: theory > (string * thm) list 
1160  83 

84 
(*meta rules*) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

115 
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

116 
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

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

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

6089  121 
signature THM = 
122 
sig 

123 
include BASIC_THM 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

143 
val terms_of_tpairs: (term * term) list > term list 
6089  144 
end; 
145 

3550  146 
structure Thm: THM = 
0  147 
struct 
250  148 

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

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

150 

250  151 
(** certified types **) 
152 

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

153 
datatype ctyp = Ctyp of {thy_ref: theory_ref, T: typ}; 
250  154 

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

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

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

157 
in {thy = thy, sign = thy, T = T} end; 
250  158 

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

159 
val theory_of_ctyp = #thy o rep_ctyp; 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

160 

250  161 
fun typ_of (Ctyp {T, ...}) = T; 
162 

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

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

164 
Ctyp {thy_ref = Theory.self_ref thy, T = Sign.certify_typ thy T}; 
250  165 

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

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

167 
Ctyp {thy_ref = Theory.self_ref thy, T = Sign.read_typ (thy, K NONE) s}; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

168 

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

169 
fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts)}) = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

170 
map (fn T => Ctyp {thy_ref = thy_ref, T = T}) Ts 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

171 
 dest_ctyp cT = [cT]; 
15087  172 

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

173 

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

174 

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

176 

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

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

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

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

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

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

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

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

184 

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

185 
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

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

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

188 

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

189 
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

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

191 
{thy = thy, sign = thy, t = t, T = Ctyp {thy_ref = thy_ref, T = T}, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

194 

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

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

196 
val sign_of_cterm = theory_of_cterm; 
9461  197 

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

199 

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

200 
fun ctyp_of_term (Cterm {thy_ref, T, ...}) = Ctyp {thy_ref = thy_ref, T = T}; 
2671  201 

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

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

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

204 
val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

205 
val sorts = Sorts.insert_term t []; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

207 

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

208 
exception CTERM of string; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

209 

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

210 
(*Destruct application in cterms*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

211 
fun dest_comb (Cterm {thy_ref, T, maxidx, sorts, t = A $ B}) = 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

212 
let val typeA = fastype_of A; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

214 
case typeA of Type("fun",[S,T]) => S 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

215 
 _ => sys_error "Function type expected in dest_comb"; 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

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

218 
Cterm {thy_ref=thy_ref, maxidx=maxidx, sorts=sorts, t=B, T=typeB}) 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

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

221 

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

222 
(*Destruct abstraction in cterms*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

223 
fun dest_abs a (Cterm {thy_ref, T as Type("fun",[_,S]), maxidx, sorts, t=Abs(x,ty,M)}) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

224 
let val (y,N) = variant_abs (if_none a x, ty, M) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

225 
in (Cterm {thy_ref = thy_ref, T = ty, maxidx = 0, sorts = sorts, t = Free(y,ty)}, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

226 
Cterm {thy_ref = thy_ref, T = S, maxidx = maxidx, sorts = sorts, t = N}) 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

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

229 

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

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

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

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

234 

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

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

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

237 
(Cterm {t=f, thy_ref=thy_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1, sorts = sorts1}) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

238 
(Cterm {t=x, thy_ref=thy_ref2, T, maxidx=maxidx2, sorts = sorts2}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

239 
if T = dty then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

240 
Cterm{t = f $ x, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

241 
thy_ref=Theory.merge_refs(thy_ref1,thy_ref2), T=rty, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

245 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  246 

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

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

248 
(Cterm {t=t1, thy_ref=thy_ref1, T=T1, maxidx=maxidx1, sorts = sorts1}) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

249 
(Cterm {t=t2, thy_ref=thy_ref2, T=T2, maxidx=maxidx2, sorts = sorts2}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

250 
let val t = lambda t1 t2 handle TERM _ => raise CTERM "cabs: first arg is not a variable" in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

251 
Cterm {t = t, T = T1 > T2, thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

252 
maxidx = Int.max (maxidx1, maxidx2), sorts = Sorts.union sorts1 sorts2} 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

254 

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

255 
(*Matching of cterms*) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

257 
(Cterm {thy_ref = thy_ref1, maxidx = maxidx1, t = t1, sorts = sorts1, ...}, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

258 
Cterm {thy_ref = thy_ref2, maxidx = maxidx2, t = t2, sorts = sorts2, ...}) = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

260 
val thy_ref = Theory.merge_refs (thy_ref1, thy_ref2); 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

261 
val tsig = Sign.tsig_of (Theory.deref thy_ref); 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

262 
val (Tinsts, tinsts) = mtch tsig (t1, t2); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

264 
val sorts = Sorts.union sorts1 sorts2; 
15797  265 
fun mk_cTinsts (ixn, (S, T)) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

266 
(Ctyp {thy_ref = thy_ref, T = TVar (ixn, S)}, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

267 
Ctyp {thy_ref = thy_ref, T = T}); 
15797  268 
fun mk_ctinsts (ixn, (T, t)) = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

269 
let val T = Envir.typ_subst_TVars Tinsts T in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

273 
in (map mk_cTinsts (Vartab.dest Tinsts), map mk_ctinsts (Vartab.dest tinsts)) end; 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

274 

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

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

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

277 

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

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

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

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

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

282 
else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

284 

2509  285 

286 

574  287 
(** read cterms **) (*exception ERROR*) 
250  288 

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

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

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

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

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

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

297 

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

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

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

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

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

302 

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

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

304 

250  305 

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

308 

2509  309 

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

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

311 

11518  312 
structure Pt = Proofterm; 
313 

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

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

317 
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

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

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

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

321 
prop: term}; (*conclusion*) 
0  322 

16024  323 
fun terms_of_tpairs tpairs = List.concat (map (fn (t, u) => [t, u]) tpairs); 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

324 
val union_tpairs = gen_merge_lists (op = : (term * term) * (term * term) > bool); 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

325 

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

326 
fun attach_tpairs tpairs prop = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

327 
Logic.list_implies (map Logic.mk_equals tpairs, prop); 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

328 

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

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

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

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

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

333 
end; 
0  334 

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

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

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

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

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

339 
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

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

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

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

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

344 
prop = cterm maxidx prop} 
1517  345 
end; 
346 

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

347 
(*errors involving theorems*) 
0  348 
exception THM of string * int * thm list; 
349 

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

350 
(*attributes subsume any kind of rules or context modifiers*) 
6089  351 
type 'a attribute = 'a * thm > 'a * thm; 
352 

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

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

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

356 

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

357 

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

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

359 

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

360 
val remove_hyps = OrdList.remove Term.term_ord; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

361 
val union_hyps = OrdList.union Term.term_ord; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

362 
val eq_set_hyps = OrdList.eq_set Term.term_ord; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

363 

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

364 

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

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

366 

3994  367 
fun eq_thm (th1, th2) = 
368 
let 

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

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

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

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

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

376 
eq_set_hyps (hyps1, hyps2) andalso 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

377 
aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso 
3994  378 
prop1 aconv prop2 
379 
end; 

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

380 

16135  381 
val eq_thms = Library.equal_lists eq_thm; 
382 

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

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

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

385 

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

388 
fun tpairs_of (Thm {tpairs, ...}) = tpairs; 
0  389 

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

390 
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

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

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

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

394 

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

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

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

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

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

399 

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

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

401 
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

402 
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

403 

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

404 

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

405 
(* merge theories of cterms/thms; raise exception if incompatible *) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

406 

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

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

408 
(Cterm {thy_ref = r1, ...}) (th as Thm {thy_ref = r2, ...}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

409 
Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

410 

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

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

412 
(th1 as Thm {thy_ref = r1, ...}) (th2 as Thm {thy_ref = r2, ...}) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

413 
Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]); 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

414 

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

415 

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

416 
(* explicit transfer thm to super theory *) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

417 

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

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

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

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

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

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

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

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

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

429 

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

430 

0  431 

1238  432 
(** sort contexts of theorems **) 
433 

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

434 
fun insert_env_sorts (env as Envir.Envir {iTs, asol, ...}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

435 
Vartab.fold (fn (_, (_, t)) => Sorts.insert_term t) asol o 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

436 
Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) iTs; 
1258  437 

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

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

439 
fold (fn (t, u) => Sorts.insert_term t o Sorts.insert_term u) tpairs o 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

440 
Sorts.insert_terms hyps o Sorts.insert_term prop; 
1238  441 

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

442 
(*dangling sort constraints of a thm*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

443 
fun extra_shyps (th as Thm {shyps, ...}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

444 
Sorts.subtract (insert_thm_sorts th []) shyps; 
1238  445 

446 

7642  447 
(* strip_shyps *) 
1238  448 

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

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

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

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

454 
val present_sorts = insert_thm_sorts thm []; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

455 
val extra_shyps = Sorts.subtract present_sorts shyps; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

456 
val witnessed_shyps = Sign.witness_sorts thy present_sorts extra_shyps; 
7642  457 
in 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

459 
shyps = Sorts.subtract (map #2 witnessed_shyps) shyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

460 
hyps = hyps, tpairs = tpairs, prop = prop} 
7642  461 
end; 
1238  462 

463 

464 

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

466 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

485 

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

487 
get_axiom_i thy o NameSpace.intern (Theory.axiom_space thy); 
15672  488 

6368  489 
fun def_name name = name ^ "_def"; 
490 
fun get_def thy = get_axiom thy o def_name; 

4847  491 

1529  492 

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

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

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

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

497 

6089  498 

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

500 

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

4018  503 

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

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

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

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

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

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

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

511 
val name_of_thm = #1 o get_name_tags; 

512 
val tags_of_thm = #2 o get_name_tags; 

513 

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

0  515 

516 

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

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

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

520 
Thm {thy_ref = thy_ref, 
2386  521 
der = der, (*No derivation recorded!*) 
522 
maxidx = maxidx, 

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

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

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

525 
tpairs = map (pairself Term.compress_term) tpairs, 
2386  526 
prop = Term.compress_term prop}; 
564  527 

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

528 

2509  529 

1529  530 
(*** Meta rules ***) 
0  531 

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

532 
(** primitive rules **) 
0  533 

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

534 
(*The assumption rule A  A in a theory*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

547 
prop = prop} 
0  548 
end; 
549 

1220  550 
(*Implication introduction 
3529  551 
[A] 
552 
: 

553 
B 

1220  554 
 
555 
A ==> B 

556 
*) 

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

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

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

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

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

561 
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

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

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

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

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

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

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

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

569 
prop = implies $ A $ prop}; 
0  570 

1529  571 

1220  572 
(*Implication elimination 
573 
A ==> B A 

574 
 

575 
B 

576 
*) 

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

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

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

579 
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

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

581 
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

582 
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

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

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

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

586 
if imp = Term.implies andalso A aconv propA then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

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

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

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

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

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

596 
end; 
250  597 

1220  598 
(*Forall introduction. The Free or Var x must not be free in the hypotheses. 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

600 
: 
1220  601 
A 
602 
 

603 
!!x.A 

604 
*) 

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

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

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

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

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

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

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

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

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

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

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

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

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

617 
fun check_occs x ts = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

618 
if exists (apl (x, Logic.occs)) ts then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

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

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

625 
 _ => raise THM ("forall_intr: not a variable", 0, [th]) 
0  626 
end; 
627 

1220  628 
(*Forall elimination 
629 
!!x.A 

630 
 

631 
A[t/x] 

632 
*) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

650 

1220  651 
(* Equality *) 
0  652 

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

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

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

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

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

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

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

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

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

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

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

663 
prop = Logic.mk_equals (t, t)}; 
0  664 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

680 
 _ => raise THM ("symmetric", 0, [th])); 
0  681 

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

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

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

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

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

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

689 
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

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

691 
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

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

693 
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

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

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

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

697 
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

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

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

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

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

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

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

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

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

706 
 _ => err "premises" 
0  707 
end; 
708 

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

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

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

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

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

713 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

728 

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

729 
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

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

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

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

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

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

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

736 
prop = Logic.mk_equals (t, Pattern.eta_contract t)}; 
0  737 

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

739 
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

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

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

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

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

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

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

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

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

749 
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

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

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

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

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

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

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

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

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

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

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

760 
if exists (apl (x, Logic.occs)) ts then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

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

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

767 
 _ => raise THM ("abstract_rule: not a variable", 0, [th]) 
0  768 
end; 
769 

770 
(*The combination rule 

3529  771 
f == g t == u 
772 
 

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

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

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

777 
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

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

779 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

800 
 _ => raise THM ("combination: premises", 0, [th1, th2]) 
0  801 
end; 
802 

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

803 
(*Equality introduction 
3529  804 
A ==> B B ==> A 
805 
 

806 
A == B 

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

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

810 
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

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

812 
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

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

814 
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

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

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

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

818 
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

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

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

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

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

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

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

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

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

827 
 _ => err "premises" 
1529  828 
end; 
829 

830 
(*The equal propositions rule 

3529  831 
A == B A 
1529  832 
 
833 
B 

834 
*) 

835 
fun equal_elim th1 th2 = 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

853 
else err "not equal" 
1529  854 
 _ => err"major premise" 
855 
end; 

0  856 

1220  857 

858 

0  859 
(**** Derived rules ****) 
860 

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

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

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

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

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

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

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

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

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

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

872 
(*remove trivial tpairs, of the form t==t*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

873 
> List.filter (not o op aconv); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

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

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

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

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

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

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

884 

0  885 

886 
(*Instantiation of Vars 

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

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

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

889 
A[t1/v1, ...., tn/vn] 
1220  890 
*) 
0  891 

6928  892 
local 
893 

0  894 
(*Check that all the terms are Vars and are distinct*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

895 
fun instl_ok ts = forall is_Var ts andalso null (findrep ts); 
0  896 

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

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

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

0  900 
(*For instantiate: process pair of cterms, merge theories*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

901 
fun add_ctpair ((ct, cu), (thy_ref, tpairs)) = 
6928  902 
let 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

903 
val Cterm {thy_ref = thy_reft, t = t, T = T, ...} = ct 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

904 
and Cterm {thy_ref = thy_refu, t = u, T = U, ...} = cu; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

905 
val thy_ref_merged = Theory.merge_refs (thy_ref, Theory.merge_refs (thy_reft, thy_refu)); 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

906 
val thy_merged = Theory.deref thy_ref_merged; 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

908 
if T = U then (thy_ref_merged, (t, u) :: tpairs) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

909 
else raise TYPE (Pretty.string_of (Pretty.block 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

910 
[Pretty.str "instantiate: type conflict", 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

911 
Pretty.fbrk, pretty_typing thy_merged t T, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

912 
Pretty.fbrk, pretty_typing thy_merged u U]), [T,U], [t,u]) 
0  913 
end; 
914 

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

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

916 
((Ctyp {T = T as TVar (_, S), thy_ref = thy_refT}, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

917 
Ctyp {T = U, thy_ref = thy_refU}), (thy_ref, vTs)) = 
15797  918 
let 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

919 
val thy_ref_merged = Theory.merge_refs 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

920 
(thy_ref, Theory.merge_refs (thy_refT, thy_refU)); 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

921 
val thy_merged = Theory.deref thy_ref_merged; 
15797  922 
in 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

923 
if Type.of_sort (Sign.tsig_of thy_merged) (U, S) then 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

924 
(thy_ref_merged, (T, U) :: vTs) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

925 
else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy_merged S, [U], []) 
15797  926 
end 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

927 
 add_ctyp ((Ctyp {T, thy_ref}, _), _) = 
15797  928 
raise TYPE (Pretty.string_of (Pretty.block 
929 
[Pretty.str "instantiate: not a type variable", 

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

930 
Pretty.fbrk, Sign.pretty_typ (Theory.deref thy_ref) T]), [T], []); 
0  931 

6928  932 
in 
933 

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

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

936 
Does NOT normalize the resulting theorem!*) 
1529  937 
fun instantiate ([], []) th = th 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

938 
 instantiate (vcTs, ctpairs) th = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

941 
val (newthy_ref, tpairs) = foldr add_ctpair (thy_ref, []) ctpairs; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

942 
val (newthy_ref, vTs) = foldr add_ctyp (newthy_ref, []) vcTs; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

943 
fun subst t = subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

945 
val newdpairs = map (pairself subst) dpairs; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

949 
maxidx = maxidx_of_terms (newprop :: terms_of_tpairs newdpairs), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

951 
> fold (Sorts.insert_typ o #2) vTs 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

952 
> fold (Sorts.insert_term o #2) tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

957 
if not (instl_ok (map #1 tpairs)) then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

958 
raise THM ("instantiate: variables not distinct", 0, [th]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

959 
else if not (null (findrep (map #1 vTs))) then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

960 
raise THM ("instantiate: type variables not distinct", 0, [th]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

961 
else newth 
0  962 
end 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

965 
end; 

966 

0  967 

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

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

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

970 
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

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

972 
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

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

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

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

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

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

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

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

980 
prop = implies $ A $ A}; 
0  981 

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

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

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

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

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

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

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

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

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

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

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

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

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

996 

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

997 

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

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

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

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

1004 
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

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

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

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

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

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

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

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

1012 
prop = prop3}, al) 
0  1013 
end; 
1014 

12500  1015 
val varifyT = #1 o varifyT' []; 
6786  1016 

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

1018 
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

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

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

1022 
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

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

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

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

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

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

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

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

1030 
prop = prop3} 
1220  1031 
end; 
0  1032 

1033 

1034 
(*** Inference rules for tactics ***) 

1035 

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

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

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

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

1040 
 _ => raise THM("dest_state", i, [state])) 
0  1041 
handle TERM _ => raise THM("dest_state", i, [state]); 
1042 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1060 
prop = Logic.list_implies (map lift_all As, lift_all B)} 
0  1061 
end; 
1062 

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

1063 
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

1064 
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

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

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

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

1068 
der = Pt.infer_derivs' (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (incr_tvar i)) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

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

1074 

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

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

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

1078 
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

1079 
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

1080 
fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

1092 
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

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

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

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

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

1097 
 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

1098 
(Seq.mapp (newth n) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

1101 
in addprfs (Logic.assum_pairs (~1, Bi)) 1 end; 
0  1102 

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

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

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

1107 
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

1108 
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

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

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

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

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

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

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

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

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

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

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

1119 
prop = Logic.list_implies (Bs, C)}) 
0  1120 
end; 
1121 

1122 

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

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

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

1126 
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

1127 
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

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

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

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

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

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

1133 
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

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

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

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

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

1138 
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

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

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

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

1142 
der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

1147 
prop = Logic.list_implies (Bs @ [Bi'], C)} 
2671  1148 
end; 
1149 

1150 

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

1151 
(*Rotates a rule's premises to the left by k, leaving the first j premises 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1152 
unchanged. Does nothing if k=0 or if k equals nj, where n is the 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1153 
number of premises. Useful with etac and underlies tactic/defer_tac*) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

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

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

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

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

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

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

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

1161 
handle Subscript => raise THM ("permute_prems: j", j, [rl]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

1163 
val m = if k < 0 then n_j + k else k; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

1168 
in Logic.list_implies (fixed_prems @ qs @ ps, concl) end 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

1172 
der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

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

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

1179 

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

1180 

0  1181 
(** User renaming of parameters in a subgoal **) 
1182 

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

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

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

1186 
preceding parameters may be renamed to make all params distinct.*) 

1187 
fun rename_params_rule (cs, i) state = 

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

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

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

1190 
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

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

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

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

1194 
if short < 0 then error "More names than abstractions!" 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

1196 
val freenames = map (#1 o dest_Free) (term_frees Bi); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

1200 
c :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ c); state) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

1203 
a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); state) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

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

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

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

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

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

1211 
prop = Logic.list_implies (Bs @ [newBi], C)}) 
0  1212 
end; 
1213 

12982  1214 

0  1215 
(*** Preservation of bound variable names ***) 
1216 

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

1217 
fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
12982  1218 
(case Term.rename_abs pat obj prop of 
15531  1219 
NONE => thm 
1220 
 SOME prop' => Thm 

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

1221 
{thy_ref = thy_ref, 
12982  1222 
der = der, 
1223 
maxidx = maxidx, 

1224 
hyps = hyps, 

1225 
shyps = shyps, 

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

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

1228 

0  1229 

250  1230 
(* strip_apply f A(,B) strips off all assumptions/parameters from A 
0  1231 
introduced by lifting over B, and applies f to remaining part of A*) 
1232 
fun strip_apply f = 

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

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

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

1237 
 strip(A,_) = f A 

0  1238 
in strip end; 
1239 

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

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

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

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

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

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

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

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

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

1250 
(case assoc(al,x) of 

15531  1251 
SOME(y) => if x mem_string vids orelse y mem_string vids then t 
250  1252 
else Var((y,i),T) 
15531  1253 
 NONE=> t) 
0  1254 
 rename(Abs(x,T,t)) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1255 
Abs (if_none (assoc_string (al, x)) x, T, rename t) 
0  1256 
 rename(f$t) = rename f $ rename t 
1257 
 rename(t) = t; 

250  1258 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1259 
in strip_ren end; 
1260 

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

1262 
fun rename_bvars(dpairs, tpairs, B) = 

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

1263 
rename_bvs(foldr Term.match_bvars [] dpairs, dpairs, tpairs, B); 
0  1264 

1265 

1266 
(*** RESOLUTION ***) 

1267 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1268 
(** Lifting optimizations **) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1269 

0  1270 
(*strip off pairs of assumptions/parameters in parallel  they are 
1271 
identical because of lifting*) 

250  1272 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1273 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1274 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1275 
Const("all",_)$Abs(_,_,t2)) = 
0  1276 
let val (B1,B2) = strip_assums2 (t1,t2) 
1277 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1278 
 strip_assums2 BB = BB; 

1279 

1280 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1281 
(*Faster normalization: skip assumptions that were lifted over*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1282 
fun norm_term_skip env 0 t = Envir.norm_term env t 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1283 
 norm_term_skip env n (Const("all",_)$Abs(a,T,t)) = 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1284 
let val Envir.Envir{iTs, ...} = env 
15797  1285 
val T' = Envir.typ_subst_TVars iTs T 
1238  1286 
(*Must instantiate types of parameters because they are flattened; 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1287 
this could be a NEW parameter*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1288 
in all T' $ Abs(a, T', norm_term_skip env n t) end 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1289 
 norm_term_skip env n (Const("==>", _) $ A $ B) = 
1238  1290 
implies $ A $ norm_term_skip env (n1) B 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1291 
 norm_term_skip env n t = error"norm_term_skip: too few assumptions??"; 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1292 

479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1293 

0  1294 
(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) 
250  1295 
Unifies B with Bi, replacing subgoal i (1 <= i <= n) 
0  1296 
If match then forbid instantiations in proof state 
1297 
If lifted then shorten the dpair using strip_assums2. 

1298 
If eres_flg then simultaneously proves A1 by assumption. 

250  1299 
nsubgoal is the number of new subgoals (written m above). 
0  1300 
Curried so that resolution calls dest_state only once. 
1301 
*) 

4270  1302 
local exception COMPOSE 
0  1303 
in 
250  1304 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1305 
(eres_flg, orule, nsubgoal) = 
1529  1306 
let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1307 
and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1308 
tpairs=rtpairs, prop=rprop,...} = orule 
1529  1309 
(*How many hyps to skip over during normalization*) 
1238  1310 
and nlift = Logic.count_prems(strip_all_body Bi, 
1311 
if eres_flg then ~1 else 0) 

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

1312 
val thy_ref = merge_thys2 state orule; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1313 
val thy = Theory.deref thy_ref; 
0  1314 
(** Add new theorem with prop = '[ Bs; As ] ==> C' to thq **) 
11518  1315 
fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = 
250  1316 
let val normt = Envir.norm_term env; 
1317 
(*perform minimal copying here by examining env*) 

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

1318 
val (ntpairs, normp) = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1319 
if Envir.is_empty env then (tpairs, (Bs @ As, C)) 
250  1320 
else 
1321 
let val ntps = map (pairself normt) tpairs 

2147  1322 
in if Envir.above (smax, env) then 
1238  1323 
(*no assignments in state; normalize the rule only*) 
1324 
if lifted 

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

1325 
then (ntps, (Bs @ map (norm_term_skip env nlift) As, C)) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1326 
else (ntps, (Bs @ map normt As, C)) 
1529  1327 
else if match then raise COMPOSE 
250  1328 
else (*normalize the new rule fully*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1329 
(ntps, (map normt (Bs @ As), normt C)) 
250  1330 
end 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

1332 
Thm{thy_ref = thy_ref, 
11518
5f2616a1c10a
Replaced old derivations by proof terms.
berghof&# 