diff --git a/Core_DOM/Core_DOM_Functions.thy b/Core_DOM/Core_DOM_Functions.thy index dc1e185..7a4a48e 100644 --- a/Core_DOM/Core_DOM_Functions.thy +++ b/Core_DOM/Core_DOM_Functions.thy @@ -2358,6 +2358,15 @@ proof - using assms(1) get_child_nodes_ptr_in_heap by blast qed + +lemma remove_child_child_in_heap: + assumes "h \ remove_child ptr' child \\<^sub>h h'" + shows "child |\| node_ptr_kinds h" + using assms + apply(auto simp add: remove_child_def elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated] split: if_splits) + by (meson is_OK_returns_result_I local.get_owner_document_ptr_in_heap node_ptr_kinds_commutes) + + lemma remove_child_in_disconnected_nodes: (* assumes "known_ptrs h" *) assumes "h \ remove_child ptr child \\<^sub>h h'" @@ -2490,6 +2499,7 @@ locale l_remove_child = l_type_wf + l_known_ptrs + l_remove_child_defs + l_get_o \ h' \ get_disconnected_nodes owner_document \\<^sub>r disc_nodes \ child \ set disc_nodes" assumes remove_child_ptr_in_heap: "h \ ok (remove_child ptr child) \ ptr |\| object_ptr_kinds h" + assumes remove_child_child_in_heap: "h \ remove_child ptr' child \\<^sub>h h' \ child |\| node_ptr_kinds h" assumes remove_child_children_subset: "known_ptrs h \ type_wf h \ h \ remove_child parent child \\<^sub>h h' \ h \ get_child_nodes ptr \\<^sub>r children @@ -2535,6 +2545,7 @@ lemma remove_child_is_l_remove_child [instances]: using remove_child_types_preserved apply(blast) using remove_child_in_disconnected_nodes apply(blast) using remove_child_ptr_in_heap apply(blast) + using remove_child_child_in_heap apply(blast) using remove_child_children_subset apply(blast) done @@ -3012,6 +3023,13 @@ proof - unfolding insert_before_def by auto qed +lemma insert_before_ptr_in_heap: + assumes "h \ ok (insert_before ptr node reference_child)" + shows "ptr |\| object_ptr_kinds h" + using assms + apply(auto simp add: insert_before_def elim!: bind_is_OK_E) + by (metis (mono_tags, lifting) ensure_pre_insertion_validity_pure is_OK_returns_result_I local.get_owner_document_ptr_in_heap next_sibling_pure pure_returns_heap_eq return_returns_heap) + lemma insert_before_child_in_heap: assumes "h \ ok (insert_before ptr node reference_child)" shows "node |\| node_ptr_kinds h" @@ -3166,10 +3184,21 @@ global_interpretation l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\< . locale l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M = - l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs + - l_get_disconnected_nodes + - l_set_tag_type + - l_create_element_defs + + l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_tag_type set_tag_type_locs + + l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs + + l_set_tag_type type_wf set_tag_type set_tag_type_locs + + l_create_element_defs create_element + + l_known_ptr known_ptr + for get_disconnected_nodes :: "(_) document_ptr \ ((_) heap, exception, (_) node_ptr list) prog" + and get_disconnected_nodes_locs :: "(_) document_ptr \ ((_) heap \ (_) heap \ bool) set" + and set_disconnected_nodes :: "(_) document_ptr \ (_) node_ptr list \ ((_) heap, exception, unit) prog" + and set_disconnected_nodes_locs :: "(_) document_ptr \ ((_) heap, exception, unit) prog set" + and set_tag_type :: "(_) element_ptr \ char list \ ((_) heap, exception, unit) prog" + and set_tag_type_locs :: "(_) element_ptr \ ((_) heap, exception, unit) prog set" + and type_wf :: "(_) heap \ bool" + and create_element :: "(_) document_ptr \ char list \ ((_) heap, exception, (_) element_ptr) prog" + and known_ptr :: "(_) object_ptr \ bool" + + assumes known_ptr_impl: "known_ptr = a_known_ptr" assumes create_element_impl: "create_element = a_create_element" begin lemmas create_element_def = a_create_element_def[folded create_element_impl] @@ -3205,12 +3234,25 @@ proof - ultimately show ?thesis by (auto simp add: document_ptr_kinds_def) qed + +lemma create_element_known_ptr: + assumes "h \ create_element document_ptr tag \\<^sub>r new_element_ptr" + shows "known_ptr (cast new_element_ptr)" +proof - + have "is_element_ptr new_element_ptr" + using assms + apply(auto simp add: create_element_def elim!: bind_returns_result_E) + using new_element_is_element_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 locale l_create_element = l_create_element_defs interpretation - i_create_element?: l_create_element\<^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_tag_type set_tag_type_locs type_wf create_element + i_create_element?: l_create_element\<^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_tag_type set_tag_type_locs type_wf create_element known_ptr by(auto simp add: l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def create_element_def instances) declare l_create_element\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances] diff --git a/Core_DOM/Core_DOM_Heap_WF.thy b/Core_DOM/Core_DOM_Heap_WF.thy index a5153d5..46d6bda 100644 --- a/Core_DOM/Core_DOM_Heap_WF.thy +++ b/Core_DOM/Core_DOM_Heap_WF.thy @@ -2623,8 +2623,7 @@ proof - by (metis (no_types, hide_lams)) moreover have "node_ptr |\| node_ptr_kinds h" using assms(2) get_parent_ptr_in_heap by blast - thm heap_is_wellformed_children_disc_nodes_different - ultimately + ultimately have 0: "\document_ptr\set |h \ document_ptr_kinds_M|\<^sub>r. node_ptr \ set |h \ get_disconnected_nodes document_ptr|\<^sub>r" by (metis DocumentMonad.ptr_kinds_ptr_kinds_M assms(1) finite_set_in heap_is_wellformed_children_disc_nodes) then obtain document_ptr where @@ -2785,6 +2784,7 @@ next by (meson bind_pure_I bind_returns_result_E2 filter_M_holds_for_result is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap local.get_disconnected_nodes_pure return_pure) qed qed + end locale l_get_owner_document_wf = l_heap_is_wellformed_defs + l_type_wf + l_known_ptrs @@ -2829,8 +2829,86 @@ lemma get_owner_document_wf_is_l_get_owner_document_wf [instances]: done -subsection \Preserving heap-wellformedness\ +subsubsection \get\_root\_node\ +locale l_get_owner_document_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M = + l_get_root_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M + + l_get_root_node_wf + + l_get_owner_document\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M + + l_get_owner_document_wf +begin + +lemma get_root_node_document: + assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" + assumes "h \ get_root_node ptr \\<^sub>r root" + assumes "is_document_ptr_kind root" + shows "h \ get_owner_document ptr \\<^sub>r the (cast root)" +proof - + have "ptr |\| object_ptr_kinds h" + using assms(4) + by (meson is_OK_returns_result_I local.get_root_node_ptr_in_heap) + then have "known_ptr ptr" + using assms(3) local.known_ptrs_known_ptr by blast + { + assume "is_document_ptr_kind ptr" + then have "ptr = root" + using assms(4) + by(auto simp add: get_root_node_def get_ancestors_def elim!: bind_returns_result_E2 split: option.splits) + then have ?thesis + using \is_document_ptr_kind ptr\ \known_ptr ptr\ \ptr |\| object_ptr_kinds h\ + apply(auto simp add: known_ptr_impl get_owner_document_def a_get_owner_document_tups_def) + apply(split invoke_splits, (rule conjI | rule impI)+)+ + apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl]) + apply(drule(1) known_ptr_not_character_data_ptr) + apply(drule(1) known_ptr_not_element_ptr) + apply(simp add: NodeClass.known_ptr_defs) + by(auto simp add: a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro!: bind_pure_returns_result_I split: option.splits) + } + moreover + { + assume "is_node_ptr_kind ptr" + then have ?thesis + using \known_ptr ptr\ \ptr |\| object_ptr_kinds h\ + apply(auto simp add: known_ptr_impl get_owner_document_def a_get_owner_document_tups_def) + apply(split invoke_splits, (rule conjI | rule impI)+)+ + apply(drule(1) known_ptr_not_document_ptr[folded known_ptr_impl]) + apply(drule(1) known_ptr_not_character_data_ptr) + apply(drule(1) known_ptr_not_element_ptr) + apply(simp add: NodeClass.known_ptr_defs) + apply(auto split: option.splits)[1] + using \h \ get_root_node ptr \\<^sub>r root\ assms(5) + by(auto simp add: a_get_owner_document\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def is_document_ptr_kind_def intro!: bind_pure_returns_result_I split: option.splits)[2] + } + ultimately + show ?thesis + using \known_ptr ptr\ + by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits) +qed + +lemma get_root_node_same_owner_document: + assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" + assumes "h \ get_root_node ptr \\<^sub>r root" + shows "h \ get_owner_document ptr \\<^sub>r owner_document \ h \ get_owner_document root \\<^sub>r owner_document" + sorry +end + +interpretation get_owner_document_wf_get_root_node_wf?: l_get_owner_document_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf known_ptr known_ptrs get_parent get_parent_locs get_child_nodes get_child_nodes_locs get_ancestors get_ancestors_locs get_root_node get_root_node_locs heap_is_wellformed parent_child_rel get_disconnected_nodes get_disconnected_nodes_locs get_owner_document + by(auto simp add: l_get_owner_document_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances) +declare l_get_owner_document_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances] + +locale l_get_owner_document_wf_get_root_node_wf = l_heap_is_wellformed_defs + l_type_wf + l_known_ptrs + l_get_root_node_defs + l_get_owner_document_defs + + assumes get_root_node_document: "heap_is_wellformed h \ type_wf h \ known_ptrs h \ h \ get_root_node ptr \\<^sub>r root \ is_document_ptr_kind root \ h \ get_owner_document ptr \\<^sub>r the (cast root)" + assumes get_root_node_same_owner_document: "heap_is_wellformed h \ type_wf h \ known_ptrs h \ h \ get_root_node ptr \\<^sub>r root \ h \ get_owner_document ptr \\<^sub>r owner_document \ h \ get_owner_document root \\<^sub>r owner_document" + +lemma get_owner_document_wf_get_root_node_wf_is_l_get_owner_document_wf_get_root_node_wf [instances]: + "l_get_owner_document_wf_get_root_node_wf heap_is_wellformed type_wf known_ptr known_ptrs get_root_node get_owner_document" + apply(auto simp add: l_get_owner_document_wf_get_root_node_wf_def l_get_owner_document_wf_get_root_node_wf_axioms_def instances) + using get_root_node_document apply blast + using get_root_node_same_owner_document apply (blast, blast) + done + + +subsection \Preserving heap-wellformedness\ subsection \set\_attribute\ @@ -5356,7 +5434,7 @@ locale l_create_element_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub l_set_tag_type_get_disconnected_nodes type_wf set_tag_type set_tag_type_locs get_disconnected_nodes get_disconnected_nodes_locs + l_create_element\<^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_tag_type set_tag_type_locs type_wf create_element + + set_disconnected_nodes_locs set_tag_type set_tag_type_locs type_wf create_element known_ptr + l_new_element_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs + l_set_tag_type_get_child_nodes type_wf set_tag_type set_tag_type_locs known_ptr get_child_nodes get_child_nodes_locs + @@ -5387,7 +5465,7 @@ lemma create_element_preserves_wellformedness: and "h \ create_element document_ptr tag \\<^sub>h h'" and "type_wf h" and "known_ptrs h" - shows "heap_is_wellformed h'" + shows "heap_is_wellformed h'" and "type_wf h'" and "known_ptrs h'" proof - obtain new_element_ptr h2 h3 disc_nodes_h3 where new_element_ptr: "h \ new_element \\<^sub>r new_element_ptr" and @@ -5399,6 +5477,11 @@ proof - by(auto simp add: create_element_def elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] ) + then have "h \ create_element document_ptr tag \\<^sub>r new_element_ptr" + apply(auto simp add: create_element_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_element_ptr \ set |h \ element_ptr_kinds_M|\<^sub>r" using new_element_ptr ElementMonad.ptr_kinds_ptr_kinds_M h2 @@ -5444,6 +5527,19 @@ proof - using object_ptr_kinds_eq_h3 by(auto simp add: node_ptr_kinds_def) + have "known_ptr (cast new_element_ptr)" + using \h \ create_element document_ptr tag \\<^sub>r new_element_ptr\ local.create_element_known_ptr by blast + then + have "known_ptrs h2" + using known_ptrs_new_ptr object_ptr_kinds_eq_h \known_ptrs h\ 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 |\| document_ptr_kinds h" using disc_nodes_h3 document_ptr_kinds_eq_h object_ptr_kinds_eq_h2 @@ -5496,7 +5592,7 @@ proof - using writes_small_big[where P="\h h'. type_wf h \ type_wf h'", OF set_tag_type_writes h3] using set_tag_type_types_preserved by(auto simp add: reflp_def transp_def) - then have "type_wf h'" + then show "type_wf h'" using writes_small_big[where P="\h h'. type_wf h \ type_wf h'", OF set_disconnected_nodes_writes h'] using set_disconnected_nodes_types_preserved by(auto simp add: reflp_def transp_def) diff --git a/Core_DOM/classes/CharacterDataClass.thy b/Core_DOM/classes/CharacterDataClass.thy index 7af6a67..47b34a0 100644 --- a/Core_DOM/classes/CharacterDataClass.thy +++ b/Core_DOM/classes/CharacterDataClass.thy @@ -336,12 +336,14 @@ lemma known_ptrs_preserved: lemma known_ptrs_subset: "object_ptr_kinds h' |\| object_ptr_kinds h \ a_known_ptrs h \ a_known_ptrs h'" by(auto simp add: a_known_ptrs_def) +lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\| {|new_ptr|} \ known_ptr new_ptr \ a_known_ptrs h \ a_known_ptrs h'" + by(simp add: a_known_ptrs_def) end global_interpretation l_known_ptrs\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a known_ptr defines known_ptrs = a_known_ptrs . lemmas known_ptrs_defs = a_known_ptrs_def lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs" - using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset + using known_ptrs_known_ptr known_ptrs_preserved known_ptrs_subset known_ptrs_new_ptr l_known_ptrs_def by blast end diff --git a/Core_DOM/classes/DocumentClass.thy b/Core_DOM/classes/DocumentClass.thy index 594e014..64cbc1f 100644 --- a/Core_DOM/classes/DocumentClass.thy +++ b/Core_DOM/classes/DocumentClass.thy @@ -326,11 +326,14 @@ lemma known_ptrs_preserved: lemma known_ptrs_subset: "object_ptr_kinds h' |\| object_ptr_kinds h \ a_known_ptrs h \ a_known_ptrs h'" by(auto simp add: a_known_ptrs_def) +lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\| {|new_ptr|} \ known_ptr new_ptr \ a_known_ptrs h \ a_known_ptrs h'" + by(simp add: a_known_ptrs_def) end global_interpretation l_known_ptrs\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t known_ptr defines known_ptrs = a_known_ptrs . lemmas known_ptrs_defs = a_known_ptrs_def lemma known_ptrs_is_l_known_ptrs [instances]: "l_known_ptrs known_ptr known_ptrs" - using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset by blast + using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset known_ptrs_new_ptr + by blast end diff --git a/Core_DOM/classes/ElementClass.thy b/Core_DOM/classes/ElementClass.thy index 02538f4..d615ac9 100644 --- a/Core_DOM/classes/ElementClass.thy +++ b/Core_DOM/classes/ElementClass.thy @@ -273,7 +273,6 @@ lemma new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>E\<^ using assms by(auto simp add: new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def) - locale l_known_ptr\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t begin definition a_known_ptr :: "(_) object_ptr \ bool" @@ -301,11 +300,13 @@ lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \| object_ptr_kinds h \ a_known_ptrs h \ a_known_ptrs h'" by(auto simp add: a_known_ptrs_def) +lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\| {|new_ptr|} \ known_ptr new_ptr \ a_known_ptrs h \ a_known_ptrs h'" + by(simp add: a_known_ptrs_def) end global_interpretation l_known_ptrs\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t known_ptr defines known_ptrs = a_known_ptrs . lemmas known_ptrs_defs = a_known_ptrs_def lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs" - using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset by blast + using known_ptrs_known_ptr known_ptrs_preserved known_ptrs_subset known_ptrs_new_ptr l_known_ptrs_def by blast end diff --git a/Core_DOM/classes/NodeClass.thy b/Core_DOM/classes/NodeClass.thy index 142c7fa..e132a30 100644 --- a/Core_DOM/classes/NodeClass.thy +++ b/Core_DOM/classes/NodeClass.thy @@ -186,12 +186,15 @@ lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \| object_ptr_kinds h \ a_known_ptrs h \ a_known_ptrs h'" by(auto simp add: a_known_ptrs_def) +lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\| {|new_ptr|} \ known_ptr new_ptr \ a_known_ptrs h \ a_known_ptrs h'" + by(simp add: a_known_ptrs_def) end global_interpretation l_known_ptrs\<^sub>N\<^sub>o\<^sub>d\<^sub>e known_ptr defines known_ptrs = a_known_ptrs . lemmas known_ptrs_defs = a_known_ptrs_def lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs" - using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset by blast + using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset known_ptrs_new_ptr + by blast lemma get_node_ptr_simp1 [simp]: "get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr (put\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr node h) = Some node" by(auto simp add: get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def) diff --git a/Core_DOM/classes/ObjectClass.thy b/Core_DOM/classes/ObjectClass.thy index 310c64b..e080277 100644 --- a/Core_DOM/classes/ObjectClass.thy +++ b/Core_DOM/classes/ObjectClass.thy @@ -128,6 +128,7 @@ locale l_known_ptrs = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr \ ptr |\| object_ptr_kinds h \ known_ptr ptr" assumes known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \ known_ptrs h = known_ptrs h'" assumes known_ptrs_subset: "object_ptr_kinds h' |\| object_ptr_kinds h \ known_ptrs h \ known_ptrs h'" + assumes known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\| {|new_ptr|} \ known_ptr new_ptr \ known_ptrs h \ known_ptrs h'" locale l_known_ptrs\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr \ bool" begin @@ -143,12 +144,15 @@ lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \| object_ptr_kinds h \ a_known_ptrs h \ a_known_ptrs h'" by(auto simp add: a_known_ptrs_def) +lemma known_ptrs_new_ptr: "object_ptr_kinds h' = object_ptr_kinds h |\| {|new_ptr|} \ known_ptr new_ptr \ a_known_ptrs h \ a_known_ptrs h'" + by(simp add: a_known_ptrs_def) end global_interpretation l_known_ptrs\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t known_ptr defines known_ptrs = a_known_ptrs . lemmas known_ptrs_defs = a_known_ptrs_def lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs" - using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset by blast + using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset known_ptrs_new_ptr + by blast lemma get_object_ptr_simp1 [simp]: "get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr object h) = Some object"