16 else Suc (length (takeWhile (\<lambda> z. z~=v) (pn @ map fst lv)))" |
16 else Suc (length (takeWhile (\<lambda> z. z~=v) (pn @ map fst lv)))" |
17 |
17 |
18 |
18 |
19 lemma index_length_pns: " |
19 lemma index_length_pns: " |
20 \<lbrakk> i = index (pns,lvars,blk,res) vn; |
20 \<lbrakk> i = index (pns,lvars,blk,res) vn; |
21 wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res)); |
21 wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res)); |
22 vn \<in> set pns\<rbrakk> |
22 vn \<in> set pns\<rbrakk> |
23 \<Longrightarrow> 0 < i \<and> i < Suc (length pns)" |
23 \<Longrightarrow> 0 < i \<and> i < Suc (length pns)" |
24 apply (simp add: wf_java_mdecl_def index_def) |
24 apply (simp add: wf_java_mdecl_def index_def) |
25 apply (subgoal_tac "vn \<noteq> This") |
25 apply (subgoal_tac "vn \<noteq> This") |
26 apply (auto intro: length_takeWhile) |
26 apply (auto intro: length_takeWhile) |
27 done |
27 done |
28 |
28 |
29 lemma index_length_lvars: " |
29 lemma index_length_lvars: " |
30 \<lbrakk> i = index (pns,lvars,blk,res) vn; |
30 \<lbrakk> i = index (pns,lvars,blk,res) vn; |
31 wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res)); |
31 wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res)); |
32 vn \<in> set (map fst lvars)\<rbrakk> |
32 vn \<in> set (map fst lvars)\<rbrakk> |
33 \<Longrightarrow> (length pns) < i \<and> i < Suc((length pns) + (length lvars))" |
33 \<Longrightarrow> (length pns) < i \<and> i < Suc((length pns) + (length lvars))" |
34 apply (simp add: wf_java_mdecl_def index_def) |
34 apply (simp add: wf_java_mdecl_def index_def) |
35 apply (subgoal_tac "vn \<noteq> This") |
35 apply (subgoal_tac "vn \<noteq> This") |
36 apply simp |
36 apply simp |
37 apply (subgoal_tac "\<forall> x \<in> set pns. (\<lambda>z. z \<noteq> vn) x") |
37 apply (subgoal_tac "\<forall> x \<in> set pns. (\<lambda>z. z \<noteq> vn) x") |
38 apply simp |
38 apply simp |
39 apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars)) < length (map fst lvars)") |
39 apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars)) < length (map fst lvars)") |
40 apply simp |
40 apply simp |
41 apply (rule length_takeWhile) |
41 apply (rule length_takeWhile) |
42 apply simp |
42 apply simp |
43 apply (simp add: map_of_in_set) |
43 apply (simp add: map_of_in_set) |
44 apply (intro strip notI) apply simp apply blast |
44 apply (intro strip notI) |
45 done |
45 apply simp |
|
46 apply blast |
|
47 done |
46 |
48 |
47 |
49 |
48 (*** index ***) |
50 (*** index ***) |
49 |
51 |
50 lemma select_at_index : |
52 lemma select_at_index : |
51 "x \<in> set (gjmb_plns (gmb G C S)) \<or> x = This |
53 "x \<in> set (gjmb_plns (gmb G C S)) \<or> x = This |
52 \<Longrightarrow> (the (loc This) # glvs (gmb G C S) loc) ! (index (gmb G C S) x) = |
54 \<Longrightarrow> (the (loc This) # glvs (gmb G C S) loc) ! (index (gmb G C S) x) = the (loc x)" |
53 the (loc x)" |
55 apply (simp only: index_def gjmb_plns_def) |
54 apply (simp only: index_def gjmb_plns_def) |
56 apply (case_tac "gmb G C S" rule: prod.exhaust) |
55 apply (case_tac "gmb G C S" rule: prod.exhaust) |
57 apply (simp add: galldefs del: set_append map_append) |
56 apply (simp add: galldefs del: set_append map_append) |
58 apply (rename_tac a b) |
57 apply (rename_tac a b) |
59 apply (case_tac b, simp add: gmb_def gjmb_lvs_def del: set_append map_append) |
58 apply (case_tac b, simp add: gmb_def gjmb_lvs_def del: set_append map_append) |
60 apply (intro strip) |
59 apply (intro strip) |
61 apply (simp del: set_append map_append) |
60 apply (simp del: set_append map_append) |
62 apply (frule length_takeWhile) |
61 apply (frule length_takeWhile) |
63 apply (frule_tac f = "(the \<circ> loc)" in nth_map) |
62 apply (frule_tac f = "(the \<circ> loc)" in nth_map) |
64 apply simp |
63 apply simp |
65 done |
64 done |
|
65 |
66 |
66 lemma lift_if: "(f (if b then t else e)) = (if b then (f t) else (f e))" |
67 lemma lift_if: "(f (if b then t else e)) = (if b then (f t) else (f e))" |
67 apply auto |
68 by auto |
68 done |
|
69 |
69 |
70 lemma update_at_index: " |
70 lemma update_at_index: " |
71 \<lbrakk> distinct (gjmb_plns (gmb G C S)); |
71 \<lbrakk> distinct (gjmb_plns (gmb G C S)); |
72 x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow> |
72 x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow> |
73 locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] = |
73 locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] = |
74 locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))" |
74 locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))" |
75 apply (simp only: locvars_xstate_def locvars_locals_def index_def) |
75 apply (simp only: locvars_xstate_def locvars_locals_def index_def) |
76 apply (case_tac "gmb G C S" rule: prod.exhaust, simp) |
76 apply (case_tac "gmb G C S" rule: prod.exhaust, simp) |
77 apply (rename_tac a b) |
77 apply (rename_tac a b) |
78 apply (case_tac b, simp) |
78 apply (case_tac b, simp) |
79 apply (rule conjI) |
79 apply (rule conjI) |
80 apply (simp add: gl_def) |
80 apply (simp add: gl_def) |
81 apply (simp add: galldefs del: set_append map_append) |
81 apply (simp add: galldefs del: set_append map_append) |
82 done |
82 done |
83 |
83 |
84 |
84 |
85 (* !!!! incomprehensible: why can't List.takeWhile_append2 be applied the same |
85 (* !!!! incomprehensible: why can't List.takeWhile_append2 be applied the same |
86 way in the second case as in the first case ? *) |
86 way in the second case as in the first case ? *) |
87 lemma index_of_var: "\<lbrakk> xvar \<notin> set pns; xvar \<notin> set (map fst zs); xvar \<noteq> This \<rbrakk> |
87 lemma index_of_var: "\<lbrakk> xvar \<notin> set pns; xvar \<notin> set (map fst zs); xvar \<noteq> This \<rbrakk> |
88 \<Longrightarrow> index (pns, zs @ ((xvar, xval) # xys), blk, res) xvar = Suc (length pns + length zs)" |
88 \<Longrightarrow> index (pns, zs @ ((xvar, xval) # xys), blk, res) xvar = Suc (length pns + length zs)" |
89 apply (simp add: index_def) |
89 apply (simp add: index_def) |
90 apply (subgoal_tac "(\<And>x. ((x \<in> (set pns)) \<Longrightarrow> ((\<lambda>z. (z \<noteq> xvar))x)))") |
90 apply (subgoal_tac "(\<And>x. ((x \<in> (set pns)) \<Longrightarrow> ((\<lambda>z. (z \<noteq> xvar))x)))") |
91 apply simp |
91 apply simp |
92 apply (subgoal_tac "(takeWhile (\<lambda>z. z \<noteq> xvar) (map fst zs @ xvar # map fst xys)) = map fst zs @ (takeWhile (\<lambda>z. z \<noteq> xvar) (xvar # map fst xys))") |
92 apply (subgoal_tac "(takeWhile (\<lambda>z. z \<noteq> xvar) (map fst zs @ xvar # map fst xys)) = map fst zs @ (takeWhile (\<lambda>z. z \<noteq> xvar) (xvar # map fst xys))") |
93 apply simp |
93 apply simp |
94 apply (rule List.takeWhile_append2) |
94 apply (rule List.takeWhile_append2) |
95 apply auto |
95 apply auto |
96 done |
96 done |
97 |
97 |
98 |
98 |
99 |
99 |
100 |
100 |
101 (* The following def should replace the conditions in WellType.thy / wf_java_mdecl |
101 (* The following def should replace the conditions in WellType.thy / wf_java_mdecl |
102 *) |
102 *) |
103 definition disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool" where |
103 definition disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool" where |
104 (* This corresponds to the original def in wf_java_mdecl: |
|
105 "disjoint_varnames pns lvars \<equiv> |
|
106 nodups pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> |
|
107 (\<forall>pn\<in>set pns. map_of lvars pn = None)" |
|
108 *) |
|
109 |
|
110 "disjoint_varnames pns lvars \<equiv> |
104 "disjoint_varnames pns lvars \<equiv> |
111 distinct pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> |
105 distinct pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> |
112 (\<forall>pn\<in>set pns. pn \<notin> set (map fst lvars))" |
106 (\<forall>pn\<in>set pns. pn \<notin> set (map fst lvars))" |
113 |
107 |
114 |
108 |
115 lemma index_of_var2: " |
109 lemma index_of_var2: " |
116 disjoint_varnames pns (lvars_pre @ (vn, ty) # lvars_post) |
110 disjoint_varnames pns (lvars_pre @ (vn, ty) # lvars_post) |
117 \<Longrightarrow> index (pns, lvars_pre @ (vn, ty) # lvars_post, blk, res) vn = |
111 \<Longrightarrow> index (pns, lvars_pre @ (vn, ty) # lvars_post, blk, res) vn = |
118 Suc (length pns + length lvars_pre)" |
112 Suc (length pns + length lvars_pre)" |
119 apply (simp add: disjoint_varnames_def index_def unique_def) |
113 apply (simp add: disjoint_varnames_def index_def unique_def) |
120 apply (subgoal_tac "vn \<noteq> This", simp) |
114 apply (subgoal_tac "vn \<noteq> This", simp) |
121 apply (subgoal_tac |
115 apply (subgoal_tac |
122 "takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars_pre @ vn # map fst lvars_post) = |
116 "takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars_pre @ vn # map fst lvars_post) = |
123 map fst lvars_pre @ takeWhile (\<lambda>z. z \<noteq> vn) (vn # map fst lvars_post)") |
117 map fst lvars_pre @ takeWhile (\<lambda>z. z \<noteq> vn) (vn # map fst lvars_post)") |
124 apply simp |
118 apply simp |
125 apply (rule List.takeWhile_append2) |
119 apply (rule List.takeWhile_append2) |
126 apply auto |
120 apply auto |
127 done |
121 done |
128 |
122 |
129 lemma wf_java_mdecl_disjoint_varnames: |
123 lemma wf_java_mdecl_disjoint_varnames: |
130 "wf_java_mdecl G C (S,rT,(pns,lvars,blk,res)) |
124 "wf_java_mdecl G C (S,rT,(pns,lvars,blk,res)) |
131 \<Longrightarrow> disjoint_varnames pns lvars" |
125 \<Longrightarrow> disjoint_varnames pns lvars" |
132 apply (cases S) |
126 apply (cases S) |
133 apply (simp add: wf_java_mdecl_def disjoint_varnames_def map_of_in_set) |
127 apply (simp add: wf_java_mdecl_def disjoint_varnames_def map_of_in_set) |
134 done |
128 done |
135 |
129 |
136 lemma wf_java_mdecl_length_pTs_pns: |
130 lemma wf_java_mdecl_length_pTs_pns: |
137 "wf_java_mdecl G C ((mn, pTs), rT, pns, lvars, blk, res) |
131 "wf_java_mdecl G C ((mn, pTs), rT, pns, lvars, blk, res) |
138 \<Longrightarrow> length pTs = length pns" |
132 \<Longrightarrow> length pTs = length pns" |
139 by (simp add: wf_java_mdecl_def) |
133 by (simp add: wf_java_mdecl_def) |
140 |
134 |
141 end |
135 end |