dropped legacy theorem bindings
authorhaftmann
Wed May 26 16:05:25 2010 +0200 (2010-05-26)
changeset 37136e0c9d3e49e15
parent 37135 636e6d8645d6
child 37137 bac3d00a910a
dropped legacy theorem bindings
src/HOL/Hoare_Parallel/OG_Tactics.thy
src/HOL/Product_Type.thy
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Hoare_Parallel/OG_Tactics.thy	Wed May 26 16:05:25 2010 +0200
     1.2 +++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy	Wed May 26 16:05:25 2010 +0200
     1.3 @@ -275,7 +275,7 @@
     1.4  ML {*
     1.5  val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"]))
     1.6  
     1.7 -val  interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [thm "split", thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list")))
     1.8 +val  interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [@{thm split}, thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list")))
     1.9  
    1.10  val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list")))
    1.11  *}
     2.1 --- a/src/HOL/Product_Type.thy	Wed May 26 16:05:25 2010 +0200
     2.2 +++ b/src/HOL/Product_Type.thy	Wed May 26 16:05:25 2010 +0200
     2.3 @@ -1147,101 +1147,6 @@
     2.4  end
     2.5  *}
     2.6  
     2.7 -
     2.8 -subsection {* Legacy bindings *}
     2.9 -
    2.10 -ML {*
    2.11 -val Collect_split = thm "Collect_split";
    2.12 -val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
    2.13 -val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
    2.14 -val PairE = thm "PairE";
    2.15 -val Pair_Rep_inject = thm "Pair_Rep_inject";
    2.16 -val Pair_def = thm "Pair_def";
    2.17 -val Pair_eq = @{thm "prod.inject"};
    2.18 -val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
    2.19 -val ProdI = thm "ProdI";
    2.20 -val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
    2.21 -val SigmaD1 = thm "SigmaD1";
    2.22 -val SigmaD2 = thm "SigmaD2";
    2.23 -val SigmaE = thm "SigmaE";
    2.24 -val SigmaE2 = thm "SigmaE2";
    2.25 -val SigmaI = thm "SigmaI";
    2.26 -val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1";
    2.27 -val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2";
    2.28 -val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1";
    2.29 -val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2";
    2.30 -val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1";
    2.31 -val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2";
    2.32 -val Sigma_Union = thm "Sigma_Union";
    2.33 -val Sigma_def = thm "Sigma_def";
    2.34 -val Sigma_empty1 = thm "Sigma_empty1";
    2.35 -val Sigma_empty2 = thm "Sigma_empty2";
    2.36 -val Sigma_mono = thm "Sigma_mono";
    2.37 -val The_split = thm "The_split";
    2.38 -val The_split_eq = thm "The_split_eq";
    2.39 -val The_split_eq = thm "The_split_eq";
    2.40 -val Times_Diff_distrib1 = thm "Times_Diff_distrib1";
    2.41 -val Times_Int_distrib1 = thm "Times_Int_distrib1";
    2.42 -val Times_Un_distrib1 = thm "Times_Un_distrib1";
    2.43 -val Times_eq_cancel2 = thm "Times_eq_cancel2";
    2.44 -val Times_subset_cancel2 = thm "Times_subset_cancel2";
    2.45 -val UNIV_Times_UNIV = thm "UNIV_Times_UNIV";
    2.46 -val UN_Times_distrib = thm "UN_Times_distrib";
    2.47 -val Unity_def = thm "Unity_def";
    2.48 -val cond_split_eta = thm "cond_split_eta";
    2.49 -val fst_conv = thm "fst_conv";
    2.50 -val fst_def = thm "fst_def";
    2.51 -val fst_eqD = thm "fst_eqD";
    2.52 -val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
    2.53 -val mem_Sigma_iff = thm "mem_Sigma_iff";
    2.54 -val mem_splitE = thm "mem_splitE";
    2.55 -val mem_splitI = thm "mem_splitI";
    2.56 -val mem_splitI2 = thm "mem_splitI2";
    2.57 -val prod_eqI = thm "prod_eqI";
    2.58 -val prod_fun = thm "prod_fun";
    2.59 -val prod_fun_compose = thm "prod_fun_compose";
    2.60 -val prod_fun_def = thm "prod_fun_def";
    2.61 -val prod_fun_ident = thm "prod_fun_ident";
    2.62 -val prod_fun_imageE = thm "prod_fun_imageE";
    2.63 -val prod_fun_imageI = thm "prod_fun_imageI";
    2.64 -val prod_induct = thm "prod.induct";
    2.65 -val snd_conv = thm "snd_conv";
    2.66 -val snd_def = thm "snd_def";
    2.67 -val snd_eqD = thm "snd_eqD";
    2.68 -val split = thm "split";
    2.69 -val splitD = thm "splitD";
    2.70 -val splitD' = thm "splitD'";
    2.71 -val splitE = thm "splitE";
    2.72 -val splitE' = thm "splitE'";
    2.73 -val splitE2 = thm "splitE2";
    2.74 -val splitI = thm "splitI";
    2.75 -val splitI2 = thm "splitI2";
    2.76 -val splitI2' = thm "splitI2'";
    2.77 -val split_beta = thm "split_beta";
    2.78 -val split_conv = thm "split_conv";
    2.79 -val split_def = thm "split_def";
    2.80 -val split_eta = thm "split_eta";
    2.81 -val split_eta_SetCompr = thm "split_eta_SetCompr";
    2.82 -val split_eta_SetCompr2 = thm "split_eta_SetCompr2";
    2.83 -val split_paired_All = thm "split_paired_All";
    2.84 -val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma";
    2.85 -val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma";
    2.86 -val split_paired_Ex = thm "split_paired_Ex";
    2.87 -val split_paired_The = thm "split_paired_The";
    2.88 -val split_paired_all = thm "split_paired_all";
    2.89 -val split_part = thm "split_part";
    2.90 -val split_split = thm "split_split";
    2.91 -val split_split_asm = thm "split_split_asm";
    2.92 -val split_tupled_all = thms "split_tupled_all";
    2.93 -val split_weak_cong = thm "split_weak_cong";
    2.94 -val surj_pair = thm "surj_pair";
    2.95 -val surjective_pairing = thm "surjective_pairing";
    2.96 -val unit_abs_eta_conv = thm "unit_abs_eta_conv";
    2.97 -val unit_all_eq1 = thm "unit_all_eq1";
    2.98 -val unit_all_eq2 = thm "unit_all_eq2";
    2.99 -val unit_eq = thm "unit_eq";
   2.100 -*}
   2.101 -
   2.102  use "Tools/inductive_set.ML"
   2.103  setup Inductive_Set.setup
   2.104  
     3.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed May 26 16:05:25 2010 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed May 26 16:05:25 2010 +0200
     3.3 @@ -113,7 +113,7 @@
     3.4  
     3.5      val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
     3.6        (fn prems =>
     3.7 -         [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
     3.8 +         [rewrite_goals_tac (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
     3.9            rtac (cterm_instantiate inst induct) 1,
    3.10            ALLGOALS Object_Logic.atomize_prems_tac,
    3.11            rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
     4.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed May 26 16:05:25 2010 +0200
     4.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed May 26 16:05:25 2010 +0200
     4.3 @@ -623,7 +623,7 @@
     4.4        val thm2 = forall_intr_list (map tych L) thm1
     4.5        val thm3 = forall_elim_list (XFILL tych a vstr) thm2
     4.6    in refl RS
     4.7 -     rewrite_rule [Thm.symmetric (surjective_pairing RS eq_reflection)] thm3
     4.8 +     rewrite_rule [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
     4.9    end;
    4.10  
    4.11  fun PGEN tych a vstr th =
    4.12 @@ -663,7 +663,7 @@
    4.13  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
    4.14   let val globals = func::G
    4.15       val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
    4.16 -     val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
    4.17 +     val pbeta_reduce = simpl_conv ss0 [@{thm split_conv} RS eq_reflection];
    4.18       val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
    4.19       val dummy = term_ref := []
    4.20       val dummy = thm_ref  := []
     5.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed May 26 16:05:25 2010 +0200
     5.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed May 26 16:05:25 2010 +0200
     5.3 @@ -389,7 +389,7 @@
     5.4            end) (rlzs ~~ rnames);
     5.5          val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
     5.6            (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
     5.7 -        val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms);
     5.8 +        val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
     5.9          val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
    5.10            [rtac (#raw_induct ind_info) 1,
    5.11             rewrite_goals_tac rews,
     6.1 --- a/src/HOL/Tools/inductive_set.ML	Wed May 26 16:05:25 2010 +0200
     6.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed May 26 16:05:25 2010 +0200
     6.3 @@ -44,7 +44,7 @@
     6.4                      ts = map Bound (length ps downto 0)
     6.5                    then
     6.6                      let val simp = full_simp_tac (Simplifier.inherit_context ss
     6.7 -                      (HOL_basic_ss addsimps [split_paired_all, split_conv])) 1
     6.8 +                      (HOL_basic_ss addsimps [@{thm split_paired_all}, @{thm split_conv}])) 1
     6.9                      in
    6.10                        SOME (Goal.prove (Simplifier.the_context ss) [] []
    6.11                          (Const ("==", T --> T --> propT) $ S $ S')
    6.12 @@ -92,7 +92,7 @@
    6.13                mkop s T (m, p, mk_collect p T (head_of u), S)
    6.14          | decomp _ = NONE;
    6.15        val simp = full_simp_tac (Simplifier.inherit_context ss
    6.16 -        (HOL_basic_ss addsimps [mem_Collect_eq, split_conv])) 1;
    6.17 +        (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}])) 1;
    6.18        fun mk_rew t = (case strip_abs_vars t of
    6.19            [] => NONE
    6.20          | xs => (case decomp (strip_abs_body t) of
    6.21 @@ -255,7 +255,7 @@
    6.22                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
    6.23            end)
    6.24    in
    6.25 -    Simplifier.simplify (HOL_basic_ss addsimps [mem_Collect_eq, split_conv]
    6.26 +    Simplifier.simplify (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}]
    6.27        addsimprocs [collect_mem_simproc]) thm'' |>
    6.28          zero_var_indexes |> eta_contract_thm (equal p)
    6.29    end;
    6.30 @@ -343,7 +343,7 @@
    6.31      thm |>
    6.32      Thm.instantiate ([], insts) |>
    6.33      Simplifier.full_simplify (HOL_basic_ss addsimprocs
    6.34 -      [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |>
    6.35 +      [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
    6.36      eta_contract_thm (is_pred pred_arities) |>
    6.37      Rule_Cases.save thm
    6.38    end;
    6.39 @@ -396,7 +396,7 @@
    6.40        then
    6.41          thm |>
    6.42          Simplifier.full_simplify (HOL_basic_ss addsimprocs
    6.43 -          [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |>
    6.44 +          [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
    6.45          eta_contract_thm (is_pred pred_arities)
    6.46        else thm
    6.47    in map preproc end;
    6.48 @@ -463,7 +463,7 @@
    6.49        end) |> split_list |>> split_list;
    6.50      val eqns' = eqns @
    6.51        map (prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)
    6.52 -        (mem_Collect_eq :: split_conv :: to_pred_simps);
    6.53 +        (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps);
    6.54  
    6.55      (* predicate version of the introduction rules *)
    6.56      val intros' =
    6.57 @@ -505,7 +505,7 @@
    6.58                   (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
    6.59                    list_comb (c, params))))))
    6.60              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
    6.61 -              [def, mem_Collect_eq, split_conv]) 1))
    6.62 +              [def, mem_Collect_eq, @{thm split_conv}]) 1))
    6.63          in
    6.64            lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
    6.65              [Attrib.internal (K pred_set_conv_att)]),
     7.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Wed May 26 16:05:25 2010 +0200
     7.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Wed May 26 16:05:25 2010 +0200
     7.3 @@ -188,7 +188,7 @@
     7.4              fun tac { context = ctxt, prems = _ } =
     7.5                ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
     7.6                THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
     7.7 -              THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
     7.8 +              THEN ALLGOALS (simp_tac (HOL_ss addsimps [@{thm fst_conv}, @{thm snd_conv}]));
     7.9            in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end;
    7.10        in
    7.11          lthy
     8.1 --- a/src/HOL/Tools/record.ML	Wed May 26 16:05:25 2010 +0200
     8.2 +++ b/src/HOL/Tools/record.ML	Wed May 26 16:05:25 2010 +0200
     8.3 @@ -2215,7 +2215,7 @@
     8.4        prove_standard [] cases_prop
     8.5          (fn _ =>
     8.6            try_param_tac rN cases_scheme 1 THEN
     8.7 -          simp_all_tac HOL_basic_ss [unit_all_eq1]);
     8.8 +          simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]);
     8.9      val cases = timeit_msg "record cases proof:" cases_prf;
    8.10  
    8.11      fun surjective_prf () =