src/HOL/Tools/Datatype/rep_datatype.ML
changeset 57983 6edc3529bb4e
parent 57964 3dfc1bf3ac3d
     1.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -395,16 +395,16 @@
     1.4      |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
     1.5    end;
     1.6  
     1.7 -fun prove_weak_case_congs new_type_names case_names descr thy =
     1.8 +fun prove_case_cong_weaks new_type_names case_names descr thy =
     1.9    let
    1.10 -    fun prove_weak_case_cong t =
    1.11 +    fun prove_case_cong_weak t =
    1.12       Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    1.13         (fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]);
    1.14  
    1.15 -    val weak_case_congs =
    1.16 -      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs case_names descr thy);
    1.17 +    val case_cong_weaks =
    1.18 +      map prove_case_cong_weak (Datatype_Prop.make_case_cong_weaks case_names descr thy);
    1.19  
    1.20 -  in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
    1.21 +  in thy |> Datatype_Aux.store_thms "case_cong_weak" new_type_names case_cong_weaks end;
    1.22  
    1.23  
    1.24  (* additional theorems for TFL *)
    1.25 @@ -470,7 +470,7 @@
    1.26  
    1.27  fun make_dt_info descr induct inducts rec_names rec_rewrites
    1.28      (index, (((((((((((_, (tname, _, _))), inject), distinct),
    1.29 -      exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
    1.30 +      exhaust), nchotomy), case_name), case_rewrites), case_cong), case_cong_weak),
    1.31          (split, split_asm))) =
    1.32    (tname,
    1.33     {index = index,
    1.34 @@ -486,7 +486,7 @@
    1.35      case_name = case_name,
    1.36      case_rewrites = case_rewrites,
    1.37      case_cong = case_cong,
    1.38 -    weak_case_cong = weak_case_cong,
    1.39 +    case_cong_weak = case_cong_weak,
    1.40      split = split,
    1.41      split_asm = split_asm});
    1.42  
    1.43 @@ -513,8 +513,8 @@
    1.44        |> prove_case_thms config new_type_names descr rec_names rec_rewrites;
    1.45      val (case_congs, thy7) = thy6
    1.46        |> prove_case_congs new_type_names case_names descr nchotomys case_rewrites;
    1.47 -    val (weak_case_congs, thy8) = thy7
    1.48 -      |> prove_weak_case_congs new_type_names case_names descr;
    1.49 +    val (case_cong_weaks, thy8) = thy7
    1.50 +      |> prove_case_cong_weaks new_type_names case_names descr;
    1.51      val (splits, thy9) = thy8
    1.52        |> prove_split_thms config new_type_names case_names descr
    1.53          inject distinct exhaust case_rewrites;
    1.54 @@ -524,7 +524,7 @@
    1.55        map_index
    1.56          (make_dt_info flat_descr induct inducts rec_names rec_rewrites)
    1.57          (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
    1.58 -          case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
    1.59 +          case_names ~~ case_rewrites ~~ case_congs ~~ case_cong_weaks ~~ splits);
    1.60      val dt_names = map fst dt_infos;
    1.61      val prfx = Binding.qualify true (space_implode "_" new_type_names);
    1.62      val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;
    1.63 @@ -553,7 +553,7 @@
    1.64          ((Binding.empty, [iff_add]), [(flat inject, [])]),
    1.65          ((Binding.empty, [Classical.safe_elim NONE]),
    1.66            [(map (fn th => th RS notE) (flat distinct), [])]),
    1.67 -        ((Binding.empty, [Simplifier.cong_add]), [(weak_case_congs, [])]),
    1.68 +        ((Binding.empty, [Simplifier.cong_add]), [(case_cong_weaks, [])]),
    1.69          ((Binding.empty, [Induct.induct_simp_add]), [(flat (distinct @ inject), [])])] @
    1.70            named_rules @ unnamed_rules)
    1.71      |> snd