author  lcp 
Mon, 21 Nov 1994 11:49:36 +0100  
changeset 721  479832ff2d29 
parent 678  6151b7f3b606 
child 776  df8f91c0e57c 
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 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

67 
val axioms_of : theory > (string * term) list 
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 additional axioms of this theory node*) 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

269 
val axioms_of = Symtab.dest o #new_axioms o rep_theory; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

270 

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

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

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

273 

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

274 

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

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

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

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

278 

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

279 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

293 

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

294 

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

295 
(* the Pure theory *) 
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 
val pure_thy = 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

298 
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

299 

0  300 

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

301 

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

302 
(** extend theory **) 
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 
fun err_dup_axms names = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

306 

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

307 
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

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

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

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

311 
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

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

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

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

315 
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

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

317 

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

318 

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

319 
(* extend signature of a theory *) 
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 
fun ext_sg extfun decls (thy as Theory {sign, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

323 

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

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

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

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

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

329 
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

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

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

332 
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

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

334 
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

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

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

337 
val add_thyname = ext_sg Sign.add_name; 
0  338 

339 

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

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

341 

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

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

343 
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

344 

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

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

346 
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

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

348 

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

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

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

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

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

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

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

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

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

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

358 

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

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

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

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

362 

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

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

367 

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

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

369 

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

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

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

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

373 
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

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

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

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

377 

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

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

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

380 

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

381 

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 
(** merge theories **) 
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 
fun merge_thy_list mk_draft thys = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

387 
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

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

389 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

403 

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

404 
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

405 

0  406 

407 

408 
(**** Primitive rules ****) 

409 

410 
(* discharge all assumptions t from ts *) 

411 
val disch = gen_rem (op aconv); 

412 

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

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

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

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

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

423 

250  424 
(* Implication introduction 
425 
A  B 

426 
 

427 
A ==> B *) 

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

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

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

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

436 
end; 

437 

438 
(* Implication elimination 

250  439 
A ==> B A 
440 
 

441 
B *) 

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

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

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

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

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

452 
prop= B} 

453 
else err("major premise") 

454 
 _ => err("major premise") 

0  455 
end; 
250  456 

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

459 
 

460 
!!x.A *) 

461 
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

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

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

469 
else result(a,T) 

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

472 
end; 

473 

474 
(* Forall elimination 

250  475 
!!x.A 
476 
 

477 
A[t/x] *) 

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

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

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

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

485 
maxidx= max[maxidx, maxt], 

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

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

0  488 
end 
489 
handle TERM _ => 

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

492 

493 
(*** Equality ***) 

494 

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

496 
val flexpair_def = 

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

499 
(read_cterm Sign.pure 

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

0  501 

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

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

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

507 

508 
(*The symmetry rule 

509 
t==u 

510 
 

511 
u==t *) 

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

513 
case prop of 

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

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

518 
(*The transitive rule 

519 
t1==u u==t2 

520 
 

521 
t1==t2 *) 

522 
fun transitive th1 th2 = 

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

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

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

526 
in case (prop1,prop2) of 

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

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

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

533 

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

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

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

540 
maxidx= maxidx_of_term t, 

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

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

0  543 
end; 
544 

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

546 
f(x) == g(x) 

547 
 

548 
f == g *) 

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

550 
case prop of 

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

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

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

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

558 
 Var _ => 

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

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

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

562 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, 

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

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

566 

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

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

569 
t == u 

570 
 

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

572 
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

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

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

0  577 
fun result T = 
578 
Thm{sign= sign, maxidx= maxidx, hyps= hyps, 

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

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

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

585 
else result T 

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

588 
end; 

589 

590 
(*The combination rule 

591 
f==g t==u 

592 
 

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

594 
fun combination th1 th2 = 

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

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

597 
in case (prop1,prop2) of 

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

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

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

603 

604 

605 
(*The equal propositions rule 

606 
A==B A 

607 
 

608 
B *) 

609 
fun equal_elim th1 th2 = 

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

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

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

613 
in case prop1 of 

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

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

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

620 

621 

622 
(* Equality introduction 

623 
A==>B B==>A 

624 
 

625 
A==B *) 

626 
fun equal_intr th1 th2 = 

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

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

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

630 
in case (prop1,prop2) of 

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

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

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

0  636 
 _ => err"premises" 
637 
end; 

638 

639 
(**** Derived rules ****) 

640 

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

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

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

644 
implies_intr_hyps 

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

0  647 
 implies_intr_hyps th = th; 
648 

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

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

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

250  654 
let fun newthm env = 
655 
let val (tpairs,horn) = 

656 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

660 
in Thm{sign= sign, hyps= hyps, 

661 
maxidx= maxidx_of_term newprop, prop= newprop} 

662 
end; 

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

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

668 
(*Instantiation of Vars 

250  669 
A 
670 
 

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

0  672 

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

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

675 

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

677 
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

678 
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

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

682 
end; 

683 

684 
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

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

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

689 
Instantiates distinct Vars by terms of same type. 

690 
Normalizes the new theorem! *) 

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

250  694 
val newprop = 
695 
Envir.norm_term (Envir.empty 0) 

696 
(subst_atomic tpairs 

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

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

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

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

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

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

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

708 
 [] => 

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

710 
ix::_ => raise THM 

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

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

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

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

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

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

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

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

727 

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

729 
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

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

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

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

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

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

735 
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

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

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

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

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

740 

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

741 

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

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

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

250  746 
prop= Type.varify(prop,tfrees)} 
0  747 
end; 
748 

749 
(* Replace all TVars by new TFrees *) 

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

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

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

753 

754 

755 
(*** Inference rules for tactics ***) 

756 

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

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

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

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

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

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

763 
end 

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

765 

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

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

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

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

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

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

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

778 
map lift_all As, lift_all B)} 

0  779 
end; 
780 

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

782 
fun assumption i state = 

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

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

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

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

788 
Logic.rule_of (tpairs, Bs, C) 

789 
else (*normalize the new rule fully*) 

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

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

793 
(Sequence.mapp newth 

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

0  796 
in addprfs (Logic.assum_pairs Bi) end; 
797 

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

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

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

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

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

0  806 
else raise THM("eq_assumption", 0, [state]) 
807 
end; 

808 

809 

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

811 

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

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

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

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

816 
fun rename_params_rule (cs, i) state = 

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

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

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

820 
val short = length iparams  length cs 

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

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

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

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

829 
 [] => (case cs inter freenames of 

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

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

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

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

836 

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

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

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

842 

843 
(* strip abstractions created by parameters *) 

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

845 

846 

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

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

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

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

854 
 strip(A,_) = f A 

0  855 
in strip end; 
856 

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

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

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

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

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

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

864 
(*unknowns appearing elsewhere be preserved!*) 

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

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

867 
(case assoc(al,x) of 

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

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

870 
 None=> t) 

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

0  874 
 rename(f$t) = rename f $ rename t 
875 
 rename(t) = t; 

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

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

880 
fun rename_bvars(dpairs, tpairs, B) = 

250  881 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  882 

883 

884 
(*** RESOLUTION ***) 

885 

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

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

887 

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

250  890 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
891 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

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

896 
 strip_assums2 BB = BB; 

897 

898 

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

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

900 
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

901 
 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

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

903 
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

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

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

906 
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

907 
 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

908 
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

909 
 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

910 

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

911 

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

916 
If eres_flg then simultaneously proves A1 by assumption. 

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

920 
local open Sequence; exception Bicompose 

921 
in 

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

925 
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

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

927 
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

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

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

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

934 
val normp = 

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

936 
else 

937 
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

938 
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

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

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

941 
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

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

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

946 
end 

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

948 
prop= Logic.rule_of normp} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

975 
(*ordinary resolution*) 

976 
fun res(None) = null 

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

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

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

982 
end; 

983 
end; (*open Sequence*) 

984 

985 

986 
fun bicompose match arg i state = 

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

988 

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

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

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

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

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

995 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  996 
end; 
997 

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

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

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

1004 
val Hs = Logic.strip_assums_hyp Bi; 

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

1006 
fun res [] = Sequence.null 

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

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

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

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

1011 
res brules)) 

1012 
else res brules 

0  1013 
in Sequence.flats (res brules) end; 
1014 

1015 

1016 

1017 
(*** Meta simp sets ***) 

1018 

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

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

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

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

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

1026 
net: discrimination net of rewrite rules 

1027 
congs: association list of congruence rules 

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

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

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

1032 

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

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

1036 
exception SIMPLIFIER of string * thm; 

1037 

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

1038 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1039 

209  1040 
val trace_simp = ref false; 
1041 

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

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

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

1045 

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

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

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

1048 
 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

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

1050 

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

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

1052 
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

1053 

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

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

1056 
is_Var(lhs) orelse 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

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

1058 
Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs)); 
0  1059 

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

1061 
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

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

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

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

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

1067 
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

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

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

1071 
else Some{thm=thm,lhs=lhs,perm=perm} 
0  1072 
end; 
1073 

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

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

1077 
in 

1078 

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

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

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

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

1086 
handle Net.INSERT => 

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

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

1089 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}); 
87  1090 

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

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

1094 
None => mss 

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

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

1097 
handle Net.INSERT => 

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

1099 
net)), 

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

1100 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews} 
87  1101 

1102 
end; 

0  1103 

1104 
val add_simps = foldl add_simp; 

87  1105 
val del_simps = foldl del_simp; 
0  1106 

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

1108 

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

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

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

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

1115 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, bounds=bounds, 
0  1116 
prems=prems, mk_rews=mk_rews} 
1117 
end; 

1118 

1119 
val (op add_congs) = foldl add_cong; 

1120 

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

1121 
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

1122 
Mss{net=net, congs=congs, bounds=bounds, prems=thms@prems, mk_rews=mk_rews}; 
0  1123 

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

1125 

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

1126 
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

1127 
Mss{net=net, congs=congs, bounds=bounds, prems=prems, mk_rews=mk_rews}; 
0  1128 
fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews; 
1129 

1130 

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

0  1135 

1136 
type prover = meta_simpset > thm > thm option; 

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

1138 
type conv = meta_simpset > termrec > termrec; 

1139 

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

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

1141 

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

1142 
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

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

1144 

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

1145 
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

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

1147 

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

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

1149 

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

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

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

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

1153 
 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

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

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

1156 

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

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

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

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

1160 
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

1161 
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

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

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

1164 

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

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

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

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

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

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

1170 
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

1171 
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

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

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

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

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

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

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

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

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

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

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

1182 

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

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

1184 

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

1187 
trace_term "Should have proved" sign prop0; 

1188 
None) 

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

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

1192 
if (lhs = lhs0) orelse 

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

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

1194 
then (trace_thm "SUCCEEDED" thm; Some(hyps,rhs)) 
0  1195 
else err() 
1196 
 _ => err() 

1197 
end; 

1198 

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

1199 
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

1200 
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

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

1202 
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

1203 
 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

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

1205 
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

1206 

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

1207 

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

1209 
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

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

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

1213 
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

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

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

1216 
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

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

1219 
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

1220 
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

1221 
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

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

1223 
then (trace_thm "Rewriting:" thm'; Some(hyps',rhs')) 
0  1224 
else (trace_thm "Trying to rewrite:" thm'; 
1225 
case prover mss thm' of 

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

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

1227 
 Some(thm2) => check_conv(thm2,prop')) 
0  1228 
end 
1229 

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

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

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

1232 
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

1233 
in case opt of None => rews rrules  some => some end; 
0  1234 

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

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

1236 
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

1237 
 _ => rews(Net.match_term net etat) 
0  1238 
end; 
1239 

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

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

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

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

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

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

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

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

1252 
fun err() = error("Failed congruence proof!") 
0  1253 

1254 
in case prover thm' of 

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

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

1256 
 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

1257 
None => err()  some => some) 
0  1258 
end; 
1259 

1260 

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

1261 

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

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

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

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

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

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

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

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

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

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

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

1272 
 None => if fail then None else Some(trec))) 
0  1273 

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

1274 
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

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

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

1277 

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

1278 
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

1279 
(trec as (hyps,t)) = 
0  1280 
(case t of 
1281 
Abs(a,T,t) => 

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

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

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

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

1286 
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

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

1288 
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

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

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

1292 
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

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

1294 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1309 
 None => None)) 
0  1310 
val (h,ts) = strip_comb t 
1311 
in case h of 

1312 
Const(a,_) => 

1313 
(case assoc(congs,a) of 

1314 
None => appc() 

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

1315 
 Some(cong) => congc (prover mss,sign) cong trec) 
0  1316 
 _ => appc() 
1317 
end) 

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

1318 
 _ => None) 
0  1319 

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

1320 
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

1321 
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

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

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

1324 
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

1325 
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

1326 
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

1327 
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

1328 
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

1329 
in (hyps3, Logic.mk_implies(s1,u1)) end 
0  1330 

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

1331 
in try_botc end; 
0  1332 

1333 

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

1335 
(* Parameters: 

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

1339 
*) 

1340 

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

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

1342 
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

1343 
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

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

1346 
in Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop} 
0  1347 
end 
1348 

1349 
end; 

250  1350 