|
1 (* Title: HOL/subtype.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 Internal interface for subtype definitions. |
|
6 *) |
|
7 |
|
8 signature SUBTYPE = |
|
9 sig |
|
10 val prove_nonempty: cterm -> thm list -> tactic option -> thm |
|
11 val add_subtype: string -> string * string list * mixfix -> |
|
12 string -> string list -> thm list -> tactic option -> theory -> theory |
|
13 val add_subtype_i: string -> string * string list * mixfix -> |
|
14 term -> string list -> thm list -> tactic option -> theory -> theory |
|
15 end; |
|
16 |
|
17 structure Subtype: SUBTYPE = |
|
18 struct |
|
19 |
|
20 open Syntax Logic HOLogic; |
|
21 |
|
22 |
|
23 (* prove non-emptyness of a set *) (*exception ERROR*) |
|
24 |
|
25 val is_def = is_equals o #prop o rep_thm; |
|
26 |
|
27 fun prove_nonempty cset thms usr_tac = |
|
28 let |
|
29 val {T = setT, t = set, maxidx, sign} = rep_cterm cset; |
|
30 val T = dest_setT setT; |
|
31 val goal = |
|
32 cterm_of sign (mk_Trueprop (mk_mem (Var (("x", maxidx + 1), T), set))); |
|
33 val tac = |
|
34 TRY (rewrite_goals_tac (filter is_def thms)) THEN |
|
35 TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN |
|
36 if_none usr_tac (TRY (ALLGOALS (fast_tac set_cs))); |
|
37 in |
|
38 prove_goalw_cterm [] goal (K [tac]) |
|
39 end |
|
40 handle ERROR => |
|
41 error ("Failed to prove non-emptyness of " ^ quote (string_of_cterm cset)); |
|
42 |
|
43 |
|
44 (* ext_subtype *) |
|
45 |
|
46 fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy = |
|
47 let |
|
48 val _ = require_thy thy "Set" "subtype definitions"; |
|
49 val sign = sign_of thy; |
|
50 |
|
51 (*rhs*) |
|
52 val cset = prep_term sign raw_set; |
|
53 val {T = setT, t = set, ...} = rep_cterm cset; |
|
54 val rhs_tfrees = term_tfrees set; |
|
55 val oldT = dest_setT setT handle TYPE _ => |
|
56 error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT)); |
|
57 |
|
58 (*lhs*) |
|
59 val lhs_tfrees = |
|
60 map (fn v => (v, if_none (assoc (rhs_tfrees, v)) termS)) vs; |
|
61 |
|
62 val tname = type_name t mx; |
|
63 val tlen = length vs; |
|
64 val newT = Type (tname, map TFree lhs_tfrees); |
|
65 |
|
66 val Rep_name = "Rep_" ^ name; |
|
67 val Abs_name = "Abs_" ^ name; |
|
68 val setC = Const (name, setT); |
|
69 val RepC = Const (Rep_name, newT --> oldT); |
|
70 val AbsC = Const (Abs_name, oldT --> newT); |
|
71 val x_new = Free ("x", newT); |
|
72 val y_old = Free ("y", oldT); |
|
73 |
|
74 (*axioms*) |
|
75 val rep_type = mk_Trueprop (mk_mem (RepC $ x_new, setC)); |
|
76 val rep_type_inv = mk_Trueprop (mk_eq (AbsC $ (RepC $ x_new), x_new)); |
|
77 val abs_type_inv = mk_implies (mk_Trueprop (mk_mem (y_old, setC)), |
|
78 mk_Trueprop (mk_eq (RepC $ (AbsC $ y_old), y_old))); |
|
79 |
|
80 |
|
81 (* errors *) |
|
82 |
|
83 val show_names = commas_quote o map fst; |
|
84 |
|
85 val illegal_vars = |
|
86 if null (term_vars set) andalso null (term_tvars set) then [] |
|
87 else ["Illegal schematic variable(s) on rhs"]; |
|
88 |
|
89 val dup_lhs_tfrees = |
|
90 (case duplicates lhs_tfrees of [] => [] |
|
91 | dups => ["Duplicate type variables on lhs: " ^ show_names dups]); |
|
92 |
|
93 val extra_rhs_tfrees = |
|
94 (case gen_rems (op =) (rhs_tfrees, lhs_tfrees) of [] => [] |
|
95 | extras => ["Extra type variables on rhs: " ^ show_names extras]); |
|
96 |
|
97 val illegal_frees = |
|
98 (case term_frees set of [] => [] |
|
99 | xs => ["Illegal variables on rhs: " ^ show_names (map dest_Free xs)]); |
|
100 |
|
101 val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees; |
|
102 in |
|
103 if null errs then () |
|
104 else error (cat_lines errs); |
|
105 |
|
106 prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac; |
|
107 |
|
108 thy |
|
109 |> add_types [(t, tlen, mx)] |
|
110 |> add_arities |
|
111 [(tname, replicate tlen logicS, logicS), |
|
112 (tname, replicate tlen termS, termS)] |
|
113 |> add_consts_i |
|
114 [(name, setT, NoSyn), |
|
115 (Rep_name, newT --> oldT, NoSyn), |
|
116 (Abs_name, oldT --> newT, NoSyn)] |
|
117 |> add_defs_i |
|
118 [(name ^ "_def", mk_equals (setC, set))] |
|
119 |> add_axioms_i |
|
120 [(Rep_name, rep_type), |
|
121 (Rep_name ^ "_inverse", rep_type_inv), |
|
122 (Abs_name ^ "_inverse", abs_type_inv)] |
|
123 end |
|
124 handle ERROR => |
|
125 error ("The error(s) above occurred in subtype definition " ^ quote name); |
|
126 |
|
127 |
|
128 (* external interfaces *) |
|
129 |
|
130 fun cert_term sg tm = |
|
131 cterm_of sg tm handle TERM (msg, _) => error msg; |
|
132 |
|
133 fun read_term sg str = |
|
134 read_cterm sg (str, termTVar); |
|
135 |
|
136 val add_subtype = ext_subtype read_term; |
|
137 val add_subtype_i = ext_subtype cert_term; |
|
138 |
|
139 |
|
140 end; |
|
141 |