src/HOL/Library/AssocList.thy
changeset 32960 69916a850301
parent 30663 0b6aff7451b2
child 34975 f099b0b20646
     1.1 --- a/src/HOL/Library/AssocList.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Library/AssocList.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -233,9 +233,9 @@
     1.4        fix v
     1.5        assume "v \<in> ran (map_of (a#al))"
     1.6        then obtain x where "map_of (a#al) x = Some v"
     1.7 -	by (auto simp add: ran_def)
     1.8 +        by (auto simp add: ran_def)
     1.9        then show "v \<in> {snd a} \<union> ran (map_of al)"
    1.10 -	by (auto split: split_if_asm simp add: ran_def)
    1.11 +        by (auto split: split_if_asm simp add: ran_def)
    1.12      qed
    1.13    next
    1.14      show "{snd a} \<union> ran (map_of al) \<subseteq> ran (map_of (a # al))"
    1.15 @@ -244,22 +244,22 @@
    1.16        assume v_in: "v \<in> {snd a} \<union> ran (map_of al)"
    1.17        show "v \<in> ran (map_of (a#al))"
    1.18        proof (cases "v=snd a")
    1.19 -	case True
    1.20 -	with v_in show ?thesis
    1.21 -	  by (auto simp add: ran_def)
    1.22 +        case True
    1.23 +        with v_in show ?thesis
    1.24 +          by (auto simp add: ran_def)
    1.25        next
    1.26 -	case False
    1.27 -	with v_in have "v \<in> ran (map_of al)" by auto
    1.28 -	then obtain x where al_x: "map_of al x = Some v"
    1.29 -	  by (auto simp add: ran_def)
    1.30 -	from map_of_SomeD [OF this]
    1.31 -	have "x \<in> fst ` set al"
    1.32 -	  by (force simp add: image_def)
    1.33 -	with Cons.prems have "x\<noteq>fst a"
    1.34 -	  by - (rule ccontr,simp)
    1.35 -	with al_x
    1.36 -	show ?thesis
    1.37 -	  by (auto simp add: ran_def)
    1.38 +        case False
    1.39 +        with v_in have "v \<in> ran (map_of al)" by auto
    1.40 +        then obtain x where al_x: "map_of al x = Some v"
    1.41 +          by (auto simp add: ran_def)
    1.42 +        from map_of_SomeD [OF this]
    1.43 +        have "x \<in> fst ` set al"
    1.44 +          by (force simp add: image_def)
    1.45 +        with Cons.prems have "x\<noteq>fst a"
    1.46 +          by - (rule ccontr,simp)
    1.47 +        with al_x
    1.48 +        show ?thesis
    1.49 +          by (auto simp add: ran_def)
    1.50        qed
    1.51      qed
    1.52    qed
    1.53 @@ -537,17 +537,17 @@
    1.54        case True
    1.55        from True delete_notin_dom [of k xs]
    1.56        have "map_of (delete (fst x) xs) k = None"
    1.57 -	by (simp add: map_of_eq_None_iff)
    1.58 +        by (simp add: map_of_eq_None_iff)
    1.59        with hyp show ?thesis
    1.60 -	using True None
    1.61 -	by simp
    1.62 +        using True None
    1.63 +        by simp
    1.64      next
    1.65        case False
    1.66        from False have "map_of (delete (fst x) xs) k = map_of xs k"
    1.67 -	by simp
    1.68 +        by simp
    1.69        with hyp show ?thesis
    1.70 -	using False None
    1.71 -	by (simp add: map_comp_def)
    1.72 +        using False None
    1.73 +        by (simp add: map_comp_def)
    1.74      qed
    1.75    next
    1.76      case (Some v)
    1.77 @@ -631,12 +631,12 @@
    1.78        case True
    1.79        with None hyp
    1.80        show ?thesis
    1.81 -	by (simp add: delete_idem)
    1.82 +        by (simp add: delete_idem)
    1.83      next
    1.84        case False
    1.85        from None False hyp
    1.86        show ?thesis
    1.87 -	by (simp add: delete_twist)
    1.88 +        by (simp add: delete_twist)
    1.89      qed
    1.90    next
    1.91      case (Some v)
    1.92 @@ -736,30 +736,30 @@
    1.93        case True
    1.94        from Cons.hyps
    1.95        show ?thesis
    1.96 -	using x_D True
    1.97 -	by simp
    1.98 +        using x_D True
    1.99 +        by simp
   1.100      next
   1.101        case False
   1.102        note not_fst_a_x = this
   1.103        show ?thesis
   1.104        proof (cases "fst a \<in> D")
   1.105 -	case True 
   1.106 -	with not_fst_a_x 
   1.107 -	have "delete x (restrict D (a#al)) = a#(delete x (restrict D al))"
   1.108 -	  by (cases a) (simp add: restrict_eq)
   1.109 -	also from not_fst_a_x True hyp have "\<dots> = restrict (D - {x}) (a # al)"
   1.110 -	  by (cases a) (simp add: restrict_eq)
   1.111 -	finally show ?thesis
   1.112 -	  using x_D by simp
   1.113 +        case True 
   1.114 +        with not_fst_a_x 
   1.115 +        have "delete x (restrict D (a#al)) = a#(delete x (restrict D al))"
   1.116 +          by (cases a) (simp add: restrict_eq)
   1.117 +        also from not_fst_a_x True hyp have "\<dots> = restrict (D - {x}) (a # al)"
   1.118 +          by (cases a) (simp add: restrict_eq)
   1.119 +        finally show ?thesis
   1.120 +          using x_D by simp
   1.121        next
   1.122 -	case False
   1.123 -	hence "delete x (restrict D (a#al)) = delete x (restrict D al)"
   1.124 -	  by (cases a) (simp add: restrict_eq)
   1.125 -	moreover from False not_fst_a_x
   1.126 -	have "restrict (D - {x}) (a # al) = restrict (D - {x}) al"
   1.127 -	  by (cases a) (simp add: restrict_eq)
   1.128 -	ultimately
   1.129 -	show ?thesis using x_D hyp by simp
   1.130 +        case False
   1.131 +        hence "delete x (restrict D (a#al)) = delete x (restrict D al)"
   1.132 +          by (cases a) (simp add: restrict_eq)
   1.133 +        moreover from False not_fst_a_x
   1.134 +        have "restrict (D - {x}) (a # al) = restrict (D - {x}) al"
   1.135 +          by (cases a) (simp add: restrict_eq)
   1.136 +        ultimately
   1.137 +        show ?thesis using x_D hyp by simp
   1.138        qed
   1.139      qed
   1.140    next