# HG changeset patch # User blanchet # Date 1410888217 -7200 # Node ID 37745650a3f43d5d7e29667f0a6dd995bb3d31c7 # Parent b3f7c69e9fcdb235b3c2f7a802be3a0405143e76 register 'prod' and 'sum' as datatypes, to allow N2M through them diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/BNF_Def.thy --- a/src/HOL/BNF_Def.thy Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/BNF_Def.thy Tue Sep 16 19:23:37 2014 +0200 @@ -48,16 +48,16 @@ unfolding rel_fun_def by (blast dest!: Collect_splitD) definition collect where -"collect F x = (\f \ F. f x)" + "collect F x = (\f \ F. f x)" lemma fstI: "x = (y, z) \ fst x = y" -by simp + by simp lemma sndI: "x = (y, z) \ snd x = z" -by simp + by simp lemma bijI': "\\x y. (f x = f y) = (x = y); \y. \x. y = f x\ \ bij f" -unfolding bij_def inj_on_def by auto blast + unfolding bij_def inj_on_def by auto blast (* Operator: *) definition "Gr A f = {(a, f a) | a. a \ A}" @@ -71,27 +71,25 @@ by (rule ext) (auto simp only: comp_apply collect_def) definition convol ("\(_,/ _)\") where -"\f, g\ \ \a. (f a, g a)" + "\f, g\ \ \a. (f a, g a)" -lemma fst_convol: -"fst \ \f, g\ = f" -apply(rule ext) -unfolding convol_def by simp +lemma fst_convol: "fst \ \f, g\ = f" + apply(rule ext) + unfolding convol_def by simp -lemma snd_convol: -"snd \ \f, g\ = g" -apply(rule ext) -unfolding convol_def by simp +lemma snd_convol: "snd \ \f, g\ = g" + apply(rule ext) + unfolding convol_def by simp lemma convol_mem_GrpI: -"x \ A \ \id, g\ x \ (Collect (split (Grp A g)))" -unfolding convol_def Grp_def by auto + "x \ A \ \id, g\ x \ (Collect (split (Grp A g)))" + unfolding convol_def Grp_def by auto definition csquare where -"csquare A f1 f2 p1 p2 \ (\ a \ A. f1 (p1 a) = f2 (p2 a))" + "csquare A f1 f2 p1 p2 \ (\ a \ A. f1 (p1 a) = f2 (p2 a))" lemma eq_alt: "op = = Grp UNIV id" -unfolding Grp_def by auto + unfolding Grp_def by auto lemma leq_conversepI: "R = op = \ R \ R^--1" by auto @@ -103,83 +101,82 @@ unfolding Grp_def by auto lemma Grp_UNIV_id: "f = id \ (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f" -unfolding Grp_def by auto + unfolding Grp_def by auto lemma Grp_UNIV_idI: "x = y \ Grp UNIV id x y" -unfolding Grp_def by auto + unfolding Grp_def by auto lemma Grp_mono: "A \ B \ Grp A f \ Grp B f" -unfolding Grp_def by auto + unfolding Grp_def by auto lemma GrpI: "\f x = y; x \ A\ \ Grp A f x y" -unfolding Grp_def by auto + unfolding Grp_def by auto lemma GrpE: "Grp A f x y \ (\f x = y; x \ A\ \ R) \ R" -unfolding Grp_def by auto + unfolding Grp_def by auto lemma Collect_split_Grp_eqD: "z \ Collect (split (Grp A f)) \ (f \ fst) z = snd z" -unfolding Grp_def comp_def by auto + unfolding Grp_def comp_def by auto lemma Collect_split_Grp_inD: "z \ Collect (split (Grp A f)) \ fst z \ A" -unfolding Grp_def comp_def by auto + unfolding Grp_def comp_def by auto definition "pick_middlep P Q a c = (SOME b. P a b \ Q b c)" lemma pick_middlep: -"(P OO Q) a c \ P a (pick_middlep P Q a c) \ Q (pick_middlep P Q a c) c" -unfolding pick_middlep_def apply(rule someI_ex) by auto + "(P OO Q) a c \ P a (pick_middlep P Q a c) \ Q (pick_middlep P Q a c) c" + unfolding pick_middlep_def apply(rule someI_ex) by auto -definition fstOp where "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))" -definition sndOp where "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))" +definition fstOp where + "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))" + +definition sndOp where + "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))" lemma fstOp_in: "ac \ Collect (split (P OO Q)) \ fstOp P Q ac \ Collect (split P)" -unfolding fstOp_def mem_Collect_eq -by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1]) + unfolding fstOp_def mem_Collect_eq + by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1]) lemma fst_fstOp: "fst bc = (fst \ fstOp P Q) bc" -unfolding comp_def fstOp_def by simp + unfolding comp_def fstOp_def by simp lemma snd_sndOp: "snd bc = (snd \ sndOp P Q) bc" -unfolding comp_def sndOp_def by simp + unfolding comp_def sndOp_def by simp lemma sndOp_in: "ac \ Collect (split (P OO Q)) \ sndOp P Q ac \ Collect (split Q)" -unfolding sndOp_def mem_Collect_eq -by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2]) + unfolding sndOp_def mem_Collect_eq + by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2]) lemma csquare_fstOp_sndOp: -"csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" -unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp + "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" + unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp lemma snd_fst_flip: "snd xy = (fst \ (%(x, y). (y, x))) xy" -by (simp split: prod.split) + by (simp split: prod.split) lemma fst_snd_flip: "fst xy = (snd \ (%(x, y). (y, x))) xy" -by (simp split: prod.split) + by (simp split: prod.split) lemma flip_pred: "A \ Collect (split (R ^--1)) \ (%(x, y). (y, x)) ` A \ Collect (split R)" -by auto + by auto lemma Collect_split_mono: "A \ B \ Collect (split A) \ Collect (split B)" by auto lemma Collect_split_mono_strong: "\X = fst ` A; Y = snd ` A; \a\X. \b \ Y. P a b \ Q a b; A \ Collect (split P)\ \ - A \ Collect (split Q)" + A \ Collect (split Q)" by fastforce lemma predicate2_eqD: "A = B \ A a b \ B a b" -by simp + by simp -lemma case_sum_o_inj: -"case_sum f g \ Inl = f" -"case_sum f g \ Inr = g" -by auto +lemma case_sum_o_inj: "case_sum f g \ Inl = f" "case_sum f g \ Inr = g" + by auto -lemma map_sum_o_inj: -"map_sum f g o Inl = Inl o f" -"map_sum f g o Inr = Inr o g" -by auto +lemma map_sum_o_inj: "map_sum f g o Inl = Inl o f" "map_sum f g o Inr = Inr o g" + by auto lemma card_order_csum_cone_cexp_def: "card_order r \ ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \ {Inr ()})|" @@ -187,13 +184,12 @@ lemma If_the_inv_into_in_Func: "\inj_on g C; C \ B \ {x}\ \ - (\i. if i \ g ` C then the_inv_into C g i else x) \ Func UNIV (B \ {x})" -unfolding Func_def by (auto dest: the_inv_into_into) + (\i. if i \ g ` C then the_inv_into C g i else x) \ Func UNIV (B \ {x})" + unfolding Func_def by (auto dest: the_inv_into_into) lemma If_the_inv_into_f_f: - "\i \ C; inj_on g C\ \ - ((\i. if i \ g ` C then the_inv_into C g i else x) \ g) i = id i" -unfolding Func_def by (auto elim: the_inv_into_f_f) + "\i \ C; inj_on g C\ \ ((\i. if i \ g ` C then the_inv_into C g i else x) \ g) i = id i" + unfolding Func_def by (auto elim: the_inv_into_f_f) lemma the_inv_f_o_f_id: "inj f \ (the_inv f \ f) z = id z" by (simp add: the_inv_f_f) @@ -213,6 +209,9 @@ lemma subst_Pair: "P x y \ a = (x, y) \ P (fst a) (snd a)" by simp +lemma comp_apply_eq: "f (g x) = h (k x) \ (f \ g) x = (h \ k) x" + unfolding comp_apply by assumption + ML_file "Tools/BNF/bnf_util.ML" ML_file "Tools/BNF/bnf_tactics.ML" ML_file "Tools/BNF/bnf_def_tactics.ML" diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/BNF_Fixpoint_Base.thy --- a/src/HOL/BNF_Fixpoint_Base.thy Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/BNF_Fixpoint_Base.thy Tue Sep 16 19:23:37 2014 +0200 @@ -5,10 +5,10 @@ Author: Martin Desharnais, TU Muenchen Copyright 2012, 2013, 2014 -Shared fixed point operations on bounded natural functors. +Shared fixpoint operations on bounded natural functors. *) -header {* Shared Fixed Point Operations on Bounded Natural Functors *} +header {* Shared Fixpoint Operations on Bounded Natural Functors *} theory BNF_Fixpoint_Base imports BNF_Composition Basic_BNFs diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/BNF_Greatest_Fixpoint.thy --- a/src/HOL/BNF_Greatest_Fixpoint.thy Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy Tue Sep 16 19:23:37 2014 +0200 @@ -4,10 +4,10 @@ Author: Jasmin Blanchette, TU Muenchen Copyright 2012, 2013, 2014 -Greatest fixed point operation on bounded natural functors. +Greatest fixpoint (codatatype) operation on bounded natural functors. *) -header {* Greatest Fixed Point Operation on Bounded Natural Functors *} +header {* Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors *} theory BNF_Greatest_Fixpoint imports BNF_Fixpoint_Base String diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/BNF_Least_Fixpoint.thy --- a/src/HOL/BNF_Least_Fixpoint.thy Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Tue Sep 16 19:23:37 2014 +0200 @@ -4,10 +4,10 @@ Author: Jasmin Blanchette, TU Muenchen Copyright 2012, 2013, 2014 -Least fixed point operation on bounded natural functors. +Least fixpoint (datatype) operation on bounded natural functors. *) -header {* Least Fixed Point Operation on Bounded Natural Functors *} +header {* Least Fixpoint (Datatype) Operation on Bounded Natural Functors *} theory BNF_Least_Fixpoint imports BNF_Fixpoint_Base @@ -234,27 +234,6 @@ ML_file "Tools/Function/old_size.ML" ML_file "Tools/datatype_realizer.ML" -lemma size_bool[code]: "size (b\bool) = 0" - by (cases b) auto - -lemma size_nat[simp, code]: "size (n\nat) = n" - by (induct n) simp_all - -declare prod.size[no_atp] - -lemma size_sum_o_map: "size_sum g1 g2 \ map_sum f1 f2 = size_sum (g1 \ f1) (g2 \ f2)" - by (rule ext) (case_tac x, auto) - -lemma size_prod_o_map: "size_prod g1 g2 \ map_prod f1 f2 = size_prod (g1 \ f1) (g2 \ f2)" - by (rule ext) auto - -setup {* -BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size} - @{thms size_sum_o_map} -#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size} - @{thms size_prod_o_map} -*} - hide_fact (open) id_transfer end diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/Basic_BNF_Least_Fixpoints.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy Tue Sep 16 19:23:37 2014 +0200 @@ -0,0 +1,81 @@ +(* Title: HOL/Basic_BNF_Least_Fixpoints.thy + Author: Jasmin Blanchette, TU Muenchen + Copyright 2014 + +Registration of basic types as BNF least fixpoints (datatypes). +*) + +theory Basic_BNF_Least_Fixpoints +imports BNF_Least_Fixpoint +begin + +subsection {* Size setup (TODO: Merge with rest of file) *} + +lemma size_bool[code]: "size (b\bool) = 0" + by (cases b) auto + +lemma size_nat[simp, code]: "size (n\nat) = n" + by (induct n) simp_all + +declare prod.size[no_atp] + +lemma size_sum_o_map: "size_sum g1 g2 \ map_sum f1 f2 = size_sum (g1 \ f1) (g2 \ f2)" + by (rule ext) (case_tac x, auto) + +lemma size_prod_o_map: "size_prod g1 g2 \ map_prod f1 f2 = size_prod (g1 \ f1) (g2 \ f2)" + by (rule ext) auto + +setup {* +BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size} + @{thms size_sum_o_map} +#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size} + @{thms size_prod_o_map} +*} + + +subsection {* FP sugar setup *} + +definition xtor :: "'a \ 'a" where + "xtor x = x" + +lemma xtor_map: "f (xtor x) = xtor (f x)" + unfolding xtor_def by (rule refl) + +lemma xtor_set: "f (xtor x) = f x" + unfolding xtor_def by (rule refl) + +lemma xtor_rel: "R (xtor x) (xtor y) = R x y" + unfolding xtor_def by (rule refl) + +lemma xtor_induct: "(\x. P (xtor x)) \ P z" + unfolding xtor_def by assumption + +lemma xtor_xtor: "xtor (xtor x) = x" + unfolding xtor_def by (rule refl) + +lemmas xtor_inject = xtor_rel[of "op ="] + +definition ctor_rec :: "'a \ 'a" where + "ctor_rec x = x" + +lemma ctor_rec: "g = id \ ctor_rec f (xtor x) = f ((BNF_Composition.id_bnf \ g \ BNF_Composition.id_bnf) x)" + unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl) + +lemma ctor_rec_o_map: "ctor_rec f \ g = ctor_rec (f \ (BNF_Composition.id_bnf \ g \ BNF_Composition.id_bnf))" + unfolding ctor_rec_def BNF_Composition.id_bnf_def comp_def by (rule refl) + +lemma xtor_rel_induct: "(\x y. vimage2p BNF_Composition.id_bnf BNF_Composition.id_bnf R x y \ IR (xtor x) (xtor y)) \ R \ IR" + unfolding xtor_def vimage2p_def BNF_Composition.id_bnf_def by default + +lemma Inl_def_alt: "Inl \ (\a. xtor (BNF_Composition.id_bnf (Inl a)))" + unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive) + +lemma Inr_def_alt: "Inr \ (\a. xtor (BNF_Composition.id_bnf (Inr a)))" + unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive) + +lemma Pair_def_alt: "Pair \ (\a b. xtor (BNF_Composition.id_bnf (a, b)))" + unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive) + +ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML" + +end diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/Main.thy --- a/src/HOL/Main.thy Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/Main.thy Tue Sep 16 19:23:37 2014 +0200 @@ -2,7 +2,7 @@ theory Main imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick - BNF_Greatest_Fixpoint Old_Datatype + Basic_BNF_Least_Fixpoints BNF_Greatest_Fixpoint Old_Datatype begin text {* diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Sep 16 19:23:37 2014 +0200 @@ -583,12 +583,12 @@ Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t end; -fun build_map_or_rel mk const of_bnf dest pre_cst_table ctxt simpleTs build_simple = +fun build_map_or_rel mk const of_bnf dest pre_cst_table ctxt simple_Ts build_simple = let fun build (TU as (T, U)) = - if exists (curry (op =) T) simpleTs then + if exists (curry (op =) T) simple_Ts then build_simple TU - else if T = U andalso not (exists_subtype_in simpleTs T) then + else if T = U andalso not (exists_subtype_in simple_Ts T) then const T else (case TU of @@ -602,7 +602,8 @@ val cst = mk live Ts Us cst0; val TUs' = map dest (fst (strip_typeN live (fastype_of cst))); in Term.list_comb (cst, map build TUs') end - else build_simple TU + else + build_simple TU | _ => build_simple TU); in build end; diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Sep 16 19:23:37 2014 +0200 @@ -919,8 +919,10 @@ val transfer_gfp_sugar_thms = morph_gfp_sugar_thms o Morphism.transfer_morphism; -fun unzip_recT (Type (@{type_name prod}, _)) T = [T] - | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts +fun unzip_recT (Type (@{type_name prod}, [_, TFree x])) + (T as Type (@{type_name prod}, Ts as [_, TFree y])) = + if x = y then [T] else Ts + | unzip_recT _ (Type (@{type_name prod}, Ts as [_, TFree _])) = Ts | unzip_recT _ T = [T]; fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy = @@ -1246,8 +1248,13 @@ if T = U then x else - build_map lthy [] (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs - (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk))) (T, U) $ x; + let + val build_simple = + indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs + (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk)); + in + build_map lthy [] build_simple (T, U) $ x + end; val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss; val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss; @@ -1594,9 +1601,13 @@ fun build_corec cqg = let val T = fastype_of cqg in if exists_subtype_in Cs T then - let val U = mk_U T in - build_map lthy [] (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ => - tack (nth cs kk, nth us kk) (nth gcorecs kk))) (T, U) $ cqg + let + val U = mk_U T; + val build_simple = + indexify fst (map2 (curry mk_sumT) fpTs Cs) + (fn kk => fn _ => tack (nth cs kk, nth us kk) (nth gcorecs kk)); + in + build_map lthy [] build_simple (T, U) $ cqg end else cqg @@ -1975,7 +1986,7 @@ |>> pair ctr_sugar) ##>> (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps - else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec + else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec #> massage_res, lthy') end; diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Sep 16 19:23:37 2014 +0200 @@ -145,7 +145,8 @@ case_unit_Unity} @ sumprod_thms_map; fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt = - unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @ + HEADGOAL (subst_tac ctxt NONE [ctr_def]) THEN + unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @ pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl); val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map; @@ -194,8 +195,8 @@ fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' fp_abs_inverses abs_inverses set_maps pre_set_defss = let val n = Integer.sum ns in - unfold_thms_tac ctxt ctr_defs THEN HEADGOAL (rtac ctor_induct') THEN - co_induct_inst_as_projs_tac ctxt 0 THEN + EVERY (map (fn th => HEADGOAL (subst_asm_tac ctxt NONE [th])) ctr_defs) THEN + HEADGOAL (rtac ctor_induct') THEN co_induct_inst_as_projs_tac ctxt 0 THEN EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps) pre_set_defss mss (unflat mss (1 upto n)) kkss) diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Sep 16 19:23:37 2014 +0200 @@ -331,28 +331,31 @@ |> force_typ names_lthy smapT |> hidden_to_unit; val smap_argTs = strip_typeN live (fastype_of smap) |> fst; - fun mk_smap_arg TU = - (if domain_type TU = range_type TU then - HOLogic.id_const (domain_type TU) + fun mk_smap_arg T_to_U = + (if domain_type T_to_U = range_type T_to_U then + HOLogic.id_const (domain_type T_to_U) else let - val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT; + val (TY, (U, X)) = T_to_U |> dest_co_algT ||> dest_co_productT; val T = mk_co_algT TY U; - fun mk_co_proj TU = build_map lthy [] (fn TU => - let - val ((T1, T2), U) = TU |> co_swap |>> dest_co_productT - in - if T1 = U then co_proj1_const TU - else mk_co_comp (mk_co_proj (co_swap (T1, U)), - co_proj1_const (co_swap (mk_co_productT T1 T2, T1))) - end) TU; + fun mk_co_proj TU = + build_map lthy [] (fn TU => + let val ((T1, T2), U) = TU |> co_swap |>> dest_co_productT in + if T1 = U then co_proj1_const TU + else mk_co_comp (mk_co_proj (co_swap (T1, U)), + co_proj1_const (co_swap (mk_co_productT T1 T2, T1))) + end) + TU; + fun default () = + mk_co_product (mk_co_proj (dest_funT T)) + (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X)))); in - if not (can dest_co_productT TY) - then mk_co_product (mk_co_proj (dest_funT T)) - (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X)))) - else mk_map_co_product - (mk_co_proj (co_swap (dest_co_productT TY |> fst, U))) - (HOLogic.id_const X) + if can dest_co_productT TY then + mk_map_co_product (mk_co_proj (co_swap (dest_co_productT TY |> fst, U))) + (HOLogic.id_const X) + handle TYPE _ => default () (*N2M involving "prod" type*) + else + default () end) val smap_args = map mk_smap_arg smap_argTs; in @@ -441,8 +444,9 @@ val Rep_o_Abss = maps mk_Rep_o_Abs type_definitions; fun tac {context = ctxt, prems = _} = - unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs, fp_pre_map_defs, - fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss, Rep_o_Abss]) THEN + unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs, + fp_pre_map_defs, fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss, + Rep_o_Abss]) THEN CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs; in Library.foldr1 HOLogic.mk_conj goals diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Sep 16 19:23:37 2014 +0200 @@ -0,0 +1,141 @@ +(* Title: HOL/Tools/BNF/bnf_lfp_basic_sugar.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2014 + +Sugared datatype and codatatype constructions. +*) + +structure BNF_LFP_Basic_Sugar : sig end = +struct + +open Ctr_Sugar +open BNF_Util +open BNF_Def +open BNF_Comp +open BNF_FP_Rec_Sugar_Util +open BNF_FP_Util +open BNF_FP_Def_Sugar +open BNF_LFP_Size + +fun trivial_absT_info_of fpT = + {absT = fpT, + repT = fpT, + abs = Const (@{const_name BNF_Composition.id_bnf}, fpT --> fpT), + rep = Const (@{const_name BNF_Composition.id_bnf}, fpT --> fpT), + abs_inject = @{thm type_definition.Abs_inject + [OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I UNIV_I]}, + abs_inverse = @{thm type_definition.Abs_inverse + [OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I]}, + type_definition = @{thm BNF_Composition.type_definition_id_bnf_UNIV}}; + +fun the_frozen_ctr_sugar_of ctxt fpT_name = + the (ctr_sugar_of ctxt fpT_name) + |> morph_ctr_sugar (Morphism.typ_morphism "BNF" Logic.unvarifyT_global + $> Morphism.term_morphism "BNF" (Term.map_types Logic.unvarifyT_global)); + +fun trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct = + {Ts = [fpT], + bnfs = [fp_bnf], + ctors = [Const (@{const_name xtor}, fpT --> fpT)], + dtors = [Const (@{const_name xtor}, fpT --> fpT)], + xtor_co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))], + xtor_co_induct = @{thm xtor_induct}, + dtor_ctors = [@{thm xtor_xtor}], + ctor_dtors = [@{thm xtor_xtor}], + ctor_injects = [@{thm xtor_inject}], + dtor_injects = [@{thm xtor_inject}], + xtor_map_thms = [xtor_map], + xtor_set_thmss = [xtor_sets], + xtor_rel_thms = [xtor_rel], + xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}], + xtor_co_rec_o_map_thms = [ctor_rec_o_map], + rel_xtor_co_induct_thm = xtor_rel_induct, + dtor_set_induct_thms = []}; + +fun fp_sugar_of_sum ctxt = + let + val fpT as Type (fpT_name, As) = @{typ "'a + 'b"}; + val fpBT = @{typ "'c + 'd"}; + val C = @{typ 'e}; + val X = @{typ 'sum}; + val ctr_Tss = map single As; + + val fp_bnf = the (bnf_of ctxt fpT_name); + val xtor_map = @{thm xtor_map[of "map_sum f1 f2" for f1 f2]}; + val xtor_sets = @{thms xtor_set[of setl] xtor_set[of setr]}; + val xtor_rel = @{thm xtor_rel[of "rel_sum R1 R2" for R1 R2]}; + val ctor_rec_o_map = @{thm ctor_rec_o_map[of _ "map_sum g1 g2" for g1 g2]}; + val xtor_rel_induct = @{thm xtor_rel_induct[of "rel_sum R1 R2" for R1 R2]}; + in + {T = fpT, + BT = fpBT, + X = X, + fp = Least_FP, + fp_res_index = 0, + fp_res = + trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct, + pre_bnf = ID_bnf (*wrong*), + absT_info = trivial_absT_info_of fpT, + fp_nesting_bnfs = [], + live_nesting_bnfs = [], + ctrXs_Tss = ctr_Tss, + ctr_defs = @{thms Inl_def_alt Inr_def_alt}, + ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, + co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), + co_rec_def = @{thm case_sum_def}, + maps = @{thms map_sum.simps}, + common_co_inducts = [@{thm sum.induct}], + co_inducts = [@{thm sum.induct}], + co_rec_thms = @{thms sum.case}, + co_rec_discs = [], + co_rec_selss = [], + rel_injects = @{thms rel_sum_simps(1,4)}, + rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}} + end; + +fun fp_sugar_of_prod ctxt = + let + val fpT as Type (fpT_name, As) = @{typ "'a * 'b"}; + val fpBT = @{typ "'c * 'd"}; + val C = @{typ 'e}; + val X = @{typ 'prod}; + val ctr_Ts = As; + + val fp_bnf = the (bnf_of ctxt fpT_name); + val xtor_map = @{thm xtor_map[of "map_prod f1 f2" for f1 f2]}; + val xtor_sets = @{thms xtor_set[of fsts] xtor_set[of snds]}; + val xtor_rel = @{thm xtor_rel[of "rel_prod R1 R2" for R1 R2]}; + val ctor_rec_o_map = @{thm ctor_rec_o_map[of _ "map_prod g1 g2" for g1 g2]}; + val xtor_rel_induct = @{thm xtor_rel_induct[of "rel_prod R1 R2" for R1 R2]}; + in + {T = fpT, + BT = fpBT, + X = X, + fp = Least_FP, + fp_res_index = 0, + fp_res = + trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct, + pre_bnf = ID_bnf (*wrong*), + absT_info = trivial_absT_info_of fpT, + fp_nesting_bnfs = [], + live_nesting_bnfs = [], + ctrXs_Tss = [ctr_Ts], + ctr_defs = [@{thm Pair_def_alt}], + ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, + co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), + co_rec_def = @{thm case_prod_def}, + maps = [@{thm map_prod_simp}], + common_co_inducts = [@{thm prod.induct}], + co_inducts = [@{thm prod.induct}], + co_rec_thms = [@{thm prod.case}], + co_rec_discs = [], + co_rec_selss = [], + rel_injects = [@{thm rel_prod_apply}], + rel_distincts = []} + end; + +val _ = Theory.setup (map_local_theory (fn lthy => + fold (BNF_FP_Def_Sugar.register_fp_sugars (fn s => s <> size_plugin) o single o (fn f => f lthy)) + [fp_sugar_of_sum, fp_sugar_of_prod] lthy)); + +end; diff -r b3f7c69e9fcd -r 37745650a3f4 src/HOL/Tools/BNF/bnf_tactics.ML --- a/src/HOL/Tools/BNF/bnf_tactics.ML Tue Sep 16 19:23:37 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML Tue Sep 16 19:23:37 2014 +0200 @@ -12,6 +12,7 @@ val fo_rtac: thm -> Proof.context -> int -> tactic val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic + val subst_asm_tac: Proof.context -> int list option -> thm list -> int -> tactic val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list -> int -> tactic @@ -44,14 +45,20 @@ (*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*) fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0]; +fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt o the_default [0]; + (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) fun mk_pointfree ctxt thm = thm - |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq + |> Drule.zero_var_indexes + |> Thm.prop_of + |> Logic.unvarify_global + |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp) |> mk_Trueprop_eq |> (fn goal => Goal.prove_sorry ctxt [] [] goal - (K (rtac @{thm ext} 1 THEN unfold_thms_tac ctxt [o_apply, mk_sym thm] THEN rtac refl 1))) + (K (rtac ext 1 THEN rtac @{thm comp_apply_eq} 1 THEN rtac thm 1))) + |> Drule.export_without_context |> Thm.close_derivation;