replaced meta_iffD2 by existing Drule.equal_elim_rule2;
authorwenzelm
Tue Sep 29 22:33:27 2009 +0200 (2009-09-29)
changeset 32764690f9cccf232
parent 32763 ebfaf9e3c03a
child 32765 3032c0308019
replaced meta_iffD2 by existing Drule.equal_elim_rule2;
replaced SymSymTab by existing Symreltab;
more antiquotations;
eliminated old-style Library.foldl, Library.foldl_map;
tuned;
src/HOL/Record.thy
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Record.thy	Tue Sep 29 21:36:49 2009 +0200
     1.2 +++ b/src/HOL/Record.thy	Tue Sep 29 22:33:27 2009 +0200
     1.3 @@ -18,10 +18,6 @@
     1.4  lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" 
     1.5    by (simp add: comp_def)
     1.6  
     1.7 -lemma meta_iffD2:
     1.8 -  "\<lbrakk> PROP P \<equiv> PROP Q; PROP Q \<rbrakk> \<Longrightarrow> PROP P"
     1.9 -  by simp
    1.10 -
    1.11  lemma o_eq_dest_lhs:
    1.12    "a o b = c \<Longrightarrow> a (b v) = c v"
    1.13    by clarsimp
     2.1 --- a/src/HOL/Tools/record.ML	Tue Sep 29 21:36:49 2009 +0200
     2.2 +++ b/src/HOL/Tools/record.ML	Tue Sep 29 22:33:27 2009 +0200
     2.3 @@ -201,24 +201,23 @@
     2.4  structure Record: RECORD =
     2.5  struct
     2.6  
     2.7 -val eq_reflection = thm "eq_reflection";
     2.8 -val Pair_eq = thm "Product_Type.prod.inject";
     2.9 -val atomize_all = thm "HOL.atomize_all";
    2.10 -val atomize_imp = thm "HOL.atomize_imp";
    2.11 -val meta_allE = thm "Pure.meta_allE";
    2.12 -val prop_subst = thm "prop_subst";
    2.13 +val eq_reflection = @{thm eq_reflection};
    2.14 +val Pair_eq = @{thm Product_Type.prod.inject};
    2.15 +val atomize_all = @{thm HOL.atomize_all};
    2.16 +val atomize_imp = @{thm HOL.atomize_imp};
    2.17 +val meta_allE = @{thm Pure.meta_allE};
    2.18 +val prop_subst = @{thm prop_subst};
    2.19  val Pair_sel_convs = [fst_conv, snd_conv];
    2.20 -val K_record_comp = @{thm "K_record_comp"};
    2.21 +val K_record_comp = @{thm K_record_comp};
    2.22  val K_comp_convs = [@{thm o_apply}, K_record_comp]
    2.23 -val transitive_thm = thm "transitive";
    2.24 -val o_assoc = @{thm "o_assoc"};
    2.25 +val transitive_thm = @{thm transitive};
    2.26 +val o_assoc = @{thm o_assoc};
    2.27  val id_apply = @{thm id_apply};
    2.28  val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
    2.29  val Not_eq_iff = @{thm Not_eq_iff};
    2.30  
    2.31 -val refl_conj_eq = thm "refl_conj_eq";
    2.32 -val meta_all_sameI = thm "meta_all_sameI";
    2.33 -val meta_iffD2 = thm "meta_iffD2";
    2.34 +val refl_conj_eq = @{thm refl_conj_eq};
    2.35 +val meta_all_sameI = @{thm meta_all_sameI};
    2.36  
    2.37  val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
    2.38  val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
    2.39 @@ -236,9 +235,9 @@
    2.40  val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"};
    2.41  val updacc_cong_from_eq = @{thm "istuple_update_accessor_cong_from_eq"};
    2.42  
    2.43 -val o_eq_dest = thm "o_eq_dest";
    2.44 -val o_eq_id_dest = thm "o_eq_id_dest";
    2.45 -val o_eq_dest_lhs = thm "o_eq_dest_lhs";
    2.46 +val o_eq_dest = @{thm o_eq_dest};
    2.47 +val o_eq_id_dest = @{thm o_eq_id_dest};
    2.48 +val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
    2.49  
    2.50  
    2.51  
    2.52 @@ -395,7 +394,7 @@
    2.53    let
    2.54      val rTs = dest_recTs T;
    2.55      val rTs' = if i < 0 then rTs else Library.take (i, rTs);
    2.56 -  in Library.foldl (fn (s, (c, T)) => s ^ c) ("", rTs') end;   (* FIXME ? *)
    2.57 +  in implode (map #1 rTs') end;
    2.58  
    2.59  
    2.60  
    2.61 @@ -443,10 +442,10 @@
    2.62      unfoldcong: Simplifier.simpset},
    2.63    equalities: thm Symtab.table,
    2.64    extinjects: thm list,
    2.65 -  extsplit: thm Symtab.table,  (* maps extension name to split rule *)
    2.66 -  splits: (thm*thm*thm*thm) Symtab.table,  (* !!, !, EX - split-equalities, induct rule *)
    2.67 -  extfields: (string*typ) list Symtab.table,  (* maps extension to its fields *)
    2.68 -  fieldext: (string*typ list) Symtab.table};  (* maps field to its extension *)
    2.69 +  extsplit: thm Symtab.table,  (*maps extension name to split rule*)
    2.70 +  splits: (thm * thm * thm * thm) Symtab.table,  (*!!, !, EX - split-equalities, induct rule*)
    2.71 +  extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
    2.72 +  fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)
    2.73  
    2.74  fun make_record_data
    2.75      records sel_upd equalities extinjects extsplit splits extfields fieldext =
    2.76 @@ -546,13 +545,12 @@
    2.77  
    2.78  val is_selector = Symtab.defined o #selectors o get_sel_upd;
    2.79  val get_updates = Symtab.lookup o #updates o get_sel_upd;
    2.80 -fun get_ss_with_context getss thy =
    2.81 -    Simplifier.theory_context thy (getss (get_sel_upd thy));
    2.82 -
    2.83 -val get_simpset = get_ss_with_context (#simpset);
    2.84 -val get_sel_upd_defs = get_ss_with_context (#defset);
    2.85 -val get_foldcong_ss = get_ss_with_context (#foldcong);
    2.86 -val get_unfoldcong_ss = get_ss_with_context (#unfoldcong);
    2.87 +fun get_ss_with_context getss thy = Simplifier.theory_context thy (getss (get_sel_upd thy));
    2.88 +
    2.89 +val get_simpset = get_ss_with_context #simpset;
    2.90 +val get_sel_upd_defs = get_ss_with_context #defset;
    2.91 +val get_foldcong_ss = get_ss_with_context #foldcong;
    2.92 +val get_unfoldcong_ss = get_ss_with_context #unfoldcong;
    2.93  
    2.94  fun get_update_details u thy =
    2.95    let val sel_upd = get_sel_upd thy in
    2.96 @@ -1157,10 +1155,6 @@
    2.97        in standard (othm RS dest) end;
    2.98    in map get_simp upd_funs end;
    2.99  
   2.100 -(* FIXME dup? *)
   2.101 -structure SymSymTab =
   2.102 -  Table(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
   2.103 -
   2.104  fun get_updupd_simp thy defset intros_tac u u' comp =
   2.105    let
   2.106      val f = Free ("f", domain_type (fastype_of u));
   2.107 @@ -1192,18 +1186,18 @@
   2.108            let
   2.109              val key = (cname u, cname upd);
   2.110              val newswaps =
   2.111 -              if SymSymTab.defined swaps key then swaps
   2.112 -              else SymSymTab.insert (K true) (key, getswap u upd) swaps;
   2.113 +              if Symreltab.defined swaps key then swaps
   2.114 +              else Symreltab.insert (K true) (key, getswap u upd) swaps;
   2.115            in
   2.116              if cname u = cname upd then newswaps
   2.117              else build_swaps_to_eq upd us newswaps
   2.118            end;
   2.119 -    fun swaps_needed [] prev seen swaps = map snd (SymSymTab.dest swaps)
   2.120 +    fun swaps_needed [] prev seen swaps = map snd (Symreltab.dest swaps)
   2.121        | swaps_needed (u :: us) prev seen swaps =
   2.122            if Symtab.defined seen (cname u)
   2.123            then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
   2.124            else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
   2.125 -  in swaps_needed upd_funs [] Symtab.empty SymSymTab.empty end;
   2.126 +  in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
   2.127  
   2.128  val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
   2.129  
   2.130 @@ -1540,13 +1534,6 @@
   2.131        end);
   2.132  
   2.133  
   2.134 -local
   2.135 -
   2.136 -val inductive_atomize = thms "induct_atomize";
   2.137 -val inductive_rulify = thms "induct_rulify";
   2.138 -
   2.139 -in
   2.140 -
   2.141  (* record_split_simp_tac *)
   2.142  
   2.143  (*Split (and simplify) all records in the goal for which P holds.
   2.144 @@ -1565,8 +1552,8 @@
   2.145            (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T
   2.146          | _ => false);
   2.147  
   2.148 -    val goal = nth (Thm.prems_of st) (i - 1);
   2.149 -    val frees = List.filter (is_recT o type_of) (OldTerm.term_frees goal);
   2.150 +    val goal = nth (Thm.prems_of st) (i - 1);    (* FIXME SUBGOAL *)
   2.151 +    val frees = filter (is_recT o type_of) (OldTerm.term_frees goal);
   2.152  
   2.153      fun mk_split_free_tac free induct_thm i =
   2.154        let
   2.155 @@ -1576,9 +1563,9 @@
   2.156          val thm = cterm_instantiate [(crec, cfree)] induct_thm;
   2.157        in
   2.158          EVERY
   2.159 -         [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
   2.160 +         [simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i,
   2.161            rtac thm i,
   2.162 -          simp_tac (HOL_basic_ss addsimps inductive_rulify) i]
   2.163 +          simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i]
   2.164        end;
   2.165  
   2.166      fun split_free_tac P i (free as Free (n, T)) =
   2.167 @@ -1604,7 +1591,6 @@
   2.168        (EVERY split_frees_tacs THEN
   2.169          Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i)
   2.170    end handle Empty => Seq.empty;
   2.171 -end;
   2.172  
   2.173  
   2.174  (* record_split_tac *)
   2.175 @@ -1746,7 +1732,7 @@
   2.176  
   2.177      (*before doing anything else, create the tree of new types
   2.178        that will back the record extension*)
   2.179 -
   2.180 +    (* FIXME cf. BalancedTree.make *)
   2.181      fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
   2.182        | mktreeT [T] = T
   2.183        | mktreeT xs =
   2.184 @@ -1759,6 +1745,7 @@
   2.185              HOLogic.mk_prodT (mktreeT left, mktreeT right)
   2.186            end;
   2.187  
   2.188 +    (* FIXME cf. BalancedTree.make *)
   2.189      fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
   2.190        | mktreeV [T] = T
   2.191        | mktreeV xs =
   2.192 @@ -1771,38 +1758,35 @@
   2.193              IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right)
   2.194            end;
   2.195  
   2.196 -    fun mk_istuple ((thy, i), (left, rght)) =
   2.197 +    fun mk_istuple (left, right) (thy, i) =
   2.198        let
   2.199          val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
   2.200          val nm = suffix suff (Long_Name.base_name name);
   2.201          val (isom, cons, thy') =
   2.202            IsTupleSupport.add_istuple_type
   2.203 -            (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
   2.204 +            (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
   2.205        in
   2.206 -        ((thy', i + 1), cons $ left $ rght)
   2.207 +        (cons $ left $ right, (thy', i + 1))
   2.208        end;
   2.209  
   2.210 -    (*trying to create a 1-element istuple will fail, and
   2.211 -      is pointless anyway*)
   2.212 -    fun mk_even_istuple ((thy, i), [arg]) = ((thy, i), arg)
   2.213 -      | mk_even_istuple ((thy, i), args) =
   2.214 -          mk_istuple ((thy, i), IsTupleSupport.dest_cons_tuple (mktreeV args));
   2.215 +    (*trying to create a 1-element istuple will fail, and is pointless anyway*)
   2.216 +    fun mk_even_istuple [arg] = pair arg
   2.217 +      | mk_even_istuple args = mk_istuple (IsTupleSupport.dest_cons_tuple (mktreeV args));
   2.218  
   2.219      fun build_meta_tree_type i thy vars more =
   2.220        let val len = length vars in
   2.221 -        if len < 1 then raise (TYPE ("meta_tree_type args too short", [], vars))
   2.222 +        if len < 1 then raise TYPE ("meta_tree_type args too short", [], vars)
   2.223          else if len > 16 then
   2.224            let
   2.225              fun group16 [] = []
   2.226                | group16 xs = Library.take (16, xs) :: group16 (Library.drop (16, xs));
   2.227              val vars' = group16 vars;
   2.228 -            val ((thy', i'), composites) =
   2.229 -              Library.foldl_map mk_even_istuple ((thy, i), vars');   (* FIXME fold_map !? *)
   2.230 +            val (composites, (thy', i')) = fold_map mk_even_istuple vars' (thy, i);
   2.231            in
   2.232              build_meta_tree_type i' thy' composites more
   2.233            end
   2.234          else
   2.235 -          let val ((thy', i'), term) = mk_istuple ((thy, 0), (mktreeV vars, more))
   2.236 +          let val (term, (thy', i')) = mk_istuple (mktreeV vars, more) (thy, 0)
   2.237            in (term, thy') end
   2.238        end;
   2.239  
   2.240 @@ -1842,7 +1826,7 @@
   2.241      val ext = mk_ext vars_more;
   2.242      val s = Free (rN, extT);
   2.243      val w = Free (wN, extT);
   2.244 -    val P = Free (Name.variant variants "P", extT-->HOLogic.boolT);
   2.245 +    val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
   2.246      val C = Free (Name.variant variants "C", HOLogic.boolT);
   2.247      val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy;
   2.248  
   2.249 @@ -1924,7 +1908,7 @@
   2.250          prove_standard [assm] concl
   2.251            (fn {prems, ...} =>
   2.252              EVERY
   2.253 -             [cut_rules_tac [split_meta RS meta_iffD2] 1,
   2.254 +             [cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1,
   2.255                resolve_tac prems 2,
   2.256                asm_simp_tac HOL_ss 1])
   2.257        end;
   2.258 @@ -1944,7 +1928,7 @@
   2.259    | chunks [] xs = [xs]
   2.260    | chunks (l :: ls) xs = Library.take (l, xs) :: chunks ls (Library.drop (l, xs));
   2.261  
   2.262 -fun chop_last [] = error "last: list should not be empty"
   2.263 +fun chop_last [] = error "chop_last: list should not be empty"
   2.264    | chop_last [x] = ([], x)
   2.265    | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
   2.266  
   2.267 @@ -2014,7 +1998,8 @@
   2.268      val alphas_ext = alphas inter alphas_fields;
   2.269      val len = length fields;
   2.270      val variants =
   2.271 -      Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants) (map fst bfields);
   2.272 +      Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
   2.273 +        (map fst bfields);
   2.274      val vars = ListPair.map Free (variants, types);
   2.275      val named_vars = names ~~ vars;
   2.276      val idxs = 0 upto (len - 1);
   2.277 @@ -2053,8 +2038,7 @@
   2.278      val extension_name = unsuffix ext_typeN (fst extension_scheme);
   2.279      val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
   2.280      val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extN];
   2.281 -    val extension_id = Library.foldl (op ^) ("", extension_names);  (* FIXME implode!? *)
   2.282 -
   2.283 +    val extension_id = implode extension_names;
   2.284  
   2.285      fun rec_schemeT n = mk_recordT (map #extension (prune n parents)) extT;
   2.286      val rec_schemeT0 = rec_schemeT 0;
   2.287 @@ -2187,7 +2171,6 @@
   2.288        end;
   2.289      val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
   2.290  
   2.291 -
   2.292      (*updates*)
   2.293      fun mk_upd_spec ((c, T), thm) =
   2.294        let
   2.295 @@ -2520,8 +2503,7 @@
   2.296              [Simplifier.simp_add, Nitpick_Const_Simps.add]),
   2.297             ((Binding.name "iffs", iffs), [iff_add])]
   2.298        |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
   2.299 -      |> put_sel_upd names full_moreN depth sel_upd_simps
   2.300 -                           sel_upd_defs (fold_congs', unfold_congs')
   2.301 +      |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
   2.302        |> add_record_equalities extension_id equality'
   2.303        |> add_extinjects ext_inject
   2.304        |> add_extsplit extension_name ext_split