forked from afp-mirror/Core_DOM
Added some missing lemmas for create_character_data.
This commit is contained in:
parent
342cac360e
commit
3e26409994
|
@ -3345,10 +3345,21 @@ global_interpretation l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^
|
||||||
.
|
.
|
||||||
|
|
||||||
locale l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
locale l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
|
||||||
l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs +
|
l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs +
|
||||||
l_get_disconnected_nodes +
|
l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs +
|
||||||
l_set_val +
|
l_set_val type_wf set_val set_val_locs +
|
||||||
l_create_character_data_defs +
|
l_create_character_data_defs create_character_data +
|
||||||
|
l_known_ptr known_ptr
|
||||||
|
for get_disconnected_nodes :: "(_) document_ptr \<Rightarrow> ((_) heap, exception, (_) node_ptr list) prog"
|
||||||
|
and get_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
|
||||||
|
and set_disconnected_nodes :: "(_) document_ptr \<Rightarrow> (_) node_ptr list \<Rightarrow> ((_) heap, exception, unit) prog"
|
||||||
|
and set_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
|
||||||
|
and set_val :: "(_) character_data_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, unit) prog"
|
||||||
|
and set_val_locs :: "(_) character_data_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
|
||||||
|
and type_wf :: "(_) heap \<Rightarrow> bool"
|
||||||
|
and create_character_data :: "(_) document_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, (_) character_data_ptr) prog"
|
||||||
|
and known_ptr :: "(_) object_ptr \<Rightarrow> bool" +
|
||||||
|
assumes known_ptr_impl: "known_ptr = a_known_ptr"
|
||||||
assumes create_character_data_impl: "create_character_data = a_create_character_data"
|
assumes create_character_data_impl: "create_character_data = a_create_character_data"
|
||||||
begin
|
begin
|
||||||
lemmas create_character_data_def = a_create_character_data_def[folded create_character_data_impl]
|
lemmas create_character_data_def = a_create_character_data_def[folded create_character_data_impl]
|
||||||
|
@ -3384,12 +3395,25 @@ proof -
|
||||||
ultimately show ?thesis
|
ultimately show ?thesis
|
||||||
by (auto simp add: document_ptr_kinds_def)
|
by (auto simp add: document_ptr_kinds_def)
|
||||||
qed
|
qed
|
||||||
|
|
||||||
|
lemma create_character_data_known_ptr:
|
||||||
|
assumes "h \<turnstile> create_character_data document_ptr text \<rightarrow>\<^sub>r new_character_data_ptr"
|
||||||
|
shows "known_ptr (cast new_character_data_ptr)"
|
||||||
|
proof -
|
||||||
|
have "is_character_data_ptr new_character_data_ptr"
|
||||||
|
using assms
|
||||||
|
apply(auto simp add: create_character_data_def elim!: bind_returns_result_E)
|
||||||
|
using new_character_data_is_character_data_ptr
|
||||||
|
by blast
|
||||||
|
then show ?thesis
|
||||||
|
by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs)
|
||||||
|
qed
|
||||||
end
|
end
|
||||||
|
|
||||||
locale l_create_character_data = l_create_character_data_defs
|
locale l_create_character_data = l_create_character_data_defs
|
||||||
|
|
||||||
interpretation
|
interpretation
|
||||||
i_create_character_data?: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs type_wf create_character_data
|
i_create_character_data?: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_val set_val_locs type_wf create_character_data known_ptr
|
||||||
by(auto simp add: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def create_character_data_def instances)
|
by(auto simp add: l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def create_character_data_def instances)
|
||||||
declare l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
|
declare l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
|
||||||
|
|
||||||
|
|
|
@ -7041,8 +7041,8 @@ locale l_create_character_data_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>
|
||||||
+ l_set_val_get_disconnected_nodes
|
+ l_set_val_get_disconnected_nodes
|
||||||
type_wf set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs
|
type_wf set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs
|
||||||
+ l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
+ l_create_character_data\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
|
||||||
set_val set_val_locs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
|
get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
|
||||||
set_disconnected_nodes_locs type_wf create_character_data
|
set_disconnected_nodes_locs set_val set_val_locs type_wf create_character_data known_ptr
|
||||||
+ l_new_character_data_get_child_nodes
|
+ l_new_character_data_get_child_nodes
|
||||||
type_wf known_ptr get_child_nodes get_child_nodes_locs
|
type_wf known_ptr get_child_nodes get_child_nodes_locs
|
||||||
+ l_set_val_get_child_nodes
|
+ l_set_val_get_child_nodes
|
||||||
|
@ -7081,7 +7081,7 @@ lemma create_character_data_preserves_wellformedness:
|
||||||
and "h \<turnstile> create_character_data document_ptr text \<rightarrow>\<^sub>h h'"
|
and "h \<turnstile> create_character_data document_ptr text \<rightarrow>\<^sub>h h'"
|
||||||
and "type_wf h"
|
and "type_wf h"
|
||||||
and "known_ptrs h"
|
and "known_ptrs h"
|
||||||
shows "heap_is_wellformed h'"
|
shows "heap_is_wellformed h'" and "type_wf h'" and "known_ptrs h'"
|
||||||
proof -
|
proof -
|
||||||
obtain new_character_data_ptr h2 h3 disc_nodes_h3 where
|
obtain new_character_data_ptr h2 h3 disc_nodes_h3 where
|
||||||
new_character_data_ptr: "h \<turnstile> new_character_data \<rightarrow>\<^sub>r new_character_data_ptr" and
|
new_character_data_ptr: "h \<turnstile> new_character_data \<rightarrow>\<^sub>r new_character_data_ptr" and
|
||||||
|
@ -7093,6 +7093,12 @@ proof -
|
||||||
by(auto simp add: create_character_data_def
|
by(auto simp add: create_character_data_def
|
||||||
elim!: bind_returns_heap_E
|
elim!: bind_returns_heap_E
|
||||||
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
|
bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
|
||||||
|
then
|
||||||
|
have "h \<turnstile> create_character_data document_ptr text \<rightarrow>\<^sub>r new_character_data_ptr"
|
||||||
|
apply(auto simp add: create_character_data_def intro!: bind_returns_result_I)
|
||||||
|
apply (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
|
||||||
|
apply (metis is_OK_returns_heap_E is_OK_returns_result_I local.get_disconnected_nodes_pure pure_returns_heap_eq)
|
||||||
|
by (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
|
||||||
|
|
||||||
|
|
||||||
have "new_character_data_ptr \<notin> set |h \<turnstile> character_data_ptr_kinds_M|\<^sub>r"
|
have "new_character_data_ptr \<notin> set |h \<turnstile> character_data_ptr_kinds_M|\<^sub>r"
|
||||||
|
@ -7255,7 +7261,7 @@ proof -
|
||||||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_val_writes h3]
|
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_val_writes h3]
|
||||||
using set_val_types_preserved
|
using set_val_types_preserved
|
||||||
by(auto simp add: reflp_def transp_def)
|
by(auto simp add: reflp_def transp_def)
|
||||||
then have "type_wf h'"
|
then show "type_wf h'"
|
||||||
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_disconnected_nodes_writes h']
|
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_disconnected_nodes_writes h']
|
||||||
using set_disconnected_nodes_types_preserved
|
using set_disconnected_nodes_types_preserved
|
||||||
by(auto simp add: reflp_def transp_def)
|
by(auto simp add: reflp_def transp_def)
|
||||||
|
@ -7441,6 +7447,18 @@ proof -
|
||||||
apply(simp add: object_ptr_kinds_eq_h)
|
apply(simp add: object_ptr_kinds_eq_h)
|
||||||
by (metis (mono_tags, lifting) \<open>cast\<^sub>c\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>_\<^sub>d\<^sub>a\<^sub>t\<^sub>a\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_character_data_ptr \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close> children_eq2_h disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h finite_set_in h' l_ptr_kinds_M.ptr_kinds_ptr_kinds_M l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes list.set_intros(2) local.l_set_disconnected_nodes_get_disconnected_nodes_axioms object_ptr_kinds_M_def select_result_I2)
|
by (metis (mono_tags, lifting) \<open>cast\<^sub>c\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>_\<^sub>d\<^sub>a\<^sub>t\<^sub>a\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_character_data_ptr \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close> children_eq2_h disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h finite_set_in h' l_ptr_kinds_M.ptr_kinds_ptr_kinds_M l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes list.set_intros(2) local.l_set_disconnected_nodes_get_disconnected_nodes_axioms object_ptr_kinds_M_def select_result_I2)
|
||||||
|
|
||||||
|
have "known_ptr (cast new_character_data_ptr)"
|
||||||
|
using \<open>h \<turnstile> create_character_data document_ptr text \<rightarrow>\<^sub>r new_character_data_ptr\<close> local.create_character_data_known_ptr by blast
|
||||||
|
then
|
||||||
|
have "known_ptrs h2"
|
||||||
|
using known_ptrs_new_ptr object_ptr_kinds_eq_h \<open>known_ptrs h\<close> h2
|
||||||
|
by blast
|
||||||
|
then
|
||||||
|
have "known_ptrs h3"
|
||||||
|
using known_ptrs_preserved object_ptr_kinds_eq_h2 by blast
|
||||||
|
then
|
||||||
|
show "known_ptrs h'"
|
||||||
|
using known_ptrs_preserved object_ptr_kinds_eq_h3 by blast
|
||||||
|
|
||||||
show "heap_is_wellformed h'"
|
show "heap_is_wellformed h'"
|
||||||
using \<open>a_acyclic_heap h'\<close> \<open>a_all_ptrs_in_heap h'\<close> \<open>a_distinct_lists h'\<close> \<open>a_owner_document_valid h'\<close>
|
using \<open>a_acyclic_heap h'\<close> \<open>a_all_ptrs_in_heap h'\<close> \<open>a_distinct_lists h'\<close> \<open>a_owner_document_valid h'\<close>
|
||||||
|
@ -7454,6 +7472,7 @@ interpretation i_create_character_data_wf?: l_create_character_data_wf\<^sub>C\<
|
||||||
set_disconnected_nodes_locs create_character_data known_ptrs
|
set_disconnected_nodes_locs create_character_data known_ptrs
|
||||||
using instances
|
using instances
|
||||||
by (auto simp add: l_create_character_data_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def)
|
by (auto simp add: l_create_character_data_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def)
|
||||||
|
declare l_create_character_data_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
|
||||||
|
|
||||||
|
|
||||||
subsection \<open>create\_document\<close>
|
subsection \<open>create\_document\<close>
|
||||||
|
|
Reference in New Issue