# HG changeset patch
# User blanchet
# Date 1409697097 -7200
# Node ID e3d1912a0c8f932e3815c9b1a98647885b3c5ef2
# Parent  d2cb7cbb3aaaca8078d0d73f0ecc808baf148ca7
tuning

diff -r d2cb7cbb3aaa -r e3d1912a0c8f src/HOL/BNF_Fixpoint_Base.thy
--- 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
diff -r d2cb7cbb3aaa -r e3d1912a0c8f src/HOL/BNF_Least_Fixpoint.thy
--- 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);
diff -r d2cb7cbb3aaa -r e3d1912a0c8f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- 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;
diff -r d2cb7cbb3aaa -r e3d1912a0c8f src/HOL/Tools/BNF/bnf_fp_util.ML
--- 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