register 'prod' and 'sum' as datatypes, to allow N2M through them
authorblanchet
Tue Sep 16 19:23:37 2014 +0200 (2014-09-16)
changeset 5835237745650a3f4
parent 58351 b3f7c69e9fcd
child 58353 c9f374b64d99
register 'prod' and 'sum' as datatypes, to allow N2M through them
src/HOL/BNF_Def.thy
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/BNF_Greatest_Fixpoint.thy
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Basic_BNF_Least_Fixpoints.thy
src/HOL/Main.thy
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
src/HOL/Tools/BNF/bnf_tactics.ML
     1.1 --- a/src/HOL/BNF_Def.thy	Tue Sep 16 19:23:37 2014 +0200
     1.2 +++ b/src/HOL/BNF_Def.thy	Tue Sep 16 19:23:37 2014 +0200
     1.3 @@ -48,16 +48,16 @@
     1.4    unfolding rel_fun_def by (blast dest!: Collect_splitD)
     1.5  
     1.6  definition collect where
     1.7 -"collect F x = (\<Union>f \<in> F. f x)"
     1.8 +  "collect F x = (\<Union>f \<in> F. f x)"
     1.9  
    1.10  lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
    1.11 -by simp
    1.12 +  by simp
    1.13  
    1.14  lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
    1.15 -by simp
    1.16 +  by simp
    1.17  
    1.18  lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
    1.19 -unfolding bij_def inj_on_def by auto blast
    1.20 +  unfolding bij_def inj_on_def by auto blast
    1.21  
    1.22  (* Operator: *)
    1.23  definition "Gr A f = {(a, f a) | a. a \<in> A}"
    1.24 @@ -71,27 +71,25 @@
    1.25    by (rule ext) (auto simp only: comp_apply collect_def)
    1.26  
    1.27  definition convol ("\<langle>(_,/ _)\<rangle>") where
    1.28 -"\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"
    1.29 +  "\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"
    1.30  
    1.31 -lemma fst_convol:
    1.32 -"fst \<circ> \<langle>f, g\<rangle> = f"
    1.33 -apply(rule ext)
    1.34 -unfolding convol_def by simp
    1.35 +lemma fst_convol: "fst \<circ> \<langle>f, g\<rangle> = f"
    1.36 +  apply(rule ext)
    1.37 +  unfolding convol_def by simp
    1.38  
    1.39 -lemma snd_convol:
    1.40 -"snd \<circ> \<langle>f, g\<rangle> = g"
    1.41 -apply(rule ext)
    1.42 -unfolding convol_def by simp
    1.43 +lemma snd_convol: "snd \<circ> \<langle>f, g\<rangle> = g"
    1.44 +  apply(rule ext)
    1.45 +  unfolding convol_def by simp
    1.46  
    1.47  lemma convol_mem_GrpI:
    1.48 -"x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (split (Grp A g)))"
    1.49 -unfolding convol_def Grp_def by auto
    1.50 +  "x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (split (Grp A g)))"
    1.51 +  unfolding convol_def Grp_def by auto
    1.52  
    1.53  definition csquare where
    1.54 -"csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
    1.55 +  "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
    1.56  
    1.57  lemma eq_alt: "op = = Grp UNIV id"
    1.58 -unfolding Grp_def by auto
    1.59 +  unfolding Grp_def by auto
    1.60  
    1.61  lemma leq_conversepI: "R = op = \<Longrightarrow> R \<le> R^--1"
    1.62    by auto
    1.63 @@ -103,83 +101,82 @@
    1.64    unfolding Grp_def by auto
    1.65  
    1.66  lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f"
    1.67 -unfolding Grp_def by auto
    1.68 +  unfolding Grp_def by auto
    1.69  
    1.70  lemma Grp_UNIV_idI: "x = y \<Longrightarrow> Grp UNIV id x y"
    1.71 -unfolding Grp_def by auto
    1.72 +  unfolding Grp_def by auto
    1.73  
    1.74  lemma Grp_mono: "A \<le> B \<Longrightarrow> Grp A f \<le> Grp B f"
    1.75 -unfolding Grp_def by auto
    1.76 +  unfolding Grp_def by auto
    1.77  
    1.78  lemma GrpI: "\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> Grp A f x y"
    1.79 -unfolding Grp_def by auto
    1.80 +  unfolding Grp_def by auto
    1.81  
    1.82  lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
    1.83 -unfolding Grp_def by auto
    1.84 +  unfolding Grp_def by auto
    1.85  
    1.86  lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
    1.87 -unfolding Grp_def comp_def by auto
    1.88 +  unfolding Grp_def comp_def by auto
    1.89  
    1.90  lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
    1.91 -unfolding Grp_def comp_def by auto
    1.92 +  unfolding Grp_def comp_def by auto
    1.93  
    1.94  definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
    1.95  
    1.96  lemma pick_middlep:
    1.97 -"(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> Q (pick_middlep P Q a c) c"
    1.98 -unfolding pick_middlep_def apply(rule someI_ex) by auto
    1.99 +  "(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> Q (pick_middlep P Q a c) c"
   1.100 +  unfolding pick_middlep_def apply(rule someI_ex) by auto
   1.101  
   1.102 -definition fstOp where "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))"
   1.103 -definition sndOp where "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))"
   1.104 +definition fstOp where
   1.105 +  "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))"
   1.106 +
   1.107 +definition sndOp where
   1.108 +  "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))"
   1.109  
   1.110  lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)"
   1.111 -unfolding fstOp_def mem_Collect_eq
   1.112 -by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1])
   1.113 +  unfolding fstOp_def mem_Collect_eq
   1.114 +  by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1])
   1.115  
   1.116  lemma fst_fstOp: "fst bc = (fst \<circ> fstOp P Q) bc"
   1.117 -unfolding comp_def fstOp_def by simp
   1.118 +  unfolding comp_def fstOp_def by simp
   1.119  
   1.120  lemma snd_sndOp: "snd bc = (snd \<circ> sndOp P Q) bc"
   1.121 -unfolding comp_def sndOp_def by simp
   1.122 +  unfolding comp_def sndOp_def by simp
   1.123  
   1.124  lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)"
   1.125 -unfolding sndOp_def mem_Collect_eq
   1.126 -by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2])
   1.127 +  unfolding sndOp_def mem_Collect_eq
   1.128 +  by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2])
   1.129  
   1.130  lemma csquare_fstOp_sndOp:
   1.131 -"csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
   1.132 -unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp
   1.133 +  "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
   1.134 +  unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp
   1.135  
   1.136  lemma snd_fst_flip: "snd xy = (fst \<circ> (%(x, y). (y, x))) xy"
   1.137 -by (simp split: prod.split)
   1.138 +  by (simp split: prod.split)
   1.139  
   1.140  lemma fst_snd_flip: "fst xy = (snd \<circ> (%(x, y). (y, x))) xy"
   1.141 -by (simp split: prod.split)
   1.142 +  by (simp split: prod.split)
   1.143  
   1.144  lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
   1.145 -by auto
   1.146 +  by auto
   1.147  
   1.148  lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
   1.149    by auto
   1.150  
   1.151  lemma Collect_split_mono_strong: 
   1.152    "\<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>
   1.153 -  A \<subseteq> Collect (split Q)"
   1.154 +   A \<subseteq> Collect (split Q)"
   1.155    by fastforce
   1.156  
   1.157  
   1.158  lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
   1.159 -by simp
   1.160 +  by simp
   1.161  
   1.162 -lemma case_sum_o_inj:
   1.163 -"case_sum f g \<circ> Inl = f"
   1.164 -"case_sum f g \<circ> Inr = g"
   1.165 -by auto
   1.166 +lemma case_sum_o_inj: "case_sum f g \<circ> Inl = f" "case_sum f g \<circ> Inr = g"
   1.167 +  by auto
   1.168  
   1.169 -lemma map_sum_o_inj:
   1.170 -"map_sum f g o Inl = Inl o f"
   1.171 -"map_sum f g o Inr = Inr o g"
   1.172 -by auto
   1.173 +lemma map_sum_o_inj: "map_sum f g o Inl = Inl o f" "map_sum f g o Inr = Inr o g"
   1.174 +  by auto
   1.175  
   1.176  lemma card_order_csum_cone_cexp_def:
   1.177    "card_order r \<Longrightarrow> ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \<union> {Inr ()})|"
   1.178 @@ -187,13 +184,12 @@
   1.179  
   1.180  lemma If_the_inv_into_in_Func:
   1.181    "\<lbrakk>inj_on g C; C \<subseteq> B \<union> {x}\<rbrakk> \<Longrightarrow>
   1.182 -  (\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<in> Func UNIV (B \<union> {x})"
   1.183 -unfolding Func_def by (auto dest: the_inv_into_into)
   1.184 +   (\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<in> Func UNIV (B \<union> {x})"
   1.185 +  unfolding Func_def by (auto dest: the_inv_into_into)
   1.186  
   1.187  lemma If_the_inv_into_f_f:
   1.188 -  "\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow>
   1.189 -  ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<circ> g) i = id i"
   1.190 -unfolding Func_def by (auto elim: the_inv_into_f_f)
   1.191 +  "\<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"
   1.192 +  unfolding Func_def by (auto elim: the_inv_into_f_f)
   1.193  
   1.194  lemma the_inv_f_o_f_id: "inj f \<Longrightarrow> (the_inv f \<circ> f) z = id z"
   1.195    by (simp add: the_inv_f_f)
   1.196 @@ -213,6 +209,9 @@
   1.197  lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
   1.198    by simp
   1.199  
   1.200 +lemma comp_apply_eq: "f (g x) = h (k x) \<Longrightarrow> (f \<circ> g) x = (h \<circ> k) x"
   1.201 +  unfolding comp_apply by assumption
   1.202 +
   1.203  ML_file "Tools/BNF/bnf_util.ML"
   1.204  ML_file "Tools/BNF/bnf_tactics.ML"
   1.205  ML_file "Tools/BNF/bnf_def_tactics.ML"
     2.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Tue Sep 16 19:23:37 2014 +0200
     2.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Tue Sep 16 19:23:37 2014 +0200
     2.3 @@ -5,10 +5,10 @@
     2.4      Author:     Martin Desharnais, TU Muenchen
     2.5      Copyright   2012, 2013, 2014
     2.6  
     2.7 -Shared fixed point operations on bounded natural functors.
     2.8 +Shared fixpoint operations on bounded natural functors.
     2.9  *)
    2.10  
    2.11 -header {* Shared Fixed Point Operations on Bounded Natural Functors *}
    2.12 +header {* Shared Fixpoint Operations on Bounded Natural Functors *}
    2.13  
    2.14  theory BNF_Fixpoint_Base
    2.15  imports BNF_Composition Basic_BNFs
     3.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Tue Sep 16 19:23:37 2014 +0200
     3.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Tue Sep 16 19:23:37 2014 +0200
     3.3 @@ -4,10 +4,10 @@
     3.4      Author:     Jasmin Blanchette, TU Muenchen
     3.5      Copyright   2012, 2013, 2014
     3.6  
     3.7 -Greatest fixed point operation on bounded natural functors.
     3.8 +Greatest fixpoint (codatatype) operation on bounded natural functors.
     3.9  *)
    3.10  
    3.11 -header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
    3.12 +header {* Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors *}
    3.13  
    3.14  theory BNF_Greatest_Fixpoint
    3.15  imports BNF_Fixpoint_Base String
     4.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 16 19:23:37 2014 +0200
     4.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 16 19:23:37 2014 +0200
     4.3 @@ -4,10 +4,10 @@
     4.4      Author:     Jasmin Blanchette, TU Muenchen
     4.5      Copyright   2012, 2013, 2014
     4.6  
     4.7 -Least fixed point operation on bounded natural functors.
     4.8 +Least fixpoint (datatype) operation on bounded natural functors.
     4.9  *)
    4.10  
    4.11 -header {* Least Fixed Point Operation on Bounded Natural Functors *}
    4.12 +header {* Least Fixpoint (Datatype) Operation on Bounded Natural Functors *}
    4.13  
    4.14  theory BNF_Least_Fixpoint
    4.15  imports BNF_Fixpoint_Base
    4.16 @@ -234,27 +234,6 @@
    4.17  ML_file "Tools/Function/old_size.ML"
    4.18  ML_file "Tools/datatype_realizer.ML"
    4.19  
    4.20 -lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    4.21 -  by (cases b) auto
    4.22 -
    4.23 -lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
    4.24 -  by (induct n) simp_all
    4.25 -
    4.26 -declare prod.size[no_atp]
    4.27 -
    4.28 -lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
    4.29 -  by (rule ext) (case_tac x, auto)
    4.30 -
    4.31 -lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
    4.32 -  by (rule ext) auto
    4.33 -
    4.34 -setup {*
    4.35 -BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
    4.36 -  @{thms size_sum_o_map}
    4.37 -#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
    4.38 -  @{thms size_prod_o_map}
    4.39 -*}
    4.40 -
    4.41  hide_fact (open) id_transfer
    4.42  
    4.43  end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy	Tue Sep 16 19:23:37 2014 +0200
     5.3 @@ -0,0 +1,81 @@
     5.4 +(*  Title:      HOL/Basic_BNF_Least_Fixpoints.thy
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +    Copyright   2014
     5.7 +
     5.8 +Registration of basic types as BNF least fixpoints (datatypes).
     5.9 +*)
    5.10 +
    5.11 +theory Basic_BNF_Least_Fixpoints
    5.12 +imports BNF_Least_Fixpoint
    5.13 +begin
    5.14 +
    5.15 +subsection {* Size setup (TODO: Merge with rest of file) *}
    5.16 +
    5.17 +lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    5.18 +  by (cases b) auto
    5.19 +
    5.20 +lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
    5.21 +  by (induct n) simp_all
    5.22 +
    5.23 +declare prod.size[no_atp]
    5.24 +
    5.25 +lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
    5.26 +  by (rule ext) (case_tac x, auto)
    5.27 +
    5.28 +lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
    5.29 +  by (rule ext) auto
    5.30 +
    5.31 +setup {*
    5.32 +BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
    5.33 +  @{thms size_sum_o_map}
    5.34 +#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
    5.35 +  @{thms size_prod_o_map}
    5.36 +*}
    5.37 +
    5.38 +
    5.39 +subsection {* FP sugar setup *}
    5.40 +
    5.41 +definition xtor :: "'a \<Rightarrow> 'a" where
    5.42 +  "xtor x = x"
    5.43 +
    5.44 +lemma xtor_map: "f (xtor x) = xtor (f x)"
    5.45 +  unfolding xtor_def by (rule refl)
    5.46 +
    5.47 +lemma xtor_set: "f (xtor x) = f x"
    5.48 +  unfolding xtor_def by (rule refl) 
    5.49 +
    5.50 +lemma xtor_rel: "R (xtor x) (xtor y) = R x y"
    5.51 +  unfolding xtor_def by (rule refl)
    5.52 +
    5.53 +lemma xtor_induct: "(\<And>x. P (xtor x)) \<Longrightarrow> P z"
    5.54 +  unfolding xtor_def by assumption
    5.55 +
    5.56 +lemma xtor_xtor: "xtor (xtor x) = x"
    5.57 +  unfolding xtor_def by (rule refl)
    5.58 +
    5.59 +lemmas xtor_inject = xtor_rel[of "op ="]
    5.60 +
    5.61 +definition ctor_rec :: "'a \<Rightarrow> 'a" where
    5.62 +  "ctor_rec x = x"
    5.63 +
    5.64 +lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((BNF_Composition.id_bnf \<circ> g \<circ> BNF_Composition.id_bnf) x)"
    5.65 +  unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
    5.66 +
    5.67 +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))"
    5.68 +  unfolding ctor_rec_def BNF_Composition.id_bnf_def comp_def by (rule refl)
    5.69 +
    5.70 +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"
    5.71 +  unfolding xtor_def vimage2p_def BNF_Composition.id_bnf_def by default
    5.72 +
    5.73 +lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inl a)))"
    5.74 +  unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    5.75 +
    5.76 +lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inr a)))"
    5.77 +  unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    5.78 +
    5.79 +lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (BNF_Composition.id_bnf (a, b)))"
    5.80 +  unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    5.81 +
    5.82 +ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
    5.83 +
    5.84 +end
     6.1 --- a/src/HOL/Main.thy	Tue Sep 16 19:23:37 2014 +0200
     6.2 +++ b/src/HOL/Main.thy	Tue Sep 16 19:23:37 2014 +0200
     6.3 @@ -2,7 +2,7 @@
     6.4  
     6.5  theory Main
     6.6  imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
     6.7 -  BNF_Greatest_Fixpoint Old_Datatype
     6.8 +  Basic_BNF_Least_Fixpoints BNF_Greatest_Fixpoint Old_Datatype
     6.9  begin
    6.10  
    6.11  text {*
     7.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Sep 16 19:23:37 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Sep 16 19:23:37 2014 +0200
     7.3 @@ -583,12 +583,12 @@
     7.4      Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
     7.5    end;
     7.6  
     7.7 -fun build_map_or_rel mk const of_bnf dest pre_cst_table  ctxt simpleTs build_simple =
     7.8 +fun build_map_or_rel mk const of_bnf dest pre_cst_table ctxt simple_Ts build_simple =
     7.9    let
    7.10      fun build (TU as (T, U)) =
    7.11 -      if exists (curry (op =) T) simpleTs then
    7.12 +      if exists (curry (op =) T) simple_Ts then
    7.13          build_simple TU
    7.14 -      else if T = U andalso not (exists_subtype_in simpleTs T) then
    7.15 +      else if T = U andalso not (exists_subtype_in simple_Ts T) then
    7.16          const T
    7.17        else
    7.18          (case TU of
    7.19 @@ -602,7 +602,8 @@
    7.20                val cst = mk live Ts Us cst0;
    7.21                val TUs' = map dest (fst (strip_typeN live (fastype_of cst)));
    7.22              in Term.list_comb (cst, map build TUs') end
    7.23 -          else build_simple TU
    7.24 +          else
    7.25 +            build_simple TU
    7.26          | _ => build_simple TU);
    7.27    in build end;
    7.28  
     8.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 16 19:23:37 2014 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 16 19:23:37 2014 +0200
     8.3 @@ -919,8 +919,10 @@
     8.4  
     8.5  val transfer_gfp_sugar_thms = morph_gfp_sugar_thms o Morphism.transfer_morphism;
     8.6  
     8.7 -fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
     8.8 -  | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts
     8.9 +fun unzip_recT (Type (@{type_name prod}, [_, TFree x]))
    8.10 +      (T as Type (@{type_name prod}, Ts as [_, TFree y])) =
    8.11 +    if x = y then [T] else Ts
    8.12 +  | unzip_recT _ (Type (@{type_name prod}, Ts as [_, TFree _])) = Ts
    8.13    | unzip_recT _ T = [T];
    8.14  
    8.15  fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy =
    8.16 @@ -1246,8 +1248,13 @@
    8.17            if T = U then
    8.18              x
    8.19            else
    8.20 -            build_map lthy [] (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
    8.21 -              (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk))) (T, U) $ x;
    8.22 +            let
    8.23 +              val build_simple =
    8.24 +                indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
    8.25 +                  (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk));
    8.26 +            in
    8.27 +              build_map lthy [] build_simple (T, U) $ x
    8.28 +            end;
    8.29  
    8.30          val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
    8.31          val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss;
    8.32 @@ -1594,9 +1601,13 @@
    8.33          fun build_corec cqg =
    8.34            let val T = fastype_of cqg in
    8.35              if exists_subtype_in Cs T then
    8.36 -              let val U = mk_U T in
    8.37 -                build_map lthy [] (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ =>
    8.38 -                  tack (nth cs kk, nth us kk) (nth gcorecs kk))) (T, U) $ cqg
    8.39 +              let
    8.40 +                val U = mk_U T;
    8.41 +                val build_simple =
    8.42 +                  indexify fst (map2 (curry mk_sumT) fpTs Cs)
    8.43 +                    (fn kk => fn _ => tack (nth cs kk, nth us kk) (nth gcorecs kk));
    8.44 +              in
    8.45 +                build_map lthy [] build_simple (T, U) $ cqg
    8.46                end
    8.47              else
    8.48                cqg
    8.49 @@ -1975,7 +1986,7 @@
    8.50             |>> pair ctr_sugar)
    8.51           ##>>
    8.52             (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps
    8.53 -           else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec
    8.54 +            else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec
    8.55           #> massage_res, lthy')
    8.56        end;
    8.57  
     9.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Sep 16 19:23:37 2014 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Sep 16 19:23:37 2014 +0200
     9.3 @@ -145,7 +145,8 @@
     9.4        case_unit_Unity} @ sumprod_thms_map;
     9.5  
     9.6  fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
     9.7 -  unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
     9.8 +  HEADGOAL (subst_tac ctxt NONE [ctr_def]) THEN
     9.9 +  unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
    9.10      pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
    9.11  
    9.12  val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map;
    9.13 @@ -194,8 +195,8 @@
    9.14  fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' fp_abs_inverses abs_inverses set_maps
    9.15      pre_set_defss =
    9.16    let val n = Integer.sum ns in
    9.17 -    unfold_thms_tac ctxt ctr_defs THEN HEADGOAL (rtac ctor_induct') THEN
    9.18 -    co_induct_inst_as_projs_tac ctxt 0 THEN
    9.19 +    EVERY (map (fn th => HEADGOAL (subst_asm_tac ctxt NONE [th])) ctr_defs) THEN
    9.20 +    HEADGOAL (rtac ctor_induct') THEN co_induct_inst_as_projs_tac ctxt 0 THEN
    9.21      EVERY (map4 (EVERY oooo map3 o
    9.22          mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps)
    9.23        pre_set_defss mss (unflat mss (1 upto n)) kkss)
    10.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Sep 16 19:23:37 2014 +0200
    10.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Sep 16 19:23:37 2014 +0200
    10.3 @@ -331,28 +331,31 @@
    10.4                    |> force_typ names_lthy smapT
    10.5                    |> hidden_to_unit;
    10.6                  val smap_argTs = strip_typeN live (fastype_of smap) |> fst;
    10.7 -                fun mk_smap_arg TU =
    10.8 -                  (if domain_type TU = range_type TU then
    10.9 -                    HOLogic.id_const (domain_type TU)
   10.10 +                fun mk_smap_arg T_to_U =
   10.11 +                  (if domain_type T_to_U = range_type T_to_U then
   10.12 +                    HOLogic.id_const (domain_type T_to_U)
   10.13                    else
   10.14                      let
   10.15 -                      val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
   10.16 +                      val (TY, (U, X)) = T_to_U |> dest_co_algT ||> dest_co_productT;
   10.17                        val T = mk_co_algT TY U;
   10.18 -                      fun mk_co_proj TU = build_map lthy [] (fn TU =>
   10.19 -                        let
   10.20 -                          val ((T1, T2), U) = TU |> co_swap |>> dest_co_productT
   10.21 -                        in
   10.22 -                          if T1 = U then co_proj1_const TU
   10.23 -                          else mk_co_comp (mk_co_proj (co_swap (T1, U)),
   10.24 -                            co_proj1_const (co_swap (mk_co_productT T1 T2, T1)))
   10.25 -                        end) TU;
   10.26 +                      fun mk_co_proj TU =
   10.27 +                        build_map lthy [] (fn TU =>
   10.28 +                          let val ((T1, T2), U) = TU |> co_swap |>> dest_co_productT in
   10.29 +                            if T1 = U then co_proj1_const TU
   10.30 +                            else mk_co_comp (mk_co_proj (co_swap (T1, U)),
   10.31 +                              co_proj1_const (co_swap (mk_co_productT T1 T2, T1)))
   10.32 +                          end)
   10.33 +                          TU;
   10.34 +                      fun default () =
   10.35 +                        mk_co_product (mk_co_proj (dest_funT T))
   10.36 +                          (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))));
   10.37                      in
   10.38 -                      if not (can dest_co_productT TY)
   10.39 -                      then mk_co_product (mk_co_proj (dest_funT T))
   10.40 -                        (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
   10.41 -                      else mk_map_co_product
   10.42 -                        (mk_co_proj (co_swap (dest_co_productT TY |> fst, U)))
   10.43 -                        (HOLogic.id_const X)
   10.44 +                      if can dest_co_productT TY then
   10.45 +                        mk_map_co_product (mk_co_proj (co_swap (dest_co_productT TY |> fst, U)))
   10.46 +                          (HOLogic.id_const X)
   10.47 +                        handle TYPE _ => default () (*N2M involving "prod" type*)
   10.48 +                      else
   10.49 +                        default ()
   10.50                      end)
   10.51                  val smap_args = map mk_smap_arg smap_argTs;
   10.52                in
   10.53 @@ -441,8 +444,9 @@
   10.54          val Rep_o_Abss = maps mk_Rep_o_Abs type_definitions;
   10.55  
   10.56          fun tac {context = ctxt, prems = _} =
   10.57 -          unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs, fp_pre_map_defs,
   10.58 -            fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss, Rep_o_Abss]) THEN
   10.59 +          unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs,
   10.60 +            fp_pre_map_defs, fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss,
   10.61 +            Rep_o_Abss]) THEN
   10.62            CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs;
   10.63        in
   10.64          Library.foldr1 HOLogic.mk_conj goals
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Sep 16 19:23:37 2014 +0200
    11.3 @@ -0,0 +1,141 @@
    11.4 +(*  Title:      HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
    11.5 +    Author:     Jasmin Blanchette, TU Muenchen
    11.6 +    Copyright   2014
    11.7 +
    11.8 +Sugared datatype and codatatype constructions.
    11.9 +*)
   11.10 +
   11.11 +structure BNF_LFP_Basic_Sugar : sig end =
   11.12 +struct
   11.13 +
   11.14 +open Ctr_Sugar
   11.15 +open BNF_Util
   11.16 +open BNF_Def
   11.17 +open BNF_Comp
   11.18 +open BNF_FP_Rec_Sugar_Util
   11.19 +open BNF_FP_Util
   11.20 +open BNF_FP_Def_Sugar
   11.21 +open BNF_LFP_Size
   11.22 +
   11.23 +fun trivial_absT_info_of fpT =
   11.24 +  {absT = fpT,
   11.25 +   repT = fpT,
   11.26 +   abs = Const (@{const_name BNF_Composition.id_bnf}, fpT --> fpT),
   11.27 +   rep = Const (@{const_name BNF_Composition.id_bnf}, fpT --> fpT),
   11.28 +   abs_inject = @{thm type_definition.Abs_inject
   11.29 +     [OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I UNIV_I]},
   11.30 +   abs_inverse = @{thm type_definition.Abs_inverse
   11.31 +     [OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I]},
   11.32 +   type_definition = @{thm BNF_Composition.type_definition_id_bnf_UNIV}};
   11.33 +
   11.34 +fun the_frozen_ctr_sugar_of ctxt fpT_name =
   11.35 +  the (ctr_sugar_of ctxt fpT_name)
   11.36 +  |> morph_ctr_sugar (Morphism.typ_morphism "BNF" Logic.unvarifyT_global
   11.37 +    $> Morphism.term_morphism "BNF" (Term.map_types Logic.unvarifyT_global));
   11.38 +
   11.39 +fun trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct =
   11.40 +  {Ts = [fpT],
   11.41 +   bnfs = [fp_bnf],
   11.42 +   ctors = [Const (@{const_name xtor}, fpT --> fpT)],
   11.43 +   dtors = [Const (@{const_name xtor}, fpT --> fpT)],
   11.44 +   xtor_co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))],
   11.45 +   xtor_co_induct = @{thm xtor_induct},
   11.46 +   dtor_ctors = [@{thm xtor_xtor}],
   11.47 +   ctor_dtors = [@{thm xtor_xtor}],
   11.48 +   ctor_injects = [@{thm xtor_inject}],
   11.49 +   dtor_injects = [@{thm xtor_inject}],
   11.50 +   xtor_map_thms = [xtor_map],
   11.51 +   xtor_set_thmss = [xtor_sets],
   11.52 +   xtor_rel_thms = [xtor_rel],
   11.53 +   xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
   11.54 +   xtor_co_rec_o_map_thms = [ctor_rec_o_map],
   11.55 +   rel_xtor_co_induct_thm = xtor_rel_induct,
   11.56 +   dtor_set_induct_thms = []};
   11.57 +
   11.58 +fun fp_sugar_of_sum ctxt =
   11.59 +  let
   11.60 +    val fpT as Type (fpT_name, As) = @{typ "'a + 'b"};
   11.61 +    val fpBT = @{typ "'c + 'd"};
   11.62 +    val C = @{typ 'e};
   11.63 +    val X = @{typ 'sum};
   11.64 +    val ctr_Tss = map single As;
   11.65 +
   11.66 +    val fp_bnf = the (bnf_of ctxt fpT_name);
   11.67 +    val xtor_map = @{thm xtor_map[of "map_sum f1 f2" for f1 f2]};
   11.68 +    val xtor_sets = @{thms xtor_set[of setl] xtor_set[of setr]};
   11.69 +    val xtor_rel = @{thm xtor_rel[of "rel_sum R1 R2" for R1 R2]};
   11.70 +    val ctor_rec_o_map = @{thm ctor_rec_o_map[of _ "map_sum g1 g2" for g1 g2]};
   11.71 +    val xtor_rel_induct = @{thm xtor_rel_induct[of "rel_sum R1 R2" for R1 R2]};
   11.72 +  in
   11.73 +    {T = fpT,
   11.74 +     BT = fpBT,
   11.75 +     X = X,
   11.76 +     fp = Least_FP,
   11.77 +     fp_res_index = 0,
   11.78 +     fp_res =
   11.79 +       trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct,
   11.80 +     pre_bnf = ID_bnf (*wrong*),
   11.81 +     absT_info = trivial_absT_info_of fpT,
   11.82 +     fp_nesting_bnfs = [],
   11.83 +     live_nesting_bnfs = [],
   11.84 +     ctrXs_Tss = ctr_Tss,
   11.85 +     ctr_defs = @{thms Inl_def_alt Inr_def_alt},
   11.86 +     ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
   11.87 +     co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
   11.88 +     co_rec_def = @{thm case_sum_def},
   11.89 +     maps = @{thms map_sum.simps},
   11.90 +     common_co_inducts = [@{thm sum.induct}],
   11.91 +     co_inducts = [@{thm sum.induct}],
   11.92 +     co_rec_thms = @{thms sum.case},
   11.93 +     co_rec_discs = [],
   11.94 +     co_rec_selss = [],
   11.95 +     rel_injects = @{thms rel_sum_simps(1,4)},
   11.96 +     rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}}
   11.97 +  end;
   11.98 +
   11.99 +fun fp_sugar_of_prod ctxt =
  11.100 +  let
  11.101 +    val fpT as Type (fpT_name, As) = @{typ "'a * 'b"};
  11.102 +    val fpBT = @{typ "'c * 'd"};
  11.103 +    val C = @{typ 'e};
  11.104 +    val X = @{typ 'prod};
  11.105 +    val ctr_Ts = As;
  11.106 +
  11.107 +    val fp_bnf = the (bnf_of ctxt fpT_name);
  11.108 +    val xtor_map = @{thm xtor_map[of "map_prod f1 f2" for f1 f2]};
  11.109 +    val xtor_sets = @{thms xtor_set[of fsts] xtor_set[of snds]};
  11.110 +    val xtor_rel = @{thm xtor_rel[of "rel_prod R1 R2" for R1 R2]};
  11.111 +    val ctor_rec_o_map = @{thm ctor_rec_o_map[of _ "map_prod g1 g2" for g1 g2]};
  11.112 +    val xtor_rel_induct = @{thm xtor_rel_induct[of "rel_prod R1 R2" for R1 R2]};
  11.113 +  in
  11.114 +    {T = fpT,
  11.115 +     BT = fpBT,
  11.116 +     X = X,
  11.117 +     fp = Least_FP,
  11.118 +     fp_res_index = 0,
  11.119 +     fp_res =
  11.120 +       trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct,
  11.121 +     pre_bnf = ID_bnf (*wrong*),
  11.122 +     absT_info = trivial_absT_info_of fpT,
  11.123 +     fp_nesting_bnfs = [],
  11.124 +     live_nesting_bnfs = [],
  11.125 +     ctrXs_Tss = [ctr_Ts],
  11.126 +     ctr_defs = [@{thm Pair_def_alt}],
  11.127 +     ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
  11.128 +     co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
  11.129 +     co_rec_def = @{thm case_prod_def},
  11.130 +     maps = [@{thm map_prod_simp}],
  11.131 +     common_co_inducts = [@{thm prod.induct}],
  11.132 +     co_inducts = [@{thm prod.induct}],
  11.133 +     co_rec_thms = [@{thm prod.case}],
  11.134 +     co_rec_discs = [],
  11.135 +     co_rec_selss = [],
  11.136 +     rel_injects = [@{thm rel_prod_apply}],
  11.137 +     rel_distincts = []}
  11.138 +  end;
  11.139 +
  11.140 +val _ = Theory.setup (map_local_theory (fn lthy =>
  11.141 +  fold (BNF_FP_Def_Sugar.register_fp_sugars (fn s => s <> size_plugin) o single o (fn f => f lthy))
  11.142 +    [fp_sugar_of_sum, fp_sugar_of_prod] lthy));
  11.143 +
  11.144 +end;
    12.1 --- a/src/HOL/Tools/BNF/bnf_tactics.ML	Tue Sep 16 19:23:37 2014 +0200
    12.2 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Tue Sep 16 19:23:37 2014 +0200
    12.3 @@ -12,6 +12,7 @@
    12.4  
    12.5    val fo_rtac: thm -> Proof.context -> int -> tactic
    12.6    val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic
    12.7 +  val subst_asm_tac: Proof.context -> int list option -> thm list -> int -> tactic
    12.8  
    12.9    val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
   12.10      int -> tactic
   12.11 @@ -44,14 +45,20 @@
   12.12  
   12.13  (*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*)
   12.14  fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
   12.15 +fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt o the_default [0];
   12.16 +
   12.17  
   12.18  (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
   12.19  fun mk_pointfree ctxt thm = thm
   12.20 -  |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
   12.21 +  |> Drule.zero_var_indexes
   12.22 +  |> Thm.prop_of
   12.23 +  |> Logic.unvarify_global
   12.24 +  |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
   12.25    |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
   12.26    |> mk_Trueprop_eq
   12.27    |> (fn goal => Goal.prove_sorry ctxt [] [] goal
   12.28 -    (K (rtac @{thm ext} 1 THEN unfold_thms_tac ctxt [o_apply, mk_sym thm] THEN rtac refl 1)))
   12.29 +    (K (rtac ext 1 THEN rtac @{thm comp_apply_eq} 1 THEN rtac thm 1)))
   12.30 +  |> Drule.export_without_context
   12.31    |> Thm.close_derivation;
   12.32  
   12.33