author  nipkow 
Thu, 16 Feb 1995 08:55:15 +0100  
changeset 900  8e22076cd3ca 
parent 898  4f9c8503d1c5 
child 922  196ca0973a6d 
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 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

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

106 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

107 
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

108 
val reflexive : cterm > thm 
0  109 
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

110 
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

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

112 
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

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

114 
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

115 
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

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

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

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

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

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

121 
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

122 
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

123 
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

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

125 
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

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

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

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

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

130 
val varifyT : thm > thm 
250  131 
end; 
0  132 

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

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

0  137 
structure Sequence = Unify.Sequence; 
138 
structure Envir = Unify.Envir; 

139 
structure Sign = Unify.Sign; 

140 
structure Type = Sign.Type; 

141 
structure Syntax = Sign.Syntax; 

142 
structure Symtab = Sign.Symtab; 

143 

144 

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

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

146 

250  147 
(** certified types **) 
148 

149 
(*certified typs under a signature*) 

150 

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

152 

153 
fun rep_ctyp (Ctyp args) = args; 

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

155 

156 
fun ctyp_of sign T = 

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

158 

159 
fun read_ctyp sign s = 

160 
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

161 

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

162 

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

163 

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

165 

250  166 
(*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

167 

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

169 

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

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

172 

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

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

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

177 
end handle TYPE (msg, _, _) 

178 
=> 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

179 

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

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

182 

250  183 
(*dest_implies for cterms. Note T=prop below*) 
184 
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

185 
(Cterm{sign=sign, T=T, maxidx=maxidx, t=A}, 
250  186 
Cterm{sign=sign, T=T, maxidx=maxidx, t=B}) 
187 
 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

188 

250  189 

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

190 

574  191 
(** read cterms **) (*exception ERROR*) 
250  192 

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

194 
fun read_def_cterm (sign, types, sorts) (a, T) = 

195 
let 

574  196 
val T' = Sign.certify_typ sign T 
197 
handle TYPE (msg, _, _) => error msg; 

623  198 
val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a; 
199 
val (_, t', tye) = Sign.infer_types sign types sorts true (ts, T'); 

574  200 
val ct = cterm_of sign t' 
201 
handle TERM (msg, _) => error msg; 

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

203 

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

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

205 

250  206 

207 

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

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

209 

0  210 
datatype thm = Thm of 
250  211 
{sign: Sign.sg, maxidx: int, hyps: term list, prop: term}; 
0  212 

250  213 
fun rep_thm (Thm args) = args; 
0  214 

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

215 
(*errors involving theorems*) 
0  216 
exception THM of string * int * thm list; 
217 

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

218 

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

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

220 
val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm; 
0  221 

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

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

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

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

226 

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

227 

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

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

229 
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

230 

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

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

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

233 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  234 

235 
(*counts premises in a rule*) 

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

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

237 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  238 

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

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

240 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  241 

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

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

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

244 
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

245 

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

246 

0  247 

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

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

249 

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

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

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

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

254 
parents: theory list}; 
0  255 

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

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

257 

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

258 
(*errors involving theories*) 
0  259 
exception THEORY of string * theory list; 
260 

261 

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

262 
val sign_of = #sign o rep_theory; 
0  263 
val syn_of = #syn o Sign.rep_sg o sign_of; 
264 

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

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

266 
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

267 

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

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

269 
val parents_of = #parents o rep_theory; 
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 

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

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

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

274 
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

275 

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

276 

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

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

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

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

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

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

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

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

284 
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

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

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

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

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

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

290 

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

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

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

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

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

295 

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

296 

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

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

298 

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

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

300 
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

301 

0  302 

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

303 

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

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

305 

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

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

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

308 

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

309 
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

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

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

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

313 
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

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

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

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

317 
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

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

319 

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

320 

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

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

322 

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

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

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

325 

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

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

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

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

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

331 
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

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

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

334 
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

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

336 
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

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

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

339 
val add_thyname = ext_sg Sign.add_name; 
0  340 

341 

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

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

343 

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

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

345 
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

346 

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

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

348 
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

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

350 

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

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

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

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

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

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

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

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

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

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

360 

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

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

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

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

364 

564  365 
fun inferT_axm sg (name, pre_tm) = 
623  366 
(name, no_vars (#2 (Sign.infer_types sg (K None) (K None) true ([pre_tm], propT)))) 
564  367 
handle ERROR => err_in_axm name; 
368 

387
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 
(* extend axioms of a theory *) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

371 

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

372 
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

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

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

375 
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

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

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

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

379 

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

380 
val add_axioms = ext_axms read_axm; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

381 
val add_axioms_i = ext_axms cert_axm; 
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 

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

384 

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

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

386 

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

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

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

389 
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

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

391 

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

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

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

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

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

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

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

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

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

400 
(if mk_draft then Sign.make_draft else I) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

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

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

405 

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

406 
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

407 

0  408 

409 

410 
(**** Primitive rules ****) 

411 

412 
(* discharge all assumptions t from ts *) 

413 
val disch = gen_rem (op aconv); 

414 

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

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

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

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

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

425 

250  426 
(* Implication introduction 
427 
A  B 

428 
 

429 
A ==> B *) 

0  430 
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

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

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

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

438 
end; 

439 

440 
(* Implication elimination 

250  441 
A ==> B A 
442 
 

443 
B *) 

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

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

0  448 
in case prop of 
250  449 
imp$A$B => 
450 
if imp=implies andalso A aconv propA 

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

451 
then Thm{sign= merge_thm_sgs(thAB,thA), 
250  452 
maxidx= max[maxA,maxidx], 
453 
hyps= hypsA union hyps, (*dups suppressed*) 

454 
prop= B} 

455 
else err("major premise") 

456 
 _ => err("major premise") 

0  457 
end; 
250  458 

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

461 
 

462 
!!x.A *) 

463 
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

464 
let val x = term_of cx; 
0  465 
fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps, 
250  466 
prop= all(T) $ Abs(a, T, abstract_over (x,prop))} 
0  467 
in case x of 
250  468 
Free(a,T) => 
469 
if exists (apl(x, Logic.occs)) hyps 

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

471 
else result(a,T) 

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

474 
end; 

475 

476 
(* Forall elimination 

250  477 
!!x.A 
478 
 

479 
A[t/x] *) 

0  480 
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

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

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

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

487 
maxidx= max[maxidx, maxt], 

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

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

0  490 
end 
491 
handle TERM _ => 

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

494 

495 
(*** Equality ***) 

496 

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

498 
val flexpair_def = 

250  499 
Thm{sign= Sign.pure, hyps= [], maxidx= 0, 
500 
prop= term_of 

501 
(read_cterm Sign.pure 

502 
("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))}; 

0  503 

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

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

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

509 

510 
(*The symmetry rule 

511 
t==u 

512 
 

513 
u==t *) 

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

515 
case prop of 

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

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

520 
(*The transitive rule 

521 
t1==u u==t2 

522 
 

523 
t1==t2 *) 

524 
fun transitive th1 th2 = 

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

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

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

528 
in case (prop1,prop2) of 

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

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

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

535 

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

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

538 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  539 
in case t of 
250  540 
Abs(_,_,bodt) $ u => 
541 
Thm{sign= sign, hyps= [], 

542 
maxidx= maxidx_of_term t, 

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

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

0  545 
end; 
546 

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

548 
f(x) == g(x) 

549 
 

550 
f == g *) 

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

552 
case prop of 

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

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

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

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

560 
 Var _ => 

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

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

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

564 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, 

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

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

568 

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

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

571 
t == u 

572 
 

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

574 
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

575 
let val x = term_of cx; 
250  576 
val (t,u) = Logic.dest_equals prop 
577 
handle TERM _ => 

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

0  579 
fun result T = 
580 
Thm{sign= sign, maxidx= maxidx, hyps= hyps, 

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

0  583 
in case x of 
250  584 
Free(_,T) => 
585 
if exists (apl(x, Logic.occs)) hyps 

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

587 
else result T 

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

590 
end; 

591 

592 
(*The combination rule 

593 
f==g t==u 

594 
 

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

596 
fun combination th1 th2 = 

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

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

599 
in case (prop1,prop2) of 

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

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

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

605 

606 

607 
(*The equal propositions rule 

608 
A==B A 

609 
 

610 
B *) 

611 
fun equal_elim th1 th2 = 

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

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

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

615 
in case prop1 of 

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

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

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

622 

623 

624 
(* Equality introduction 

625 
A==>B B==>A 

626 
 

627 
A==B *) 

628 
fun equal_intr th1 th2 = 

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

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

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

632 
in case (prop1,prop2) of 

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

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

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

0  638 
 _ => err"premises" 
639 
end; 

640 

641 
(**** Derived rules ****) 

642 

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

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

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

646 
implies_intr_hyps 

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

0  649 
 implies_intr_hyps th = th; 
650 

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

250  652 
Instantiates the theorem and deletes trivial tpairs. 
0  653 
Resulting sequence may contain multiple elements if the tpairs are 
654 
not all flexflex. *) 

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

250  656 
let fun newthm env = 
657 
let val (tpairs,horn) = 

658 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

662 
in Thm{sign= sign, hyps= hyps, 

663 
maxidx= maxidx_of_term newprop, prop= newprop} 

664 
end; 

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

250  667 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  668 
end; 
669 

670 
(*Instantiation of Vars 

250  671 
A 
672 
 

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

0  674 

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

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

677 

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

679 
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

680 
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

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

684 
end; 

685 

686 
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

687 
let val {T,sign} = rep_ctyp ctyp 
0  688 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
689 

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

691 
Instantiates distinct Vars by terms of same type. 

692 
Normalizes the new theorem! *) 

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

250  696 
val newprop = 
697 
Envir.norm_term (Envir.empty 0) 

698 
(subst_atomic tpairs 

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

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

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

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

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

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

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

710 
 [] => 

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

712 
ix::_ => raise THM 

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

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

193  715 
 [] => newth 
0  716 
end 
250  717 
handle TERM _ => 
0  718 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  719 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  720 

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

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

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

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

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

729 

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

731 
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

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

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

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

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

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

737 
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

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

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

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

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

742 

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

743 

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

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

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

250  748 
prop= Type.varify(prop,tfrees)} 
0  749 
end; 
750 

751 
(* Replace all TVars by new TFrees *) 

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

753 
let val prop' = Type.freeze (K true) prop 

754 
in Thm{sign=sign, maxidx=maxidx_of_term prop', hyps=hyps, prop=prop'} end; 

755 

756 

757 
(*** Inference rules for tactics ***) 

758 

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

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

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

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

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

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

765 
end 

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

767 

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

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

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

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

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

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

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

780 
map lift_all As, lift_all B)} 

0  781 
end; 
782 

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

784 
fun assumption i state = 

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

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

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

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

790 
Logic.rule_of (tpairs, Bs, C) 

791 
else (*normalize the new rule fully*) 

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

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

795 
(Sequence.mapp newth 

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

0  798 
in addprfs (Logic.assum_pairs Bi) end; 
799 

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

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

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

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

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

0  808 
else raise THM("eq_assumption", 0, [state]) 
809 
end; 

810 

811 

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

813 

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

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

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

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

818 
fun rename_params_rule (cs, i) state = 

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

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

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

822 
val short = length iparams  length cs 

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

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

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

250  828 
in 
0  829 
case findrep cs of 
830 
c::_ => error ("Bound variables not distinct: " ^ c) 

831 
 [] => (case cs inter freenames of 

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

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

250  834 
Logic.rule_of(tpairs, Bs@[newBi], C)}) 
0  835 
end; 
836 

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

838 

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

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

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

844 

845 
(* strip abstractions created by parameters *) 

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

847 

848 

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

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

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

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

856 
 strip(A,_) = f A 

0  857 
in strip end; 
858 

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

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

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

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

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

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

866 
(*unknowns appearing elsewhere be preserved!*) 

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

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

869 
(case assoc(al,x) of 

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

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

872 
 None=> t) 

0  873 
 rename(Abs(x,T,t)) = 
250  874 
Abs(case assoc(al,x) of Some(y) => y  None => x, 
875 
T, rename t) 

0  876 
 rename(f$t) = rename f $ rename t 
877 
 rename(t) = t; 

250  878 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  879 
in strip_ren end; 
880 

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

882 
fun rename_bvars(dpairs, tpairs, B) = 

250  883 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  884 

885 

886 
(*** RESOLUTION ***) 

887 

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

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

889 

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

250  892 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
893 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  894 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  895 
Const("all",_)$Abs(_,_,t2)) = 
0  896 
let val (B1,B2) = strip_assums2 (t1,t2) 
897 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

898 
 strip_assums2 BB = BB; 

899 

900 

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

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

902 
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

903 
 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

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

905 
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

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

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

908 
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

909 
 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

910 
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

911 
 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

912 

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

913 

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

918 
If eres_flg then simultaneously proves A1 by assumption. 

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

922 
local open Sequence; exception Bicompose 

923 
in 

250  924 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  925 
(eres_flg, orule, nsubgoal) = 
926 
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

927 
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

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

929 
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

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

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

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

936 
val normp = 

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

938 
else 

939 
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

940 
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

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

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

943 
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

944 
else (ntps, Bs @ map normt As, C) 
250  945 
else if match then raise Bicompose 
946 
else (*normalize the new rule fully*) 

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

948 
end 

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

950 
prop= Logic.rule_of normp} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

977 
(*ordinary resolution*) 

978 
fun res(None) = null 

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

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

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

984 
end; 

985 
end; (*open Sequence*) 

986 

987 

988 
fun bicompose match arg i state = 

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

990 

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

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

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

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

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

997 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  998 
end; 
999 

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

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

250  1002 
fun biresolution match brules i state = 
0  1003 
let val lift = lift_rule(state, i); 
250  1004 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
1005 
val B = Logic.strip_assums_concl Bi; 

1006 
val Hs = Logic.strip_assums_hyp Bi; 

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

1008 
fun res [] = Sequence.null 

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

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

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

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

1013 
res brules)) 

1014 
else res brules 

0  1015 
in Sequence.flats (res brules) end; 
1016 

1017 

1018 

1019 
(*** Meta simp sets ***) 

1020 

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

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

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

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

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

1028 
net: discrimination net of rewrite rules 

1029 
congs: association list of congruence rules 

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

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

1031 
for generating new names when rewriting under lambda abstractions 
0  1032 
mk_rews: used when local assumptions are added 
1033 
*) 

1034 

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

1035 
val empty_mss = Mss{net= Net.empty, congs= [], bounds=[], prems= [], 
0  1036 
mk_rews = K[]}; 
1037 

1038 
exception SIMPLIFIER of string * thm; 

1039 

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

1040 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1041 

209  1042 
val trace_simp = ref false; 
1043 

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

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

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

1047 

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

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

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

1050 
 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

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

1052 

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

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

1054 
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

1055 

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

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

1058 
is_Var(lhs) orelse 
900  1059 
(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

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

1061 
Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs)); 
0  1062 

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

1064 
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

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

1066 
val (lhs,_) = Logic.dest_equals concl handle TERM _ => 
0  1067 
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

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

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

1070 
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

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

1072 
in if not perm andalso loops sign prems (elhs,erhs) 
0  1073 
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

1074 
else Some{thm=thm,lhs=lhs,perm=perm} 
0  1075 
end; 
1076 

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

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

1080 
in 

1081 

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

1082 
fun add_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, 
0  1083 
thm as Thm{sign,prop,...}) = 
87  1084 
case mk_rrule thm of 
1085 
None => mss 

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

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

1089 
handle Net.INSERT => 

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

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

1092 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}); 
87  1093 

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

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

1097 
None => mss 

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

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

1100 
handle Net.INSERT => 

1101 
(prtm "Warning: rewrite rule not in simpset" 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 

1105 
end; 

0  1106 

1107 
val add_simps = foldl add_simp; 

87  1108 
val del_simps = foldl del_simp; 
0  1109 

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

1111 

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

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

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

1115 
(* val lhs = Pattern.eta_contract lhs*) 
0  1116 
val (a,_) = dest_Const (head_of lhs) handle TERM _ => 
1117 
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

1118 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, bounds=bounds, 
0  1119 
prems=prems, mk_rews=mk_rews} 
1120 
end; 

1121 

1122 
val (op add_congs) = foldl add_cong; 

1123 

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

1124 
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

1125 
Mss{net=net, congs=congs, bounds=bounds, prems=thms@prems, mk_rews=mk_rews}; 
0  1126 

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

1128 

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

1129 
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

1130 
Mss{net=net, congs=congs, bounds=bounds, prems=prems, mk_rews=mk_rews}; 
0  1131 
fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews; 
1132 

1133 

250  1134 
(*** Metalevel rewriting 
0  1135 
uses conversions, omitting proofs for efficiency. See 
250  1136 
L C Paulson, A higherorder implementation of rewriting, 
1137 
Science of Computer Programming 3 (1983), pages 119149. ***) 

0  1138 

1139 
type prover = meta_simpset > thm > thm option; 

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

1141 
type conv = meta_simpset > termrec > termrec; 

1142 

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

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

1144 

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

1145 
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

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

1147 

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

1148 
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

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

1150 

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

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

1152 

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

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

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

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

1156 
 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

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

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

1159 

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

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

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

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

1163 
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

1164 
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

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

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

1167 

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

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

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

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

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

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

1173 
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

1174 
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

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

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

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

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

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

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

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

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

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

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

1185 

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

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

1187 

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

1190 
trace_term "Should have proved" sign prop0; 

1191 
None) 

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

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

1195 
if (lhs = lhs0) orelse 

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

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

1197 
then (trace_thm "SUCCEEDED" thm; Some(hyps,rhs)) 
0  1198 
else err() 
1199 
 _ => err() 

1200 
end; 

1201 

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

1202 
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

1203 
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

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

1205 
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

1206 
 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

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

1208 
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

1209 

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

1210 

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

1212 
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

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

1214 
fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs, perm} = 
250  1215 
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

1216 
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

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

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

1219 
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

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

1222 
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

1223 
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

1224 
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

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

1226 
then (trace_thm "Rewriting:" thm'; Some(hyps',rhs')) 
0  1227 
else (trace_thm "Trying to rewrite:" thm'; 
1228 
case prover mss thm' of 

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

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

1230 
 Some(thm2) => check_conv(thm2,prop')) 
0  1231 
end 
1232 

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

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

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

1235 
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

1236 
in case opt of None => rews rrules  some => some end; 
0  1237 

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

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

1239 
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

1240 
 _ => rews(Net.match_term net etat) 
0  1241 
end; 
1242 

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

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

1244 
fun congc (prover,signt) {thm=cong,lhs=lhs} (hypst,t) = 
0  1245 
let val Thm{sign,hyps,maxidx,prop,...} = cong 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1246 
val unit = if Sign.subsig(sign,signt) then () 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1247 
else error("Congruence rule from different theory") 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1248 
val tsig = #tsig(Sign.rep_sg signt) 
0  1249 
val insts = Pattern.match tsig (lhs,t) handle Pattern.MATCH => 
1250 
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

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

1252 
val thm' = Thm{sign=signt, hyps=hyps union hypst, 
0  1253 
prop=prop', maxidx=maxidx} 
1254 
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

1255 
fun err() = error("Failed congruence proof!") 
0  1256 

1257 
in case prover thm' of 

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

1258 
None => err() 
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

1259 
 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

1260 
None => err()  some => some) 
0  1261 
end; 
1262 

1263 

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

1264 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1265 
fun bottomc ((simprem,useprem),prover,sign) = 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1266 
let fun botc fail mss trec = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1267 
(case subc mss trec of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1268 
some as Some(trec1) => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1269 
(case rewritec (prover,sign) mss trec1 of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1270 
Some(trec2) => botc false mss trec2 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1271 
 None => some) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1272 
 None => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1273 
(case rewritec (prover,sign) mss trec of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1274 
Some(trec2) => botc false mss trec2 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1275 
 None => if fail then None else Some(trec))) 
0  1276 

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

1277 
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

1278 
Some(trec1) => trec1 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1279 
 None => trec) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1280 

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

1281 
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

1282 
(trec as (hyps,t)) = 
0  1283 
(case t of 
1284 
Abs(a,T,t) => 

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

1285 
let val b = variant bounds a 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1286 
val v = Free("." ^ b,T) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1287 
val mss' = Mss{net=net, congs=congs, bounds=b::bounds, 
0  1288 
prems=prems,mk_rews=mk_rews} 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1289 
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

1290 
Some(hyps',t') => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1291 
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

1292 
 None => None 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1293 
end 
0  1294 
 t$u => (case t of 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1295 
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

1296 
 Abs(_,_,body) => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1297 
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

1298 
in case subc mss trec of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1299 
None => Some(trec) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1300 
 trec => trec 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

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

1302 
 _ => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1303 
let fun appc() = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1304 
(case botc true mss (hyps,t) of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1305 
Some(hyps1,t1) => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1306 
(case botc true mss (hyps1,u) of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1307 
Some(hyps2,u1) => Some(hyps2,t1$u1) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1308 
 None => Some(hyps1,t1$u)) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1309 
 None => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1310 
(case botc true mss (hyps,u) of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1311 
Some(hyps1,u1) => Some(hyps1,t$u1) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1312 
 None => None)) 
0  1313 
val (h,ts) = strip_comb t 
1314 
in case h of 

1315 
Const(a,_) => 

1316 
(case assoc(congs,a) of 

1317 
None => appc() 

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

1318 
 Some(cong) => congc (prover mss,sign) cong trec) 
0  1319 
 _ => appc() 
1320 
end) 

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

1321 
 _ => None) 
0  1322 

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

1323 
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

1324 
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

1325 
else (hyps,s) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1326 
val mss1 = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1327 
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

1328 
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

1329 
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

1330 
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

1331 
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

1332 
in (hyps3, Logic.mk_implies(s1,u1)) end 
0  1333 

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

1334 
in try_botc end; 
0  1335 

1336 

1337 
(*** Metarewriting: rewrites t to u and returns the theorem t==u ***) 

1338 
(* Parameters: 

250  1339 
mode = (simplify A, use A in simplifying B) when simplifying A ==> B 
0  1340 
mss: contains equality theorems of the form [p1,...] ==> t==u 
1341 
prover: how to solve premises in conditional rewrites and congruences 

1342 
*) 

1343 

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

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

1345 
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

1346 
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

1347 
val (hyps,u) = bottomc (mode,prover,sign) mss ([],t); 
0  1348 
val prop = Logic.mk_equals(t,u) 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1349 
in Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop} 
0  1350 
end 
1351 

1352 
end; 

250  1353 