forked from afp-mirror/Core_DOM
Renamed folder.
This commit is contained in:
parent
4ed7af1ec9
commit
3f02e81f83
|
@ -4118,6 +4118,8 @@ interpretation i_remove_child_wf2?: l_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<
|
||||||
heap_is_wellformed parent_child_rel
|
heap_is_wellformed parent_child_rel
|
||||||
by unfold_locales
|
by unfold_locales
|
||||||
|
|
||||||
|
declare l_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
|
||||||
|
|
||||||
lemma remove_child_wf2_is_l_remove_child_wf2 [instances]:
|
lemma remove_child_wf2_is_l_remove_child_wf2 [instances]:
|
||||||
"l_remove_child_wf2 type_wf known_ptr known_ptrs remove_child heap_is_wellformed get_child_nodes remove"
|
"l_remove_child_wf2 type_wf known_ptr known_ptrs remove_child heap_is_wellformed get_child_nodes remove"
|
||||||
apply(auto simp add: l_remove_child_wf2_def l_remove_child_wf2_axioms_def instances)[1]
|
apply(auto simp add: l_remove_child_wf2_def l_remove_child_wf2_axioms_def instances)[1]
|
||||||
|
@ -6128,7 +6130,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
|
||||||
|
@ -6140,6 +6142,11 @@ 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)[1]
|
||||||
|
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"
|
||||||
|
@ -6192,6 +6199,18 @@ proof -
|
||||||
using object_ptr_kinds_eq_h3
|
using object_ptr_kinds_eq_h3
|
||||||
by(auto simp add: node_ptr_kinds_def)
|
by(auto simp add: node_ptr_kinds_def)
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
have "document_ptr |\<in>| document_ptr_kinds h"
|
have "document_ptr |\<in>| document_ptr_kinds h"
|
||||||
using disc_nodes_h3 document_ptr_kinds_eq_h object_ptr_kinds_eq_h2
|
using disc_nodes_h3 document_ptr_kinds_eq_h object_ptr_kinds_eq_h2
|
||||||
|
@ -6302,7 +6321,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)
|
Reference in New Issue