renamed theorem
authorblanchet
Tue Sep 04 13:02:31 2012 +0200 (2012-09-04)
changeset 49118b815fa776b91
parent 49117 000deee4913e
child 49119 1f605c36869c
renamed theorem
src/HOL/Codatatype/Tools/bnf_wrap.ML
src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:02:30 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:02:31 2012 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  val case_congN = "case_cong";
     1.5  val case_eqN = "case_eq";
     1.6  val casesN = "cases";
     1.7 -val ctr_selsN = "ctr_sels";
     1.8 +val collapseN = "collapse";
     1.9  val disc_exclusN = "disc_exclus";
    1.10  val disc_exhaustN = "disc_exhaust";
    1.11  val discsN = "discs";
    1.12 @@ -350,7 +350,7 @@
    1.13                   mk_disc_exhaust_tac n exhaust_thm discI_thms)]
    1.14              end;
    1.15  
    1.16 -        val ctr_sel_thms =
    1.17 +        val collapse_thms =
    1.18            let
    1.19              fun mk_goal ctr disc sels =
    1.20                let
    1.21 @@ -366,7 +366,7 @@
    1.22            in
    1.23              map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
    1.24                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
    1.25 -                mk_ctr_sel_tac ctxt m discD sel_thms))) ms discD_thms sel_thmss goals
    1.26 +                mk_collapse_tac ctxt m discD sel_thms))) ms discD_thms sel_thmss goals
    1.27              |> map_filter I
    1.28            end;
    1.29  
    1.30 @@ -437,7 +437,7 @@
    1.31            [(case_congN, [case_cong_thm]),
    1.32             (case_eqN, [case_eq_thm]),
    1.33             (casesN, case_thms),
    1.34 -           (ctr_selsN, ctr_sel_thms),
    1.35 +           (collapseN, collapse_thms),
    1.36             (discsN, disc_thms),
    1.37             (disc_exclusN, disc_exclus_thms),
    1.38             (disc_exhaustN, disc_exhaust_thms),
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Tue Sep 04 13:02:30 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Tue Sep 04 13:02:31 2012 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  sig
     2.5    val mk_case_cong_tac: thm -> thm list -> tactic
     2.6    val mk_case_eq_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
     2.7 -  val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic
     2.8 +  val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
     2.9    val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
    2.10    val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic
    2.11    val mk_nchotomy_tac: int -> thm -> tactic
    2.12 @@ -56,7 +56,7 @@
    2.13     EVERY' (map2 (fn k => fn discI =>
    2.14       dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1;
    2.15  
    2.16 -fun mk_ctr_sel_tac ctxt m discD sel_thms =
    2.17 +fun mk_collapse_tac ctxt m discD sel_thms =
    2.18    (dtac discD THEN'
    2.19     (if m = 0 then
    2.20        atac