1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Mar 28 17:31:36 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Mar 28 17:32:24 2000 +0200
     1.3 @@ -38,6 +38,9 @@
     1.4    val prove_nchotomys : string list -> (int * (string * DatatypeAux.dtyp list *
     1.5      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     1.6        thm list -> theory -> theory * thm list
     1.7 +  val prove_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
     1.8 +    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     1.9 +      theory -> theory * thm list
    1.10    val prove_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    1.11      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.12        thm list -> thm list list -> theory -> theory * thm list
    1.13 @@ -461,6 +464,16 @@
    1.14      Theory.parent_path |> apsnd flat
    1.15    end;
    1.16  
    1.17 +fun prove_weak_case_congs new_type_names descr sorts thy =
    1.18 +  let
    1.19 +    fun prove_weak_case_cong t =
    1.20 +       prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t)
    1.21 +         (fn prems => [rtac ((hd prems) RS arg_cong) 1])
    1.22 +
    1.23 +    val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
    1.24 +      new_type_names descr sorts thy)
    1.25 +
    1.26 +  in thy |> store_thms "weak_case_cong" new_type_names weak_case_congs end;
    1.27  
    1.28  (************************* additional theorems for TFL ************************)
    1.29  

     2.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Mar 28 17:31:36 2000 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Mar 28 17:32:24 2000 +0200
     2.3 @@ -514,6 +514,8 @@
     2.4        (DatatypeProp.make_nchotomys descr sorts) thy8;
     2.5      val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
     2.6        (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
     2.7 +    val (thy11, weak_case_congs) = add_and_get_axioms "weak_case_cong" new_type_names
     2.8 +      (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10;
     2.9  
    2.10      val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
    2.11        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
    2.12 @@ -522,17 +524,18 @@
    2.13  
    2.14      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
    2.15  
    2.16 -    val thy11 = thy10 |>
    2.17 +    val thy12 = thy11 |>
    2.18        Theory.add_path (space_implode "_" new_type_names) |>
    2.19        (#1 o PureThy.add_thmss [(("simps", simps), []),
    2.20          (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
    2.21 -        (("", flat (inject @ distinct)), [iff_add_global])]) |>
    2.22 +        (("", flat (inject @ distinct)), [iff_add_global]),
    2.23 +        (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>
    2.24        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    2.25        add_cases_induct dt_infos |>
    2.26        Theory.parent_path;
    2.27  
    2.28    in
    2.29 -    (thy11,
    2.30 +    (thy12,
    2.31       {distinct = distinct,
    2.32        inject = inject,
    2.33        exhaustion = exhaustion,
    2.34 @@ -568,8 +571,10 @@
    2.35        descr sorts casedist_thms thy7;
    2.36      val (thy9, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
    2.37        descr sorts nchotomys case_thms thy8;
    2.38 -    val (thy10, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
    2.39 -      descr sorts reccomb_names rec_thms thy9;
    2.40 +    val (thy10, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    2.41 +      descr sorts thy9;
    2.42 +    val (thy11, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
    2.43 +      descr sorts reccomb_names rec_thms thy10;
    2.44  
    2.45      val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
    2.46        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
    2.47 @@ -577,17 +582,18 @@
    2.48  
    2.49      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
    2.50  
    2.51 -    val thy11 = thy10 |>
    2.52 +    val thy12 = thy11 |>
    2.53        Theory.add_path (space_implode "_" new_type_names) |>
    2.54        (#1 o PureThy.add_thmss [(("simps", simps), []),
    2.55          (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
    2.56 -        (("", flat (inject @ distinct)), [iff_add_global])]) |>
    2.57 +        (("", flat (inject @ distinct)), [iff_add_global]),
    2.58 +        (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>
    2.59        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    2.60        add_cases_induct dt_infos |>
    2.61        Theory.parent_path;
    2.62  
    2.63    in
    2.64 -    (thy11,
    2.65 +    (thy12,
    2.66       {distinct = distinct,
    2.67        inject = inject,
    2.68        exhaustion = casedist_thms,
    2.69 @@ -663,11 +669,13 @@
    2.70        [descr] sorts casedist_thms thy5;
    2.71      val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
    2.72        [descr] sorts nchotomys case_thms thy6;
    2.73 -    val (thy8, size_thms) =
    2.74 -      if exists (equal "Arith") (Sign.stamp_names_of (Theory.sign_of thy7)) then
    2.75 +    val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    2.76 +      [descr] sorts thy7;
    2.77 +    val (thy9, size_thms) =
    2.78 +      if exists (equal "Arith") (Sign.stamp_names_of (Theory.sign_of thy8)) then
    2.79          DatatypeAbsProofs.prove_size_thms false new_type_names
    2.80 -          [descr] sorts reccomb_names rec_thms thy7
    2.81 -      else (thy7, []);
    2.82 +          [descr] sorts reccomb_names rec_thms thy8
    2.83 +      else (thy8, []);
    2.84  
    2.85      val dt_infos = map (make_dt_info descr induction reccomb_names rec_thms)
    2.86        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~
    2.87 @@ -675,20 +683,21 @@
    2.88  
    2.89      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
    2.90  
    2.91 -    val (thy9, [induction']) = thy8 |>
    2.92 +    val (thy10, [induction']) = thy9 |>
    2.93        (#1 o store_thmss "inject" new_type_names inject) |>
    2.94        (#1 o store_thmss "distinct" new_type_names distinct) |>
    2.95        Theory.add_path (space_implode "_" new_type_names) |>
    2.96        PureThy.add_thms [(("induct", induction), [case_names_induct])] |>>
    2.97        (#1 o PureThy.add_thmss [(("simps", simps), []),
    2.98          (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
    2.99 -        (("", flat (inject @ distinct)), [iff_add_global])]) |>>
   2.100 +        (("", flat (inject @ distinct)), [iff_add_global]),
   2.101 +        (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>>
   2.102        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>>
   2.103        add_cases_induct dt_infos |>>
   2.104        Theory.parent_path;
   2.105  
   2.106    in
   2.107 -    (thy9,
   2.108 +    (thy10,
   2.109       {distinct = distinct,
   2.110        inject = inject,
   2.111        exhaustion = casedist_thms,

     3.1 --- a/src/HOL/Tools/datatype_prop.ML	Tue Mar 28 17:31:36 2000 +0200
     3.2 +++ b/src/HOL/Tools/datatype_prop.ML	Tue Mar 28 17:32:24 2000 +0200
     3.3 @@ -34,6 +34,9 @@
     3.4    val make_size : string list -> (int * (string * DatatypeAux.dtyp list *
     3.5      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     3.6        theory -> term list
     3.7 +  val make_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
     3.8 +    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     3.9 +      theory -> term list
    3.10    val make_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    3.11      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    3.12        theory -> term list
    3.13 @@ -430,6 +433,24 @@
    3.14  
    3.15  (************************* additional rules for TFL ***************************)
    3.16  
    3.17 +fun make_weak_case_congs new_type_names descr sorts thy =
    3.18 +  let
    3.19 +    val case_combs = make_case_combs new_type_names descr sorts thy "f";
    3.20 +
    3.21 +    fun mk_case_cong comb =
    3.22 +      let 
    3.23 +        val Type ("fun", [T, _]) = fastype_of comb;
    3.24 +        val M = Free ("M", T);
    3.25 +        val M' = Free ("M'", T);
    3.26 +      in
    3.27 +        Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')),
    3.28 +          HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb $ M')))
    3.29 +      end
    3.30 +  in
    3.31 +    map mk_case_cong case_combs
    3.32 +  end;
    3.33 + 
    3.34 +
    3.35  (*---------------------------------------------------------------------------
    3.36   * Structure of case congruence theorem looks like this:
    3.37   *