--- 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 = (\<Union>f \<in> F. f x)"
+ "collect F x = (\<Union>f \<in> F. f x)"
lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
-by simp
+ by simp
lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
-by simp
+ by simp
lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> 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 \<in> A}"
@@ -71,27 +71,25 @@
by (rule ext) (auto simp only: comp_apply collect_def)
definition convol ("\<langle>(_,/ _)\<rangle>") where
-"\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"
+ "\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"
-lemma fst_convol:
-"fst \<circ> \<langle>f, g\<rangle> = f"
-apply(rule ext)
-unfolding convol_def by simp
+lemma fst_convol: "fst \<circ> \<langle>f, g\<rangle> = f"
+ apply(rule ext)
+ unfolding convol_def by simp
-lemma snd_convol:
-"snd \<circ> \<langle>f, g\<rangle> = g"
-apply(rule ext)
-unfolding convol_def by simp
+lemma snd_convol: "snd \<circ> \<langle>f, g\<rangle> = g"
+ apply(rule ext)
+ unfolding convol_def by simp
lemma convol_mem_GrpI:
-"x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (split (Grp A g)))"
-unfolding convol_def Grp_def by auto
+ "x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (split (Grp A g)))"
+ unfolding convol_def Grp_def by auto
definition csquare where
-"csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
+ "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> 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 = \<Longrightarrow> R \<le> R^--1"
by auto
@@ -103,83 +101,82 @@
unfolding Grp_def by auto
lemma Grp_UNIV_id: "f = id \<Longrightarrow> (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 \<Longrightarrow> Grp UNIV id x y"
-unfolding Grp_def by auto
+ unfolding Grp_def by auto
lemma Grp_mono: "A \<le> B \<Longrightarrow> Grp A f \<le> Grp B f"
-unfolding Grp_def by auto
+ unfolding Grp_def by auto
lemma GrpI: "\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> Grp A f x y"
-unfolding Grp_def by auto
+ unfolding Grp_def by auto
lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
-unfolding Grp_def by auto
+ unfolding Grp_def by auto
lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
-unfolding Grp_def comp_def by auto
+ unfolding Grp_def comp_def by auto
lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> 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 \<and> Q b c)"
lemma pick_middlep:
-"(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> Q (pick_middlep P Q a c) c"
-unfolding pick_middlep_def apply(rule someI_ex) by auto
+ "(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> 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 \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> 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 \<circ> fstOp P Q) bc"
-unfolding comp_def fstOp_def by simp
+ unfolding comp_def fstOp_def by simp
lemma snd_sndOp: "snd bc = (snd \<circ> sndOp P Q) bc"
-unfolding comp_def sndOp_def by simp
+ unfolding comp_def sndOp_def by simp
lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> 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 \<circ> (%(x, y). (y, x))) xy"
-by (simp split: prod.split)
+ by (simp split: prod.split)
lemma fst_snd_flip: "fst xy = (snd \<circ> (%(x, y). (y, x))) xy"
-by (simp split: prod.split)
+ by (simp split: prod.split)
lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
-by auto
+ by auto
lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
by auto
lemma Collect_split_mono_strong:
"\<lbrakk>X = fst ` A; Y = snd ` A; \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (split P)\<rbrakk> \<Longrightarrow>
- A \<subseteq> Collect (split Q)"
+ A \<subseteq> Collect (split Q)"
by fastforce
lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
-by simp
+ by simp
-lemma case_sum_o_inj:
-"case_sum f g \<circ> Inl = f"
-"case_sum f g \<circ> Inr = g"
-by auto
+lemma case_sum_o_inj: "case_sum f g \<circ> Inl = f" "case_sum f g \<circ> 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 \<Longrightarrow> ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \<union> {Inr ()})|"
@@ -187,13 +184,12 @@
lemma If_the_inv_into_in_Func:
"\<lbrakk>inj_on g C; C \<subseteq> B \<union> {x}\<rbrakk> \<Longrightarrow>
- (\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<in> Func UNIV (B \<union> {x})"
-unfolding Func_def by (auto dest: the_inv_into_into)
+ (\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<in> Func UNIV (B \<union> {x})"
+ unfolding Func_def by (auto dest: the_inv_into_into)
lemma If_the_inv_into_f_f:
- "\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow>
- ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<circ> g) i = id i"
-unfolding Func_def by (auto elim: the_inv_into_f_f)
+ "\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow> ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<circ> g) i = id i"
+ unfolding Func_def by (auto elim: the_inv_into_f_f)
lemma the_inv_f_o_f_id: "inj f \<Longrightarrow> (the_inv f \<circ> f) z = id z"
by (simp add: the_inv_f_f)
@@ -213,6 +209,9 @@
lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
by simp
+lemma comp_apply_eq: "f (g x) = h (k x) \<Longrightarrow> (f \<circ> g) x = (h \<circ> 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"
--- 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
--- 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
--- 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\<Colon>bool) = 0"
- by (cases b) auto
-
-lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
- by (induct n) simp_all
-
-declare prod.size[no_atp]
-
-lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
- by (rule ext) (case_tac x, auto)
-
-lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> 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
--- /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\<Colon>bool) = 0"
+ by (cases b) auto
+
+lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
+ by (induct n) simp_all
+
+declare prod.size[no_atp]
+
+lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
+ by (rule ext) (case_tac x, auto)
+
+lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> 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 \<Rightarrow> '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: "(\<And>x. P (xtor x)) \<Longrightarrow> 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 \<Rightarrow> 'a" where
+ "ctor_rec x = x"
+
+lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((BNF_Composition.id_bnf \<circ> g \<circ> 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 \<circ> g = ctor_rec (f \<circ> (BNF_Composition.id_bnf \<circ> g \<circ> BNF_Composition.id_bnf))"
+ unfolding ctor_rec_def BNF_Composition.id_bnf_def comp_def by (rule refl)
+
+lemma xtor_rel_induct: "(\<And>x y. vimage2p BNF_Composition.id_bnf BNF_Composition.id_bnf R x y \<Longrightarrow> IR (xtor x) (xtor y)) \<Longrightarrow> R \<le> IR"
+ unfolding xtor_def vimage2p_def BNF_Composition.id_bnf_def by default
+
+lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inl a)))"
+ unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
+
+lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inr a)))"
+ unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
+
+lemma Pair_def_alt: "Pair \<equiv> (\<lambda>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
--- 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 {*
--- 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;
--- 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;
--- 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)
--- 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
--- /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;
--- 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;