23 -> theory -> theory |
23 -> theory -> theory |
24 val add_sigclass: class * class list -> (string * string * mixfix) list |
24 val add_sigclass: class * class list -> (string * string * mixfix) list |
25 -> theory -> theory |
25 -> theory -> theory |
26 val add_sigclass_i: class * class list -> (string * typ * mixfix) list |
26 val add_sigclass_i: class * class list -> (string * typ * mixfix) list |
27 -> theory -> theory |
27 -> theory -> theory |
28 val axclass_tac: theory -> thm list -> tactic |
|
29 val prove_classrel: theory -> class * class -> thm list |
28 val prove_classrel: theory -> class * class -> thm list |
30 -> tactic option -> thm |
29 -> tactic option -> thm |
31 val prove_arity: theory -> string * sort list * class -> thm list |
30 val prove_arity: theory -> string * sort list * class -> thm list |
32 -> tactic option -> thm |
31 -> tactic option -> thm |
33 val add_inst_subclass: class * class -> string list -> thm list |
32 val add_inst_subclass: class * class -> string list -> thm list |
34 -> tactic option -> theory -> theory |
33 -> tactic option -> theory -> theory |
35 val add_inst_arity: string * sort list * class list -> string list |
34 val add_inst_arity: string * sort list * class list -> string list |
36 -> thm list -> tactic option -> theory -> theory |
35 -> thm list -> tactic option -> theory -> theory |
37 val add_defns: (string * string) list -> theory -> theory (* FIXME *) |
36 val add_defns: (string * string) list -> theory -> theory |
38 val add_defns_i: (string * term) list -> theory -> theory (* FIXME *) |
37 val add_defns_i: (string * term) list -> theory -> theory |
39 val mk_classrel: class * class -> term |
38 val mk_classrel: class * class -> term |
40 val dest_classrel: term -> class * class |
39 val dest_classrel: term -> class * class |
41 val mk_arity: string * sort list * class -> term |
40 val mk_arity: string * sort list * class -> term |
42 val dest_arity: term -> string * sort list * class |
41 val dest_arity: term -> string * sort list * class |
43 val class_axms: theory -> thm list |
42 val class_axms: theory -> thm list |
53 |
52 |
54 structure Tactical = Goals.Tactical; |
53 structure Tactical = Goals.Tactical; |
55 structure Thm = Tactical.Thm; |
54 structure Thm = Tactical.Thm; |
56 structure Sign = Thm.Sign; |
55 structure Sign = Thm.Sign; |
57 structure Type = Sign.Type; |
56 structure Type = Sign.Type; |
|
57 structure Pretty = Sign.Syntax.Pretty; |
58 |
58 |
59 open Logic Thm Tactical Tactic Goals; |
59 open Logic Thm Tactical Tactic Goals; |
60 |
60 |
61 |
61 |
62 (* FIXME fake! - remove *) |
62 (** add constant definitions **) (* FIXME -> drule.ML (?) *) |
63 |
63 |
64 val add_defns = add_axioms; |
64 (* all_axioms_of *) |
65 val add_defns_i = add_axioms_i; |
65 |
|
66 (*results may contain duplicates!*) |
|
67 |
|
68 fun ancestry_of thy = |
|
69 thy :: flat (map ancestry_of (parents_of thy)); |
|
70 |
|
71 val all_axioms_of = flat o map axioms_of o ancestry_of; |
|
72 |
|
73 |
|
74 (* clash_types, clash_consts *) |
|
75 |
|
76 (*check if types have common instance (ignoring sorts)*) |
|
77 |
|
78 fun clash_types ty1 ty2 = |
|
79 let |
|
80 val ty1' = Type.varifyT ty1; |
|
81 val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2); |
|
82 in |
|
83 Type.raw_unify (ty1', ty2') |
|
84 end; |
|
85 |
|
86 fun clash_consts (c1, ty1) (c2, ty2) = |
|
87 c1 = c2 andalso clash_types ty1 ty2; |
|
88 |
|
89 |
|
90 (* clash_defns *) |
|
91 |
|
92 fun clash_defn c_ty (name, tm) = |
|
93 let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in |
|
94 if clash_consts c_ty (c, ty') then Some (name, ty') else None |
|
95 end handle TERM _ => None; |
|
96 |
|
97 fun clash_defns c_ty axms = |
|
98 distinct (mapfilter (clash_defn c_ty) axms); |
|
99 |
|
100 |
|
101 (* dest_defn *) |
|
102 |
|
103 fun dest_defn tm = |
|
104 let |
|
105 fun err msg = raise_term msg [tm]; |
|
106 |
|
107 val (lhs, rhs) = Logic.dest_equals tm |
|
108 handle TERM _ => err "Not a meta-equality (==)"; |
|
109 val (head, args) = strip_comb lhs; |
|
110 val (c, ty) = dest_Const head |
|
111 handle TERM _ => err "Head of lhs not a constant"; |
|
112 |
|
113 fun occs_const (Const c_ty') = clash_consts (c, ty) c_ty' |
|
114 | occs_const (Abs (_, _, t)) = occs_const t |
|
115 | occs_const (t $ u) = occs_const t orelse occs_const u |
|
116 | occs_const _ = false; |
|
117 in |
|
118 if not (forall is_Free args) then |
|
119 err "Arguments of lhs have to be variables" |
|
120 else if not (null (duplicates args)) then |
|
121 err "Duplicate variables on lhs" |
|
122 else if not (term_frees rhs subset args) then |
|
123 err "Extra variables on rhs" |
|
124 else if not (term_tfrees rhs subset typ_tfrees ty) then |
|
125 err "Extra type variables on rhs" |
|
126 else if occs_const rhs then |
|
127 err "Constant to be defined clashes with occurrence(s) on rhs" |
|
128 else (c, ty) |
|
129 end; |
|
130 |
|
131 |
|
132 (* check_defn *) |
|
133 |
|
134 fun err_in_axm name msg = |
|
135 (writeln msg; error ("The error(s) above occurred in axiom " ^ quote name)); |
|
136 |
|
137 fun check_defn sign (axms, (name, tm)) = |
|
138 let |
|
139 fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block |
|
140 [Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty])); |
|
141 |
|
142 fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn; |
|
143 fun show_defns c = commas o map (show_defn c); |
|
144 |
|
145 val (c, ty) = dest_defn tm |
|
146 handle TERM (msg, _) => err_in_axm name msg; |
|
147 val defns = clash_defns (c, ty) axms; |
|
148 in |
|
149 if not (null defns) then |
|
150 err_in_axm name ("Definition of " ^ show_const (c, ty) ^ |
|
151 " clashes with " ^ show_defns c defns) |
|
152 else (name, tm) :: axms |
|
153 end; |
|
154 |
|
155 |
|
156 (* add_defns *) |
|
157 |
|
158 fun ext_defns prep_axm raw_axms thy = |
|
159 let |
|
160 val axms = map (prep_axm (sign_of thy)) raw_axms; |
|
161 val all_axms = all_axioms_of thy; |
|
162 in |
|
163 foldl (check_defn (sign_of thy)) (all_axms, axms); |
|
164 add_axioms_i axms thy |
|
165 end; |
|
166 |
|
167 val add_defns_i = ext_defns cert_axm; |
|
168 val add_defns = ext_defns read_axm; |
66 |
169 |
67 |
170 |
68 |
171 |
69 (** utilities **) |
172 (** utilities **) |
70 |
173 |