summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Nested_Environment.thy

changeset 23394 | 474ff28210c0 |

parent 20503 | 503ac4c5ef91 |

child 24433 | 4a405457e9d6 |

1.1 --- a/src/HOL/Library/Nested_Environment.thy Thu Jun 14 23:04:36 2007 +0200 1.2 +++ b/src/HOL/Library/Nested_Environment.thy Thu Jun 14 23:04:39 2007 +0200 1.3 @@ -103,7 +103,7 @@ 1.4 theorem lookup_append_none: 1.5 assumes "lookup env xs = None" 1.6 shows "lookup env (xs @ ys) = None" 1.7 - using prems 1.8 + using assms 1.9 proof (induct xs arbitrary: env) 1.10 case Nil 1.11 then have False by simp 1.12 @@ -140,7 +140,7 @@ 1.13 theorem lookup_append_some: 1.14 assumes "lookup env xs = Some e" 1.15 shows "lookup env (xs @ ys) = lookup e ys" 1.16 - using prems 1.17 + using assms 1.18 proof (induct xs arbitrary: env e) 1.19 case Nil 1.20 then have "env = e" by simp 1.21 @@ -190,7 +190,7 @@ 1.22 assumes "lookup env (xs @ ys) = Some e" 1.23 shows "\<exists>e. lookup env xs = Some e" 1.24 proof - 1.25 - from prems have "lookup env (xs @ ys) \<noteq> None" by simp 1.26 + from assms have "lookup env (xs @ ys) \<noteq> None" by simp 1.27 then have "lookup env xs \<noteq> None" 1.28 by (rule contrapos_nn) (simp only: lookup_append_none) 1.29 then show ?thesis by (simp) 1.30 @@ -208,7 +208,7 @@ 1.31 lookup env xs = Some (Env b' es') \<and> 1.32 es' y = Some env' \<and> 1.33 lookup env' ys = Some e" 1.34 - using prems 1.35 + using assms 1.36 proof (induct xs arbitrary: env e) 1.37 case Nil 1.38 from Nil.prems have "lookup env (y # ys) = Some e" 1.39 @@ -328,7 +328,7 @@ 1.40 theorem lookup_update_some: 1.41 assumes "lookup env xs = Some e" 1.42 shows "lookup (update xs (Some env') env) xs = Some env'" 1.43 - using prems 1.44 + using assms 1.45 proof (induct xs arbitrary: env e) 1.46 case Nil 1.47 then have "env = e" by simp 1.48 @@ -377,7 +377,7 @@ 1.49 theorem update_append_none: 1.50 assumes "lookup env xs = None" 1.51 shows "update (xs @ y # ys) opt env = env" 1.52 - using prems 1.53 + using assms 1.54 proof (induct xs arbitrary: env) 1.55 case Nil 1.56 then have False by simp 1.57 @@ -420,7 +420,7 @@ 1.58 theorem update_append_some: 1.59 assumes "lookup env xs = Some e" 1.60 shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)" 1.61 - using prems 1.62 + using assms 1.63 proof (induct xs arbitrary: env e) 1.64 case Nil 1.65 then have "env = e" by simp