src/HOL/Library/RBT_Set.thy
changeset 63649 e690d6f2185b
parent 63194 0b7bdb75f451
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Wed Aug 10 09:33:54 2016 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Wed Aug 10 14:50:59 2016 +0200
     1.3 @@ -273,12 +273,14 @@
     1.4    assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
     1.5    assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
     1.6    shows "P t"
     1.7 -using assms
     1.8 -  apply (induction t)
     1.9 -  apply simp
    1.10 -  apply (case_tac "t1 = rbt.Empty")
    1.11 -  apply simp_all
    1.12 -done
    1.13 +  using assms
    1.14 +proof (induct t)
    1.15 +  case Empty
    1.16 +  then show ?case by simp
    1.17 +next
    1.18 +  case (Branch x1 t1 x3 x4 t2)
    1.19 +  then show ?case by (cases "t1 = rbt.Empty") simp_all
    1.20 +qed
    1.21  
    1.22  lemma rbt_min_opt_in_set: 
    1.23    fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
    1.24 @@ -372,12 +374,14 @@
    1.25    assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
    1.26    assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
    1.27    shows "P t"
    1.28 -using assms
    1.29 -  apply (induction t)
    1.30 -  apply simp
    1.31 -  apply (case_tac "t2 = rbt.Empty")
    1.32 -  apply simp_all
    1.33 -done
    1.34 +  using assms
    1.35 +proof (induct t)
    1.36 +  case Empty
    1.37 +  then show ?case by simp
    1.38 +next
    1.39 +  case (Branch x1 t1 x3 x4 t2)
    1.40 +  then show ?case by (cases "t2 = rbt.Empty") simp_all
    1.41 +qed
    1.42  
    1.43  lemma rbt_max_opt_in_set: 
    1.44    fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
    1.45 @@ -468,27 +472,26 @@
    1.46  using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
    1.47  
    1.48  lemma fold_keys_min_top_eq:
    1.49 -  fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
    1.50 +  fixes t :: "('a::{linorder,bounded_lattice_top}, unit) rbt"
    1.51    assumes "\<not> (RBT.is_empty t)"
    1.52    shows "fold_keys min t top = fold1_keys min t"
    1.53  proof -
    1.54    have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
    1.55 -    List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
    1.56 +      List.fold min (hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t)) top"
    1.57      by (simp add: hd_Cons_tl[symmetric])
    1.58 -  { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
    1.59 -    have "List.fold min (x#xs) top = List.fold min xs x"
    1.60 +  have **: "List.fold min (x # xs) top = List.fold min xs x" for x :: 'a and xs
    1.61      by (simp add: inf_min[symmetric])
    1.62 -  } note ** = this
    1.63 -  show ?thesis using assms
    1.64 +  show ?thesis
    1.65 +    using assms
    1.66      unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
    1.67      apply transfer 
    1.68      apply (case_tac t) 
    1.69 -    apply simp 
    1.70 +     apply simp 
    1.71      apply (subst *)
    1.72 -    apply simp
    1.73 +     apply simp
    1.74      apply (subst **)
    1.75      apply simp
    1.76 -  done
    1.77 +    done
    1.78  qed
    1.79  
    1.80  (* maximum *)
    1.81 @@ -506,27 +509,26 @@
    1.82  using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
    1.83  
    1.84  lemma fold_keys_max_bot_eq:
    1.85 -  fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
    1.86 +  fixes t :: "('a::{linorder,bounded_lattice_bot}, unit) rbt"
    1.87    assumes "\<not> (RBT.is_empty t)"
    1.88    shows "fold_keys max t bot = fold1_keys max t"
    1.89  proof -
    1.90    have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
    1.91 -    List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
    1.92 +      List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
    1.93      by (simp add: hd_Cons_tl[symmetric])
    1.94 -  { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
    1.95 -    have "List.fold max (x#xs) bot = List.fold max xs x"
    1.96 +  have **: "List.fold max (x # xs) bot = List.fold max xs x" for x :: 'a and xs
    1.97      by (simp add: sup_max[symmetric])
    1.98 -  } note ** = this
    1.99 -  show ?thesis using assms
   1.100 +  show ?thesis
   1.101 +    using assms
   1.102      unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   1.103      apply transfer 
   1.104      apply (case_tac t) 
   1.105 -    apply simp 
   1.106 +     apply simp 
   1.107      apply (subst *)
   1.108 -    apply simp
   1.109 +     apply simp
   1.110      apply (subst **)
   1.111      apply simp
   1.112 -  done
   1.113 +    done
   1.114  qed
   1.115  
   1.116  end