src/HOL/Statespace/DistinctTreeProver.thy
changeset 32960 69916a850301
parent 32740 9dd0a2f83429
child 35408 b48ab741683b
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -132,15 +132,15 @@
     1.4        case (Some r')
     1.5        with Node.hyps
     1.6        have "set_of r' \<subseteq> set_of r"
     1.7 -	by simp
     1.8 +        by simp
     1.9        with l'_l Some x_l_Some del
    1.10        show ?thesis
    1.11 -	by (auto split: split_if_asm)
    1.12 +        by (auto split: split_if_asm)
    1.13      next
    1.14        case None
    1.15        with l'_l Some x_l_Some del
    1.16        show ?thesis
    1.17 -	by (fastsimp split: split_if_asm)
    1.18 +        by (fastsimp split: split_if_asm)
    1.19      qed
    1.20    next
    1.21      case None
    1.22 @@ -150,15 +150,15 @@
    1.23        case (Some r')
    1.24        with Node.hyps
    1.25        have "set_of r' \<subseteq> set_of r"
    1.26 -	by simp
    1.27 +        by simp
    1.28        with Some x_l_None del
    1.29        show ?thesis
    1.30 -	by (fastsimp split: split_if_asm)
    1.31 +        by (fastsimp split: split_if_asm)
    1.32      next
    1.33        case None
    1.34        with x_l_None del
    1.35        show ?thesis
    1.36 -	by (fastsimp split: split_if_asm)
    1.37 +        by (fastsimp split: split_if_asm)
    1.38      qed
    1.39    qed
    1.40  qed
    1.41 @@ -191,18 +191,18 @@
    1.42        case (Some r')
    1.43        from Node.hyps (2) [OF Some dist_r]
    1.44        have dist_r': "all_distinct r'"
    1.45 -	by simp
    1.46 +        by simp
    1.47        from delete_Some_set_of [OF Some]
    1.48        have "set_of r' \<subseteq> set_of r".
    1.49        
    1.50        with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r
    1.51        show ?thesis
    1.52 -	by fastsimp
    1.53 +        by fastsimp
    1.54      next
    1.55        case None
    1.56        with l'_l dist_l'  x_l_Some del d dist_l_r dist_r
    1.57        show ?thesis
    1.58 -	by fastsimp
    1.59 +        by fastsimp
    1.60      qed
    1.61    next
    1.62      case None
    1.63 @@ -212,17 +212,17 @@
    1.64        case (Some r')
    1.65        with Node.hyps (2) [OF Some dist_r]
    1.66        have dist_r': "all_distinct r'"
    1.67 -	by simp
    1.68 +        by simp
    1.69        from delete_Some_set_of [OF Some]
    1.70        have "set_of r' \<subseteq> set_of r".
    1.71        with Some dist_r' x_l_None del dist_l d dist_l_r
    1.72        show ?thesis
    1.73 -	by fastsimp
    1.74 +        by fastsimp
    1.75      next
    1.76        case None
    1.77        with x_l_None del dist_l dist_r d dist_l_r
    1.78        show ?thesis
    1.79 -	by (fastsimp split: split_if_asm)
    1.80 +        by (fastsimp split: split_if_asm)
    1.81      qed
    1.82    qed
    1.83  qed
    1.84 @@ -255,17 +255,17 @@
    1.85        case (Some r')
    1.86        from Node.hyps (2) [OF Some]
    1.87        obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"
    1.88 -	by simp
    1.89 +        by simp
    1.90        from x_r x_l Some x_l_Some del 
    1.91        show ?thesis
    1.92 -	by (clarsimp split: split_if_asm)
    1.93 +        by (clarsimp split: split_if_asm)
    1.94      next
    1.95        case None
    1.96        then have "x \<notin> set_of r"
    1.97 -	by (simp add: delete_None_set_of_conv)
    1.98 +        by (simp add: delete_None_set_of_conv)
    1.99        with x_l None x_l_Some del
   1.100        show ?thesis
   1.101 -	by (clarsimp split: split_if_asm)
   1.102 +        by (clarsimp split: split_if_asm)
   1.103      qed
   1.104    next
   1.105      case None
   1.106 @@ -277,17 +277,17 @@
   1.107        case (Some r')
   1.108        from Node.hyps (2) [OF Some]
   1.109        obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"
   1.110 -	by simp
   1.111 +        by simp
   1.112        from x_r x_notin_l Some x_l_None del 
   1.113        show ?thesis
   1.114 -	by (clarsimp split: split_if_asm)
   1.115 +        by (clarsimp split: split_if_asm)
   1.116      next
   1.117        case None
   1.118        then have "x \<notin> set_of r"
   1.119 -	by (simp add: delete_None_set_of_conv)
   1.120 +        by (simp add: delete_None_set_of_conv)
   1.121        with None x_l_None x_notin_l del
   1.122        show ?thesis
   1.123 -	by (clarsimp split: split_if_asm)
   1.124 +        by (clarsimp split: split_if_asm)
   1.125      qed
   1.126    qed
   1.127  qed
   1.128 @@ -324,23 +324,23 @@
   1.129        have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
   1.130        show ?thesis
   1.131        proof (cases "subtract r t\<^isub>2''")
   1.132 -	case (Some t\<^isub>2''')
   1.133 -	from Node.hyps (2) [OF Some ] 
   1.134 -	have "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''" .
   1.135 -	with Some sub_l_Some del_x_Some sub t2''_t2' t2'_t2
   1.136 -	show ?thesis
   1.137 -	  by simp
   1.138 +        case (Some t\<^isub>2''')
   1.139 +        from Node.hyps (2) [OF Some ] 
   1.140 +        have "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''" .
   1.141 +        with Some sub_l_Some del_x_Some sub t2''_t2' t2'_t2
   1.142 +        show ?thesis
   1.143 +          by simp
   1.144        next
   1.145 -	case None
   1.146 -	with del_x_Some sub_l_Some sub
   1.147 -	show ?thesis
   1.148 -	  by simp
   1.149 +        case None
   1.150 +        with del_x_Some sub_l_Some sub
   1.151 +        show ?thesis
   1.152 +          by simp
   1.153        qed
   1.154      next
   1.155        case None
   1.156        with del_x_Some sub 
   1.157        show ?thesis
   1.158 -	by simp
   1.159 +        by simp
   1.160      qed
   1.161    next
   1.162      case None
   1.163 @@ -374,23 +374,23 @@
   1.164        have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
   1.165        show ?thesis
   1.166        proof (cases "subtract r t\<^isub>2''")
   1.167 -	case (Some t\<^isub>2''')
   1.168 -	from Node.hyps (2) [OF Some ] 
   1.169 -	have r_t\<^isub>2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
   1.170 -	from Some sub_l_Some del_x_Some sub r_t\<^isub>2'' l_t2' t2'_t2 t2''_t2' x_t2
   1.171 -	show ?thesis
   1.172 -	  by auto
   1.173 +        case (Some t\<^isub>2''')
   1.174 +        from Node.hyps (2) [OF Some ] 
   1.175 +        have r_t\<^isub>2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
   1.176 +        from Some sub_l_Some del_x_Some sub r_t\<^isub>2'' l_t2' t2'_t2 t2''_t2' x_t2
   1.177 +        show ?thesis
   1.178 +          by auto
   1.179        next
   1.180 -	case None
   1.181 -	with del_x_Some sub_l_Some sub
   1.182 -	show ?thesis
   1.183 -	  by simp
   1.184 +        case None
   1.185 +        with del_x_Some sub_l_Some sub
   1.186 +        show ?thesis
   1.187 +          by simp
   1.188        qed
   1.189      next
   1.190        case None
   1.191        with del_x_Some sub 
   1.192        show ?thesis
   1.193 -	by simp
   1.194 +        by simp
   1.195      qed
   1.196    next
   1.197      case None
   1.198 @@ -420,24 +420,24 @@
   1.199        have dist_t2'': "all_distinct t\<^isub>2''" .
   1.200        show ?thesis
   1.201        proof (cases "subtract r t\<^isub>2''")
   1.202 -	case (Some t\<^isub>2''')
   1.203 -	from Node.hyps (2) [OF Some dist_t2''] 
   1.204 -	have dist_t2''': "all_distinct t\<^isub>2'''" .
   1.205 -	from Some sub_l_Some del_x_Some sub 
   1.206 +        case (Some t\<^isub>2''')
   1.207 +        from Node.hyps (2) [OF Some dist_t2''] 
   1.208 +        have dist_t2''': "all_distinct t\<^isub>2'''" .
   1.209 +        from Some sub_l_Some del_x_Some sub 
   1.210               dist_t2'''
   1.211 -	show ?thesis
   1.212 -	  by simp
   1.213 +        show ?thesis
   1.214 +          by simp
   1.215        next
   1.216 -	case None
   1.217 -	with del_x_Some sub_l_Some sub
   1.218 -	show ?thesis
   1.219 -	  by simp
   1.220 +        case None
   1.221 +        with del_x_Some sub_l_Some sub
   1.222 +        show ?thesis
   1.223 +          by simp
   1.224        qed
   1.225      next
   1.226        case None
   1.227        with del_x_Some sub 
   1.228        show ?thesis
   1.229 -	by simp
   1.230 +        by simp
   1.231      qed
   1.232    next
   1.233      case None
   1.234 @@ -472,34 +472,34 @@
   1.235        have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
   1.236        show ?thesis
   1.237        proof (cases "subtract r t\<^isub>2''")
   1.238 -	case (Some t\<^isub>2''')
   1.239 -	from Node.hyps (2) [OF Some] 
   1.240 -	have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}" .
   1.241 -	from subtract_Some_set_of_res [OF Some]
   1.242 -	have t2'''_t2'': "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''".
   1.243 -	
   1.244 -	from Some sub_l_Some del_x_Some sub t2'''_t2'' dist_l_t2'' dist_r_t2'''
   1.245 +        case (Some t\<^isub>2''')
   1.246 +        from Node.hyps (2) [OF Some] 
   1.247 +        have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}" .
   1.248 +        from subtract_Some_set_of_res [OF Some]
   1.249 +        have t2'''_t2'': "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''".
   1.250 +        
   1.251 +        from Some sub_l_Some del_x_Some sub t2'''_t2'' dist_l_t2'' dist_r_t2'''
   1.252               t2''_t2' t2'_t2 x_not_t2'
   1.253 -	show ?thesis
   1.254 -	  by auto
   1.255 +        show ?thesis
   1.256 +          by auto
   1.257        next
   1.258 -	case None
   1.259 -	with del_x_Some sub_l_Some sub
   1.260 -	show ?thesis
   1.261 -	  by simp
   1.262 +        case None
   1.263 +        with del_x_Some sub_l_Some sub
   1.264 +        show ?thesis
   1.265 +          by simp
   1.266        qed
   1.267      next
   1.268        case None
   1.269        with del_x_Some sub 
   1.270        show ?thesis
   1.271 -	by simp
   1.272 +        by simp
   1.273      qed
   1.274    next
   1.275      case None
   1.276      with sub show ?thesis by simp
   1.277    qed
   1.278  qed
   1.279 -	
   1.280 +        
   1.281  lemma subtract_Some_all_distinct:
   1.282    "\<And>t\<^isub>2 t. \<lbrakk>subtract t\<^isub>1 t\<^isub>2 = Some t; all_distinct t\<^isub>2\<rbrakk> \<Longrightarrow> all_distinct t\<^isub>1"
   1.283  proof (induct t\<^isub>1)
   1.284 @@ -536,29 +536,29 @@
   1.285        have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}".
   1.286        show ?thesis
   1.287        proof (cases "subtract r t\<^isub>2''")
   1.288 -	case (Some t\<^isub>2''')
   1.289 -	from Node.hyps (2) [OF Some dist_t2''] 
   1.290 -	have dist_r: "all_distinct r" .
   1.291 -	from subtract_Some_set_of [OF Some]
   1.292 -	have r_t2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
   1.293 -	from subtract_Some_dist_res [OF Some]
   1.294 -	have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}".
   1.295 +        case (Some t\<^isub>2''')
   1.296 +        from Node.hyps (2) [OF Some dist_t2''] 
   1.297 +        have dist_r: "all_distinct r" .
   1.298 +        from subtract_Some_set_of [OF Some]
   1.299 +        have r_t2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
   1.300 +        from subtract_Some_dist_res [OF Some]
   1.301 +        have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}".
   1.302  
   1.303 -	from dist_l dist_r Some sub_l_Some del_x_Some r_t2'' l_t2' x_t2 x_not_t2' 
   1.304 -	     t2''_t2' dist_l_t2'' dist_r_t2'''
   1.305 -	show ?thesis
   1.306 -	  by auto
   1.307 +        from dist_l dist_r Some sub_l_Some del_x_Some r_t2'' l_t2' x_t2 x_not_t2' 
   1.308 +             t2''_t2' dist_l_t2'' dist_r_t2'''
   1.309 +        show ?thesis
   1.310 +          by auto
   1.311        next
   1.312 -	case None
   1.313 -	with del_x_Some sub_l_Some sub
   1.314 -	show ?thesis
   1.315 -	  by simp
   1.316 +        case None
   1.317 +        with del_x_Some sub_l_Some sub
   1.318 +        show ?thesis
   1.319 +          by simp
   1.320        qed
   1.321      next
   1.322        case None
   1.323        with del_x_Some sub 
   1.324        show ?thesis
   1.325 -	by simp
   1.326 +        by simp
   1.327      qed
   1.328    next
   1.329      case None