author  clasohm 
Wed, 15 Mar 1995 12:52:03 +0100  
changeset 959  35c2e5e114c4 
parent 949  83c588d6fee9 
child 979  a29142d703bc 
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 

250  6 
The abstract types "theory" and "thm". 
7 
Also "cterm" / "ctyp" (certified terms / typs under a signature). 

0  8 
*) 
9 

250  10 
signature THM = 
11 
sig 

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

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

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

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

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

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

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

18 
type theory 
0  19 
type meta_simpset 
20 
exception THM of string * int * thm list 

21 
exception THEORY of string * theory list 

22 
exception SIMPLIFIER of string * thm 

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

23 
(*certified terms/types; previously in sign.ML*) 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

24 
val cterm_of : Sign.sg > term > cterm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

25 
val ctyp_of : Sign.sg > typ > ctyp 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

26 
val read_ctyp : Sign.sg > string > ctyp 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

27 
val read_cterm : Sign.sg > string * typ > cterm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

28 
val rep_cterm : cterm > {T:typ, t:term, sign:Sign.sg, maxidx:int} 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

29 
val rep_ctyp : ctyp > {T: typ, sign: Sign.sg} 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

30 
val term_of : cterm > term 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

31 
val typ_of : ctyp > typ 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

32 
val cterm_fun : (term > term) > (cterm > cterm) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

33 
(*end of cterm/ctyp functions*) 
564  34 
local open Sign.Syntax in 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

35 
val add_classes : (class * class list) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

36 
val add_classrel : (class * class) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

37 
val add_defsort : sort > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

38 
val add_types : (string * int * mixfix) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

39 
val add_tyabbrs : (string * string list * string * mixfix) list 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

41 
val add_tyabbrs_i : (string * string list * typ * mixfix) list 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

43 
val add_arities : (string * sort list * sort) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

44 
val add_consts : (string * string * mixfix) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

45 
val add_consts_i : (string * typ * mixfix) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

46 
val add_syntax : (string * string * mixfix) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

47 
val add_syntax_i : (string * typ * mixfix) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

49 
(string * (ast list > ast)) list * 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

50 
(string * (term list > term)) list * 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

51 
(string * (term list > term)) list * 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

52 
(string * (ast list > ast)) list > theory > theory 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

53 
val add_trrules : xrule list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

54 
val add_axioms : (string * string) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

55 
val add_axioms_i : (string * term) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

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

58 
val cert_axm : Sign.sg > string * term > string * term 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

59 
val read_axm : Sign.sg > string * string > string * term 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

60 
val inferT_axm : Sign.sg > string * term > string * term 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

61 
val abstract_rule : string > cterm > thm > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

62 
val add_congs : meta_simpset * thm list > meta_simpset 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

63 
val add_prems : meta_simpset * thm list > meta_simpset 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

64 
val add_simps : meta_simpset * thm list > meta_simpset 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

65 
val assume : cterm > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

66 
val assumption : int > thm > thm Sequence.seq 
776
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

67 
val axioms_of : theory > (string * thm) list 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

68 
val beta_conversion : cterm > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

69 
val bicompose : bool > bool * thm * int > int > thm > 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

71 
val biresolution : bool > (bool*thm)list > int > thm > 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

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

74 
val concl_of : thm > term 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

75 
val cprop_of : thm > cterm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

76 
val del_simps : meta_simpset * thm list > meta_simpset 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

77 
val dest_cimplies : cterm > cterm*cterm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

78 
val dest_state : thm*int > (term*term)list * term list * term * term 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

80 
val eq_assumption : int > thm > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

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

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

84 
val flexflex_rule : thm > thm Sequence.seq 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

86 
val forall_elim : cterm > thm > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

87 
val forall_intr : cterm > thm > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

89 
val get_axiom : theory > string > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

91 
val implies_intr : cterm > thm > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

93 
val instantiate : (indexname*ctyp)list * (cterm*cterm)list > 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

95 
val lift_rule : (thm * int) > thm > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

96 
val merge_theories : theory * theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

97 
val merge_thy_list : bool > theory list > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

98 
val mk_rews_of_mss : meta_simpset > thm > thm list 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

99 
val mss_of : thm list > meta_simpset 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

100 
val nprems_of : thm > int 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

101 
val parents_of : theory > theory list 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

102 
val prems_of : thm > term list 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

103 
val prems_of_mss : meta_simpset > thm list 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

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

105 
val pure_thy : theory 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

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

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

108 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

109 
string list > bool > string * typ > cterm * (indexname * typ) list 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

110 
val reflexive : cterm > thm 
0  111 
val rename_params_rule: string list * int > thm > thm 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

112 
val rep_thm : thm > {prop: term, hyps: term list, 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

113 
maxidx: int, sign: Sign.sg} 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

114 
val rewrite_cterm : bool*bool > meta_simpset > 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

115 
(meta_simpset > thm > thm option) > cterm > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

116 
val set_mk_rews : meta_simpset * (thm > thm list) > meta_simpset 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

117 
val rep_theory : theory > {sign: Sign.sg, 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

118 
new_axioms: term Sign.Symtab.table, 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

120 
val subthy : theory * theory > bool 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

121 
val eq_thy : theory * theory > bool 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

122 
val sign_of : theory > Sign.sg 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

123 
val syn_of : theory > Sign.Syntax.syntax 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

124 
val stamps_of_thm : thm > string ref list 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

125 
val stamps_of_thy : theory > string ref list 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

127 
val tpairs_of : thm > (term*term)list 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

128 
val trace_simp : bool ref 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

130 
val trivial : cterm > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

131 
val class_triv : theory > class > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

132 
val varifyT : thm > thm 
250  133 
end; 
0  134 

250  135 
functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern: PATTERN 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

136 
and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig): THM = 
0  137 
struct 
250  138 

0  139 
structure Sequence = Unify.Sequence; 
140 
structure Envir = Unify.Envir; 

141 
structure Sign = Unify.Sign; 

142 
structure Type = Sign.Type; 

143 
structure Syntax = Sign.Syntax; 

144 
structure Symtab = Sign.Symtab; 

145 

146 

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

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

148 

250  149 
(** certified types **) 
150 

151 
(*certified typs under a signature*) 

152 

153 
datatype ctyp = Ctyp of {sign: Sign.sg, T: typ}; 

154 

155 
fun rep_ctyp (Ctyp args) = args; 

156 
fun typ_of (Ctyp {T, ...}) = T; 

157 

158 
fun ctyp_of sign T = 

159 
Ctyp {sign = sign, T = Sign.certify_typ sign T}; 

160 

161 
fun read_ctyp sign s = 

162 
Ctyp {sign = sign, T = Sign.read_typ (sign, K None) s}; 

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

163 

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

164 

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

165 

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

167 

250  168 
(*certified terms under a signature, with checked typ and maxidx of Vars*) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

169 

250  170 
datatype cterm = Cterm of {sign: Sign.sg, 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

171 

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

172 
fun rep_cterm (Cterm args) = args; 
250  173 
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

174 

250  175 
(*create a cterm by checking a "raw" term with respect to a signature*) 
176 
fun cterm_of sign tm = 

177 
let val (t, T, maxidx) = Sign.certify_term sign tm 

178 
in Cterm {sign = sign, t = t, T = T, maxidx = maxidx} 

179 
end handle TYPE (msg, _, _) 

180 
=> raise TERM ("Term not in signature\n" ^ msg, [tm]); 

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

181 

250  182 
fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t); 
183 

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

184 

250  185 
(*dest_implies for cterms. Note T=prop below*) 
186 
fun dest_cimplies (Cterm{sign, T, maxidx, t=Const("==>", _) $ A $ B}) = 

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

187 
(Cterm{sign=sign, T=T, maxidx=maxidx, t=A}, 
250  188 
Cterm{sign=sign, T=T, maxidx=maxidx, t=B}) 
189 
 dest_cimplies ct = raise TERM ("dest_cimplies", [term_of ct]); 

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

190 

250  191 

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

192 

574  193 
(** read cterms **) (*exception ERROR*) 
250  194 

195 
(*read term, infer types, certify term*) 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

196 
fun read_def_cterm (sign, types, sorts) used freeze (a, T) = 
250  197 
let 
574  198 
val T' = Sign.certify_typ sign T 
199 
handle TYPE (msg, _, _) => error msg; 

623  200 
val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a; 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

201 
val (_, t', tye) = 
959  202 
Sign.infer_types sign types sorts used freeze (ts, T'); 
574  203 
val ct = cterm_of sign t' 
204 
handle TERM (msg, _) => error msg; 

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

206 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

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

208 

250  209 

210 

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

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

212 

0  213 
datatype thm = Thm of 
250  214 
{sign: Sign.sg, maxidx: int, hyps: term list, prop: term}; 
0  215 

250  216 
fun rep_thm (Thm args) = args; 
0  217 

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

218 
(*errors involving theorems*) 
0  219 
exception THM of string * int * thm list; 
220 

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

221 

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

222 
val sign_of_thm = #sign o rep_thm; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

223 
val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm; 
0  224 

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

225 
(*merge signatures of two theorems; raise exception if incompatible*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

226 
fun merge_thm_sgs (th1, th2) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

227 
Sign.merge (pairself sign_of_thm (th1, th2)) 
574  228 
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

229 

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

230 

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

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

232 
fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

233 

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

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

235 
fun prems_of (Thm {prop, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

236 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  237 

238 
(*counts premises in a rule*) 

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

239 
fun nprems_of (Thm {prop, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

240 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  241 

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

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

243 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  244 

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

245 
(*the statement of any thm is a cterm*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

246 
fun cprop_of (Thm {sign, maxidx, hyps, prop}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

247 
Cterm {sign = sign, 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

248 

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

249 

0  250 

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

251 
(*** Theories ***) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

252 

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

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

255 
sign: Sign.sg, 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

256 
new_axioms: term Symtab.table, 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

257 
parents: theory list}; 
0  258 

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

259 
fun rep_theory (Theory args) = args; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

260 

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

261 
(*errors involving theories*) 
0  262 
exception THEORY of string * theory list; 
263 

264 

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

265 
val sign_of = #sign o rep_theory; 
0  266 
val syn_of = #syn o Sign.rep_sg o sign_of; 
267 

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

268 
(*stamps associated with a theory*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

269 
val stamps_of_thy = #stamps o Sign.rep_sg o sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

270 

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

271 
(*return the immediate ancestors*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

272 
val parents_of = #parents o rep_theory; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

273 

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

274 

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

275 
(*compare theories*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

276 
val subthy = Sign.subsig o pairself sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

277 
val eq_thy = Sign.eq_sg o pairself sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

278 

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

279 

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

280 
(*look up the named axiom in the theory*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

281 
fun get_axiom theory name = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

283 
fun get_ax [] = raise Match 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

284 
 get_ax (Theory {sign, new_axioms, parents} :: thys) = 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

285 
(case Symtab.lookup (new_axioms, name) of 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

286 
Some t => 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

287 
Thm {sign = sign, maxidx = maxidx_of_term t, hyps = [], prop = t} 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

288 
 None => get_ax parents handle Match => get_ax thys); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

290 
get_ax [theory] handle Match 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

291 
=> raise THEORY ("get_axiom: no axiom " ^ quote name, [theory]) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

293 

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

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

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

296 
map (fn (s, _) => (s, get_axiom thy s)) 
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

297 
(Symtab.dest (#new_axioms (rep_theory thy))); 
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

298 

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

299 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

300 
(* the Pure theories *) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

301 

196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

302 
val proto_pure_thy = 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

303 
Theory {sign = Sign.proto_pure, new_axioms = Symtab.null, parents = []}; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

304 

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

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

306 
Theory {sign = Sign.pure, new_axioms = Symtab.null, parents = []}; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

307 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

308 
val cpure_thy = 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

309 
Theory {sign = Sign.cpure, new_axioms = Symtab.null, parents = []}; 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

310 

0  311 

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

312 

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

313 
(** extend theory **) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

314 

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

315 
fun err_dup_axms names = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

316 
error ("Duplicate axiom name(s) " ^ commas_quote names); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

317 

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

318 
fun ext_thy (thy as Theory {sign, new_axioms, parents}) sign1 new_axms = 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

320 
val draft = Sign.is_draft sign; 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

322 
Symtab.extend_new (if draft then new_axioms else Symtab.null, new_axms) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

323 
handle Symtab.DUPS names => err_dup_axms names; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

324 
val parents1 = if draft then parents else [thy]; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

326 
Theory {sign = sign1, new_axioms = new_axioms1, parents = parents1} 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

328 

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

329 

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

330 
(* extend signature of a theory *) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

331 

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

332 
fun ext_sg extfun decls (thy as Theory {sign, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

333 
ext_thy thy (extfun decls sign) []; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

334 

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

335 
val add_classes = ext_sg Sign.add_classes; 
421  336 
val add_classrel = ext_sg Sign.add_classrel; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

337 
val add_defsort = ext_sg Sign.add_defsort; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

338 
val add_types = ext_sg Sign.add_types; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

339 
val add_tyabbrs = ext_sg Sign.add_tyabbrs; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

340 
val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

341 
val add_arities = ext_sg Sign.add_arities; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

342 
val add_consts = ext_sg Sign.add_consts; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

343 
val add_consts_i = ext_sg Sign.add_consts_i; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

344 
val add_syntax = ext_sg Sign.add_syntax; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

345 
val add_syntax_i = ext_sg Sign.add_syntax_i; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

346 
val add_trfuns = ext_sg Sign.add_trfuns; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

347 
val add_trrules = ext_sg Sign.add_trrules; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

348 
val add_thyname = ext_sg Sign.add_name; 
0  349 

350 

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

351 
(* prepare axioms *) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

352 

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

353 
fun err_in_axm name = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

354 
error ("The error(s) above occurred in axiom " ^ quote name); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

355 

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

356 
fun no_vars tm = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

357 
if null (term_vars tm) andalso null (term_tvars tm) then tm 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

358 
else error "Illegal schematic variable(s) in term"; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

359 

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

360 
fun cert_axm sg (name, raw_tm) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

362 
val Cterm {t, T, ...} = cterm_of sg raw_tm 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

363 
handle TERM (msg, _) => error msg; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

365 
assert (T = propT) "Term not of type prop"; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

366 
(name, no_vars t) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

368 
handle ERROR => err_in_axm name; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

369 

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

370 
fun read_axm sg (name, str) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

371 
(name, no_vars (term_of (read_cterm sg (str, propT)))) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

372 
handle ERROR => err_in_axm name; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

373 

564  374 
fun inferT_axm sg (name, pre_tm) = 
959  375 
let val t = #2(Sign.infer_types sg (K None) (K None) [] true 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

376 
([pre_tm], propT)) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

377 
in (name, no_vars t) end 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

378 
handle ERROR => err_in_axm name; 
564  379 

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

380 

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

381 
(* extend axioms of a theory *) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

382 

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

383 
fun ext_axms prep_axm axms (thy as Theory {sign, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

385 
val sign1 = Sign.make_draft sign; 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

386 
val axioms = map (apsnd Logic.varify o prep_axm sign) axms; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

389 
end; 
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 
val add_axioms = ext_axms read_axm; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

392 
val add_axioms_i = ext_axms cert_axm; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

393 

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

394 

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

395 

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

396 
(** merge theories **) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

397 

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

398 
fun merge_thy_list mk_draft thys = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

400 
fun is_union thy = forall (fn t => subthy (t, thy)) thys; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

401 
val is_draft = Sign.is_draft o sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

402 

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

403 
fun add_sign (sg, Theory {sign, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

404 
Sign.merge (sg, sign) handle TERM (msg, _) => error msg; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

406 
(case (find_first is_union thys, exists is_draft thys) of 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

407 
(Some thy, _) => thy 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

408 
 (None, true) => raise THEORY ("Illegal merge of draft theories", thys) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

409 
 (None, false) => Theory { 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

411 
(if mk_draft then Sign.make_draft else I) 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

412 
(foldl add_sign (Sign.proto_pure, thys)), 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

413 
new_axioms = Symtab.null, 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

414 
parents = thys}) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

416 

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

417 
fun merge_theories (thy1, thy2) = merge_thy_list false [thy1, thy2]; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

418 

0  419 

420 

421 
(**** Primitive rules ****) 

422 

423 
(* discharge all assumptions t from ts *) 

424 
val disch = gen_rem (op aconv); 

425 

426 
(*The assumption rule AA in a theory *) 

250  427 
fun assume ct : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

428 
let val {sign, t=prop, T, maxidx} = rep_cterm ct 
250  429 
in if T<>propT then 
430 
raise THM("assume: assumptions must have type prop", 0, []) 

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

0  434 
else Thm{sign = sign, maxidx = ~1, hyps = [prop], prop = prop} 
435 
end; 

436 

250  437 
(* Implication introduction 
438 
A  B 

439 
 

440 
A ==> B *) 

0  441 
fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop}) : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

442 
let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA 
0  443 
in if T<>propT then 
250  444 
raise THM("implies_intr: assumptions must have type prop", 0, [thB]) 
445 
else Thm{sign= Sign.merge (sign,signA), maxidx= max[maxidxA, maxidx], 

446 
hyps= disch(hyps,A), prop= implies$A$prop} 

0  447 
handle TERM _ => 
448 
raise THM("implies_intr: incompatible signatures", 0, [thB]) 

449 
end; 

450 

451 
(* Implication elimination 

250  452 
A ==> B A 
453 
 

454 
B *) 

0  455 
fun implies_elim thAB thA : thm = 
456 
let val Thm{maxidx=maxA, hyps=hypsA, prop=propA,...} = thA 

250  457 
and Thm{sign, maxidx, hyps, prop,...} = thAB; 
458 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 

0  459 
in case prop of 
250  460 
imp$A$B => 
461 
if imp=implies andalso A aconv propA 

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

462 
then Thm{sign= merge_thm_sgs(thAB,thA), 
250  463 
maxidx= max[maxA,maxidx], 
464 
hyps= hypsA union hyps, (*dups suppressed*) 

465 
prop= B} 

466 
else err("major premise") 

467 
 _ => err("major premise") 

0  468 
end; 
250  469 

0  470 
(* Forall introduction. The Free or Var x must not be free in the hypotheses. 
471 
A 

472 
 

473 
!!x.A *) 

474 
fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop}) = 

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

475 
let val x = term_of cx; 
0  476 
fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps, 
250  477 
prop= all(T) $ Abs(a, T, abstract_over (x,prop))} 
0  478 
in case x of 
250  479 
Free(a,T) => 
480 
if exists (apl(x, Logic.occs)) hyps 

481 
then raise THM("forall_intr: variable free in assumptions", 0, [th]) 

482 
else result(a,T) 

0  483 
 Var((a,_),T) => result(a,T) 
484 
 _ => raise THM("forall_intr: not a variable", 0, [th]) 

485 
end; 

486 

487 
(* Forall elimination 

250  488 
!!x.A 
489 
 

490 
A[t/x] *) 

0  491 
fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop}) : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

492 
let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct 
0  493 
in case prop of 
250  494 
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => 
495 
if T<>qary then 

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

497 
else Thm{sign= Sign.merge(sign,signt), 

498 
maxidx= max[maxidx, maxt], 

499 
hyps= hyps, prop= betapply(A,t)} 

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

0  501 
end 
502 
handle TERM _ => 

250  503 
raise THM("forall_elim: incompatible signatures", 0, [th]); 
0  504 

505 

506 
(*** Equality ***) 

507 

508 
(*Definition of the relation =?= *) 

509 
val flexpair_def = 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

510 
Thm{sign= Sign.proto_pure, hyps= [], maxidx= 0, 
250  511 
prop= term_of 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

512 
(read_cterm Sign.proto_pure 
250  513 
("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))}; 
0  514 

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

250  516 
fun reflexive ct = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

517 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  518 
in Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)} 
519 
end; 

520 

521 
(*The symmetry rule 

522 
t==u 

523 
 

524 
u==t *) 

525 
fun symmetric (th as Thm{sign,hyps,prop,maxidx}) = 

526 
case prop of 

527 
(eq as Const("==",_)) $ t $ u => 

250  528 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= eq$u$t} 
0  529 
 _ => raise THM("symmetric", 0, [th]); 
530 

531 
(*The transitive rule 

532 
t1==u u==t2 

533 
 

534 
t1==t2 *) 

535 
fun transitive th1 th2 = 

536 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

537 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

538 
fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) 

539 
in case (prop1,prop2) of 

540 
((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) => 

250  541 
if not (u aconv u') then err"middle term" else 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

542 
Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, 
250  543 
maxidx= max[max1,max2], prop= eq$t1$t2} 
0  544 
 _ => err"premises" 
545 
end; 

546 

547 
(*Betaconversion: maps (%(x)t)(u) to the theorem (%(x)t)(u) == t[u/x] *) 

250  548 
fun beta_conversion ct = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

549 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  550 
in case t of 
250  551 
Abs(_,_,bodt) $ u => 
552 
Thm{sign= sign, hyps= [], 

553 
maxidx= maxidx_of_term t, 

554 
prop= Logic.mk_equals(t, subst_bounds([u],bodt))} 

555 
 _ => raise THM("beta_conversion: not a redex", 0, []) 

0  556 
end; 
557 

558 
(*The extensionality rule (proviso: x not free in f, g, or hypotheses) 

559 
f(x) == g(x) 

560 
 

561 
f == g *) 

562 
fun extensional (th as Thm{sign,maxidx,hyps,prop}) = 

563 
case prop of 

564 
(Const("==",_)) $ (f$x) $ (g$y) => 

250  565 
let fun err(msg) = raise THM("extensional: "^msg, 0, [th]) 
0  566 
in (if x<>y then err"different variables" else 
567 
case y of 

250  568 
Free _ => 
569 
if exists (apl(y, Logic.occs)) (f::g::hyps) 

570 
then err"variable free in hyps or functions" else () 

571 
 Var _ => 

572 
if Logic.occs(y,f) orelse Logic.occs(y,g) 

573 
then err"variable free in functions" else () 

574 
 _ => err"not a variable"); 

575 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, 

576 
prop= Logic.mk_equals(f,g)} 

0  577 
end 
578 
 _ => raise THM("extensional: premise", 0, [th]); 

579 

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

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

582 
t == u 

583 
 

584 
%(x)t == %(x)u *) 

585 
fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop}) = 

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

586 
let val x = term_of cx; 
250  587 
val (t,u) = Logic.dest_equals prop 
588 
handle TERM _ => 

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

0  590 
fun result T = 
591 
Thm{sign= sign, maxidx= maxidx, hyps= hyps, 

250  592 
prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 
593 
Abs(a, T, abstract_over (x,u)))} 

0  594 
in case x of 
250  595 
Free(_,T) => 
596 
if exists (apl(x, Logic.occs)) hyps 

597 
then raise THM("abstract_rule: variable free in assumptions", 0, [th]) 

598 
else result T 

0  599 
 Var(_,T) => result T 
600 
 _ => raise THM("abstract_rule: not a variable", 0, [th]) 

601 
end; 

602 

603 
(*The combination rule 

604 
f==g t==u 

605 
 

606 
f(t)==g(u) *) 

607 
fun combination th1 th2 = 

608 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

609 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2 

610 
in case (prop1,prop2) of 

611 
(Const("==",_) $ f $ g, Const("==",_) $ t $ u) => 

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

612 
Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, 
250  613 
maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)} 
0  614 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
615 
end; 

616 

617 

618 
(*The equal propositions rule 

619 
A==B A 

620 
 

621 
B *) 

622 
fun equal_elim th1 th2 = 

623 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

624 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

625 
fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2]) 

626 
in case prop1 of 

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

250  628 
if not (prop2 aconv A) then err"not equal" else 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

629 
Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, 
250  630 
maxidx= max[max1,max2], prop= B} 
0  631 
 _ => err"major premise" 
632 
end; 

633 

634 

635 
(* Equality introduction 

636 
A==>B B==>A 

637 
 

638 
A==B *) 

639 
fun equal_intr th1 th2 = 

640 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

641 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

642 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 

643 
in case (prop1,prop2) of 

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

250  645 
if A aconv A' andalso B aconv B' 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

646 
then Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, 
250  647 
maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)} 
648 
else err"not equal" 

0  649 
 _ => err"premises" 
650 
end; 

651 

652 
(**** Derived rules ****) 

653 

654 
(*Discharge all hypotheses (need not verify cterms) 

655 
Repeated hypotheses are discharged only once; fold cannot do this*) 

656 
fun implies_intr_hyps (Thm{sign, maxidx, hyps=A::As, prop}) = 

657 
implies_intr_hyps 

250  658 
(Thm{sign=sign, maxidx=maxidx, 
659 
hyps= disch(As,A), prop= implies$A$prop}) 

0  660 
 implies_intr_hyps th = th; 
661 

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

250  663 
Instantiates the theorem and deletes trivial tpairs. 
0  664 
Resulting sequence may contain multiple elements if the tpairs are 
665 
not all flexflex. *) 

666 
fun flexflex_rule (Thm{sign,maxidx,hyps,prop}) = 

250  667 
let fun newthm env = 
668 
let val (tpairs,horn) = 

669 
Logic.strip_flexpairs (Envir.norm_term env prop) 

670 
(*Remove trivial tpairs, of the form t=t*) 

671 
val distpairs = filter (not o op aconv) tpairs 

672 
val newprop = Logic.list_flexpairs(distpairs, horn) 

673 
in Thm{sign= sign, hyps= hyps, 

674 
maxidx= maxidx_of_term newprop, prop= newprop} 

675 
end; 

0  676 
val (tpairs,_) = Logic.strip_flexpairs prop 
677 
in Sequence.maps newthm 

250  678 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  679 
end; 
680 

681 
(*Instantiation of Vars 

250  682 
A 
683 
 

684 
A[t1/v1,....,tn/vn] *) 

0  685 

686 
(*Check that all the terms are Vars and are distinct*) 

687 
fun instl_ok ts = forall is_Var ts andalso null(findrep ts); 

688 

689 
(*For instantiate: process pair of cterms, merge theories*) 

690 
fun add_ctpair ((ct,cu), (sign,tpairs)) = 

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

691 
let val {sign=signt, t=t, T= T, ...} = rep_cterm ct 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

692 
and {sign=signu, t=u, T= U, ...} = rep_cterm cu 
0  693 
in if T=U then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs) 
694 
else raise TYPE("add_ctpair", [T,U], [t,u]) 

695 
end; 

696 

697 
fun add_ctyp ((v,ctyp), (sign',vTs)) = 

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

698 
let val {T,sign} = rep_ctyp ctyp 
0  699 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
700 

701 
(*Lefttoright replacements: ctpairs = [...,(vi,ti),...]. 

702 
Instantiates distinct Vars by terms of same type. 

703 
Normalizes the new theorem! *) 

250  704 
fun instantiate (vcTs,ctpairs) (th as Thm{sign,maxidx,hyps,prop}) = 
0  705 
let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[])); 
706 
val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[])); 

250  707 
val newprop = 
708 
Envir.norm_term (Envir.empty 0) 

709 
(subst_atomic tpairs 

710 
(Type.inst_term_tvars(#tsig(Sign.rep_sg newsign),vTs) prop)) 

0  711 
val newth = Thm{sign= newsign, hyps= hyps, 
250  712 
maxidx= maxidx_of_term newprop, prop= newprop} 
713 
in if not(instl_ok(map #1 tpairs)) 

193  714 
then raise THM("instantiate: variables not distinct", 0, [th]) 
715 
else if not(null(findrep(map #1 vTs))) 

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

717 
else (*Check types of Vars for agreement*) 

718 
case findrep (map (#1 o dest_Var) (term_vars newprop)) of 

250  719 
ix::_ => raise THM("instantiate: conflicting types for variable " ^ 
720 
Syntax.string_of_vname ix ^ "\n", 0, [newth]) 

721 
 [] => 

722 
case findrep (map #1 (term_tvars newprop)) of 

723 
ix::_ => raise THM 

724 
("instantiate: conflicting sorts for type variable " ^ 

725 
Syntax.string_of_vname ix ^ "\n", 0, [newth]) 

193  726 
 [] => newth 
0  727 
end 
250  728 
handle TERM _ => 
0  729 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  730 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  731 

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

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

250  734 
fun trivial ct : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

735 
let val {sign, t=A, T, maxidx} = rep_cterm ct 
250  736 
in if T<>propT then 
737 
raise THM("trivial: the term must have type prop", 0, []) 

0  738 
else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A} 
739 
end; 

740 

480  741 
(*Axiomscheme reflecting signature contents: "OFCLASS(?'a::c, c_class)". 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

742 
Is weaker than some definition of c_class, e.g. "c_class == %x.T"; 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

743 
may be interpreted as an instance of A==>A.*) 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

744 
fun class_triv thy c = 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

746 
val sign = sign_of thy; 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

747 
val Cterm {t, maxidx, ...} = 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

748 
cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

749 
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

751 
Thm {sign = sign, maxidx = maxidx, hyps = [], prop = t} 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

753 

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

754 

0  755 
(* Replace all TFrees not in the hyps by new TVars *) 
756 
fun varifyT(Thm{sign,maxidx,hyps,prop}) = 

757 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 

758 
in Thm{sign=sign, maxidx=max[0,maxidx], hyps=hyps, 

250  759 
prop= Type.varify(prop,tfrees)} 
0  760 
end; 
761 

762 
(* Replace all TVars by new TFrees *) 

763 
fun freezeT(Thm{sign,maxidx,hyps,prop}) = 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

764 
let val prop' = Type.freeze prop 
0  765 
in Thm{sign=sign, maxidx=maxidx_of_term prop', hyps=hyps, prop=prop'} end; 
766 

767 

768 
(*** Inference rules for tactics ***) 

769 

770 
(*Destruct proof state into constraints, other goals, goal(i), rest *) 

771 
fun dest_state (state as Thm{prop,...}, i) = 

772 
let val (tpairs,horn) = Logic.strip_flexpairs prop 

773 
in case Logic.strip_prems(i, [], horn) of 

774 
(B::rBs, C) => (tpairs, rev rBs, B, C) 

775 
 _ => raise THM("dest_state", i, [state]) 

776 
end 

777 
handle TERM _ => raise THM("dest_state", i, [state]); 

778 

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

782 
let val Thm{prop=sprop,maxidx=smax,...} = state; 

783 
val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) 

250  784 
handle TERM _ => raise THM("lift_rule", i, [orule,state]); 
0  785 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1); 
786 
val (Thm{sign,maxidx,hyps,prop}) = orule 

787 
val (tpairs,As,B) = Logic.strip_horn prop 

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

788 
in Thm{hyps=hyps, sign= merge_thm_sgs(state,orule), 
250  789 
maxidx= maxidx+smax+1, 
790 
prop= Logic.rule_of(map (pairself lift_abs) tpairs, 

791 
map lift_all As, lift_all B)} 

0  792 
end; 
793 

794 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) 

795 
fun assumption i state = 

796 
let val Thm{sign,maxidx,hyps,prop} = state; 

797 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 

250  798 
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = 
799 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= 

800 
if Envir.is_empty env then (*avoid wasted normalizations*) 

801 
Logic.rule_of (tpairs, Bs, C) 

802 
else (*normalize the new rule fully*) 

803 
Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))}; 

0  804 
fun addprfs [] = Sequence.null 
805 
 addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull 

806 
(Sequence.mapp newth 

250  807 
(Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs)) 
808 
(addprfs apairs))) 

0  809 
in addprfs (Logic.assum_pairs Bi) end; 
810 

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

814 
let val Thm{sign,maxidx,hyps,prop} = state; 

815 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 

816 
in if exists (op aconv) (Logic.assum_pairs Bi) 

250  817 
then Thm{sign=sign, hyps=hyps, maxidx=maxidx, 
818 
prop=Logic.rule_of(tpairs, Bs, C)} 

0  819 
else raise THM("eq_assumption", 0, [state]) 
820 
end; 

821 

822 

823 
(** User renaming of parameters in a subgoal **) 

824 

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

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

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

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

829 
fun rename_params_rule (cs, i) state = 

830 
let val Thm{sign,maxidx,hyps,prop} = state 

831 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 

832 
val iparams = map #1 (Logic.strip_params Bi) 

833 
val short = length iparams  length cs 

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

836 
else variantlist(take (short,iparams), cs) @ cs 

0  837 
val freenames = map (#1 o dest_Free) (term_frees prop) 
838 
val newBi = Logic.list_rename_params (newnames, Bi) 

250  839 
in 
0  840 
case findrep cs of 
841 
c::_ => error ("Bound variables not distinct: " ^ c) 

842 
 [] => (case cs inter freenames of 

843 
a::_ => error ("Bound/Free variable clash: " ^ a) 

844 
 [] => Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= 

250  845 
Logic.rule_of(tpairs, Bs@[newBi], C)}) 
0  846 
end; 
847 

848 
(*** Preservation of bound variable names ***) 

849 

250  850 
(*Scan a pair of terms; while they are similar, 
0  851 
accumulate corresponding bound vars in "al"*) 
852 
fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s,t,(x,y)::al) 

853 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 

854 
 match_bvs(_,_,al) = al; 

855 

856 
(* strip abstractions created by parameters *) 

857 
fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al); 

858 

859 

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

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

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

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

867 
 strip(A,_) = f A 

0  868 
in strip end; 
869 

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

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

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

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

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

250  875 
let val vars = foldr add_term_vars 
876 
(map fst dpairs @ map fst tpairs @ map snd tpairs, []) 

877 
(*unknowns appearing elsewhere be preserved!*) 

878 
val vids = map (#1 o #1 o dest_Var) vars; 

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

880 
(case assoc(al,x) of 

881 
Some(y) => if x mem vids orelse y mem vids then t 

882 
else Var((y,i),T) 

883 
 None=> t) 

0  884 
 rename(Abs(x,T,t)) = 
250  885 
Abs(case assoc(al,x) of Some(y) => y  None => x, 
886 
T, rename t) 

0  887 
 rename(f$t) = rename f $ rename t 
888 
 rename(t) = t; 

250  889 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  890 
in strip_ren end; 
891 

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

893 
fun rename_bvars(dpairs, tpairs, B) = 

250  894 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  895 

896 

897 
(*** RESOLUTION ***) 

898 

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

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

900 

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

250  903 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
904 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  905 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  906 
Const("all",_)$Abs(_,_,t2)) = 
0  907 
let val (B1,B2) = strip_assums2 (t1,t2) 
908 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

909 
 strip_assums2 BB = BB; 

910 

911 

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

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

913 
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

914 
 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

915 
let val Envir.Envir{iTs, ...} = env 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

916 
val T' = typ_subst_TVars iTs T 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

917 
(*Must instantiate types of parameters because they are flattened; 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

918 
this could be a NEW parameter*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

919 
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

920 
 norm_term_skip env n (Const("==>", _) $ A $ B) = 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

921 
implies $ A $ norm_term_skip env (n1) B 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

922 
 norm_term_skip env n t = error"norm_term_skip: too few assumptions??"; 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

923 

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

924 

0  925 
(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) 
250  926 
Unifies B with Bi, replacing subgoal i (1 <= i <= n) 
0  927 
If match then forbid instantiations in proof state 
928 
If lifted then shorten the dpair using strip_assums2. 

929 
If eres_flg then simultaneously proves A1 by assumption. 

250  930 
nsubgoal is the number of new subgoals (written m above). 
0  931 
Curried so that resolution calls dest_state only once. 
932 
*) 

933 
local open Sequence; exception Bicompose 

934 
in 

250  935 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  936 
(eres_flg, orule, nsubgoal) = 
937 
let val Thm{maxidx=smax, hyps=shyps, ...} = state 

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

938 
and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

939 
(*How many hyps to skip over during normalization*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

940 
and nlift = Logic.count_prems(strip_all_body Bi, 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

941 
if eres_flg then ~1 else 0) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

942 
val sign = merge_thm_sgs(state,orule); 
0  943 
(** Add new theorem with prop = '[ Bs; As ] ==> C' to thq **) 
250  944 
fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = 
945 
let val normt = Envir.norm_term env; 

946 
(*perform minimal copying here by examining env*) 

947 
val normp = 

948 
if Envir.is_empty env then (tpairs, Bs @ As, C) 

949 
else 

950 
let val ntps = map (pairself normt) tpairs 

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

951 
in if the (Envir.minidx env) > smax then 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

952 
(*no assignments in state; normalize the rule only*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

954 
then (ntps, Bs @ map (norm_term_skip env nlift) As, C) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

955 
else (ntps, Bs @ map normt As, C) 
250  956 
else if match then raise Bicompose 
957 
else (*normalize the new rule fully*) 

958 
(ntps, map normt (Bs @ As), normt C) 

959 
end 

960 
val th = Thm{sign=sign, hyps=rhyps union shyps, maxidx=maxidx, 

961 
prop= Logic.rule_of normp} 

0  962 
in cons(th, thq) end handle Bicompose => thq 
963 
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); 

964 
val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) 

965 
handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); 

966 
(*Modify assumptions, deleting nth if n>0 for eresolution*) 

967 
fun newAs(As0, n, dpairs, tpairs) = 

968 
let val As1 = if !Logic.auto_rename orelse not lifted then As0 

250  969 
else map (rename_bvars(dpairs,tpairs,B)) As0 
0  970 
in (map (Logic.flatten_params n) As1) 
250  971 
handle TERM _ => 
972 
raise THM("bicompose: 1st premise", 0, [orule]) 

0  973 
end; 
974 
val env = Envir.empty(max[rmax,smax]); 

975 
val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); 

976 
val dpairs = BBi :: (rtpairs@stpairs); 

977 
(*elimresolution: try each assumption in turn. Initially n=1*) 

978 
fun tryasms (_, _, []) = null 

979 
 tryasms (As, n, (t,u)::apairs) = 

250  980 
(case pull(Unify.unifiers(sign, env, (t,u)::dpairs)) of 
981 
None => tryasms (As, n+1, apairs) 

982 
 cell as Some((_,tpairs),_) => 

983 
its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs))) 

984 
(seqof (fn()=> cell), 

985 
seqof (fn()=> pull (tryasms (As, n+1, apairs))))); 

0  986 
fun eres [] = raise THM("bicompose: no premises", 0, [orule,state]) 
987 
 eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1); 

988 
(*ordinary resolution*) 

989 
fun res(None) = null 

250  990 
 res(cell as Some((_,tpairs),_)) = 
991 
its_right (addth(newAs(rev rAs, 0, [BBi], tpairs))) 

992 
(seqof (fn()=> cell), null) 

0  993 
in if eres_flg then eres(rev rAs) 
994 
else res(pull(Unify.unifiers(sign, env, dpairs))) 

995 
end; 

996 
end; (*open Sequence*) 

997 

998 

999 
fun bicompose match arg i state = 

1000 
bicompose_aux match (state, dest_state(state,i), false) arg; 

1001 

1002 
(*Quick test whether rule is resolvable with the subgoal with hyps Hs 

1003 
and conclusion B. If eres_flg then checks 1st premise of rule also*) 

1004 
fun could_bires (Hs, B, eres_flg, rule) = 

1005 
let fun could_reshyp (A1::_) = exists (apl(A1,could_unify)) Hs 

250  1006 
 could_reshyp [] = false; (*no premise  illegal*) 
1007 
in could_unify(concl_of rule, B) andalso 

1008 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1009 
end; 
1010 

1011 
(*Biresolution of a state with a list of (flag,rule) pairs. 

1012 
Puts the rule above: rule/state. Renames vars in the rules. *) 

250  1013 
fun biresolution match brules i state = 
0  1014 
let val lift = lift_rule(state, i); 
250  1015 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
1016 
val B = Logic.strip_assums_concl Bi; 

1017 
val Hs = Logic.strip_assums_hyp Bi; 

1018 
val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true); 

1019 
fun res [] = Sequence.null 

1020 
 res ((eres_flg, rule)::brules) = 

1021 
if could_bires (Hs, B, eres_flg, rule) 

1022 
then Sequence.seqof (*delay processing remainder til needed*) 

1023 
(fn()=> Some(comp (eres_flg, lift rule, nprems_of rule), 

1024 
res brules)) 

1025 
else res brules 

0  1026 
in Sequence.flats (res brules) end; 
1027 

1028 

1029 

1030 
(*** Meta simp sets ***) 

1031 

288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1032 
type rrule = {thm:thm, lhs:term, perm:bool}; 
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1033 
type cong = {thm:thm, lhs:term}; 
0  1034 
datatype meta_simpset = 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1035 
Mss of {net:rrule Net.net, congs:(string * cong)list, bounds:string list, 
0  1036 
prems: thm list, mk_rews: thm > thm list}; 
1037 

1038 
(*A "mss" contains data needed during conversion: 

1039 
net: discrimination net of rewrite rules 

1040 
congs: association list of congruence rules 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1041 
bounds: names of bound variables already used; 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1042 
for generating new names when rewriting under lambda abstractions 
0  1043 
mk_rews: used when local assumptions are added 
1044 
*) 

1045 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1046 
val empty_mss = Mss{net= Net.empty, congs= [], bounds=[], prems= [], 
0  1047 
mk_rews = K[]}; 
1048 

1049 
exception SIMPLIFIER of string * thm; 

1050 

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

1051 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1052 

209  1053 
val trace_simp = ref false; 
1054 

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

1055 
fun trace_term a sign t = if !trace_simp then prtm a sign t else (); 
209  1056 

1057 
fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop; 

1058 

427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1059 
fun vperm(Var _, Var _) = true 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1060 
 vperm(Abs(_,_,s), Abs(_,_,t)) = vperm(s,t) 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1061 
 vperm(t1$t2, u1$u2) = vperm(t1,u1) andalso vperm(t2,u2) 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1062 
 vperm(t,u) = (t=u); 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1063 

427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1064 
fun var_perm(t,u) = vperm(t,u) andalso 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1065 
eq_set(add_term_vars(t,[]), add_term_vars(u,[])) 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1066 

0  1067 
(*simple test for looping rewrite*) 
1068 
fun loops sign prems (lhs,rhs) = 

427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1069 
is_Var(lhs) orelse 
900  1070 
(is_Free(lhs) andalso (lhs mem (foldr add_term_frees (rhs::prems,[])))) orelse 
427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1071 
(null(prems) andalso 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1072 
Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs)); 
0  1073 

1074 
fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) = 

1075 
let val prems = Logic.strip_imp_prems prop 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1076 
val concl = Logic.strip_imp_concl prop 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1077 
val (lhs,_) = Logic.dest_equals concl handle TERM _ => 
0  1078 
raise SIMPLIFIER("Rewrite rule not a metaequality",thm) 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1079 
val econcl = Pattern.eta_contract concl 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1080 
val (elhs,erhs) = Logic.dest_equals econcl 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1081 
val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1082 
andalso not(is_Var(elhs)) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1083 
in if not perm andalso loops sign prems (elhs,erhs) 
0  1084 
then (prtm "Warning: ignoring looping rewrite rule" sign prop; None) 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1085 
else Some{thm=thm,lhs=lhs,perm=perm} 
0  1086 
end; 
1087 

87  1088 
local 
1089 
fun eq({thm=Thm{prop=p1,...},...}:rrule, 

1090 
{thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2 

1091 
in 

1092 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1093 
fun add_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, 
0  1094 
thm as Thm{sign,prop,...}) = 
87  1095 
case mk_rrule thm of 
1096 
None => mss 

1097 
 Some(rrule as {lhs,...}) => 

209  1098 
(trace_thm "Adding rewrite rule:" thm; 
1099 
Mss{net= (Net.insert_term((lhs,rrule),net,eq) 

1100 
handle Net.INSERT => 

87  1101 
(prtm "Warning: ignoring duplicate rewrite rule" sign prop; 
1102 
net)), 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1103 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}); 
87  1104 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1105 
fun del_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, 
87  1106 
thm as Thm{sign,prop,...}) = 
1107 
case mk_rrule thm of 

1108 
None => mss 

1109 
 Some(rrule as {lhs,...}) => 

1110 
Mss{net= (Net.delete_term((lhs,rrule),net,eq) 

1111 
handle Net.INSERT => 

1112 
(prtm "Warning: rewrite rule not in simpset" sign prop; 

1113 
net)), 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1114 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews} 
87  1115 

1116 
end; 

0  1117 

1118 
val add_simps = foldl add_simp; 

87  1119 
val del_simps = foldl del_simp; 
0  1120 

1121 
fun mss_of thms = add_simps(empty_mss,thms); 

1122 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1123 
fun add_cong(Mss{net,congs,bounds,prems,mk_rews},thm) = 
0  1124 
let val (lhs,_) = Logic.dest_equals(concl_of thm) handle TERM _ => 
1125 
raise SIMPLIFIER("Congruence not a metaequality",thm) 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1126 
(* val lhs = Pattern.eta_contract lhs*) 
0  1127 
val (a,_) = dest_Const (head_of lhs) handle TERM _ => 
1128 
raise SIMPLIFIER("Congruence must start with a constant",thm) 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1129 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, bounds=bounds, 
0  1130 
prems=prems, mk_rews=mk_rews} 
1131 
end; 

1132 

1133 
val (op add_congs) = foldl add_cong; 

1134 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1135 
fun add_prems(Mss{net,congs,bounds,prems,mk_rews},thms) = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1136 
Mss{net=net, congs=congs, bounds=bounds, prems=thms@prems, mk_rews=mk_rews}; 
0  1137 

1138 
fun prems_of_mss(Mss{prems,...}) = prems; 

1139 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1140 
fun set_mk_rews(Mss{net,congs,bounds,prems,...},mk_rews) = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1141 
Mss{net=net, congs=congs, bounds=bounds, prems=prems, mk_rews=mk_rews}; 
0  1142 
fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews; 
1143 

1144 

250  1145 
(*** Metalevel rewriting 
0  1146 
uses conversions, omitting proofs for efficiency. See 
250  1147 
L C Paulson, A higherorder implementation of rewriting, 
1148 
Science of Computer Programming 3 (1983), pages 119149. ***) 

0  1149 

1150 
type prover = meta_simpset > thm > thm option; 

1151 
type termrec = (Sign.sg * term list) * term; 

1152 
type conv = meta_simpset > termrec > termrec; 

1153 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1154 
datatype order = LESS  EQUAL  GREATER; 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1155 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1156 
fun stringord(a,b:string) = if a<b then LESS else 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1157 
if a=b then EQUAL else GREATER; 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1158 

4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1159 
fun intord(i,j:int) = if i<j then LESS else 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1160 
if i=j then EQUAL else GREATER; 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1161 

427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1162 
(* NB: nonlinearity of the ordering is not a soundness problem *) 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1163 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1164 
(* FIXME: "***ABSTRACTION***" is a hack and makes the ordering nonlinear *) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1165 
fun string_of_hd(Const(a,_)) = a 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1166 
 string_of_hd(Free(a,_)) = a 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1167 
 string_of_hd(Var(v,_)) = Syntax.string_of_vname v 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1168 
 string_of_hd(Bound i) = string_of_int i 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1169 
 string_of_hd(Abs _) = "***ABSTRACTION***"; 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1170 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1171 
(* a strict (not reflexive) linear wellfounded ACcompatible ordering 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1172 
* for terms: 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1173 
* s < t <=> 1. size(s) < size(t) or 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1174 
2. size(s) = size(t) and s=f(...) and t = g(...) and f<g or 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1175 
3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1176 
(s1..sn) < (t1..tn) (lexicographically) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1177 
*) 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1178 

b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1179 
(* FIXME: should really take types into account as well. 
427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1180 
* Otherwise nonlinear *) 
622
bf9821f58781
Modified termord to take account of the AbsAbs case.
nipkow
parents:
574
diff
changeset

1181 
fun termord(Abs(_,_,t),Abs(_,_,u)) = termord(t,u) 
bf9821f58781
Modified termord to take account of the AbsAbs case.
nipkow
parents:
574
diff
changeset

1182 
 termord(t,u) = 
305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1183 
(case intord(size_of_term t,size_of_term u) of 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1184 
EQUAL => let val (f,ts) = strip_comb t and (g,us) = strip_comb u 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1185 
in case stringord(string_of_hd f, string_of_hd g) of 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1186 
EQUAL => lextermord(ts,us) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1187 
 ord => ord 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1188 
end 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1189 
 ord => ord) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1190 
and lextermord(t::ts,u::us) = 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1191 
(case termord(t,u) of 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1192 
EQUAL => lextermord(ts,us) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1193 
 ord => ord) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1194 
 lextermord([],[]) = EQUAL 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1195 
 lextermord _ = error("lextermord"); 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1196 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1197 
fun termless tu = (termord tu = LESS); 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1198 

432  1199 
fun check_conv(thm as Thm{hyps,prop,sign,...}, prop0) = 
1200 
let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; 

1201 
trace_term "Should have proved" sign prop0; 

1202 
None) 

0  1203 
val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0) 
1204 
in case prop of 

1205 
Const("==",_) $ lhs $ rhs => 

1206 
if (lhs = lhs0) orelse 

427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1207 
(lhs aconv Envir.norm_term (Envir.empty 0) lhs0) 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1208 
then (trace_thm "SUCCEEDED" thm; Some(hyps,rhs)) 
0  1209 
else err() 
1210 
 _ => err() 

1211 
end; 

1212 

659
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1213 
fun ren_inst(insts,prop,pat,obj) = 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1214 
let val ren = match_bvs(pat,obj,[]) 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1215 
fun renAbs(Abs(x,T,b)) = 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1216 
Abs(case assoc(ren,x) of None => x  Some(y) => y, T, renAbs(b)) 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1217 
 renAbs(f$t) = renAbs(f) $ renAbs(t) 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1218 
 renAbs(t) = t 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1219 
in subst_vars insts (if null(ren) then prop else renAbs(prop)) end; 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1220 

659
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1221 

0  1222 
(*Conversion to apply the meta simpset to a term*) 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1223 
fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,t) = 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1224 
let val etat = Pattern.eta_contract t; 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1225 
fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs, perm} = 
250  1226 
let val unit = if Sign.subsig(sign,signt) then () 
446
3ee5c9314efe
rewritec now uses trace_thm for it's "rewrite rule from different theory"
clasohm
parents:
432
diff
changeset

1227 
else (trace_thm"Warning: rewrite rule from different theory" 
3ee5c9314efe
rewritec now uses trace_thm for it's "rewrite rule from different theory"
clasohm
parents:
432
diff
changeset

1228 
thm; 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1229 
raise Pattern.MATCH) 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1230 
val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (lhs,etat) 
659
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1231 
val prop' = ren_inst(insts,prop,lhs,t); 
0  1232 
val hyps' = hyps union hypst; 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1233 
val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx} 
427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1234 
val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop') 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1235 
in if perm andalso not(termless(rhs',lhs')) then None else 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1236 
if Logic.count_prems(prop',0) = 0 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1237 
then (trace_thm "Rewriting:" thm'; Some(hyps',rhs')) 
0  1238 
else (trace_thm "Trying to rewrite:" thm'; 
1239 
case prover mss thm' of 

1240 
None => (trace_thm "FAILED" thm'; None) 

112
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

1241 
 Some(thm2) => check_conv(thm2,prop')) 
0  1242 
end 
1243 

225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

1244 
fun rews [] = None 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

1245 
 rews (rrule::rrules) = 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

1246 
let val opt = rew rrule handle Pattern.MATCH => None 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

1247 
in case opt of None => rews rrules  some => some end; 
0  1248 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1249 
in case etat of 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1250 
Abs(_,_,body) $ u => Some(hypst,subst_bounds([u], body)) 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1251 
 _ => rews(Net.match_term net etat) 
0  1252 
end; 
1253 

1254 
(*Conversion to apply a congruence rule to a term*) 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1255 
fun congc (prover,signt) {thm=cong,lhs=lhs} (hypst,t) = 
0  1256 
let val Thm{sign,hyps,maxidx,prop,...} = cong 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1257 
val unit = if Sign.subsig(sign,signt) then () 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1258 
else error("Congruence rule from different theory") 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1259 
val tsig = #tsig(Sign.rep_sg signt) 
0  1260 
val insts = Pattern.match tsig (lhs,t) handle Pattern.MATCH => 
1261 
error("Congruence rule did not match") 

659
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1262 
val prop' = ren_inst(insts,prop,lhs,t); 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1263 
val thm' = Thm{sign=signt, hyps=hyps union hypst, 
0  1264 
prop=prop', maxidx=maxidx} 
1265 
val unit = trace_thm "Applying congruence rule" thm'; 

112
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

1266 
fun err() = error("Failed congruence proof!") 
0  1267 

1268 
in case prover thm' of 

112
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

1269 
None => err() 
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

1270 
 Some(thm2) => (case check_conv(thm2,prop') of 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1271 
None => err()  some => some) 
0  1272 
end; 
1273 

1274 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1275 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1276 
fun bottomc ((simprem,useprem),prover,sign) = 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1277 
let fun botc fail mss trec = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1278 
(case subc mss trec of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1279 
some as Some(trec1) => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1280 
(case rewritec (prover,sign) mss trec1 of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1281 
Some(trec2) => botc false mss trec2 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1282 
 None => some) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1283 
 None => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1284 
(case rewritec (prover,sign) mss trec of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1285 
Some(trec2) => botc false mss trec2 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1286 
 None => if fail then None else Some(trec))) 
0  1287 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1288 
and try_botc mss trec = (case botc true mss trec of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1289 
Some(trec1) => trec1 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1290 
 None => trec) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1291 

c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1292 
and subc (mss as Mss{net,congs,bounds,prems,mk_rews}) 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1293 
(trec as (hyps,t)) = 
0  1294 
(case t of 
1295 
Abs(a,T,t) => 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1296 
let val b = variant bounds a 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1297 
val v = Free("." ^ b,T) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1298 
val mss' = Mss{net=net, congs=congs, bounds=b::bounds, 
0  1299 
prems=prems,mk_rews=mk_rews} 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1300 
in case botc true mss' (hyps,subst_bounds([v],t)) of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1301 
Some(hyps',t') => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1302 
Some(hyps', Abs(a, T, abstract_over(v,t'))) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1303 
 None => None 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1304 
end 
0  1305 
 t$u => (case t of 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1306 
Const("==>",_)$s => Some(impc(hyps,s,u,mss)) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1307 
 Abs(_,_,body) => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1308 
let val trec = (hyps,subst_bounds([u], body)) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1309 
in case subc mss trec of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1310 
None => Some(trec) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1311 
 trec => trec 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1312 
end 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1313 
 _ => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1314 
let fun appc() = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1315 
(case botc true mss (hyps,t) of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1316 
Some(hyps1,t1) => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1317 
(case botc true mss (hyps1,u) of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1318 
Some(hyps2,u1) => Some(hyps2,t1$u1) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1319 
 None => Some(hyps1,t1$u)) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1320 
 None => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1321 
(case botc true mss (hyps,u) of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1322 
Some(hyps1,u1) => Some(hyps1,t$u1) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1323 
 None => None)) 
0  1324 
val (h,ts) = strip_comb t 
1325 
in case h of 

1326 
Const(a,_) => 

1327 
(case assoc(congs,a) of 

1328 
None => appc() 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1329 
 Some(cong) => congc (prover mss,sign) cong trec) 
0  1330 
 _ => appc() 
1331 
end) 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1332 
 _ => None) 
0  1333 

208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1334 
and impc(hyps,s,u,mss as Mss{mk_rews,...}) = 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1335 
let val (hyps1,s1) = if simprem then try_botc mss (hyps,s) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1336 
else (hyps,s) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1337 
val mss1 = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1338 
if not useprem orelse maxidx_of_term s1 <> ~1 then mss 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1339 
else let val thm = Thm{sign=sign,hyps=[s1],prop=s1,maxidx= ~1} 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1340 
in add_simps(add_prems(mss,[thm]), mk_rews thm) end 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1341 
val (hyps2,u1) = try_botc mss1 (hyps1,u) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1342 
val hyps3 = if s1 mem hyps1 then hyps2 else hyps2\s1 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1343 
in (hyps3, Logic.mk_implies(s1,u1)) end 
0  1344 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1345 
in try_botc end; 
0  1346 

1347 

1348 
(*** Metarewriting: rewrites t to u and returns the theorem t==u ***) 

1349 
(* Parameters: 

250  1350 
mode = (simplify A, use A in simplifying B) when simplifying A ==> B 
0  1351 
mss: contains equality theorems of the form [p1,...] ==> t==u 
1352 
prover: how to solve premises in conditional rewrites and congruences 

1353 
*) 

1354 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1355 
(*** FIXME: check that #bounds(mss) does not "occur" in ct alread ***) 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1356 
fun rewrite_cterm mode mss prover ct = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

1357 
let val {sign, t, T, maxidx} = rep_cterm ct; 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1358 
val (hyps,u) = bottomc (mode,prover,sign) mss ([],t); 
0  1359 
val prop = Logic.mk_equals(t,u) 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1360 
in Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop} 
0  1361 
end 
1362 

1363 
end; 

250  1364 