equal
deleted
inserted
replaced
13 by (auto elim: widen.cases) |
13 by (auto elim: widen.cases) |
14 |
14 |
15 |
15 |
16 lemma sup_loc_some [rule_format]: |
16 lemma sup_loc_some [rule_format]: |
17 "\<forall>y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = OK t \<longrightarrow> |
17 "\<forall>y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = OK t \<longrightarrow> |
18 (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b") |
18 (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" |
19 proof (induct ?P b) |
19 proof (induct b) |
20 show "?P []" by simp |
20 case Nil |
|
21 show ?case by simp |
21 next |
22 next |
22 case (Cons a list) |
23 case (Cons a list) |
23 show "?P (a#list)" |
24 show ?case |
24 proof (clarsimp simp add: list_all2_Cons1 sup_loc_def Listn.le_def lesub_def) |
25 proof (clarsimp simp add: list_all2_Cons1 sup_loc_def Listn.le_def lesub_def) |
25 fix z zs n |
26 fix z zs n |
26 assume *: |
27 assume *: |
27 "G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs" |
28 "G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs" |
28 "n < Suc (length list)" "(z # zs) ! n = OK t" |
29 "n < Suc (length list)" "(z # zs) ! n = OK t" |
58 qed |
59 qed |
59 qed |
60 qed |
60 |
61 |
61 |
62 |
62 lemma append_length_n [rule_format]: |
63 lemma append_length_n [rule_format]: |
63 "\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x") |
64 "\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" |
64 proof (induct ?P x) |
65 proof (induct x) |
65 show "?P []" by simp |
66 case Nil |
|
67 show ?case by simp |
66 next |
68 next |
67 fix l ls assume Cons: "?P ls" |
69 case (Cons l ls) |
68 |
70 |
69 show "?P (l#ls)" |
71 show ?case |
70 proof (intro allI impI) |
72 proof (intro allI impI) |
71 fix n |
73 fix n |
72 assume l: "n \<le> length (l # ls)" |
74 assume l: "n \<le> length (l # ls)" |
73 |
75 |
74 show "\<exists>a b. l # ls = a @ b \<and> length a = n" |
76 show "\<exists>a b. l # ls = a @ b \<and> length a = n" |