--- a/src/HOL/BNF_Fixpoint_Base.thy Wed Sep 03 00:06:32 2014 +0200
+++ b/src/HOL/BNF_Fixpoint_Base.thy Wed Sep 03 00:31:37 2014 +0200
@@ -21,25 +21,25 @@
by default simp_all
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
-by auto
+ by auto
lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
by auto
lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
-by blast
+ by blast
lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
-by (cases u) (hypsubst, rule unit.case)
+ by (cases u) (hypsubst, rule unit.case)
lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
-by simp
+ by simp
lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
-by simp
+ by simp
lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
-unfolding comp_def fun_eq_iff by simp
+ unfolding comp_def fun_eq_iff by simp
lemma o_bij:
assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
@@ -55,15 +55,16 @@
thus "EX a. b = f a" by blast
qed
-lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
+lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X"
+ by simp
lemma case_sum_step:
-"case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p"
-"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
-by auto
+ "case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p"
+ "case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
+ by auto
lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
-by blast
+ by blast
lemma type_copy_obj_one_point_absE:
assumes "type_definition Rep Abs UNIV" "\<forall>x. s = Abs x \<longrightarrow> P" shows P
@@ -78,20 +79,20 @@
qed
lemma case_sum_if:
-"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
-by simp
+ "case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
+ by simp
lemma prod_set_simps:
-"fsts (x, y) = {x}"
-"snds (x, y) = {y}"
-unfolding fsts_def snds_def by simp+
+ "fsts (x, y) = {x}"
+ "snds (x, y) = {y}"
+ unfolding fsts_def snds_def by simp+
lemma sum_set_simps:
-"setl (Inl x) = {x}"
-"setl (Inr x) = {}"
-"setr (Inl x) = {}"
-"setr (Inr x) = {x}"
-unfolding sum_set_defs by simp+
+ "setl (Inl x) = {x}"
+ "setl (Inr x) = {}"
+ "setr (Inl x) = {}"
+ "setr (Inr x) = {x}"
+ unfolding sum_set_defs by simp+
lemma Inl_Inr_False: "(Inl x = Inr y) = False"
by simp
@@ -100,7 +101,7 @@
by simp
lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
-by blast
+ by blast
lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r"
unfolding comp_def fun_eq_iff by auto
--- a/src/HOL/BNF_Least_Fixpoint.thy Wed Sep 03 00:06:32 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Wed Sep 03 00:31:37 2014 +0200
@@ -66,13 +66,12 @@
lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
unfolding bij_betw_def by auto
-lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow>
- (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
+lemma f_the_inv_into_f_bij_betw:
+ "bij_betw f A B \<Longrightarrow> (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
lemma ex_bij_betw: "|A| \<le>o (r :: 'b rel) \<Longrightarrow> \<exists>f B :: 'b set. bij_betw f B A"
- by (subst (asm) internalize_card_of_ordLeq)
- (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
+ by (subst (asm) internalize_card_of_ordLeq) (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
lemma bij_betwI':
"\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Sep 03 00:06:32 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Sep 03 00:31:37 2014 +0200
@@ -264,14 +264,6 @@
fun mk_set Ts t =
subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
-fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
- | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts
- | unzip_recT _ T = [T];
-
-fun unzip_corecT (Type (@{type_name sum}, _)) T = [T]
- | unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts
- | unzip_corecT _ T = [T];
-
fun liveness_of_fp_bnf n bnf =
(case T_of_bnf bnf of
Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts
@@ -336,6 +328,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
+ | unzip_recT _ T = [T];
+
fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy =
let
val Css = map2 replicate ns Cs;
@@ -356,6 +352,10 @@
((f_Tss, x_Tssss, fss, xssss), lthy)
end;
+fun unzip_corecT (Type (@{type_name sum}, _)) T = [T]
+ | unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts
+ | unzip_corecT _ T = [T];
+
(*avoid "'a itself" arguments in corecursors*)
fun repair_nullary_single_ctr [[]] = [[HOLogic.unitT]]
| repair_nullary_single_ctr Tss = Tss;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Sep 03 00:06:32 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Sep 03 00:31:37 2014 +0200
@@ -160,6 +160,7 @@
val split_conj_prems: int -> thm -> thm
val mk_sumTN: typ list -> typ
+ val mk_sumTN_balanced: typ list -> typ
val mk_tupleT_balanced: typ list -> typ
val mk_sumprodT_balanced: typ list list -> typ
@@ -181,6 +182,8 @@
val mk_absumprod: typ -> term -> int -> int -> term list -> term
val dest_sumT: typ -> typ * typ
+ val dest_sumTN_balanced: int -> typ -> typ list
+ val dest_tupleT_balanced: int -> typ -> typ list
val dest_absumprodT: typ -> typ -> int -> int list -> typ -> typ list list
val If_const: typ -> term