# HG changeset patch # User nipkow # Date 954257544 -7200 # Node ID 8fb3a81b4ccfaf9b893a03338e10ac40db5c0d97 # Parent a466c687c72631d71793a089b82bdc8a1e15438f added weak_case_cong feature diff -r a466c687c726 -r 8fb3a81b4ccf src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Mar 28 17:31:36 2000 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Mar 28 17:32:24 2000 +0200 @@ -38,6 +38,9 @@ val prove_nchotomys : string list -> (int * (string * DatatypeAux.dtyp list * (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> thm list -> theory -> theory * thm list + val prove_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list * + (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> + theory -> theory * thm list val prove_case_congs : string list -> (int * (string * DatatypeAux.dtyp list * (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> thm list -> thm list list -> theory -> theory * thm list @@ -461,6 +464,16 @@ Theory.parent_path |> apsnd flat end; +fun prove_weak_case_congs new_type_names descr sorts thy = + let + fun prove_weak_case_cong t = + prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) + (fn prems => [rtac ((hd prems) RS arg_cong) 1]) + + val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs + new_type_names descr sorts thy) + + in thy |> store_thms "weak_case_cong" new_type_names weak_case_congs end; (************************* additional theorems for TFL ************************) diff -r a466c687c726 -r 8fb3a81b4ccf src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Mar 28 17:31:36 2000 +0200 +++ b/src/HOL/Tools/datatype_package.ML Tue Mar 28 17:32:24 2000 +0200 @@ -514,6 +514,8 @@ (DatatypeProp.make_nchotomys descr sorts) thy8; val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9; + val (thy11, weak_case_congs) = add_and_get_axioms "weak_case_cong" new_type_names + (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10; val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms) ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~ @@ -522,17 +524,18 @@ val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; - val thy11 = thy10 |> + val thy12 = thy11 |> Theory.add_path (space_implode "_" new_type_names) |> (#1 o PureThy.add_thmss [(("simps", simps), []), (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]), - (("", flat (inject @ distinct)), [iff_add_global])]) |> + (("", flat (inject @ distinct)), [iff_add_global]), + (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |> put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |> add_cases_induct dt_infos |> Theory.parent_path; in - (thy11, + (thy12, {distinct = distinct, inject = inject, exhaustion = exhaustion, @@ -568,8 +571,10 @@ descr sorts casedist_thms thy7; val (thy9, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names descr sorts nchotomys case_thms thy8; - val (thy10, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names - descr sorts reccomb_names rec_thms thy9; + val (thy10, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names + descr sorts thy9; + val (thy11, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names + descr sorts reccomb_names rec_thms thy10; val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms) ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~ @@ -577,17 +582,18 @@ val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; - val thy11 = thy10 |> + val thy12 = thy11 |> Theory.add_path (space_implode "_" new_type_names) |> (#1 o PureThy.add_thmss [(("simps", simps), []), (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]), - (("", flat (inject @ distinct)), [iff_add_global])]) |> + (("", flat (inject @ distinct)), [iff_add_global]), + (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |> put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |> add_cases_induct dt_infos |> Theory.parent_path; in - (thy11, + (thy12, {distinct = distinct, inject = inject, exhaustion = casedist_thms, @@ -663,11 +669,13 @@ [descr] sorts casedist_thms thy5; val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names [descr] sorts nchotomys case_thms thy6; - val (thy8, size_thms) = - if exists (equal "Arith") (Sign.stamp_names_of (Theory.sign_of thy7)) then + val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names + [descr] sorts thy7; + val (thy9, size_thms) = + if exists (equal "Arith") (Sign.stamp_names_of (Theory.sign_of thy8)) then DatatypeAbsProofs.prove_size_thms false new_type_names - [descr] sorts reccomb_names rec_thms thy7 - else (thy7, []); + [descr] sorts reccomb_names rec_thms thy8 + else (thy8, []); val dt_infos = map (make_dt_info descr induction reccomb_names rec_thms) ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ @@ -675,20 +683,21 @@ val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; - val (thy9, [induction']) = thy8 |> + val (thy10, [induction']) = thy9 |> (#1 o store_thmss "inject" new_type_names inject) |> (#1 o store_thmss "distinct" new_type_names distinct) |> Theory.add_path (space_implode "_" new_type_names) |> PureThy.add_thms [(("induct", induction), [case_names_induct])] |>> (#1 o PureThy.add_thmss [(("simps", simps), []), (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]), - (("", flat (inject @ distinct)), [iff_add_global])]) |>> + (("", flat (inject @ distinct)), [iff_add_global]), + (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>> put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>> add_cases_induct dt_infos |>> Theory.parent_path; in - (thy9, + (thy10, {distinct = distinct, inject = inject, exhaustion = casedist_thms, diff -r a466c687c726 -r 8fb3a81b4ccf src/HOL/Tools/datatype_prop.ML --- a/src/HOL/Tools/datatype_prop.ML Tue Mar 28 17:31:36 2000 +0200 +++ b/src/HOL/Tools/datatype_prop.ML Tue Mar 28 17:32:24 2000 +0200 @@ -34,6 +34,9 @@ val make_size : string list -> (int * (string * DatatypeAux.dtyp list * (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> theory -> term list + val make_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list * + (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> + theory -> term list val make_case_congs : string list -> (int * (string * DatatypeAux.dtyp list * (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> theory -> term list @@ -430,6 +433,24 @@ (************************* additional rules for TFL ***************************) +fun make_weak_case_congs new_type_names descr sorts thy = + let + val case_combs = make_case_combs new_type_names descr sorts thy "f"; + + fun mk_case_cong comb = + let + val Type ("fun", [T, _]) = fastype_of comb; + val M = Free ("M", T); + val M' = Free ("M'", T); + in + Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')), + HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb $ M'))) + end + in + map mk_case_cong case_combs + end; + + (*--------------------------------------------------------------------------- * Structure of case congruence theorem looks like this: *