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
```