src/HOL/Tools/record.ML
changeset 32764 690f9cccf232
parent 32763 ebfaf9e3c03a
child 32765 3032c0308019
     1.1 --- a/src/HOL/Tools/record.ML	Tue Sep 29 21:36:49 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Sep 29 22:33:27 2009 +0200
     1.3 @@ -201,24 +201,23 @@
     1.4  structure Record: RECORD =
     1.5  struct
     1.6  
     1.7 -val eq_reflection = thm "eq_reflection";
     1.8 -val Pair_eq = thm "Product_Type.prod.inject";
     1.9 -val atomize_all = thm "HOL.atomize_all";
    1.10 -val atomize_imp = thm "HOL.atomize_imp";
    1.11 -val meta_allE = thm "Pure.meta_allE";
    1.12 -val prop_subst = thm "prop_subst";
    1.13 +val eq_reflection = @{thm eq_reflection};
    1.14 +val Pair_eq = @{thm Product_Type.prod.inject};
    1.15 +val atomize_all = @{thm HOL.atomize_all};
    1.16 +val atomize_imp = @{thm HOL.atomize_imp};
    1.17 +val meta_allE = @{thm Pure.meta_allE};
    1.18 +val prop_subst = @{thm prop_subst};
    1.19  val Pair_sel_convs = [fst_conv, snd_conv];
    1.20 -val K_record_comp = @{thm "K_record_comp"};
    1.21 +val K_record_comp = @{thm K_record_comp};
    1.22  val K_comp_convs = [@{thm o_apply}, K_record_comp]
    1.23 -val transitive_thm = thm "transitive";
    1.24 -val o_assoc = @{thm "o_assoc"};
    1.25 +val transitive_thm = @{thm transitive};
    1.26 +val o_assoc = @{thm o_assoc};
    1.27  val id_apply = @{thm id_apply};
    1.28  val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
    1.29  val Not_eq_iff = @{thm Not_eq_iff};
    1.30  
    1.31 -val refl_conj_eq = thm "refl_conj_eq";
    1.32 -val meta_all_sameI = thm "meta_all_sameI";
    1.33 -val meta_iffD2 = thm "meta_iffD2";
    1.34 +val refl_conj_eq = @{thm refl_conj_eq};
    1.35 +val meta_all_sameI = @{thm meta_all_sameI};
    1.36  
    1.37  val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
    1.38  val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
    1.39 @@ -236,9 +235,9 @@
    1.40  val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"};
    1.41  val updacc_cong_from_eq = @{thm "istuple_update_accessor_cong_from_eq"};
    1.42  
    1.43 -val o_eq_dest = thm "o_eq_dest";
    1.44 -val o_eq_id_dest = thm "o_eq_id_dest";
    1.45 -val o_eq_dest_lhs = thm "o_eq_dest_lhs";
    1.46 +val o_eq_dest = @{thm o_eq_dest};
    1.47 +val o_eq_id_dest = @{thm o_eq_id_dest};
    1.48 +val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
    1.49  
    1.50  
    1.51  
    1.52 @@ -395,7 +394,7 @@
    1.53    let
    1.54      val rTs = dest_recTs T;
    1.55      val rTs' = if i < 0 then rTs else Library.take (i, rTs);
    1.56 -  in Library.foldl (fn (s, (c, T)) => s ^ c) ("", rTs') end;   (* FIXME ? *)
    1.57 +  in implode (map #1 rTs') end;
    1.58  
    1.59  
    1.60  
    1.61 @@ -443,10 +442,10 @@
    1.62      unfoldcong: Simplifier.simpset},
    1.63    equalities: thm Symtab.table,
    1.64    extinjects: thm list,
    1.65 -  extsplit: thm Symtab.table,  (* maps extension name to split rule *)
    1.66 -  splits: (thm*thm*thm*thm) Symtab.table,  (* !!, !, EX - split-equalities, induct rule *)
    1.67 -  extfields: (string*typ) list Symtab.table,  (* maps extension to its fields *)
    1.68 -  fieldext: (string*typ list) Symtab.table};  (* maps field to its extension *)
    1.69 +  extsplit: thm Symtab.table,  (*maps extension name to split rule*)
    1.70 +  splits: (thm * thm * thm * thm) Symtab.table,  (*!!, !, EX - split-equalities, induct rule*)
    1.71 +  extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
    1.72 +  fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)
    1.73  
    1.74  fun make_record_data
    1.75      records sel_upd equalities extinjects extsplit splits extfields fieldext =
    1.76 @@ -546,13 +545,12 @@
    1.77  
    1.78  val is_selector = Symtab.defined o #selectors o get_sel_upd;
    1.79  val get_updates = Symtab.lookup o #updates o get_sel_upd;
    1.80 -fun get_ss_with_context getss thy =
    1.81 -    Simplifier.theory_context thy (getss (get_sel_upd thy));
    1.82 -
    1.83 -val get_simpset = get_ss_with_context (#simpset);
    1.84 -val get_sel_upd_defs = get_ss_with_context (#defset);
    1.85 -val get_foldcong_ss = get_ss_with_context (#foldcong);
    1.86 -val get_unfoldcong_ss = get_ss_with_context (#unfoldcong);
    1.87 +fun get_ss_with_context getss thy = Simplifier.theory_context thy (getss (get_sel_upd thy));
    1.88 +
    1.89 +val get_simpset = get_ss_with_context #simpset;
    1.90 +val get_sel_upd_defs = get_ss_with_context #defset;
    1.91 +val get_foldcong_ss = get_ss_with_context #foldcong;
    1.92 +val get_unfoldcong_ss = get_ss_with_context #unfoldcong;
    1.93  
    1.94  fun get_update_details u thy =
    1.95    let val sel_upd = get_sel_upd thy in
    1.96 @@ -1157,10 +1155,6 @@
    1.97        in standard (othm RS dest) end;
    1.98    in map get_simp upd_funs end;
    1.99  
   1.100 -(* FIXME dup? *)
   1.101 -structure SymSymTab =
   1.102 -  Table(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
   1.103 -
   1.104  fun get_updupd_simp thy defset intros_tac u u' comp =
   1.105    let
   1.106      val f = Free ("f", domain_type (fastype_of u));
   1.107 @@ -1192,18 +1186,18 @@
   1.108            let
   1.109              val key = (cname u, cname upd);
   1.110              val newswaps =
   1.111 -              if SymSymTab.defined swaps key then swaps
   1.112 -              else SymSymTab.insert (K true) (key, getswap u upd) swaps;
   1.113 +              if Symreltab.defined swaps key then swaps
   1.114 +              else Symreltab.insert (K true) (key, getswap u upd) swaps;
   1.115            in
   1.116              if cname u = cname upd then newswaps
   1.117              else build_swaps_to_eq upd us newswaps
   1.118            end;
   1.119 -    fun swaps_needed [] prev seen swaps = map snd (SymSymTab.dest swaps)
   1.120 +    fun swaps_needed [] prev seen swaps = map snd (Symreltab.dest swaps)
   1.121        | swaps_needed (u :: us) prev seen swaps =
   1.122            if Symtab.defined seen (cname u)
   1.123            then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
   1.124            else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
   1.125 -  in swaps_needed upd_funs [] Symtab.empty SymSymTab.empty end;
   1.126 +  in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
   1.127  
   1.128  val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
   1.129  
   1.130 @@ -1540,13 +1534,6 @@
   1.131        end);
   1.132  
   1.133  
   1.134 -local
   1.135 -
   1.136 -val inductive_atomize = thms "induct_atomize";
   1.137 -val inductive_rulify = thms "induct_rulify";
   1.138 -
   1.139 -in
   1.140 -
   1.141  (* record_split_simp_tac *)
   1.142  
   1.143  (*Split (and simplify) all records in the goal for which P holds.
   1.144 @@ -1565,8 +1552,8 @@
   1.145            (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T
   1.146          | _ => false);
   1.147  
   1.148 -    val goal = nth (Thm.prems_of st) (i - 1);
   1.149 -    val frees = List.filter (is_recT o type_of) (OldTerm.term_frees goal);
   1.150 +    val goal = nth (Thm.prems_of st) (i - 1);    (* FIXME SUBGOAL *)
   1.151 +    val frees = filter (is_recT o type_of) (OldTerm.term_frees goal);
   1.152  
   1.153      fun mk_split_free_tac free induct_thm i =
   1.154        let
   1.155 @@ -1576,9 +1563,9 @@
   1.156          val thm = cterm_instantiate [(crec, cfree)] induct_thm;
   1.157        in
   1.158          EVERY
   1.159 -         [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
   1.160 +         [simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i,
   1.161            rtac thm i,
   1.162 -          simp_tac (HOL_basic_ss addsimps inductive_rulify) i]
   1.163 +          simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i]
   1.164        end;
   1.165  
   1.166      fun split_free_tac P i (free as Free (n, T)) =
   1.167 @@ -1604,7 +1591,6 @@
   1.168        (EVERY split_frees_tacs THEN
   1.169          Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i)
   1.170    end handle Empty => Seq.empty;
   1.171 -end;
   1.172  
   1.173  
   1.174  (* record_split_tac *)
   1.175 @@ -1746,7 +1732,7 @@
   1.176  
   1.177      (*before doing anything else, create the tree of new types
   1.178        that will back the record extension*)
   1.179 -
   1.180 +    (* FIXME cf. BalancedTree.make *)
   1.181      fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
   1.182        | mktreeT [T] = T
   1.183        | mktreeT xs =
   1.184 @@ -1759,6 +1745,7 @@
   1.185              HOLogic.mk_prodT (mktreeT left, mktreeT right)
   1.186            end;
   1.187  
   1.188 +    (* FIXME cf. BalancedTree.make *)
   1.189      fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
   1.190        | mktreeV [T] = T
   1.191        | mktreeV xs =
   1.192 @@ -1771,38 +1758,35 @@
   1.193              IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right)
   1.194            end;
   1.195  
   1.196 -    fun mk_istuple ((thy, i), (left, rght)) =
   1.197 +    fun mk_istuple (left, right) (thy, i) =
   1.198        let
   1.199          val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
   1.200          val nm = suffix suff (Long_Name.base_name name);
   1.201          val (isom, cons, thy') =
   1.202            IsTupleSupport.add_istuple_type
   1.203 -            (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
   1.204 +            (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
   1.205        in
   1.206 -        ((thy', i + 1), cons $ left $ rght)
   1.207 +        (cons $ left $ right, (thy', i + 1))
   1.208        end;
   1.209  
   1.210 -    (*trying to create a 1-element istuple will fail, and
   1.211 -      is pointless anyway*)
   1.212 -    fun mk_even_istuple ((thy, i), [arg]) = ((thy, i), arg)
   1.213 -      | mk_even_istuple ((thy, i), args) =
   1.214 -          mk_istuple ((thy, i), IsTupleSupport.dest_cons_tuple (mktreeV args));
   1.215 +    (*trying to create a 1-element istuple will fail, and is pointless anyway*)
   1.216 +    fun mk_even_istuple [arg] = pair arg
   1.217 +      | mk_even_istuple args = mk_istuple (IsTupleSupport.dest_cons_tuple (mktreeV args));
   1.218  
   1.219      fun build_meta_tree_type i thy vars more =
   1.220        let val len = length vars in
   1.221 -        if len < 1 then raise (TYPE ("meta_tree_type args too short", [], vars))
   1.222 +        if len < 1 then raise TYPE ("meta_tree_type args too short", [], vars)
   1.223          else if len > 16 then
   1.224            let
   1.225              fun group16 [] = []
   1.226                | group16 xs = Library.take (16, xs) :: group16 (Library.drop (16, xs));
   1.227              val vars' = group16 vars;
   1.228 -            val ((thy', i'), composites) =
   1.229 -              Library.foldl_map mk_even_istuple ((thy, i), vars');   (* FIXME fold_map !? *)
   1.230 +            val (composites, (thy', i')) = fold_map mk_even_istuple vars' (thy, i);
   1.231            in
   1.232              build_meta_tree_type i' thy' composites more
   1.233            end
   1.234          else
   1.235 -          let val ((thy', i'), term) = mk_istuple ((thy, 0), (mktreeV vars, more))
   1.236 +          let val (term, (thy', i')) = mk_istuple (mktreeV vars, more) (thy, 0)
   1.237            in (term, thy') end
   1.238        end;
   1.239  
   1.240 @@ -1842,7 +1826,7 @@
   1.241      val ext = mk_ext vars_more;
   1.242      val s = Free (rN, extT);
   1.243      val w = Free (wN, extT);
   1.244 -    val P = Free (Name.variant variants "P", extT-->HOLogic.boolT);
   1.245 +    val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
   1.246      val C = Free (Name.variant variants "C", HOLogic.boolT);
   1.247      val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy;
   1.248  
   1.249 @@ -1924,7 +1908,7 @@
   1.250          prove_standard [assm] concl
   1.251            (fn {prems, ...} =>
   1.252              EVERY
   1.253 -             [cut_rules_tac [split_meta RS meta_iffD2] 1,
   1.254 +             [cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1,
   1.255                resolve_tac prems 2,
   1.256                asm_simp_tac HOL_ss 1])
   1.257        end;
   1.258 @@ -1944,7 +1928,7 @@
   1.259    | chunks [] xs = [xs]
   1.260    | chunks (l :: ls) xs = Library.take (l, xs) :: chunks ls (Library.drop (l, xs));
   1.261  
   1.262 -fun chop_last [] = error "last: list should not be empty"
   1.263 +fun chop_last [] = error "chop_last: list should not be empty"
   1.264    | chop_last [x] = ([], x)
   1.265    | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
   1.266  
   1.267 @@ -2014,7 +1998,8 @@
   1.268      val alphas_ext = alphas inter alphas_fields;
   1.269      val len = length fields;
   1.270      val variants =
   1.271 -      Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants) (map fst bfields);
   1.272 +      Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
   1.273 +        (map fst bfields);
   1.274      val vars = ListPair.map Free (variants, types);
   1.275      val named_vars = names ~~ vars;
   1.276      val idxs = 0 upto (len - 1);
   1.277 @@ -2053,8 +2038,7 @@
   1.278      val extension_name = unsuffix ext_typeN (fst extension_scheme);
   1.279      val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
   1.280      val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extN];
   1.281 -    val extension_id = Library.foldl (op ^) ("", extension_names);  (* FIXME implode!? *)
   1.282 -
   1.283 +    val extension_id = implode extension_names;
   1.284  
   1.285      fun rec_schemeT n = mk_recordT (map #extension (prune n parents)) extT;
   1.286      val rec_schemeT0 = rec_schemeT 0;
   1.287 @@ -2187,7 +2171,6 @@
   1.288        end;
   1.289      val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
   1.290  
   1.291 -
   1.292      (*updates*)
   1.293      fun mk_upd_spec ((c, T), thm) =
   1.294        let
   1.295 @@ -2520,8 +2503,7 @@
   1.296              [Simplifier.simp_add, Nitpick_Const_Simps.add]),
   1.297             ((Binding.name "iffs", iffs), [iff_add])]
   1.298        |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
   1.299 -      |> put_sel_upd names full_moreN depth sel_upd_simps
   1.300 -                           sel_upd_defs (fold_congs', unfold_congs')
   1.301 +      |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
   1.302        |> add_record_equalities extension_id equality'
   1.303        |> add_extinjects ext_inject
   1.304        |> add_extsplit extension_name ext_split