author  wenzelm 
Fri, 17 Jun 2005 18:33:08 +0200  
changeset 16425  2427be27cc60 
parent 16352  d7f9978e5752 
child 16601  ee8eefade568 
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 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

23 
val rep_cterm: cterm > {thy: theory, sign: theory, t: term, T: typ, maxidx: int} 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

24 
val crep_cterm: cterm > {thy: theory, sign: theory, t: term, T: ctyp, maxidx: int} 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

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

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

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

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

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

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

36 
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

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

38 
> cterm list * (indexname * typ)list 
1160  39 

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

40 
type tag (* = string * string list *) 
1529  41 

1160  42 
(*meta theorems*) 
43 
type thm 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

82 
(*meta rules*) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

104 
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

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

106 
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

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

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

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

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

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

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

114 
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

115 
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

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

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

6089  120 
signature THM = 
121 
sig 

122 
include BASIC_THM 

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

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

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

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

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

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

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

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

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

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

132 
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

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

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

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

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

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

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

139 
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

140 
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

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

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

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

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

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

149 

250  150 
(** certified types **) 
151 

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

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

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

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

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

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

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

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

159 

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

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

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

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

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

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

166 
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

167 

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

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

169 
map (fn T => Ctyp {thy_ref = thy_ref, T = T}) Ts 
15087  170 
 dest_ctyp ct = [ct]; 
171 

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

172 

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

173 

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

175 

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

176 
(*certified terms with checked typ and maxidx of Vars/TVars*) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

177 

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

178 
datatype cterm = Cterm of {thy_ref: theory_ref, t: term, T: typ, maxidx: int}; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

179 

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

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

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

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

183 

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

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

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

186 
{thy = thy, sign = thy, t = t, T = Ctyp {thy_ref = thy_ref, T = T}, maxidx = maxidx} 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

188 

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

189 
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

190 
val sign_of_cterm = theory_of_cterm; 
9461  191 

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

193 

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

194 
fun ctyp_of_term (Cterm {thy_ref, T, ...}) = Ctyp {thy_ref = thy_ref, T = T}; 
2671  195 

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

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

197 
let val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

198 
in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx} 
1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

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

200 

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

201 

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

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

203 

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

204 
(*Destruct application in cterms*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

208 
case typeA of Type("fun",[S,T]) => S 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

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

211 
(Cterm {thy_ref=thy_ref, maxidx=maxidx, t=A, T=typeA}, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

215 

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

216 
(*Destruct abstraction in cterms*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

218 
let val (y,N) = variant_abs (if_none a x, ty, M) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

219 
in (Cterm {thy_ref = thy_ref, T = ty, maxidx = 0, t = Free(y,ty)}, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

223 

2147  224 
(*Makes maxidx precise: it is often too big*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

226 
if maxidx = ~1 then ct 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

228 

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

229 
(*Form cterm out of a function and an argument*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

230 
fun capply (Cterm {t=f, thy_ref=thy_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1}) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

231 
(Cterm {t=x, thy_ref=thy_ref2, T, maxidx=maxidx2}) = 
8291  232 
if T = dty then 
15797  233 
Cterm{t = f $ x, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

234 
thy_ref=Theory.merge_refs(thy_ref1,thy_ref2), T=rty, 
8291  235 
maxidx=Int.max(maxidx1, maxidx2)} 
1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

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

237 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  238 

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

239 
fun cabs (Cterm {t=t1, thy_ref=thy_ref1, T=T1, maxidx=maxidx1}) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

240 
(Cterm {t=t2, thy_ref=thy_ref2, T=T2, maxidx=maxidx2}) = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

241 
Cterm {t = lambda t1 t2, thy_ref = Theory.merge_refs (thy_ref1,thy_ref2), 
15264
a881ad2e9edc
Changed function cabs to also allow abstraction over Vars.
berghofe
parents:
15087
diff
changeset

242 
T = T1 > T2, maxidx=Int.max(maxidx1, maxidx2)} 
a881ad2e9edc
Changed function cabs to also allow abstraction over Vars.
berghofe
parents:
15087
diff
changeset

243 
handle TERM _ => raise CTERM "cabs: first arg is not a variable"; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

244 

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

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

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

247 
(Cterm {thy_ref = thy_ref1, maxidx = maxidx1, t = t1, ...}, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

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

253 
val maxidx = Int.max (maxidx1, maxidx2); 
15797  254 
fun mk_cTinsts (ixn, (S, T)) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

256 
Ctyp {thy_ref = thy_ref, T = T}); 
15797  257 
fun mk_ctinsts (ixn, (T, t)) = 
258 
let val T = Envir.typ_subst_TVars Tinsts T 

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

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

260 
(Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = Var (ixn, T)}, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

262 
end; 
15797  263 
in (map mk_cTinsts (Vartab.dest Tinsts), 
264 
map mk_ctinsts (Vartab.dest tinsts)) 

265 
end; 

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

266 

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

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

268 
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

269 

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

270 
(*Incrementing indexes*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

272 
if i < 0 then raise CTERM "negative increment" else 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

273 
if i = 0 then ct else 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

274 
Cterm {thy_ref = thy_ref, maxidx = maxidx + i, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

275 
t = Logic.incr_indexes ([], i) t, T = Term.incr_tvar i T}; 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

276 

2509  277 

278 

574  279 
(** read cterms **) (*exception ERROR*) 
250  280 

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

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

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

284 
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

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

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

289 

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

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

291 
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

292 
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

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

294 

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

295 
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

296 

250  297 

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

300 

2509  301 

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

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

303 

11518  304 
structure Pt = Proofterm; 
305 

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

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

309 
maxidx: int, (*maximum index of any Var or TVar*) 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

310 
shyps: sort list, (*sort hypotheses*) 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

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

313 
prop: term}; (*conclusion*) 
0  314 

16024  315 
fun terms_of_tpairs tpairs = List.concat (map (fn (t, u) => [t, u]) tpairs); 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

316 

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

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

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

319 

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

320 
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

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

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

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

324 
end; 
0  325 

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

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

327 
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

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

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

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

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

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

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

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

335 
prop = cterm maxidx prop} 
1517  336 
end; 
337 

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

338 
(*errors involving theorems*) 
0  339 
exception THM of string * int * thm list; 
340 

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

341 
(*attributes subsume any kind of rules or context modifiers*) 
6089  342 
type 'a attribute = 'a * thm > 'a * thm; 
343 

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

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

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

347 

3994  348 
fun eq_thm (th1, th2) = 
349 
let 

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

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

352 
val {thy = thy2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = 
9031  353 
rep_thm th2; 
3994  354 
in 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

355 
(subthy (thy1, thy2) orelse subthy (thy2, thy1)) andalso 
14791  356 
Sorts.eq_set_sort (shyps1, shyps2) andalso 
3994  357 
aconvs (hyps1, hyps2) andalso 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

358 
aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso 
3994  359 
prop1 aconv prop2 
360 
end; 

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

361 

16135  362 
val eq_thms = Library.equal_lists eq_thm; 
363 

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

364 
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

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

366 

12803  367 
fun prop_of (Thm {prop, ...}) = prop; 
13528  368 
fun proof_of (Thm {der = (_, proof), ...}) = proof; 
0  369 

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

370 
(*merge theories of two theorems; raise exception if incompatible*) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

373 
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

374 

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

375 
(*transfer thm to super theory (nondestructive)*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

378 
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

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

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

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

383 
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

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

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

387 

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

388 
(*maps objectrule to tpairs*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

389 
fun tpairs_of (Thm {tpairs, ...}) = tpairs; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

390 

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

391 
(*maps objectrule to premises*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

392 
fun prems_of (Thm {prop, ...}) = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

393 
Logic.strip_imp_prems prop; 
0  394 

395 
(*counts premises in a rule*) 

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

396 
fun nprems_of (Thm {prop, ...}) = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

397 
Logic.count_prems (prop, 0); 
0  398 

8299  399 
fun major_prem_of thm = 
400 
(case prems_of thm of 

11692  401 
prem :: _ => Logic.strip_assums_concl prem 
8299  402 
 [] => raise THM ("major_prem_of: rule with no premises", 0, [thm])); 
403 

7534  404 
fun no_prems thm = nprems_of thm = 0; 
405 

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

406 
(*maps objectrule to conclusion*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

407 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  408 

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

409 
(*the statement of any thm is a cterm*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

410 
fun cprop_of (Thm {thy_ref, maxidx, prop, ...}) = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

411 
Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop}; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

412 

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

413 

0  414 

1238  415 
(** sort contexts of theorems **) 
416 

417 
(* basic utils *) 

418 

2163  419 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  420 
to improve efficiency a bit*) 
421 

422 
fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss) 

14791  423 
 add_typ_sorts (TFree (_, S), Ss) = Sorts.ins_sort(S,Ss) 
424 
 add_typ_sorts (TVar (_, S), Ss) = Sorts.ins_sort(S,Ss) 

1238  425 
and add_typs_sorts ([], Ss) = Ss 
426 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

427 

428 
fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss) 

429 
 add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss) 

430 
 add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss) 

431 
 add_term_sorts (Bound _, Ss) = Ss 

2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

432 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  433 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
434 

435 
fun add_terms_sorts ([], Ss) = Ss 

2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

436 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  437 

15797  438 
fun env_codT (Envir.Envir {iTs, ...}) = map (snd o snd) (Vartab.dest iTs); 
1258  439 

8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
8299
diff
changeset

440 
fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) = 
15797  441 
Vartab.foldl (add_term_sorts o swap o apsnd (snd o snd)) 
442 
(Vartab.foldl (add_typ_sorts o swap o apsnd (snd o snd)) (Ss, iTs), asol); 

1258  443 

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

444 
fun add_insts_sorts ((iTs, is), Ss) = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

445 
add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss)); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

446 

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

447 
fun add_thm_sorts (Thm {hyps, tpairs, prop, ...}, Ss) = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

448 
add_terms_sorts (hyps @ terms_of_tpairs tpairs, add_term_sorts (prop, Ss)); 
1238  449 

450 
fun add_thms_shyps ([], Ss) = Ss 

451 
 add_thms_shyps (Thm {shyps, ...} :: ths, Ss) = 

14791  452 
add_thms_shyps (ths, Sorts.union_sort (shyps, Ss)); 
1238  453 

454 

455 
(*get 'dangling' sort constraints of a thm*) 

456 
fun extra_shyps (th as Thm {shyps, ...}) = 

14791  457 
Sorts.rems_sort (shyps, add_thm_sorts (th, [])); 
1238  458 

459 

460 
(* fix_shyps *) 

461 

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

462 
val all_sorts_nonempty = is_some o Sign.universal_witness o Theory.deref; 
7642  463 

1238  464 
(*preserve sort contexts of rule premises and substituted types*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

465 
fun fix_shyps thms Ts (thm as Thm {thy_ref, der, maxidx, hyps, tpairs, prop, ...}) = 
7642  466 
Thm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

467 
{thy_ref = thy_ref, 
7642  468 
der = der, (*no new derivation, as other rules call this*) 
469 
maxidx = maxidx, 

470 
shyps = 

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

471 
if all_sorts_nonempty thy_ref then [] 
7642  472 
else add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

473 
hyps = hyps, tpairs = tpairs, prop = prop} 
1238  474 

475 

7642  476 
(* strip_shyps *) 
1238  477 

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

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

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

482 
val thy = Theory.deref thy_ref; 
7642  483 
val present_sorts = add_thm_sorts (thm, []); 
14791  484 
val extra_shyps = Sorts.rems_sort (shyps, present_sorts); 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

487 
Thm {thy_ref = thy_ref, der = der, maxidx = maxidx, 
14791  488 
shyps = Sorts.rems_sort (shyps, map #2 witnessed_shyps), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

489 
hyps = hyps, tpairs = tpairs, prop = prop} 
7642  490 
end; 
1238  491 

492 

493 

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

495 

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

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

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

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

500 
Symtab.lookup (#2 (#axioms (Theory.rep_theory thy)), name) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

501 
> Option.map (fn t => 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

502 
fix_shyps [] [] 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

503 
(Thm {thy_ref = Theory.self_ref thy, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

504 
der = Pt.infer_derivs' I (false, Pt.axm_proof name t), 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

505 
maxidx = maxidx_of_term t, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

507 
hyps = [], 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

508 
tpairs = [], 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

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

515 

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

517 
get_axiom_i thy o NameSpace.intern (Theory.axiom_space thy); 
15672  518 

6368  519 
fun def_name name = name ^ "_def"; 
520 
fun get_def thy = get_axiom thy o def_name; 

4847  521 

1529  522 

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

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

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

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

527 

6089  528 

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

530 

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

4018  533 

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

534 
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

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

536 
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

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

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

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

541 
val name_of_thm = #1 o get_name_tags; 

542 
val tags_of_thm = #2 o get_name_tags; 

543 

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

0  545 

546 

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

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

549 
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

550 
Thm {thy_ref = thy_ref, 
2386  551 
der = der, (*No derivation recorded!*) 
552 
maxidx = maxidx, 

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

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

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

555 
tpairs = map (pairself Term.compress_term) tpairs, 
2386  556 
prop = Term.compress_term prop}; 
564  557 

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

558 

2509  559 

1529  560 
(*** Meta rules ***) 
0  561 

1220  562 
(** 'primitive' rules **) 
563 

564 
(*discharge all assumptions t from ts*) 

0  565 
val disch = gen_rem (op aconv); 
566 

1220  567 
(*The assumption rule AA in a theory*) 
5344  568 
fun assume raw_ct : thm = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

569 
let val ct as Cterm {thy_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct 
250  570 
in if T<>propT then 
571 
raise THM("assume: assumptions must have type prop", 0, []) 

0  572 
else if maxidx <> ~1 then 
250  573 
raise THM("assume: assumptions may not contain scheme variables", 
574 
maxidx, []) 

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

575 
else Thm{thy_ref = thy_ref, 
11518  576 
der = Pt.infer_derivs' I (false, Pt.Hyp prop), 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

577 
maxidx = ~1, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

578 
shyps = add_term_sorts(prop,[]), 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

579 
hyps = [prop], 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

580 
tpairs = [], 
2386  581 
prop = prop} 
0  582 
end; 
583 

1220  584 
(*Implication introduction 
3529  585 
[A] 
586 
: 

587 
B 

1220  588 
 
589 
A ==> B 

590 
*) 

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

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

592 
let val Cterm {thy_ref=thy_refA, t=A, T, maxidx=maxidxA} = cA 
0  593 
in if T<>propT then 
250  594 
raise THM("implies_intr: assumptions must have type prop", 0, [thB]) 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

596 
Thm{thy_ref = Theory.merge_refs (thy_ref,thy_refA), 
11518  597 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
2386  598 
maxidx = Int.max(maxidxA, maxidx), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

599 
shyps = add_term_sorts (A, shyps), 
2386  600 
hyps = disch(hyps,A), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

602 
prop = implies$A$prop} 
0  603 
handle TERM _ => 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

604 
raise THM("implies_intr: incompatible theories", 0, [thB]) 
0  605 
end; 
606 

1529  607 

1220  608 
(*Implication elimination 
609 
A ==> B A 

610 
 

611 
B 

612 
*) 

0  613 
fun implies_elim thAB thA : thm = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

614 
let val Thm{maxidx=maxA, der=derA, hyps=hypsA, shyps=shypsA, tpairs=tpairsA, prop=propA, ...} = thA 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

615 
and Thm{der, maxidx, hyps, shyps, tpairs, prop, ...} = thAB; 
250  616 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 
0  617 
in case prop of 
250  618 
imp$A$B => 
619 
if imp=implies andalso A aconv propA 

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

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

621 
Thm{thy_ref= merge_thm_thys (thAB, thA), 
11612  622 
der = Pt.infer_derivs (curry Pt.%%) der derA, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

623 
maxidx = Int.max(maxA,maxidx), 
14791  624 
shyps = Sorts.union_sort (shypsA, shyps), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

625 
hyps = union_term(hypsA,hyps), (*dups suppressed*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

626 
tpairs = tpairsA @ tpairs, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

627 
prop = B} 
250  628 
else err("major premise") 
629 
 _ => err("major premise") 

0  630 
end; 
250  631 

1220  632 
(*Forall introduction. The Free or Var x must not be free in the hypotheses. 
633 
A 

634 
 

635 
!!x.A 

636 
*) 

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

637 
fun forall_intr cx (th as Thm{thy_ref,der,maxidx,hyps,tpairs,prop,...}) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

638 
let val x = term_of cx; 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

639 
fun result a T = fix_shyps [th] [] 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

640 
(Thm{thy_ref = thy_ref, 
11518  641 
der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, 
2386  642 
maxidx = maxidx, 
643 
shyps = [], 

644 
hyps = hyps, 

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

645 
tpairs = tpairs, 
2386  646 
prop = all(T) $ Abs(a, T, abstract_over (x,prop))}) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

647 
fun check_occs x ts = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

648 
if exists (apl(x, Logic.occs)) ts 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

649 
then raise THM("forall_intr: variable free in assumptions", 0, [th]) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

650 
else () 
0  651 
in case x of 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

652 
Free(a,T) => (check_occs x (hyps @ terms_of_tpairs tpairs); result a T) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

653 
 Var((a,_),T) => (check_occs x (terms_of_tpairs tpairs); result a T) 
0  654 
 _ => raise THM("forall_intr: not a variable", 0, [th]) 
655 
end; 

656 

1220  657 
(*Forall elimination 
658 
!!x.A 

659 
 

660 
A[t/x] 

661 
*) 

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

662 
fun forall_elim ct (th as Thm{thy_ref,der,maxidx,hyps,tpairs,prop,...}) : thm = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

663 
let val Cterm {thy_ref=thy_reft, t, T, maxidx=maxt} = ct 
0  664 
in case prop of 
2386  665 
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => 
666 
if T<>qary then 

667 
raise THM("forall_elim: type mismatch", 0, [th]) 

15797  668 
else fix_shyps [th] [] 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

669 
(Thm{thy_ref= Theory.merge_refs(thy_ref,thy_reft), 
15531  670 
der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der, 
2386  671 
maxidx = Int.max(maxidx, maxt), 
672 
shyps = [], 

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

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

674 
tpairs = tpairs, 
2386  675 
prop = betapply(A,t)}) 
2147  676 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  677 
end 
678 
handle TERM _ => 

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

679 
raise THM("forall_elim: incompatible theories", 0, [th]); 
0  680 

681 

1220  682 
(* Equality *) 
0  683 

684 
(*The reflexivity rule: maps t to the theorem t==t *) 

250  685 
fun reflexive ct = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

687 
in Thm{thy_ref= thy_ref, 
11518  688 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

689 
shyps = add_term_sorts (t, []), 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

690 
hyps = [], 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

692 
tpairs = [], 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

693 
prop = Logic.mk_equals(t,t)} 
0  694 
end; 
695 

696 
(*The symmetry rule 

1220  697 
t==u 
698 
 

699 
u==t 

700 
*) 

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

701 
fun symmetric (th as Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) = 
0  702 
case prop of 
11518  703 
(eq as Const("==", Type (_, [T, _]))) $ t $ u => 
1238  704 
(*no fix_shyps*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

705 
Thm{thy_ref = thy_ref, 
11518  706 
der = Pt.infer_derivs' Pt.symmetric der, 
2386  707 
maxidx = maxidx, 
708 
shyps = shyps, 

709 
hyps = hyps, 

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

710 
tpairs = tpairs, 
2386  711 
prop = eq$u$t} 
0  712 
 _ => raise THM("symmetric", 0, [th]); 
713 

714 
(*The transitive rule 

1220  715 
t1==u u==t2 
716 
 

717 
t1==t2 

718 
*) 

0  719 
fun transitive th1 th2 = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

720 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, tpairs=tpairs1, prop=prop1,...} = th1 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

721 
and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, tpairs=tpairs2, prop=prop2,...} = th2; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

722 
fun err msg = raise THM("transitive: "^msg, 0, [th1,th2]) 
0  723 
in case (prop1,prop2) of 
11518  724 
((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) => 
1634  725 
if not (u aconv u') then err"middle term" 
15797  726 
else 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

727 
Thm{thy_ref= merge_thm_thys (th1, th2), 
11518  728 
der = Pt.infer_derivs (Pt.transitive u T) der1 der2, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

729 
maxidx = Int.max(max1,max2), 
14791  730 
shyps = Sorts.union_sort (shyps1, shyps2), 
2386  731 
hyps = union_term(hyps1,hyps2), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

732 
tpairs = tpairs1 @ tpairs2, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

733 
prop = eq$t1$t2} 
0  734 
 _ => err"premises" 
735 
end; 

736 

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

737 
(*Betaconversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

740 
fun beta_conversion full ct = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

741 
let val Cterm {thy_ref, t, T, maxidx} = ct 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

743 
{thy_ref = thy_ref, 
11518  744 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

745 
maxidx = maxidx, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

746 
shyps = add_term_sorts (t, []), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

747 
hyps = [], 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

748 
tpairs = [], 
10486  749 
prop = Logic.mk_equals (t, if full then Envir.beta_norm t 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

750 
else case t of 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

751 
Abs(_, _, bodt) $ u => subst_bound (u, bodt) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

752 
 _ => raise THM ("beta_conversion: not a redex", 0, []))} 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

754 

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

755 
fun eta_conversion ct = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

756 
let val Cterm {thy_ref, t, T, maxidx} = ct 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

758 
{thy_ref = thy_ref, 
11518  759 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

760 
maxidx = maxidx, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

761 
shyps = add_term_sorts (t, []), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

762 
hyps = [], 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

763 
tpairs = [], 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

764 
prop = Logic.mk_equals (t, Pattern.eta_contract t)} 
0  765 
end; 
766 

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

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

1220  769 
t == u 
770 
 

771 
%x.t == %x.u 

772 
*) 

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

773 
fun abstract_rule a cx (th as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs,prop}) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

774 
let val x = term_of cx; 
250  775 
val (t,u) = Logic.dest_equals prop 
776 
handle TERM _ => 

777 
raise THM("abstract_rule: premise not an equality", 0, [th]) 

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

778 
fun result T = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

779 
Thm{thy_ref = thy_ref, 
11518  780 
der = Pt.infer_derivs' (Pt.abstract_rule x a) der, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

782 
shyps = add_typ_sorts (T, shyps), 
2386  783 
hyps = hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

784 
tpairs = tpairs, 
2386  785 
prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

786 
Abs(a, T, abstract_over (x,u)))} 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

787 
fun check_occs x ts = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

788 
if exists (apl(x, Logic.occs)) ts 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

789 
then raise THM("abstract_rule: variable free in assumptions", 0, [th]) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

790 
else () 
0  791 
in case x of 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

792 
Free(_,T) => (check_occs x (hyps @ terms_of_tpairs tpairs); result T) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

793 
 Var(_,T) => (check_occs x (terms_of_tpairs tpairs); result T) 
0  794 
 _ => raise THM("abstract_rule: not a variable", 0, [th]) 
795 
end; 

796 

797 
(*The combination rule 

3529  798 
f == g t == u 
799 
 

800 
f(t) == g(u) 

1220  801 
*) 
0  802 
fun combination th1 th2 = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

803 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

804 
tpairs=tpairs1, prop=prop1,...} = th1 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

805 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

806 
tpairs=tpairs2, prop=prop2,...} = th2 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

807 
fun chktypes fT tT = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

809 
Type("fun",[T1,T2]) => 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

810 
if T1 <> tT then 
2386  811 
raise THM("combination: types", 0, [th1,th2]) 
812 
else () 

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

813 
 _ => raise THM("combination: not function type", 0, 
2386  814 
[th1,th2])) 
1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

815 
in case (prop1,prop2) of 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

816 
(Const ("==", Type ("fun", [fT, _])) $ f $ g, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

817 
Const ("==", Type ("fun", [tT, _])) $ t $ u) => 
15797  818 
(chktypes fT tT; 
819 
(*no fix_shyps*) 

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

820 
Thm{thy_ref = merge_thm_thys(th1,th2), 
11518  821 
der = Pt.infer_derivs 
822 
(Pt.combination f g t u fT) der1 der2, 

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

823 
maxidx = Int.max(max1,max2), 
14791  824 
shyps = Sorts.union_sort(shyps1,shyps2), 
2386  825 
hyps = union_term(hyps1,hyps2), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

826 
tpairs = tpairs1 @ tpairs2, 
15797  827 
prop = Logic.mk_equals(f$t, g$u)}) 
0  828 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
829 
end; 

830 

831 

832 
(* Equality introduction 

3529  833 
A ==> B B ==> A 
834 
 

835 
A == B 

1220  836 
*) 
0  837 
fun equal_intr th1 th2 = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

838 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

839 
tpairs=tpairs1, prop=prop1,...} = th1 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

840 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

841 
tpairs=tpairs2, prop=prop2,...} = th2; 
1529  842 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
843 
in case (prop1,prop2) of 

844 
(Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A') => 

2386  845 
if A aconv A' andalso B aconv B' 
846 
then 

847 
(*no fix_shyps*) 

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

848 
Thm{thy_ref = merge_thm_thys(th1,th2), 
11518  849 
der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, 
2386  850 
maxidx = Int.max(max1,max2), 
14791  851 
shyps = Sorts.union_sort(shyps1,shyps2), 
2386  852 
hyps = union_term(hyps1,hyps2), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

853 
tpairs = tpairs1 @ tpairs2, 
2386  854 
prop = Logic.mk_equals(A,B)} 
855 
else err"not equal" 

1529  856 
 _ => err"premises" 
857 
end; 

858 

859 

860 
(*The equal propositions rule 

3529  861 
A == B A 
1529  862 
 
863 
B 

864 
*) 

865 
fun equal_elim th1 th2 = 

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

866 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, tpairs=tpairs1, prop=prop1,...} = th1 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

867 
and Thm{der=der2, maxidx=max2, hyps=hyps2, tpairs=tpairs2, prop=prop2,...} = th2; 
1529  868 
fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2]) 
869 
in case prop1 of 

870 
Const("==",_) $ A $ B => 

871 
if not (prop2 aconv A) then err"not equal" else 

872 
fix_shyps [th1, th2] [] 

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

873 
(Thm{thy_ref= merge_thm_thys(th1,th2), 
11518  874 
der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, 
2386  875 
maxidx = Int.max(max1,max2), 
876 
shyps = [], 

877 
hyps = union_term(hyps1,hyps2), 

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

878 
tpairs = tpairs1 @ tpairs2, 
2386  879 
prop = B}) 
1529  880 
 _ => err"major premise" 
881 
end; 

0  882 

1220  883 

884 

0  885 
(**** Derived rules ****) 
886 

1503  887 
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. 
0  888 
Repeated hypotheses are discharged only once; fold cannot do this*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

889 
fun implies_intr_hyps (Thm{thy_ref, der, maxidx, shyps, hyps=A::As, tpairs, prop}) = 
1238  890 
implies_intr_hyps (*no fix_shyps*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

891 
(Thm{thy_ref = thy_ref, 
11518  892 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

893 
maxidx = maxidx, 
2386  894 
shyps = shyps, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

895 
hyps = disch(As,A), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

896 
tpairs = tpairs, 
2386  897 
prop = implies$A$prop}) 
0  898 
 implies_intr_hyps th = th; 
899 

900 
(*Smash" unifies the list of term pairs leaving no flexflex pairs. 

250  901 
Instantiates the theorem and deletes trivial tpairs. 
0  902 
Resulting sequence may contain multiple elements if the tpairs are 
903 
not all flexflex. *) 

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

904 
fun flexflex_rule (th as Thm{thy_ref, der, maxidx, hyps, tpairs, prop, ...}) = 
250  905 
let fun newthm env = 
1529  906 
if Envir.is_empty env then th 
907 
else 

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

908 
let val ntpairs = map (pairself (Envir.norm_term env)) tpairs; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

909 
val newprop = Envir.norm_term env prop; 
250  910 
(*Remove trivial tpairs, of the form t=t*) 
15570  911 
val distpairs = List.filter (not o op aconv) ntpairs 
1220  912 
in fix_shyps [th] (env_codT env) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

913 
(Thm{thy_ref = thy_ref, 
11518  914 
der = Pt.infer_derivs' (Pt.norm_proof' env) der, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

915 
maxidx = maxidx_of_terms (newprop :: 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

916 
terms_of_tpairs distpairs), 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

917 
shyps = [], 
2386  918 
hyps = hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

919 
tpairs = distpairs, 
2386  920 
prop = newprop}) 
250  921 
end; 
4270  922 
in Seq.map newthm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

923 
(Unify.smash_unifiers(Theory.deref thy_ref, Envir.empty maxidx, tpairs)) 
0  924 
end; 
925 

926 
(*Instantiation of Vars 

1220  927 
A 
928 
 

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

930 
*) 

0  931 

6928  932 
local 
933 

0  934 
(*Check that all the terms are Vars and are distinct*) 
935 
fun instl_ok ts = forall is_Var ts andalso null(findrep ts); 

936 

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

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

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

0  940 
(*For instantiate: process pair of cterms, merge theories*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

941 
fun add_ctpair ((ct,cu), (thy_ref,tpairs)) = 
6928  942 
let 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

943 
val Cterm {thy_ref=thy_reft, t=t, T= T, ...} = ct 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

945 
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

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

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

948 
if T=U then (thy_ref_merged, (t,u)::tpairs) 
6928  949 
else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

951 
Pretty.fbrk, pretty_typing thy_merged u U]), [T,U], [t,u]) 
0  952 
end; 
953 

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

954 
fun add_ctyp ((Ctyp {T = T as TVar (_, S), thy_ref = thy_refT}, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

958 
(thy_ref, Theory.merge_refs (thy_refT, thy_refU)); 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

961 
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

962 
(thy_ref_merged, (T, U) :: vTs) 
15797  963 
else raise TYPE ("Type not of sort " ^ 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

964 
Sign.string_of_sort thy_merged S, [U], []) 
15797  965 
end 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

6928  971 
in 
972 

0  973 
(*Lefttoright replacements: ctpairs = [...,(vi,ti),...]. 
974 
Instantiates distinct Vars by terms of same type. 

8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8066
diff
changeset

975 
No longer normalizes the new theorem! *) 
1529  976 
fun instantiate ([], []) th = th 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

977 
 instantiate (vcTs,ctpairs) (th as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) = 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

978 
let val (newthy_ref,tpairs) = foldr add_ctpair (thy_ref,[]) ctpairs; 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

979 
val (newthy_ref,vTs) = foldr add_ctyp (newthy_ref,[]) vcTs; 
14828  980 
fun subst t = 
15797  981 
subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t); 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

982 
val newprop = subst prop; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

983 
val newdpairs = map (pairself subst) dpairs; 
1220  984 
val newth = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

985 
(Thm{thy_ref = newthy_ref, 
11518  986 
der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

987 
maxidx = maxidx_of_terms (newprop :: 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

988 
terms_of_tpairs newdpairs), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

989 
shyps = add_insts_sorts ((vTs, tpairs), shyps), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

991 
tpairs = newdpairs, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

992 
prop = newprop}) 
250  993 
in if not(instl_ok(map #1 tpairs)) 
193  994 
then raise THM("instantiate: variables not distinct", 0, [th]) 
995 
else if not(null(findrep(map #1 vTs))) 

996 
then raise THM("instantiate: type variables not distinct", 0, [th]) 

15797  997 
else newth 
0  998 
end 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

999 
handle TERM _ => raise THM("instantiate: incompatible theories", 0, [th]) 
6928  1000 
 TYPE (msg, _, _) => raise THM (msg, 0, [th]); 
1001 

1002 
end; 

1003 

0  1004 

1005 
(*The trivial implication A==>A, justified by assume and forall rules. 

1006 
A can contain Vars, not so for assume! *) 

250  1007 
fun trivial ct : thm = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1008 
let val Cterm {thy_ref, t=A, T, maxidx} = ct 
250  1009 
in if T<>propT then 
1010 
raise THM("trivial: the term must have type prop", 0, []) 

1238  1011 
else fix_shyps [] [] 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1012 
(Thm{thy_ref = thy_ref, 
15531  1013 
der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)), 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

1015 
shyps = [], 
2386  1016 
hyps = [], 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1017 
tpairs = [], 
2386  1018 
prop = implies$A$A}) 
0  1019 
end; 
1020 

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

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

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

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

1026 
in 
1238  1027 
fix_shyps [] [] 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1028 
(Thm {thy_ref = thy_ref, 
11518  1029 
der = Pt.infer_derivs' I 
15531  1030 
(false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])), 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

1033 
hyps = [], 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

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

1037 

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

1038 

6786  1039 
(* Replace all TFrees not fixed or in the hyps by new TVars *) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

1044 
val (prop2, al) = Type.varify (prop1, tfrees); 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1045 
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) 
15797  1046 
in (*no fix_shyps*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1047 
(Thm{thy_ref = thy_ref, 
11518  1048 
der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1049 
maxidx = Int.max(0,maxidx), 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1050 
shyps = shyps, 
2386  1051 
hyps = hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1052 
tpairs = rev (map Logic.dest_equals ts), 
15797  1053 
prop = prop3}, al) 
0  1054 
end; 
1055 

12500  1056 
val varifyT = #1 o varifyT' []; 
6786  1057 

0  1058 
(* Replace all TVars by new TFrees *) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1059 
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

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

1061 
val prop1 = attach_tpairs tpairs prop; 
16287  1062 
val prop2 = Type.freeze prop1; 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1063 
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) 
1238  1064 
in (*no fix_shyps*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1065 
Thm{thy_ref = thy_ref, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1066 
der = Pt.infer_derivs' (Pt.freezeT prop1) der, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1067 
maxidx = maxidx_of_term prop2, 
2386  1068 
shyps = shyps, 
1069 
hyps = hyps, 

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

1070 
tpairs = rev (map Logic.dest_equals ts), 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1071 
prop = prop3} 
1220  1072 
end; 
0  1073 

1074 

1075 
(*** Inference rules for tactics ***) 

1076 

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

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

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

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

1081 
 _ => raise THM("dest_state", i, [state])) 
0  1082 
handle TERM _ => raise THM("dest_state", i, [state]); 
1083 

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

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

1087 
let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, thy_ref=sthy_ref,...} = state 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1088 
val (Bi::_, _) = Logic.strip_prems(i, [], sprop) 
1529  1089 
handle TERM _ => raise THM("lift_rule", i, [orule,state]) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1090 
val ct_Bi = Cterm {thy_ref=sthy_ref, maxidx=smax, T=propT, t=Bi} 
1529  1091 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

1093 
val (As, B) = Logic.strip_horn prop 
1238  1094 
in (*no fix_shyps*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1095 
Thm{thy_ref = merge_thm_thys(state,orule), 
11518  1096 
der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der, 
2386  1097 
maxidx = maxidx+smax+1, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1098 
shyps = Sorts.union_sort(sshyps,shyps), 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

1100 
tpairs = map (pairself lift_abs) tpairs, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1101 
prop = Logic.list_implies (map lift_all As, lift_all B)} 
0  1102 
end; 
1103 

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

1104 
fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1105 
if i < 0 then raise THM ("negative increment", 0, [thm]) else 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1106 
if i = 0 then thm else 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1107 
Thm {thy_ref = thy_ref, 
11518  1108 
der = Pt.infer_derivs' (Pt.map_proof_terms 
1109 
(Logic.incr_indexes ([], i)) (incr_tvar i)) der, 

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

1110 
maxidx = maxidx + i, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1111 
shyps = shyps, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

1113 
tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

1115 

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

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

1118 
let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state; 
0  1119 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
11518  1120 
fun newth n (env as Envir.Envir{maxidx, ...}, tpairs) = 
1220  1121 
fix_shyps [state] (env_codT env) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1122 
(Thm{thy_ref = thy_ref, 
11518  1123 
der = Pt.infer_derivs' 
1124 
((if Envir.is_empty env then I else (Pt.norm_proof' env)) o 

1125 
Pt.assumption_proof Bs Bi n) der, 

2386  1126 
maxidx = maxidx, 
1127 
shyps = [], 

1128 
hyps = hyps, 

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

1129 
tpairs = if Envir.is_empty env then tpairs else 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1130 
map (pairself (Envir.norm_term env)) tpairs, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1131 
prop = 
2386  1132 
if Envir.is_empty env then (*avoid wasted normalizations*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1133 
Logic.list_implies (Bs, C) 
2386  1134 
else (*normalize the new rule fully*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1135 
Envir.norm_term env (Logic.list_implies (Bs, C))}); 
11518  1136 
fun addprfs [] _ = Seq.empty 
1137 
 addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull 

1138 
(Seq.mapp (newth n) 

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

1139 
(Unify.unifiers(Theory.deref thy_ref,Envir.empty maxidx, (t,u)::tpairs)) 
11518  1140 
(addprfs apairs (n+1)))) 
15454  1141 
in addprfs (Logic.assum_pairs (~1,Bi)) 1 end; 
0  1142 

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

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

1146 
let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state; 
0  1147 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
15454  1148 
in (case find_index (op aconv) (Logic.assum_pairs (~1,Bi)) of 
11518  1149 
(~1) => raise THM("eq_assumption", 0, [state]) 
1150 
 n => fix_shyps [state] [] 

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

1151 
(Thm{thy_ref = thy_ref, 
11518  1152 
der = Pt.infer_derivs' 
1153 
(Pt.assumption_proof Bs Bi (n+1)) der, 

1154 
maxidx = maxidx, 

1155 
shyps = [], 

1156 
hyps = hyps, 

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

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

1158 
prop = Logic.list_implies (Bs, C)})) 
0  1159 
end; 
1160 

1161 

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

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

1164 
let val Thm{thy_ref,der,maxidx,hyps,prop,shyps,...} = state; 
2671  1165 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
8066
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1166 
val params = Term.strip_all_vars Bi 
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1167 
and rest = Term.strip_all_body Bi 
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1168 
val asms = Logic.strip_imp_prems rest 
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1169 
and concl = Logic.strip_imp_concl rest 
2671  1170 
val n = length asms 
11563  1171 
val m = if k<0 then n+k else k 
1172 
val Bi' = if 0=m orelse m=n then Bi 

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

1173 
else if 0<m andalso m<n 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1174 
then let val (ps,qs) = splitAt(m,asms) 
13629  1175 
in list_all(params, Logic.list_implies(qs @ ps, concl)) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

1177 
else raise THM("rotate_rule", k, [state]) 
7264  1178 
in (*no fix_shyps*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1179 
Thm{thy_ref = thy_ref, 
11563  1180 
der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

1185 
prop = Logic.list_implies (Bs @ [Bi'], C)} 
2671  1186 
end; 
1187 

1188 

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

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

1190 
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

1191 
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

1192 
fun permute_prems j k rl = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1193 
let val Thm{thy_ref,der,maxidx,hyps,tpairs,prop,shyps} = rl 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1194 
val prems = Logic.strip_imp_prems prop 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1195 
and concl = Logic.strip_imp_concl prop 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1196 
val moved_prems = List.drop(prems, j) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1197 
and fixed_prems = List.take(prems, j) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1198 
handle Subscript => raise THM("permute_prems:j", j, [rl]) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1199 
val n_j = length moved_prems 
11563  1200 
val m = if k<0 then n_j + k else k 
1201 
val prop' = if 0 = m orelse m = n_j then prop 

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

1202 
else if 0<m andalso m<n_j 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1203 
then let val (ps,qs) = splitAt(m,moved_prems) 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1204 
in Logic.list_implies(fixed_prems @ qs @ ps, concl) end 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1205 
else raise THM("permute_prems:k", k, [rl]) 
7264  1206 
in (*no fix_shyps*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1207 
Thm{thy_ref = thy_ref, 
11563  1208 
der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

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

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

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

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

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

1215 

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

1216 

0  1217 
(** User renaming of parameters in a subgoal **) 
1218 

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

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

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

1222 
preceding parameters may be renamed to make all params distinct.*) 

1223 
fun rename_params_rule (cs, i) state = 

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

1224 
let val Thm{thy_ref,der,maxidx,hyps,shyps,...} = state 
0  1225 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
1226 
val iparams = map #1 (Logic.strip_params Bi) 

1227 
val short = length iparams  length cs 

250  1228 
val newnames = 
1229 
if short<0 then error"More names than abstractions!" 

15570  1230 
else variantlist(Library.take (short,iparams), cs) @ cs 
3037
99ed078e6ae7
rename_params_rule used to check if the new name clashed with a free name in
nipkow
parents:
3012
diff
changeset

1231 
val freenames = map (#1 o dest_Free) (term_frees Bi) 
0  1232 
val newBi = Logic.list_rename_params (newnames, Bi) 
250  1233 
in 
0  1234 
case findrep cs of 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1235 
c::_ => (warning ("Can't rename. Bound variables not distinct: " ^ c); 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1236 
state) 
1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1569
diff
changeset

1237 
 [] => (case cs inter_string freenames of 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1238 
a::_ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

1240 
 [] => Thm{thy_ref = thy_ref, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

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

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

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

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

1246 
prop = Logic.list_implies (Bs @ [newBi], C)}) 
0  1247 
end; 
1248 

12982  1249 

0  1250 
(*** Preservation of bound variable names ***) 
1251 

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

1252 
fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) = 
12982  1253 
(case Term.rename_abs pat obj prop of 
15531  1254 
NONE => thm 
1255 
 SOME prop' => Thm 

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

1256 
{thy_ref = thy_ref, 
12982  1257 
der = der, 
1258 
maxidx = maxidx, 

1259 
hyps = hyps, 

1260 
shyps = shyps, 

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

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

1263 

0  1264 

250  1265 
(* strip_apply f A(,B) strips off all assumptions/parameters from A 
0  1266 
introduced by lifting over B, and applies f to remaining part of A*) 
1267 
fun strip_apply f = 

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

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

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

1272 
 strip(A,_) = f A 

0  1273 
in strip end; 
1274 

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

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

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

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

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

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

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

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

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

1285 
(case assoc(al,x) of 

15531  1286 
SOME(y) => if x mem_string vids orelse y mem_string vids then t 
250  1287 
else Var((y,i),T) 
15531  1288 
 NONE=> t) 
0  1289 
 rename(Abs(x,T,t)) = 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

1290 
Abs (if_none (assoc_string (al, x)) x, T, rename t) 
0  1291 
 rename(f$t) = rename f $ rename t 
1292 
 rename(t) = t; 

250  1293 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1294 
in strip_ren end; 
1295 

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

1297 
fun rename_bvars(dpairs, tpairs, B) = 

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

1298 
rename_bvs(foldr Term.match_bvars [] dpairs, dpairs, tpairs, B); 
0  1299 

1300 

1301 
(*** RESOLUTION ***) 

1302 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1303 
(** Lifting optimizations **) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1304 

0  1305 
(*strip off pairs of assumptions/parameters in parallel  they are 
1306 
identical because of lifting*) 

250  1307 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1308 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1309 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1310 
Const("all",_)$Abs(_,_,t2)) = 
0  1311 
let val (B1,B2) = strip_assums2 (t1,t2) 
1312 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1313 
 strip_assums2 BB = BB; 

1314 

1315 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

1317 
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

1318 
 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

1319 
let val Envir.Envir{iTs, ...} = env 
15797  1320 
val T' = Envir.typ_subst_TVars iTs T 
1238  1321 
(*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

1322 
this could be a NEW parameter*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1323 
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

1324 
 norm_term_skip env n (Const("==>", _) $ A $ B) = 