1 (* Title: HOL/Tools/ntuple_support.ML |
1 (* Title: HOL/Tools/ntuple_support.ML |
2 Author: Thomas Sewell, NICTA |
2 Author: Thomas Sewell, NICTA |
3 |
3 |
4 Support for defining instances of tuple-like types and extracting |
4 Support for defining instances of tuple-like types and supplying |
5 introduction rules needed by the record package. |
5 introduction rules needed by the record package. |
6 *) |
6 *) |
7 |
7 |
8 |
8 |
9 signature ISTUPLE_SUPPORT = |
9 signature ISTUPLE_SUPPORT = |
10 sig |
10 sig |
11 val add_istuple_type: bstring * string list -> (typ * typ) -> theory -> |
11 val add_istuple_type: bstring * string list -> (typ * typ) -> theory -> |
12 (term * theory); |
12 (term * term * theory); |
13 type tagged_net = ((string * int) * thm) Net.net; |
|
14 |
13 |
15 val get_istuple_intros: theory -> tagged_net; |
14 val mk_cons_tuple: term * term -> term; |
|
15 val dest_cons_tuple: term -> term * term; |
16 |
16 |
17 val build_tagged_net: string -> thm list -> tagged_net; |
17 val istuple_intros_tac: theory -> int -> tactic; |
18 val resolve_from_tagged_net: tagged_net -> int -> tactic; |
18 |
19 val tag_thm_trace: thm list ref; |
19 val named_cterm_instantiate: (string * cterm) list -> thm -> thm; |
20 val merge_tagged_nets: (tagged_net * tagged_net) -> tagged_net; |
|
21 end; |
20 end; |
22 |
21 |
23 structure IsTupleSupport : ISTUPLE_SUPPORT = |
22 structure IsTupleSupport : ISTUPLE_SUPPORT = |
24 struct |
23 struct |
25 |
24 |
26 val consN = "_NTupleCons"; |
25 val isomN = "_TupleIsom"; |
27 val defN = "_def"; |
26 val defN = "_def"; |
28 |
27 |
29 val istuple_UNIV_I = thm "istuple_UNIV_I"; |
28 val istuple_UNIV_I = @{thm "istuple_UNIV_I"}; |
30 val istuple_True_simp = thm "istuple_True_simp"; |
29 val istuple_True_simp = @{thm "istuple_True_simp"}; |
31 |
30 |
32 val istuple_intro = thm "isomorphic_tuple.intro"; |
31 val istuple_intro = @{thm "isomorphic_tuple_intro"}; |
33 val istuple_intros = thms "isomorphic_tuple.intros"; |
32 val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"}); |
34 |
33 |
35 val init_intros = thms "tuple_automorphic.intros"; |
34 val constname = fst o dest_Const; |
|
35 val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple}); |
36 |
36 |
37 type tagged_net = ((string * int) * thm) Net.net; |
37 val istuple_constN = constname @{term isomorphic_tuple}; |
|
38 val istuple_consN = constname @{term istuple_cons}; |
38 |
39 |
39 (* broadly similar to the use of nets in Tactic.resolve_from_net_tac. |
40 val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"}); |
40 the tag strings identify which group of theorems a theorem in the |
|
41 net belongs to. *) |
|
42 fun build_tagged_net tag thms = let |
|
43 fun add_to_net thm (i, net) = |
|
44 (i + 1, Net.insert_term (K false) (concl_of thm, ((tag, i), thm)) net); |
|
45 val (n, net) = fold add_to_net thms (0, Net.empty); |
|
46 in net end; |
|
47 |
41 |
48 val tag_thm_trace = ref ([] : thm list); |
42 fun named_cterm_instantiate values thm = let |
|
43 fun match name (Var ((name', _), _)) = name = name' |
|
44 | match name _ = false; |
|
45 fun getvar name = case (find_first (match name) |
|
46 (OldTerm.term_vars (prop_of thm))) |
|
47 of SOME var => cterm_of (theory_of_thm thm) var |
|
48 | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]) |
|
49 in |
|
50 cterm_instantiate (map (apfst getvar) values) thm |
|
51 end; |
49 |
52 |
50 (* we check here that only theorems from a single group are being |
53 structure IsTupleThms = TheoryDataFun |
51 selected for unification, and that there are no duplicates. this |
|
52 is a good test that the net is doing its job, picking exactly the |
|
53 appropriate rules rather than overapproximating. *) |
|
54 fun tagged_thms_check t xs = let |
|
55 val tags = sort_distinct string_ord (map (fst o fst) xs); |
|
56 val ids = sort_distinct int_ord (map (snd o fst) xs); |
|
57 val thms = map snd xs; |
|
58 in |
|
59 if length tags > 1 |
|
60 then (tag_thm_trace := t :: thms; |
|
61 raise THM ("tag mismatch " ^ hd tags ^ ", " ^ nth tags 1, 1, t :: thms)) |
|
62 else if length ids < length xs |
|
63 then (tag_thm_trace := t :: thms; |
|
64 raise THM ("tag match duplicate id ", 1, t :: thms)) |
|
65 else () |
|
66 end; |
|
67 |
|
68 fun resolve_from_tagged_net net i t = |
|
69 SUBGOAL (fn (prem, i) => let |
|
70 val options = Net.unify_term net (Logic.strip_assums_concl prem); |
|
71 val sorted = sort (int_ord o pairself (snd o fst)) options; |
|
72 val check = tagged_thms_check t sorted; |
|
73 in resolve_tac (map snd sorted) i end) i t; |
|
74 |
|
75 val merge_tagged_nets = Net.merge (Thm.eq_thm_prop o pairself snd); |
|
76 |
|
77 structure IsTupleIntros = TheoryDataFun |
|
78 ( |
54 ( |
79 type T = tagged_net; |
55 type T = thm Symtab.table; |
80 val empty = build_tagged_net "initial introduction rules" init_intros; |
56 val empty = Symtab.make [tuple_istuple]; |
81 val copy = I; |
57 val copy = I; |
82 val extend = I; |
58 val extend = I; |
83 val merge = K merge_tagged_nets; |
59 val merge = K (Symtab.merge Thm.eq_thm_prop); |
84 ); |
60 ); |
85 |
|
86 val get_istuple_intros = IsTupleIntros.get; |
|
87 |
61 |
88 fun do_typedef name repT alphas thy = |
62 fun do_typedef name repT alphas thy = |
89 let |
63 let |
90 fun get_thms thy name = |
64 fun get_thms thy name = |
91 let |
65 let |
92 val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT, |
66 val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT, |
93 Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name; |
67 Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name; |
94 val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp]; |
68 val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp]; |
95 in (map rewrite_rule [rep_inject, abs_inverse], |
69 in (map rewrite_rule [rep_inject, abs_inverse], |
96 Const (absN, repT --> absT)) end; |
70 Const (absN, repT --> absT), absT) end; |
97 in |
71 in |
98 thy |
72 thy |
99 |> Typecopy.typecopy (Binding.name name, alphas) repT NONE |
73 |> Typecopy.typecopy (Binding.name name, alphas) repT NONE |
100 |-> (fn (name, _) => `(fn thy => get_thms thy name)) |
74 |-> (fn (name, _) => `(fn thy => get_thms thy name)) |
101 end; |
75 end; |
102 |
76 |
103 (* copied from earlier version of HOLogic *) |
77 fun mk_cons_tuple (left, right) = let |
104 fun mk_curry t = |
78 val (leftT, rightT) = (fastype_of left, fastype_of right); |
105 (case Term.fastype_of t of |
79 val prodT = HOLogic.mk_prodT (leftT, rightT); |
106 T as (Type ("fun", [Type ("*", [A, B]), C])) => |
80 val isomT = Type (tup_isom_typeN, [prodT, leftT, rightT]); |
107 Const ("curry", T --> A --> B --> C) $ t |
81 in |
108 | _ => raise TERM ("mk_curry: bad body type", [t])); |
82 Const (istuple_consN, isomT --> leftT --> rightT --> prodT) |
|
83 $ Const (fst tuple_istuple, isomT) $ left $ right |
|
84 end; |
109 |
85 |
110 fun add_istuple_type (name, alphas) (left, right) thy = |
86 fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right) |
|
87 = if ic = istuple_consN then (left, right) |
|
88 else raise TERM ("dest_cons_tuple", [v]) |
|
89 | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]); |
|
90 |
|
91 fun add_istuple_type (name, alphas) (leftT, rightT) thy = |
111 let |
92 let |
112 val repT = HOLogic.mk_prodT (left, right); |
93 val repT = HOLogic.mk_prodT (leftT, rightT); |
113 |
94 |
114 val (([rep_inject, abs_inverse], abs), typ_thy) = |
95 val (([rep_inject, abs_inverse], absC, absT), typ_thy) = |
115 thy |
96 thy |
116 |> do_typedef name repT alphas |
97 |> do_typedef name repT alphas |
117 ||> Sign.add_path name; |
98 ||> Sign.add_path name; |
118 |
99 |
119 val abs_curry = mk_curry abs; |
100 (* construct a type and body for the isomorphism constant by |
120 val consT = fastype_of abs_curry; |
101 instantiating the theorem to which the definition will be applied *) |
121 val consBind = Binding.name (name ^ consN); |
102 val intro_inst = rep_inject RS |
122 val cons = Const (Sign.full_name typ_thy consBind, consT); |
103 (named_cterm_instantiate [("abst", cterm_of typ_thy absC)] |
123 val cons_spec = (name ^ consN ^ defN, Logic.mk_equals (cons, abs_curry)); |
104 istuple_intro); |
|
105 val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst)); |
|
106 val isomT = fastype_of body; |
|
107 val isomBind = Binding.name (name ^ isomN); |
|
108 val isom = Const (Sign.full_name typ_thy isomBind, isomT); |
|
109 val isom_spec = (name ^ isomN ^ defN, Logic.mk_equals (isom, body)); |
124 |
110 |
125 val ([cons_def], cdef_thy) = |
111 val ([isom_def], cdef_thy) = |
126 typ_thy |
112 typ_thy |
127 |> Sign.add_consts_i [Syntax.no_syn (consBind, consT)] |
113 |> Sign.add_consts_i [Syntax.no_syn (isomBind, isomT)] |
128 |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name cons_spec)]; |
114 |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)]; |
129 |
115 |
130 val istuple = [abs_inverse, cons_def] MRS (rep_inject RS istuple_intro); |
116 val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro)); |
131 val intros = [istuple] RL istuple_intros; |
117 val cons = Const (istuple_consN, isomT --> leftT --> rightT --> absT) |
132 val intro_net = build_tagged_net name intros; |
|
133 |
118 |
134 val thm_thy = |
119 val thm_thy = |
135 cdef_thy |
120 cdef_thy |
136 |> IsTupleIntros.map (curry merge_tagged_nets intro_net) |
121 |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop |
|
122 (constname isom, istuple)) |
137 |> Sign.parent_path; |
123 |> Sign.parent_path; |
138 in |
124 in |
139 (cons, thm_thy) |
125 (isom, cons $ isom, thm_thy) |
140 end; |
126 end; |
|
127 |
|
128 fun istuple_intros_tac thy = let |
|
129 val isthms = IsTupleThms.get thy; |
|
130 fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]); |
|
131 val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let |
|
132 val goal' = Envir.beta_eta_contract goal; |
|
133 val isom = case goal' of (Const tp $ (Const pr $ Const is)) |
|
134 => if fst tp = "Trueprop" andalso fst pr = istuple_constN |
|
135 then Const is |
|
136 else err "unexpected goal predicate" goal' |
|
137 | _ => err "unexpected goal format" goal'; |
|
138 val isthm = case Symtab.lookup isthms (constname isom) of |
|
139 SOME isthm => isthm |
|
140 | NONE => err "no thm found for constant" isom; |
|
141 in rtac isthm n end); |
|
142 in |
|
143 fn n => resolve_from_net_tac istuple_intros n |
|
144 THEN use_istuple_thm_tac n |
|
145 end; |
141 |
146 |
142 end; |
147 end; |
143 |
148 |
144 |
149 |