clean up lemmas used for composition
authorblanchet
Fri Sep 21 17:02:23 2012 +0200 (2012-09-21)
changeset 4951282d99fe04018
parent 49511 9f5bfef8bd82
child 49513 796b3139f5a8
clean up lemmas used for composition
src/HOL/BNF/BNF_Comp.thy
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_comp_tactics.ML
     1.1 --- a/src/HOL/BNF/BNF_Comp.thy	Fri Sep 21 16:53:38 2012 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Comp.thy	Fri Sep 21 17:02:23 2012 +0200
     1.3 @@ -70,19 +70,7 @@
     1.4  lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R"
     1.5  unfolding Gr_def by auto
     1.6  
     1.7 -lemma subst_rel_def: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
     1.8 -by simp
     1.9 -
    1.10 -lemma abs_pred_def: "\<lbrakk>\<And>x y. (x, y) \<in> rel = pred x y\<rbrakk> \<Longrightarrow> rel = Collect (split pred)"
    1.11 -by auto
    1.12 -
    1.13 -lemma Collect_split_cong: "Collect (split pred) = Collect (split pred') \<Longrightarrow> pred = pred'"
    1.14 -by blast
    1.15 -
    1.16 -lemma pred_def_abs: "rel = Collect (split pred) \<Longrightarrow> pred = (\<lambda>x y. (x, y) \<in> rel)"
    1.17 -by auto
    1.18 -
    1.19 -lemma mem_Id_eq_eq: "(\<lambda>x y. (x, y) \<in> Id) = (op =)"
    1.20 +lemma O_Gr_cong: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
    1.21  by simp
    1.22  
    1.23  ML_file "Tools/bnf_comp_tactics.ML"
     2.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Sep 21 16:53:38 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri Sep 21 17:02:23 2012 +0200
     2.3 @@ -236,7 +236,7 @@
     2.4          val outer_srel_Gr = srel_Gr_of_bnf outer RS sym;
     2.5          val outer_srel_cong = srel_cong_of_bnf outer;
     2.6          val thm =
     2.7 -          (trans OF [in_alt_thm RS @{thm subst_rel_def},
     2.8 +          (trans OF [in_alt_thm RS @{thm O_Gr_cong},
     2.9               trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
    2.10                 [trans OF [outer_srel_Gr RS @{thm arg_cong[of _ _ converse]},
    2.11                   srel_converse_of_bnf outer RS sym], outer_srel_Gr],
    2.12 @@ -345,7 +345,7 @@
    2.13        let
    2.14          val srel_Gr = srel_Gr_of_bnf bnf RS sym
    2.15          val thm =
    2.16 -          (trans OF [in_alt_thm RS @{thm subst_rel_def},
    2.17 +          (trans OF [in_alt_thm RS @{thm O_Gr_cong},
    2.18              trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
    2.19                [trans OF [srel_Gr RS @{thm arg_cong[of _ _ converse]},
    2.20                  srel_converse_of_bnf bnf RS sym], srel_Gr],
     3.1 --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Fri Sep 21 16:53:38 2012 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Fri Sep 21 17:02:23 2012 +0200
     3.3 @@ -409,7 +409,7 @@
     3.4  
     3.5  fun mk_simple_srel_O_Gr_tac ctxt srel_def srel_O_Gr in_alt_thm =
     3.6    rtac (unfold_thms ctxt [srel_def]
     3.7 -    (trans OF [srel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym])) 1;
     3.8 +    (trans OF [srel_O_Gr, in_alt_thm RS @{thm O_Gr_cong} RS sym])) 1;
     3.9  
    3.10  fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
    3.11