1 (* Title: HOL/Tools/record.ML |
1 (* Title: HOL/Tools/record.ML |
2 Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen |
2 Authors: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen |
|
3 Thomas Sewell, NICTA |
3 |
4 |
4 Extensible records with structural subtyping in HOL. |
5 Extensible records with structural subtyping in HOL. |
5 *) |
6 *) |
6 |
7 |
7 signature BASIC_RECORD = |
8 signature BASIC_RECORD = |
1027 (buildswapstoeq u prev swaps) |
1028 (buildswapstoeq u prev swaps) |
1028 else swapsneeded us (u::prev) |
1029 else swapsneeded us (u::prev) |
1029 (Symtab.insert (K true) (cname u, ()) seen) swaps; |
1030 (Symtab.insert (K true) (cname u, ()) seen) swaps; |
1030 in swapsneeded updfuns [] Symtab.empty SymSymTab.empty end; |
1031 in swapsneeded updfuns [] Symtab.empty SymSymTab.empty end; |
1031 |
1032 |
1032 fun named_cterm_instantiate values thm = let |
1033 val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate; |
1033 fun match name (Var ((name', _), _)) = name = name' |
|
1034 | match name _ = false; |
|
1035 fun getvar name = case (find_first (match name) |
|
1036 (OldTerm.term_vars (prop_of thm))) |
|
1037 of SOME var => cterm_of (theory_of_thm thm) var |
|
1038 | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]) |
|
1039 in |
|
1040 cterm_instantiate (map (apfst getvar) values) thm |
|
1041 end; |
|
1042 |
1034 |
1043 fun prove_unfold_defs thy ss T ex_simps ex_simprs prop = |
1035 fun prove_unfold_defs thy ss T ex_simps ex_simprs prop = |
1044 let |
1036 let |
1045 val defset = get_sel_upd_defs thy; |
1037 val defset = get_sel_upd_defs thy; |
1046 val intros = IsTupleSupport.get_istuple_intros thy; |
1038 val in_tac = IsTupleSupport.istuple_intros_tac thy; |
1047 val in_tac = IsTupleSupport.resolve_from_tagged_net intros; |
|
1048 val prop' = Envir.beta_eta_contract prop; |
1039 val prop' = Envir.beta_eta_contract prop; |
1049 val (lhs, rhs) = Logic.dest_equals (Logic.strip_assums_concl prop'); |
1040 val (lhs, rhs) = Logic.dest_equals (Logic.strip_assums_concl prop'); |
1050 val (head, args) = strip_comb lhs; |
1041 val (head, args) = strip_comb lhs; |
1051 val simps = if length args = 1 |
1042 val simps = if length args = 1 |
1052 then get_accupd_simps thy lhs defset in_tac |
1043 then get_accupd_simps thy lhs defset in_tac |
1134 | NONE => NONE) |
1125 | NONE => NONE) |
1135 else NONE |
1126 else NONE |
1136 | _ => NONE)); |
1127 | _ => NONE)); |
1137 |
1128 |
1138 fun get_upd_acc_cong_thm upd acc thy simpset = let |
1129 fun get_upd_acc_cong_thm upd acc thy simpset = let |
1139 val intros = IsTupleSupport.get_istuple_intros thy; |
1130 val in_tac = IsTupleSupport.istuple_intros_tac thy; |
1140 val in_tac = IsTupleSupport.resolve_from_tagged_net intros; |
|
1141 |
1131 |
1142 val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)] |
1132 val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)] |
1143 val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv); |
1133 val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv); |
1144 in Goal.prove (ProofContext.init thy) [] [] prop (fn prems => |
1134 in Goal.prove (ProofContext.init thy) [] [] prop (fn prems => |
1145 EVERY [simp_tac simpset 1, |
1135 EVERY [simp_tac simpset 1, |
1565 val len = length xs; |
1555 val len = length xs; |
1566 val half = len div 2; |
1556 val half = len div 2; |
1567 val left = List.take (xs, half); |
1557 val left = List.take (xs, half); |
1568 val right = List.drop (xs, half); |
1558 val right = List.drop (xs, half); |
1569 in |
1559 in |
1570 HOLogic.mk_prod (mktreeV left, mktreeV right) |
1560 IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right) |
1571 end; |
1561 end; |
1572 |
1562 |
1573 fun mk_istuple ((thy, i), (left, rght)) = |
1563 fun mk_istuple ((thy, i), (left, rght)) = |
1574 let |
1564 let |
1575 val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i); |
1565 val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i); |
1576 val nm = suffix suff (Long_Name.base_name name); |
1566 val nm = suffix suff (Long_Name.base_name name); |
1577 val (cons, thy') = IsTupleSupport.add_istuple_type |
1567 val (isom, cons, thy') = IsTupleSupport.add_istuple_type |
1578 (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy; |
1568 (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy; |
1579 in |
1569 in |
1580 ((thy', i + 1), cons $ left $ rght) |
1570 ((thy', i + 1), cons $ left $ rght) |
1581 end; |
1571 end; |
1582 |
1572 |
1583 (* trying to create a 1-element istuple will fail, and |
1573 (* trying to create a 1-element istuple will fail, and |
1584 is pointless anyway *) |
1574 is pointless anyway *) |
1585 fun mk_even_istuple ((thy, i), [arg]) = |
1575 fun mk_even_istuple ((thy, i), [arg]) = |
1586 ((thy, i), arg) |
1576 ((thy, i), arg) |
1587 | mk_even_istuple ((thy, i), args) = |
1577 | mk_even_istuple ((thy, i), args) = |
1588 mk_istuple ((thy, i), HOLogic.dest_prod (mktreeV args)); |
1578 mk_istuple ((thy, i), IsTupleSupport.dest_cons_tuple (mktreeV args)); |
1589 |
1579 |
1590 fun build_meta_tree_type i thy vars more = |
1580 fun build_meta_tree_type i thy vars more = |
1591 let |
1581 let |
1592 val len = length vars; |
1582 val len = length vars; |
1593 in |
1583 in |
1643 val ext = mk_ext vars_more; |
1633 val ext = mk_ext vars_more; |
1644 val s = Free (rN, extT); |
1634 val s = Free (rN, extT); |
1645 val w = Free (wN, extT); |
1635 val w = Free (wN, extT); |
1646 val P = Free (Name.variant variants "P", extT-->HOLogic.boolT); |
1636 val P = Free (Name.variant variants "P", extT-->HOLogic.boolT); |
1647 val C = Free (Name.variant variants "C", HOLogic.boolT); |
1637 val C = Free (Name.variant variants "C", HOLogic.boolT); |
1648 val intros = IsTupleSupport.get_istuple_intros defs_thy; |
1638 val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy; |
1649 val intros_tac = IsTupleSupport.resolve_from_tagged_net intros; |
|
1650 |
1639 |
1651 val inject_prop = |
1640 val inject_prop = |
1652 let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more; |
1641 let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more; |
1653 in |
1642 in |
1654 ((HOLogic.mk_conj (HOLogic.eq_const extT $ |
1643 ((HOLogic.mk_conj (HOLogic.eq_const extT $ |
1932 val recordT_specs = |
1921 val recordT_specs = |
1933 [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn), |
1922 [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn), |
1934 (Binding.name bname, alphas, recT0, Syntax.NoSyn)]; |
1923 (Binding.name bname, alphas, recT0, Syntax.NoSyn)]; |
1935 |
1924 |
1936 val ext_defs = ext_def :: map #extdef parents; |
1925 val ext_defs = ext_def :: map #extdef parents; |
1937 val intros = IsTupleSupport.get_istuple_intros extension_thy; |
1926 val intros_tac = IsTupleSupport.istuple_intros_tac extension_thy; |
1938 val intros_tac = IsTupleSupport.resolve_from_tagged_net intros; |
|
1939 |
1927 |
1940 (* Theorems from the istuple intros. |
1928 (* Theorems from the istuple intros. |
1941 This is complex enough to deserve a full comment. |
1929 This is complex enough to deserve a full comment. |
1942 By unfolding ext_defs from r_rec0 we create a tree of constructor |
1930 By unfolding ext_defs from r_rec0 we create a tree of constructor |
1943 calls (many of them Pair, but others as well). The introduction |
1931 calls (many of them Pair, but others as well). The introduction |