eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
authortraytel
Mon Jul 15 14:23:51 2013 +0200 (2013-07-15)
changeset 5265958b87aa4dc3b
parent 52658 1e7896c7f781
child 52660 7f7311d04727
eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit)
src/HOL/BNF/BNF_Def.thy
src/HOL/BNF/BNF_FP_Basic.thy
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/Countable_Type.thy
src/HOL/BNF/More_BNFs.thy
src/HOL/BNF/Tools/bnf_comp_tactics.ML
src/HOL/BNF/Tools/bnf_def_tactics.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_gfp_tactics.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_lfp_tactics.ML
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Mon Jul 15 11:29:19 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Mon Jul 15 14:23:51 2013 +0200
     1.3 @@ -171,9 +171,6 @@
     1.4  lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
     1.5  by auto
     1.6  
     1.7 -lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
     1.8 -unfolding o_def fun_eq_iff by simp
     1.9 -
    1.10  lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
    1.11    by auto
    1.12  
     2.1 --- a/src/HOL/BNF/BNF_FP_Basic.thy	Mon Jul 15 11:29:19 2013 +0200
     2.2 +++ b/src/HOL/BNF/BNF_FP_Basic.thy	Mon Jul 15 14:23:51 2013 +0200
     2.3 @@ -35,18 +35,6 @@
     2.4  lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
     2.5  by auto
     2.6  
     2.7 -lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()"
     2.8 -by simp
     2.9 -
    2.10 -lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))"
    2.11 -by clarsimp
    2.12 -
    2.13 -lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
    2.14 -by simp
    2.15 -
    2.16 -lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
    2.17 -by simp
    2.18 -
    2.19  lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
    2.20  unfolding o_def fun_eq_iff by simp
    2.21  
     3.1 --- a/src/HOL/BNF/BNF_GFP.thy	Mon Jul 15 11:29:19 2013 +0200
     3.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Mon Jul 15 14:23:51 2013 +0200
     3.3 @@ -247,11 +247,6 @@
     3.4  lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
     3.5  unfolding cpow_def clists_def card_of_ordIso_czero_iff_empty by auto
     3.6  
     3.7 -lemma incl_UNION_I:
     3.8 -assumes "i \<in> I" and "A \<subseteq> F i"
     3.9 -shows "A \<subseteq> UNION I F"
    3.10 -using assms by auto
    3.11 -
    3.12  lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
    3.13  unfolding clists_def Field_card_of by auto
    3.14  
     4.1 --- a/src/HOL/BNF/Countable_Type.thy	Mon Jul 15 11:29:19 2013 +0200
     4.2 +++ b/src/HOL/BNF/Countable_Type.thy	Mon Jul 15 14:23:51 2013 +0200
     4.3 @@ -92,10 +92,6 @@
     4.4  "countable (rcset C)"
     4.5  using Rep_cset by simp
     4.6  
     4.7 -lemma rcset_inj[simp]:
     4.8 -"rcset C = rcset D \<longleftrightarrow> C = D"
     4.9 -by (metis acset_rcset)
    4.10 -
    4.11  lemma rcset_surj:
    4.12  assumes "countable A"
    4.13  shows "\<exists> C. rcset C = A"
     5.1 --- a/src/HOL/BNF/More_BNFs.thy	Mon Jul 15 11:29:19 2013 +0200
     5.2 +++ b/src/HOL/BNF/More_BNFs.thy	Mon Jul 15 14:23:51 2013 +0200
     5.3 @@ -297,7 +297,7 @@
     5.4  
     5.5  lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
     5.6  apply (rule f_the_inv_into_f)
     5.7 -unfolding inj_on_def rcset_inj using rcset_surj by auto
     5.8 +unfolding inj_on_def Rep_cset_inject using rcset_surj by auto
     5.9  
    5.10  lemma Collect_Int_Times:
    5.11  "{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
     6.1 --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Mon Jul 15 11:29:19 2013 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Mon Jul 15 14:23:51 2013 +0200
     6.3 @@ -78,7 +78,7 @@
     6.4       [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
     6.5       rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
     6.6       rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
     6.7 -     rtac @{thm trans[OF pointfreeE[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
     6.8 +     rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
     6.9       rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]},
    6.10       rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
    6.11       [REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]},
     7.1 --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Mon Jul 15 11:29:19 2013 +0200
     7.2 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Mon Jul 15 14:23:51 2013 +0200
     7.3 @@ -45,7 +45,7 @@
     7.4  fun mk_map_cong_tac ctxt cong0 =
     7.5    (hyp_subst_tac ctxt THEN' rtac cong0 THEN'
     7.6     REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
     7.7 -fun mk_set_map' set_map = set_map RS @{thm pointfreeE};
     7.8 +fun mk_set_map' set_map = set_map RS @{thm comp_eq_dest};
     7.9  fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
    7.10    else (rtac subsetI THEN'
    7.11    rtac CollectI) 1 THEN
     8.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Jul 15 11:29:19 2013 +0200
     8.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Jul 15 14:23:51 2013 +0200
     8.3 @@ -1174,7 +1174,7 @@
     8.4                    end;
     8.5  
     8.6                  val sumEN_thm' =
     8.7 -                  unfold_thms lthy @{thms all_unit_eq}
     8.8 +                  unfold_thms lthy @{thms unit_all_eq1}
     8.9                      (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
    8.10                         (mk_sumEN_balanced n))
    8.11                    |> Morphism.thm phi;
     9.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Jul 15 11:29:19 2013 +0200
     9.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Jul 15 14:23:51 2013 +0200
     9.3 @@ -78,7 +78,7 @@
     9.4  
     9.5  fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
     9.6    unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN
     9.7 -  unfold_thms_tac ctxt @{thms all_prod_eq} THEN
     9.8 +  unfold_thms_tac ctxt @{thms split_paired_all} THEN
     9.9    HEADGOAL (EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k,
    9.10      REPEAT_DETERM o dtac meta_spec, etac meta_mp, atac]) (1 upto n)));
    9.11  
    10.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Jul 15 11:29:19 2013 +0200
    10.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Jul 15 14:23:51 2013 +0200
    10.3 @@ -2219,7 +2219,7 @@
    10.4                  |> Thm.close_derivation)
    10.5                goals cTs dtor_unfold_thms map_comp's map_cong0s;
    10.6            in
    10.7 -            map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
    10.8 +            map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
    10.9            end;
   10.10  
   10.11          val map_comp_thms =
    11.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Jul 15 11:29:19 2013 +0200
    11.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Jul 15 14:23:51 2013 +0200
    11.3 @@ -140,12 +140,14 @@
    11.4  val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
    11.5  val sum_case_weak_cong = @{thm sum_case_weak_cong};
    11.6  val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
    11.7 -val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]}
    11.8 +val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
    11.9 +val rev_bspec = Drule.rotate_prems 1 bspec;
   11.10 +val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}
   11.11  
   11.12  fun mk_coalg_set_tac coalg_def =
   11.13    dtac (coalg_def RS iffD1) 1 THEN
   11.14    REPEAT_DETERM (etac conjE 1) THEN
   11.15 -  EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN
   11.16 +  EVERY' [dtac rev_bspec, atac] 1 THEN
   11.17    REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
   11.18  
   11.19  fun mk_mor_elim_tac mor_def =
   11.20 @@ -183,7 +185,7 @@
   11.21      EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
   11.22      stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
   11.23      CONJ_WRAP' (fn i =>
   11.24 -      EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm pointfreeE}]) (1 upto n)] 1
   11.25 +      EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm comp_eq_dest}]) (1 upto n)] 1
   11.26    end;
   11.27  
   11.28  fun mk_mor_str_tac ks mor_UNIV =
   11.29 @@ -194,7 +196,7 @@
   11.30  
   11.31  fun mk_set_incl_hset_tac def rec_Suc =
   11.32    EVERY' (stac def ::
   11.33 -    map rtac [@{thm incl_UNION_I}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1},
   11.34 +    map rtac [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1},
   11.35        sym, rec_Suc]) 1;
   11.36  
   11.37  fun mk_set_hset_incl_hset_tac n defs rec_Suc i =
   11.38 @@ -238,10 +240,10 @@
   11.39        (fn (rec_Suc, (morE, ((passive_set_maps, active_set_maps), coalg_sets))) =>
   11.40          EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
   11.41            if m = 0 then K all_tac
   11.42 -          else EVERY' [rtac @{thm Un_cong}, rtac box_equals,
   11.43 +          else EVERY' [rtac Un_cong, rtac box_equals,
   11.44              rtac (nth passive_set_maps (j - 1) RS sym),
   11.45              rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
   11.46 -          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
   11.47 +          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
   11.48              (fn (i, (set_map, coalg_set)) =>
   11.49                EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
   11.50                  etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map,
   11.51 @@ -360,7 +362,7 @@
   11.52          EVERY' [rtac allI, rtac allI, rtac impI, etac @{thm UN_E}, dtac bspec, atac,
   11.53            dtac conjunct2, dtac (mk_conjunctN n i), etac allE, etac allE, dtac mp,
   11.54            atac, etac bexE, rtac bexI, atac, rtac in_mono,
   11.55 -          REPEAT_DETERM_N n o etac @{thm incl_UNION_I[OF _ subset_refl]},
   11.56 +          REPEAT_DETERM_N n o etac @{thm SUP_upper2[OF _ subset_refl]},
   11.57            atac]) (ks ~~ in_monos)] 1
   11.58    end;
   11.59  
   11.60 @@ -374,7 +376,7 @@
   11.61    end;
   11.62  
   11.63  fun mk_incl_lsbis_tac n i lsbis_def =
   11.64 -  EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI,
   11.65 +  EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm SUP_upper2}, rtac CollectI,
   11.66      REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
   11.67      rtac (mk_nth_conv n i)] 1;
   11.68  
   11.69 @@ -1122,8 +1124,8 @@
   11.70        CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY'
   11.71          [SELECT_GOAL (unfold_thms_tac ctxt
   11.72            (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
   11.73 -        rtac @{thm Un_cong}, rtac refl,
   11.74 -        CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
   11.75 +        rtac Un_cong, rtac refl,
   11.76 +        CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
   11.77            (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
   11.78              REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
   11.79        (rec_Sucs ~~ (dtor_maps ~~ set_mapss))] 1
    12.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Jul 15 11:29:19 2013 +0200
    12.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Jul 15 14:23:51 2013 +0200
    12.3 @@ -1451,7 +1451,7 @@
    12.4                  |> Thm.close_derivation)
    12.5                goals ctor_fold_thms map_comp_id_thms map_cong0s;
    12.6            in
    12.7 -            map (fn thm => thm RS @{thm pointfreeE}) maps
    12.8 +            map (fn thm => thm RS @{thm comp_eq_dest}) maps
    12.9            end;
   12.10  
   12.11          val (ctor_map_unique_thms, ctor_map_unique_thm) =
    13.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Mon Jul 15 11:29:19 2013 +0200
    13.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Mon Jul 15 14:23:51 2013 +0200
    13.3 @@ -87,6 +87,8 @@
    13.4  val ord_eq_le_trans = @{thm ord_eq_le_trans};
    13.5  val subset_trans = @{thm subset_trans};
    13.6  val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
    13.7 +val rev_bspec = Drule.rotate_prems 1 bspec;
    13.8 +val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}
    13.9  
   13.10  fun mk_alg_set_tac alg_def =
   13.11    dtac (alg_def RS iffD1) 1 THEN
   13.12 @@ -123,7 +125,7 @@
   13.13      val fbetw_tac = EVERY' [rtac ballI, stac o_apply, etac bspec, etac bspec, atac];
   13.14      fun mor_tac (set_map', map_comp_id) =
   13.15        EVERY' [rtac ballI, stac o_apply, rtac trans,
   13.16 -        rtac trans, dtac @{thm rev_bspec}, atac, etac arg_cong,
   13.17 +        rtac trans, dtac rev_bspec, atac, etac arg_cong,
   13.18           REPEAT o eresolve_tac [CollectE, conjE], etac bspec, rtac CollectI] THEN'
   13.19        CONJ_WRAP' (fn thm =>
   13.20          FIRST' [rtac subset_UNIV,
   13.21 @@ -147,7 +149,7 @@
   13.22            (EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
   13.23              etac @{thm image_mono}, atac])]) set_map';
   13.24      fun mor_tac (set_map', ((morE, map_comp_id), map_cong0L)) =
   13.25 -      EVERY' [rtac ballI, ftac @{thm rev_bspec}, atac,
   13.26 +      EVERY' [rtac ballI, ftac rev_bspec, atac,
   13.27           REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym,
   13.28           etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_map',
   13.29           rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map',
   13.30 @@ -270,7 +272,7 @@
   13.31    let
   13.32      val minG_tac = EVERY' [rtac @{thm UN_cong}, rtac refl, dtac bspec, atac, etac arg_cong];
   13.33      fun minH_tac thm =
   13.34 -      EVERY' [rtac @{thm Un_cong}, minG_tac, rtac @{thm image_cong}, rtac thm,
   13.35 +      EVERY' [rtac Un_cong, minG_tac, rtac @{thm image_cong}, rtac thm,
   13.36          REPEAT_DETERM_N (length in_congs) o minG_tac, rtac refl];
   13.37    in
   13.38      (rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ssubst THEN'
   13.39 @@ -391,7 +393,7 @@
   13.40    let
   13.41      val n = length alg_sets;
   13.42      val fbetw_tac =
   13.43 -      CONJ_WRAP' (K (EVERY' [rtac ballI, etac @{thm rev_bspec}, etac CollectE, atac])) alg_sets;
   13.44 +      CONJ_WRAP' (K (EVERY' [rtac ballI, etac rev_bspec, etac CollectE, atac])) alg_sets;
   13.45      val mor_tac =
   13.46        CONJ_WRAP' (fn thm => EVERY' [rtac ballI, rtac thm]) str_init_defs;
   13.47      fun alg_epi_tac ((alg_set, str_init_def), set_map') =
   13.48 @@ -583,7 +585,7 @@
   13.49  fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_cong0s =
   13.50    let
   13.51      val n = length map_cong0s;
   13.52 -    fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE},
   13.53 +    fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm comp_eq_dest},
   13.54        rtac sym, rtac trans, rtac o_apply, rtac trans, rtac (comp_id RS arg_cong),
   13.55        rtac (cong RS arg_cong),
   13.56        REPEAT_DETERM_N m o rtac refl,
   13.57 @@ -603,9 +605,9 @@
   13.58      fun mk_UN thm = rtac (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
   13.59        rtac @{thm Union_image_eq};
   13.60    in
   13.61 -    EVERY' [rtac (set RS @{thm pointfreeE} RS trans), rtac @{thm Un_cong},
   13.62 +    EVERY' [rtac (set RS @{thm comp_eq_dest} RS trans), rtac Un_cong,
   13.63        rtac (trans OF [set_map', trans_fun_cong_image_id_id_apply]),
   13.64 -      REPEAT_DETERM_N (n - 1) o rtac @{thm Un_cong},
   13.65 +      REPEAT_DETERM_N (n - 1) o rtac Un_cong,
   13.66        EVERY' (map mk_UN set_map's)] 1
   13.67    end;
   13.68  
   13.69 @@ -621,9 +623,9 @@
   13.70      fun mk_set_nat cset ctor_map ctor_set set_nats =
   13.71        EVERY' [rtac trans, rtac @{thm image_cong}, rtac ctor_set, rtac refl,
   13.72          rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, ctor_set RS trans]),
   13.73 -        rtac sym, EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
   13.74 +        rtac sym, EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
   13.75          rtac sym, rtac (nth set_nats (i - 1)),
   13.76 -        REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
   13.77 +        REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
   13.78          EVERY' (map useIH (drop m set_nats))];
   13.79    in
   13.80      (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_map'ss)) 1