# HG changeset patch
# User Andreas Lochbihler
# Date 1458302060 -3600
# Node ID d3a5b127eb81a955078f781729f5c87b10dca80f
# Parent  66568c9b82163a711c28d48c625ba240ae26e66c# Parent  7248d106c6078e39f4ad9f4982c8c601f9562e35
merged

diff -r 7248d106c607 -r d3a5b127eb81 src/HOL/Data_Structures/Tree2.thy
--- a/src/HOL/Data_Structures/Tree2.thy	Fri Mar 18 08:01:49 2016 +0100
+++ b/src/HOL/Data_Structures/Tree2.thy	Fri Mar 18 12:54:20 2016 +0100
@@ -14,4 +14,15 @@
 "height Leaf = 0" |
 "height (Node _ l a r) = max (height l) (height r) + 1"
 
+definition size1 :: "('a,'b) tree \<Rightarrow> nat" where
+"size1 t = size t + 1"
+
+lemma size1_simps[simp]:
+  "size1 \<langle>\<rangle> = 1"
+  "size1 \<langle>u, l, x, r\<rangle> = size1 l + size1 r"
+by (simp_all add: size1_def)
+
+lemma size1_ge0[simp]: "0 < size1 t"
+by (simp add: size1_def)
+
 end
diff -r 7248d106c607 -r d3a5b127eb81 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Mar 18 08:01:49 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Mar 18 12:54:20 2016 +0100
@@ -2062,7 +2062,7 @@
 done
 
 lemma one_step_implies_mult:
-  "trans r \<Longrightarrow> J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
+  "J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
     \<Longrightarrow> (I + K, I + J) \<in> mult r"
 using one_step_implies_mult_aux by blast
 
diff -r 7248d106c607 -r d3a5b127eb81 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Fri Mar 18 08:01:49 2016 +0100
+++ b/src/HOL/Library/Tree.thy	Fri Mar 18 12:54:20 2016 +0100
@@ -24,6 +24,9 @@
   "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
 by (simp_all add: size1_def)
 
+lemma size1_ge0[simp]: "0 < size1 t"
+by (simp add: size1_def)
+
 lemma size_0_iff_Leaf: "size t = 0 \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
diff -r 7248d106c607 -r d3a5b127eb81 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Mar 18 08:01:49 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Mar 18 12:54:20 2016 +0100
@@ -165,7 +165,7 @@
 
     val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
     val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct)
-      |> map (unfold_thms lthy (id_apply :: rel_unfolds));
+      |> map (zero_var_indexes o unfold_thms lthy (id_apply :: rel_unfolds));
 
     val rel_defs = map rel_def_of_bnf bnfs;
     val rel_monos = map rel_mono_of_bnf bnfs;
diff -r 7248d106c607 -r d3a5b127eb81 src/HOL/ZF/LProd.thy
--- a/src/HOL/ZF/LProd.thy	Fri Mar 18 08:01:49 2016 +0100
+++ b/src/HOL/ZF/LProd.thy	Fri Mar 18 12:54:20 2016 +0100
@@ -59,7 +59,7 @@
   proof (cases "a = b")
     case True    
     have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R"
-      apply (rule one_step_implies_mult[OF transR])
+      apply (rule one_step_implies_mult)
       apply (auto simp add: decomposed)
       done
     then show ?thesis
@@ -71,7 +71,7 @@
     case False
     from False lprod_list have False: "(a, b) \<in> R" by blast
     have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R"
-      apply (rule one_step_implies_mult[OF transR])
+      apply (rule one_step_implies_mult)
       apply (auto simp add: False decomposed)
       done
     then show ?thesis