48 -> (string * typ * mixfix) list -> theory -> theory |
48 -> (string * typ * mixfix) list -> theory -> theory |
49 val setup: theory -> theory |
49 val setup: theory -> theory |
50 end; |
50 end; |
51 |
51 |
52 |
52 |
53 signature ISTUPLE_SUPPORT = |
53 signature ISO_TUPLE_SUPPORT = |
54 sig |
54 sig |
55 val add_istuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory |
55 val add_iso_tuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory |
56 val mk_cons_tuple: term * term -> term |
56 val mk_cons_tuple: term * term -> term |
57 val dest_cons_tuple: term -> term * term |
57 val dest_cons_tuple: term -> term * term |
58 val istuple_intros_tac: int -> tactic |
58 val iso_tuple_intros_tac: int -> tactic |
59 val named_cterm_instantiate: (string * cterm) list -> thm -> thm |
59 val named_cterm_instantiate: (string * cterm) list -> thm -> thm |
60 end; |
60 end; |
61 |
61 |
62 structure IsTupleSupport: ISTUPLE_SUPPORT = |
62 structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT = |
63 struct |
63 struct |
64 |
64 |
65 val isomN = "_TupleIsom"; |
65 val isoN = "_Tuple_Iso"; |
66 |
66 |
67 val istuple_intro = @{thm isomorphic_tuple_intro}; |
67 val iso_tuple_intro = @{thm isomorphic_tuple_intro}; |
68 val istuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros}; |
68 val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros}; |
69 |
69 |
70 val tuple_istuple = (@{const_name tuple_istuple}, @{thm tuple_istuple}); |
70 val tuple_iso_tuple = (@{const_name tuple_iso_tuple}, @{thm tuple_iso_tuple}); |
71 |
71 |
72 fun named_cterm_instantiate values thm = |
72 fun named_cterm_instantiate values thm = |
73 let |
73 let |
74 fun match name ((name', _), _) = name = name' |
74 fun match name ((name', _), _) = name = name' |
75 | match name _ = false; |
75 | match name _ = false; |
79 | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])); |
79 | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])); |
80 in |
80 in |
81 cterm_instantiate (map (apfst getvar) values) thm |
81 cterm_instantiate (map (apfst getvar) values) thm |
82 end; |
82 end; |
83 |
83 |
84 structure IsTupleThms = Theory_Data |
84 structure Iso_Tuple_Thms = Theory_Data |
85 ( |
85 ( |
86 type T = thm Symtab.table; |
86 type T = thm Symtab.table; |
87 val empty = Symtab.make [tuple_istuple]; |
87 val empty = Symtab.make [tuple_iso_tuple]; |
88 val extend = I; |
88 val extend = I; |
89 fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *) |
89 fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *) |
90 ); |
90 ); |
91 |
91 |
92 fun do_typedef name repT alphas thy = |
92 fun do_typedef name repT alphas thy = |
94 fun get_thms thy name = |
94 fun get_thms thy name = |
95 let |
95 let |
96 val SOME {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT, |
96 val SOME {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT, |
97 Abs_inverse = abs_inverse, ...} = Typedef.get_info thy name; |
97 Abs_inverse = abs_inverse, ...} = Typedef.get_info thy name; |
98 val rewrite_rule = |
98 val rewrite_rule = |
99 MetaSimplifier.rewrite_rule [@{thm istuple_UNIV_I}, @{thm istuple_True_simp}]; |
99 MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}]; |
100 in |
100 in |
101 (map rewrite_rule [rep_inject, abs_inverse], Const (absN, repT --> absT), absT) |
101 (map rewrite_rule [rep_inject, abs_inverse], Const (absN, repT --> absT), absT) |
102 end; |
102 end; |
103 in |
103 in |
104 thy |
104 thy |
110 let |
110 let |
111 val (leftT, rightT) = (fastype_of left, fastype_of right); |
111 val (leftT, rightT) = (fastype_of left, fastype_of right); |
112 val prodT = HOLogic.mk_prodT (leftT, rightT); |
112 val prodT = HOLogic.mk_prodT (leftT, rightT); |
113 val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]); |
113 val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]); |
114 in |
114 in |
115 Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> prodT) $ |
115 Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $ |
116 Const (fst tuple_istuple, isomT) $ left $ right |
116 Const (fst tuple_iso_tuple, isomT) $ left $ right |
117 end; |
117 end; |
118 |
118 |
119 fun dest_cons_tuple (Const (@{const_name istuple_cons}, _) $ Const _ $ t $ u) = (t, u) |
119 fun dest_cons_tuple (Const (@{const_name iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u) |
120 | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]); |
120 | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]); |
121 |
121 |
122 fun add_istuple_type (name, alphas) (leftT, rightT) thy = |
122 fun add_iso_tuple_type (name, alphas) (leftT, rightT) thy = |
123 let |
123 let |
124 val repT = HOLogic.mk_prodT (leftT, rightT); |
124 val repT = HOLogic.mk_prodT (leftT, rightT); |
125 |
125 |
126 val (([rep_inject, abs_inverse], absC, absT), typ_thy) = |
126 val (([rep_inject, abs_inverse], absC, absT), typ_thy) = |
127 thy |
127 thy |
129 ||> Sign.add_path name; |
129 ||> Sign.add_path name; |
130 |
130 |
131 (*construct a type and body for the isomorphism constant by |
131 (*construct a type and body for the isomorphism constant by |
132 instantiating the theorem to which the definition will be applied*) |
132 instantiating the theorem to which the definition will be applied*) |
133 val intro_inst = |
133 val intro_inst = |
134 rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] istuple_intro; |
134 rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro; |
135 val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst)); |
135 val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst)); |
136 val isomT = fastype_of body; |
136 val isomT = fastype_of body; |
137 val isom_bind = Binding.name (name ^ isomN); |
137 val isom_bind = Binding.name (name ^ isoN); |
138 val isom_name = Sign.full_name typ_thy isom_bind; |
138 val isom_name = Sign.full_name typ_thy isom_bind; |
139 val isom = Const (isom_name, isomT); |
139 val isom = Const (isom_name, isomT); |
140 val isom_spec = (Thm.def_name (name ^ isomN), Logic.mk_equals (isom, body)); |
140 val isom_spec = (Thm.def_name (name ^ isoN), Logic.mk_equals (isom, body)); |
141 |
141 |
142 val ([isom_def], cdef_thy) = |
142 val ([isom_def], cdef_thy) = |
143 typ_thy |
143 typ_thy |
144 |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)] |
144 |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)] |
145 |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)]; |
145 |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)]; |
146 |
146 |
147 val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro)); |
147 val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro)); |
148 val cons = Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> absT); |
148 val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT); |
149 |
149 |
150 val thm_thy = |
150 val thm_thy = |
151 cdef_thy |
151 cdef_thy |
152 |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (isom_name, istuple)) |
152 |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple)) |
153 |> Sign.parent_path |
153 |> Sign.parent_path |
154 |> Code.add_default_eqn isom_def; |
154 |> Code.add_default_eqn isom_def; |
155 in |
155 in |
156 ((isom, cons $ isom), thm_thy) |
156 ((isom, cons $ isom), thm_thy) |
157 end; |
157 end; |
158 |
158 |
159 val istuple_intros_tac = resolve_from_net_tac istuple_intros THEN' |
159 val iso_tuple_intros_tac = resolve_from_net_tac iso_tuple_intros THEN' |
160 CSUBGOAL (fn (cgoal, i) => |
160 CSUBGOAL (fn (cgoal, i) => |
161 let |
161 let |
162 val thy = Thm.theory_of_cterm cgoal; |
162 val thy = Thm.theory_of_cterm cgoal; |
163 val goal = Thm.term_of cgoal; |
163 val goal = Thm.term_of cgoal; |
164 |
164 |
165 val isthms = IsTupleThms.get thy; |
165 val isthms = Iso_Tuple_Thms.get thy; |
166 fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]); |
166 fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]); |
167 |
167 |
168 val goal' = Envir.beta_eta_contract goal; |
168 val goal' = Envir.beta_eta_contract goal; |
169 val is = |
169 val is = |
170 (case goal' of |
170 (case goal' of |
171 Const (@{const_name Trueprop}, _) $ |
171 Const (@{const_name Trueprop}, _) $ |
195 val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}]; |
195 val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}]; |
196 val Not_eq_iff = @{thm Not_eq_iff}; |
196 val Not_eq_iff = @{thm Not_eq_iff}; |
197 |
197 |
198 val refl_conj_eq = @{thm refl_conj_eq}; |
198 val refl_conj_eq = @{thm refl_conj_eq}; |
199 |
199 |
200 val surject_assistI = @{thm "istuple_surjective_proof_assistI"}; |
200 val surject_assistI = @{thm "iso_tuple_surjective_proof_assistI"}; |
201 val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"}; |
201 val surject_assist_idE = @{thm "iso_tuple_surjective_proof_assist_idE"}; |
202 |
202 |
203 val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"}; |
203 val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"}; |
204 val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"}; |
204 val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"}; |
205 val updacc_eq_idI = @{thm "istuple_update_accessor_eq_assist_idI"}; |
205 val updacc_eq_idI = @{thm "iso_tuple_update_accessor_eq_assist_idI"}; |
206 val updacc_eq_triv = @{thm "istuple_update_accessor_eq_assist_triv"}; |
206 val updacc_eq_triv = @{thm "iso_tuple_update_accessor_eq_assist_triv"}; |
207 |
207 |
208 val updacc_foldE = @{thm "update_accessor_congruence_foldE"}; |
208 val updacc_foldE = @{thm "update_accessor_congruence_foldE"}; |
209 val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"}; |
209 val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"}; |
210 val updacc_noopE = @{thm "update_accessor_noopE"}; |
210 val updacc_noopE = @{thm "update_accessor_noopE"}; |
211 val updacc_noop_compE = @{thm "update_accessor_noop_compE"}; |
211 val updacc_noop_compE = @{thm "update_accessor_noop_compE"}; |
212 val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"}; |
212 val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"}; |
213 val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"}; |
213 val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"}; |
214 val updacc_cong_from_eq = @{thm "istuple_update_accessor_cong_from_eq"}; |
214 val updacc_cong_from_eq = @{thm "iso_tuple_update_accessor_cong_from_eq"}; |
215 |
215 |
216 val o_eq_dest = @{thm o_eq_dest}; |
216 val o_eq_dest = @{thm o_eq_dest}; |
217 val o_eq_id_dest = @{thm o_eq_id_dest}; |
217 val o_eq_id_dest = @{thm o_eq_id_dest}; |
218 val o_eq_dest_lhs = @{thm o_eq_dest_lhs}; |
218 val o_eq_dest_lhs = @{thm o_eq_dest_lhs}; |
219 |
219 |
1087 val prop = lhs === rhs; |
1087 val prop = lhs === rhs; |
1088 val othm = |
1088 val othm = |
1089 Goal.prove (ProofContext.init thy) [] [] prop |
1089 Goal.prove (ProofContext.init thy) [] [] prop |
1090 (fn _ => |
1090 (fn _ => |
1091 simp_tac defset 1 THEN |
1091 simp_tac defset 1 THEN |
1092 REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN |
1092 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN |
1093 TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)); |
1093 TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)); |
1094 val dest = if comp then o_eq_dest_lhs else o_eq_dest; |
1094 val dest = if comp then o_eq_dest_lhs else o_eq_dest; |
1095 in Drule.standard (othm RS dest) end; |
1095 in Drule.standard (othm RS dest) end; |
1096 |
1096 |
1097 fun get_updupd_simps thy term defset = |
1097 fun get_updupd_simps thy term defset = |
1115 if Symtab.defined seen (cname u) |
1115 if Symtab.defined seen (cname u) |
1116 then swaps_needed us prev seen (build_swaps_to_eq u prev swaps) |
1116 then swaps_needed us prev seen (build_swaps_to_eq u prev swaps) |
1117 else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps; |
1117 else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps; |
1118 in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end; |
1118 in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end; |
1119 |
1119 |
1120 val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate; |
1120 val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate; |
1121 |
1121 |
1122 fun prove_unfold_defs thy ex_simps ex_simprs prop = |
1122 fun prove_unfold_defs thy ex_simps ex_simprs prop = |
1123 let |
1123 let |
1124 val defset = get_sel_upd_defs thy; |
1124 val defset = get_sel_upd_defs thy; |
1125 val prop' = Envir.beta_eta_contract prop; |
1125 val prop' = Envir.beta_eta_contract prop; |
1610 |
1610 |
1611 |
1611 |
1612 (*before doing anything else, create the tree of new types |
1612 (*before doing anything else, create the tree of new types |
1613 that will back the record extension*) |
1613 that will back the record extension*) |
1614 |
1614 |
1615 val mktreeV = Balanced_Tree.make IsTupleSupport.mk_cons_tuple; |
1615 val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple; |
1616 |
1616 |
1617 fun mk_istuple (left, right) (thy, i) = |
1617 fun mk_iso_tuple (left, right) (thy, i) = |
1618 let |
1618 let |
1619 val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i; |
1619 val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i; |
1620 val nm = suffix suff (Long_Name.base_name name); |
1620 val nm = suffix suff (Long_Name.base_name name); |
1621 val ((_, cons), thy') = |
1621 val ((_, cons), thy') = |
1622 IsTupleSupport.add_istuple_type |
1622 Iso_Tuple_Support.add_iso_tuple_type |
1623 (nm, alphas_zeta) (fastype_of left, fastype_of right) thy; |
1623 (nm, alphas_zeta) (fastype_of left, fastype_of right) thy; |
1624 in |
1624 in |
1625 (cons $ left $ right, (thy', i + 1)) |
1625 (cons $ left $ right, (thy', i + 1)) |
1626 end; |
1626 end; |
1627 |
1627 |
1628 (*trying to create a 1-element istuple will fail, and is pointless anyway*) |
1628 (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*) |
1629 fun mk_even_istuple [arg] = pair arg |
1629 fun mk_even_iso_tuple [arg] = pair arg |
1630 | mk_even_istuple args = mk_istuple (IsTupleSupport.dest_cons_tuple (mktreeV args)); |
1630 | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args)); |
1631 |
1631 |
1632 fun build_meta_tree_type i thy vars more = |
1632 fun build_meta_tree_type i thy vars more = |
1633 let val len = length vars in |
1633 let val len = length vars in |
1634 if len < 1 then raise TYPE ("meta_tree_type args too short", [], vars) |
1634 if len < 1 then raise TYPE ("meta_tree_type args too short", [], vars) |
1635 else if len > 16 then |
1635 else if len > 16 then |
1636 let |
1636 let |
1637 fun group16 [] = [] |
1637 fun group16 [] = [] |
1638 | group16 xs = take 16 xs :: group16 (drop 16 xs); |
1638 | group16 xs = take 16 xs :: group16 (drop 16 xs); |
1639 val vars' = group16 vars; |
1639 val vars' = group16 vars; |
1640 val (composites, (thy', i')) = fold_map mk_even_istuple vars' (thy, i); |
1640 val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i); |
1641 in |
1641 in |
1642 build_meta_tree_type i' thy' composites more |
1642 build_meta_tree_type i' thy' composites more |
1643 end |
1643 end |
1644 else |
1644 else |
1645 let val (term, (thy', _)) = mk_istuple (mktreeV vars, more) (thy, 0) |
1645 let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0) |
1646 in (term, thy') end |
1646 in (term, thy') end |
1647 end; |
1647 end; |
1648 |
1648 |
1649 val _ = timing_msg "record extension preparing definitions"; |
1649 val _ = timing_msg "record extension preparing definitions"; |
1650 |
1650 |
1728 let |
1728 let |
1729 val cterm_ext = cterm_of defs_thy ext; |
1729 val cterm_ext = cterm_of defs_thy ext; |
1730 val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE; |
1730 val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE; |
1731 val tactic1 = |
1731 val tactic1 = |
1732 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN |
1732 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN |
1733 REPEAT_ALL_NEW IsTupleSupport.istuple_intros_tac 1; |
1733 REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1; |
1734 val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1); |
1734 val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1); |
1735 val [halfway] = Seq.list_of (tactic1 start); |
1735 val [halfway] = Seq.list_of (tactic1 start); |
1736 val [surject] = Seq.list_of (tactic2 (Drule.standard halfway)); |
1736 val [surject] = Seq.list_of (tactic2 (Drule.standard halfway)); |
1737 in |
1737 in |
1738 surject |
1738 surject |
1952 [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn), |
1952 [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn), |
1953 (Binding.name bname, alphas, recT0, Syntax.NoSyn)]; |
1953 (Binding.name bname, alphas, recT0, Syntax.NoSyn)]; |
1954 |
1954 |
1955 val ext_defs = ext_def :: map #extdef parents; |
1955 val ext_defs = ext_def :: map #extdef parents; |
1956 |
1956 |
1957 (*Theorems from the istuple intros. |
1957 (*Theorems from the iso_tuple intros. |
1958 This is complex enough to deserve a full comment. |
1958 This is complex enough to deserve a full comment. |
1959 By unfolding ext_defs from r_rec0 we create a tree of constructor |
1959 By unfolding ext_defs from r_rec0 we create a tree of constructor |
1960 calls (many of them Pair, but others as well). The introduction |
1960 calls (many of them Pair, but others as well). The introduction |
1961 rules for update_accessor_eq_assist can unify two different ways |
1961 rules for update_accessor_eq_assist can unify two different ways |
1962 on these constructors. If we take the complete result sequence of |
1962 on these constructors. If we take the complete result sequence of |
1977 val insts = [("v", cterm_rec), ("v'", cterm_vrs)]; |
1977 val insts = [("v", cterm_rec), ("v'", cterm_vrs)]; |
1978 val init_thm = named_cterm_instantiate insts updacc_eq_triv; |
1978 val init_thm = named_cterm_instantiate insts updacc_eq_triv; |
1979 val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1; |
1979 val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1; |
1980 val tactic = |
1980 val tactic = |
1981 simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN |
1981 simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN |
1982 REPEAT (IsTupleSupport.istuple_intros_tac 1 ORELSE terminal); |
1982 REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal); |
1983 val updaccs = Seq.list_of (tactic init_thm); |
1983 val updaccs = Seq.list_of (tactic init_thm); |
1984 in |
1984 in |
1985 (updaccs RL [updacc_accessor_eqE], |
1985 (updaccs RL [updacc_accessor_eqE], |
1986 updaccs RL [updacc_updator_eqE], |
1986 updaccs RL [updacc_updator_eqE], |
1987 updaccs RL [updacc_cong_from_eq]) |
1987 updaccs RL [updacc_cong_from_eq]) |