BrowserSecurity
/
Core_DOM-dev
Archived
forked from afp-mirror/Core_DOM
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Preparing AFP update.

This commit is contained in:
Achim D. Brucker 2020-04-16 07:46:14 +01:00
parent 25e85825bd
commit 9a96718e9f
11 changed files with 125 additions and 129 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Core_DOM/Core_DOM/ROOT
View File

@ -2,7 +2,7 @@ chapter AFP
session "Core_DOM" (AFP) = "HOL-Library" +
options [timeout = 1200]
directories
directories
"common"
"common/classes"
"common/monads"

2
Core_DOM/Core_DOM/common/classes/CharacterDataClass.thy
View File

@ -64,7 +64,7 @@ type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'docume
= "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr,
'Object, 'CharacterData option RCharacterData_ext + 'Node, 'Element) heap"
register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr,
'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData) heap"
'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData) heap"
type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap"

2
Core_DOM/Core_DOM/common/classes/DocumentClass.thy
View File

@ -64,7 +64,7 @@ type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'docume
'Element, 'CharacterData) heap"
register_default_tvars
"('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr,
'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData, 'Document) heap"
'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData, 'Document) heap"
type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap"

2
Core_DOM/Core_DOM/common/classes/ObjectClass.thy
View File

@ -44,7 +44,7 @@ type_synonym 'Object Object = "'Object RObject_scheme"
register_default_tvars "'Object Object"
datatype ('object_ptr, 'Object) heap = Heap (the_heap: "((_) object_ptr, (_) Object) fmap")
register_default_tvars "('object_ptr, 'Object) heap"
register_default_tvars "('object_ptr, 'Object) heap"
type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit) heap"
definition object_ptr_kinds :: "(_) heap \<Rightarrow> (_) object_ptr fset"

2
Core_DOM/Core_DOM/common/monads/CharacterDataMonad.thy
View File

@ -57,7 +57,7 @@ lemma character_data_ptr_kinds_M_eq:
lemma character_data_ptr_kinds_M_reads:
"reads (\<Union>node_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t node_ptr RObject.nothing)}) character_data_ptr_kinds_M h h'"
using node_ptr_kinds_M_reads
apply(simp add: reads_def node_ptr_kinds_M_defs character_data_ptr_kinds_M_defs
apply (simp add: reads_def node_ptr_kinds_M_defs character_data_ptr_kinds_M_defs
character_data_ptr_kinds_def preserved_def)
by (smt node_ptr_kinds_small preserved_def unit_all_impI)

6
Core_DOM/Core_DOM/common/monads/DocumentMonad.thy
View File

@ -55,7 +55,7 @@ lemma document_ptr_kinds_M_eq:
lemma document_ptr_kinds_M_reads:
"reads (\<Union>object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) document_ptr_kinds_M h h'"
using object_ptr_kinds_M_reads
apply(simp add: reads_def object_ptr_kinds_M_defs document_ptr_kinds_M_defs
apply (simp add: reads_def object_ptr_kinds_M_defs document_ptr_kinds_M_defs
document_ptr_kinds_def preserved_def cong del: image_cong_simp)
apply (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
done
@ -453,7 +453,7 @@ lemma new_document_type_wf_preserved [simp]: "h \<turnstile> new_document \<righ
intro!: type_wf_put_I ElementMonad.type_wf_put_I CharacterDataMonad.type_wf_put_I
NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I
split: if_splits)[1]
apply(auto simp add: type_wf_defs ElementClass.type_wf_defs CharacterDataClass.type_wf_defs
apply(auto simp add: type_wf_defs ElementClass.type_wf_defs CharacterDataClass.type_wf_defs
NodeClass.type_wf_defs ObjectClass.type_wf_defs is_document_kind_def
split: option.splits)[1]
using document_ptrs_def apply fastforce
@ -520,7 +520,7 @@ lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_docu
split: option.splits)[1]
by (metis finite_set_in)
lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_disconnected_nodes_type_wf_preserved [simp]:
lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_disconnected_nodes_type_wf_preserved [simp]:
"h \<turnstile> put_M document_ptr disconnected_nodes_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
apply(auto simp add: put_M_defs put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
DocumentClass.type_wf\<^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

4
Core_DOM/Core_DOM/common/monads/ElementMonad.thy
View File

@ -54,7 +54,7 @@ lemma element_ptr_kinds_M_eq:
lemma element_ptr_kinds_M_reads:
"reads (\<Union>element_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t element_ptr RObject.nothing)}) element_ptr_kinds_M h h'"
apply(simp add: reads_def node_ptr_kinds_M_defs element_ptr_kinds_M_defs element_ptr_kinds_def
apply (simp add: reads_def node_ptr_kinds_M_defs element_ptr_kinds_M_defs element_ptr_kinds_def
node_ptr_kinds_M_reads preserved_def cong del: image_cong_simp)
apply (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
done
@ -323,7 +323,7 @@ lemma new_element_type_wf_preserved [simp]: "h \<turnstile> new_element \<righta
get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
split: prod.splits if_splits elim!: bind_returns_heap_E)[1]
apply (metis element_ptr_kinds_commutes element_ptrs_def fempty_iff ffmember_filter finite_set_in
is_element_ptr_ref)
is_element_ptr_ref)
apply (metis element_ptrs_def fempty_iff ffmember_filter finite_set_in is_element_ptr_ref)
apply (metis (no_types, lifting) Suc_n_not_le_n element_ptr.sel(1) element_ptr_kinds_commutes
element_ptrs_def fMax_ge ffmember_filter fimage_eqI is_element_ptr_ref notin_fset)

2
Core_DOM/Core_DOM/common/monads/NodeMonad.thy
View File

@ -75,7 +75,7 @@ global_interpretation l_get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e_lemmas type_wf by
lemma node_ptr_kinds_M_reads:
"reads (\<Union>object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) node_ptr_kinds_M h h'"
using object_ptr_kinds_M_reads
apply(simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def
apply (simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def
object_ptr_kinds_M_reads preserved_def)
by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI)

4
Core_DOM/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy
View File

@ -278,7 +278,7 @@ structure Hide_Tvar : HIDE_TVAR = struct
fun parse_ast ((Ast.Constant const)::[]) = (const,NONE)
| parse_ast ((Ast.Constant sort)::(Ast.Constant const)::[])
= (const,SOME sort)
| parse_ast _ = error("AST type not supported.")
| parse_ast _ = error("AST type not supported.")
val (decorated_name, decorated_sort) = parse_ast ast
@ -295,7 +295,7 @@ structure Hide_Tvar : HIDE_TVAR = struct
let fun mk_tvar n =
case decorated_sort of
NONE => Ast.Variable(name_of_tvar n)
| SOME sort => Ast.Appl([Ast.Constant("_ofsort"),
| SOME sort => Ast.Appl([Ast.Constant("_ofsort"),
Ast.Variable(name_of_tvar n),
Ast.Constant(sort)])
in

226
Core_DOM/Core_DOM/standard/Core_DOM_Heap_WF.thy
View File

@ -3576,7 +3576,7 @@ have "type_wf h2"
apply(auto simp add: a_owner_document_valid_def object_ptr_kinds_eq3 document_ptr_kinds_eq3
node_ptr_kinds_eq3)[1]
proof -
fix node_ptr
fix node_ptr
assume 0: "\<forall>node_ptr\<in>fset (node_ptr_kinds h'). (\<exists>document_ptr. document_ptr |\<in>| document_ptr_kinds h' \<and> node_ptr \<in> set |h \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r) \<or> (\<exists>parent_ptr. parent_ptr |\<in>| object_ptr_kinds h' \<and> node_ptr \<in> set |h \<turnstile> get_child_nodes parent_ptr|\<^sub>r)"
and 1: "node_ptr |\<in>| node_ptr_kinds h'"
and 2: "\<forall>parent_ptr. parent_ptr |\<in>| object_ptr_kinds h' \<longrightarrow> node_ptr \<notin> set |h' \<turnstile> get_child_nodes parent_ptr|\<^sub>r"
@ -4528,9 +4528,9 @@ proof -
using wellformed_h2 by (simp add: heap_is_wellformed_def)
then have "a_owner_document_valid h'"
apply(simp add: a_owner_document_valid_def node_ptr_kinds_eq_h2 node_ptr_kinds_eq3_h3
object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 document_ptr_kinds_eq2_h2
object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 document_ptr_kinds_eq2_h2
document_ptr_kinds_eq2_h3 children_eq2_h2 children_eq2_h3 )
by (metis (no_types) disc_nodes_document_ptr_h' disc_nodes_document_ptr_h2
by (smt disc_nodes_document_ptr_h' disc_nodes_document_ptr_h2
disc_nodes_old_document_h2 disc_nodes_old_document_h3
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_in_heap
document_ptr_kinds_eq3_h2 document_ptr_kinds_eq3_h3 in_set_remove1
@ -5486,7 +5486,7 @@ proof -
have "a_all_ptrs_in_heap h3"
using \<open>a_all_ptrs_in_heap h2\<close>
apply(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_M_eq2_h2 node_ptr_kinds_eq2_h2
children_eq_h2)[1]
children_eq_h2)[1]
using disconnected_nodes_eq2_h2 disconnected_nodes_h2 disconnected_nodes_h3
using node_ptr_kinds_eq2_h2 apply auto[1]
apply (metis \<open>known_ptrs h2\<close> \<open>type_wf h3\<close> children_eq_h2 local.get_child_nodes_ok local.heap_is_wellformed_children_in_heap local.known_ptrs_known_ptr object_ptr_kinds_M_eq3_h2 returns_result_select_result wellformed_h2)
@ -5501,12 +5501,12 @@ proof -
using node_in_heap
apply(auto simp add: node_ptr_kinds_eq2_h node_ptr_kinds_eq2_h2 node_ptr_kinds_eq2_h3)[1]
by (metis (no_types, hide_lams) contra_subsetD finite_set_in insert_before_list_in_set
node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h'
object_ptr_kinds_M_eq3_h2)
node_ptr_kinds_commutes object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h'
object_ptr_kinds_M_eq3_h2)
then show ?thesis
using \<open>a_all_ptrs_in_heap h3\<close>
apply(auto simp add: object_ptr_kinds_M_eq3_h' a_all_ptrs_in_heap_def node_ptr_kinds_def
node_ptr_kinds_eq2_h3 disconnected_nodes_eq_h3)[1]
node_ptr_kinds_eq2_h3 disconnected_nodes_eq_h3)[1]
using children_eq_h3 children_h'
apply (metis (no_types, lifting) children_eq2_h3 finite_set_in select_result_I2 subsetD)
by (metis (no_types) \<open>type_wf h'\<close> disconnected_nodes_eq2_h3 disconnected_nodes_eq_h3 finite_set_in is_OK_returns_result_I local.get_disconnected_nodes_ok local.get_disconnected_nodes_ptr_in_heap returns_result_select_result subsetD)
@ -5516,14 +5516,14 @@ proof -
using wellformed_h2 by (simp add: heap_is_wellformed_def)
then have "a_distinct_lists h3"
proof(auto simp add: a_distinct_lists_def object_ptr_kinds_M_eq2_h2 document_ptr_kinds_eq2_h2
children_eq2_h2 intro!: distinct_concat_map_I)[1]
children_eq2_h2 intro!: distinct_concat_map_I)[1]
fix x
assume 1: "x |\<in>| document_ptr_kinds h3"
and 2: "distinct (concat (map (\<lambda>document_ptr. |h2 \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r)
(sorted_list_of_set (fset (document_ptr_kinds h3)))))"
show "distinct |h3 \<turnstile> get_disconnected_nodes x|\<^sub>r"
using distinct_concat_map_E(2)[OF 2] select_result_I2[OF disconnected_nodes_h3]
disconnected_nodes_eq2_h2 select_result_I2[OF disconnected_nodes_h2] 1
disconnected_nodes_eq2_h2 select_result_I2[OF disconnected_nodes_h2] 1
by (metis (full_types) distinct_remove1 finite_fset fmember.rep_eq set_sorted_list_of_set)
next
fix x y xa
@ -5550,17 +5550,17 @@ proof -
proof (cases "y = owner_document")
case True
then show ?thesis
using distinct_concat_map_E(1)[OF 1]
using 2 3 4 5 6 select_result_I2[OF disconnected_nodes_h3] select_result_I2[OF disconnected_nodes_h2]
apply(auto simp add: True disconnected_nodes_eq2_h2[OF \<open>x \<noteq> owner_document\<close>])[1]
by (metis (no_types, hide_lams) disconnected_nodes_eq2_h2 disjoint_iff_not_equal notin_set_remove1)
using distinct_concat_map_E(1)[OF 1]
using 2 3 4 5 6 select_result_I2[OF disconnected_nodes_h3] select_result_I2[OF disconnected_nodes_h2]
apply(auto simp add: True disconnected_nodes_eq2_h2[OF \<open>x \<noteq> owner_document\<close>])[1]
by (metis (no_types, hide_lams) disconnected_nodes_eq2_h2 disjoint_iff_not_equal notin_set_remove1)
next
case False
then show ?thesis
using distinct_concat_map_E(1)[OF 1, simplified, OF 2 3 4] 5 6
using disconnected_nodes_eq2_h2 disconnected_nodes_h2 disconnected_nodes_h3
disjoint_iff_not_equal finite_fset fmember.rep_eq notin_set_remove1 select_result_I2
set_sorted_list_of_set
disjoint_iff_not_equal finite_fset fmember.rep_eq notin_set_remove1 select_result_I2
set_sorted_list_of_set
by (metis (no_types, lifting))
qed
qed
@ -5575,10 +5575,10 @@ proof -
have 6: "set |h3 \<turnstile> get_child_nodes xa|\<^sub>r \<inter> set |h2 \<turnstile> get_disconnected_nodes xb|\<^sub>r = {}"
using 1 2 4
by (metis \<open>type_wf h2\<close> children_eq2_h2 document_ptr_kinds_commutes known_ptrs
local.get_child_nodes_ok local.get_disconnected_nodes_ok
local.heap_is_wellformed_children_disc_nodes_different local.known_ptrs_known_ptr
object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h2 returns_result_select_result
wellformed_h2)
local.get_child_nodes_ok local.get_disconnected_nodes_ok
local.heap_is_wellformed_children_disc_nodes_different local.known_ptrs_known_ptr
object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h2 returns_result_select_result
wellformed_h2)
show False
proof (cases "xb = owner_document")
case True
@ -5593,11 +5593,11 @@ proof -
qed
then have "a_distinct_lists h'"
proof(auto simp add: a_distinct_lists_def document_ptr_kinds_eq2_h3 object_ptr_kinds_M_eq2_h3
disconnected_nodes_eq2_h3 intro!: distinct_concat_map_I)[1]
disconnected_nodes_eq2_h3 intro!: distinct_concat_map_I)[1]
fix x
assume 1: "distinct (concat (map (\<lambda>ptr. |h3 \<turnstile> get_child_nodes ptr|\<^sub>r)
(sorted_list_of_set (fset (object_ptr_kinds h')))))" and
2: "x |\<in>| object_ptr_kinds h'"
2: "x |\<in>| object_ptr_kinds h'"
have 3: "\<And>p. p |\<in>| object_ptr_kinds h' \<Longrightarrow> distinct |h3 \<turnstile> get_child_nodes p|\<^sub>r"
using 1 by (auto elim: distinct_concat_map_E)
show "distinct |h' \<turnstile> get_child_nodes x|\<^sub>r"
@ -5606,7 +5606,7 @@ proof -
show ?thesis
using 3[OF 2] children_h3 children_h'
by(auto simp add: True insert_before_list_distinct
dest: child_not_in_any_children[unfolded children_eq_h2])
dest: child_not_in_any_children[unfolded children_eq_h2])
next
case False
show ?thesis
@ -5632,9 +5632,9 @@ proof -
using children_h3 children_h' child_not_in_any_children[unfolded children_eq_h2] 5 6
apply(auto simp add: True children_eq2_h3[OF \<open>ptr \<noteq> y\<close>])[1]
by (metis (no_types, hide_lams) "3" "7" \<open>type_wf h3\<close> children_eq2_h3 disjoint_iff_not_equal
get_child_nodes_ok insert_before_list_in_set known_ptrs local.known_ptrs_known_ptr
object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h'
object_ptr_kinds_M_eq3_h2 returns_result_select_result select_result_I2)
get_child_nodes_ok insert_before_list_in_set known_ptrs local.known_ptrs_known_ptr
object_ptr_kinds_M_eq3_h object_ptr_kinds_M_eq3_h'
object_ptr_kinds_M_eq3_h2 returns_result_select_result select_result_I2)
next
case False
then show ?thesis
@ -5644,10 +5644,10 @@ proof -
using children_h3 children_h' child_not_in_any_children[unfolded children_eq_h2] 5 6
apply(auto simp add: True children_eq2_h3[OF \<open>ptr \<noteq> x\<close>])[1]
by (metis (no_types, hide_lams) "2" "4" "7" IntI \<open>known_ptrs h3\<close> \<open>type_wf h'\<close>
children_eq_h3 empty_iff insert_before_list_in_set local.get_child_nodes_ok
local.known_ptrs_known_ptr object_ptr_kinds_M_eq3_h'
returns_result_select_result select_result_I2)
next
children_eq_h3 empty_iff insert_before_list_in_set local.get_child_nodes_ok
local.known_ptrs_known_ptr object_ptr_kinds_M_eq3_h'
returns_result_select_result select_result_I2)
next
case False
then show ?thesis
using children_eq2_h3[OF \<open>ptr \<noteq> x\<close>] children_eq2_h3[OF \<open>ptr \<noteq> y\<close>] 5 6 7 by auto
@ -5680,13 +5680,13 @@ proof -
case True
show ?thesis
using 6 node_not_in_disconnected_nodes 3 4 5 select_result_I2[OF children_h']
select_result_I2[OF children_h3] True disconnected_nodes_eq2_h3
select_result_I2[OF children_h3] True disconnected_nodes_eq2_h3
by (metis (no_types, lifting) "2" DocumentMonad.ptr_kinds_ptr_kinds_M
\<open>a_distinct_lists h3\<close> \<open>type_wf h'\<close> disconnected_nodes_eq_h3
distinct_lists_no_parent document_ptr_kinds_eq2_h3 get_disconnected_nodes_ok
insert_before_list_in_set object_ptr_kinds_M_eq3_h' returns_result_select_result)
\<open>a_distinct_lists h3\<close> \<open>type_wf h'\<close> disconnected_nodes_eq_h3
distinct_lists_no_parent document_ptr_kinds_eq2_h3 get_disconnected_nodes_ok
insert_before_list_in_set object_ptr_kinds_M_eq3_h' returns_result_select_result)
next
next
case False
then show ?thesis
using 1 2 3 4 5 children_eq2_h3[OF False] by fastforce
@ -5697,11 +5697,11 @@ proof -
using wellformed_h2 by (simp add: heap_is_wellformed_def)
then have "a_owner_document_valid h'"
apply(auto simp add: a_owner_document_valid_def object_ptr_kinds_M_eq2_h2
object_ptr_kinds_M_eq2_h3 node_ptr_kinds_eq2_h2 node_ptr_kinds_eq2_h3
document_ptr_kinds_eq2_h2 document_ptr_kinds_eq2_h3 children_eq2_h2)[1]
object_ptr_kinds_M_eq2_h3 node_ptr_kinds_eq2_h2 node_ptr_kinds_eq2_h3
document_ptr_kinds_eq2_h2 document_ptr_kinds_eq2_h3 children_eq2_h2)[1]
apply(auto simp add: document_ptr_kinds_eq2_h2[simplified] document_ptr_kinds_eq2_h3[simplified]
object_ptr_kinds_M_eq2_h2[simplified] object_ptr_kinds_M_eq2_h3[simplified]
node_ptr_kinds_eq2_h2[simplified] node_ptr_kinds_eq2_h3[simplified])[1]
object_ptr_kinds_M_eq2_h2[simplified] object_ptr_kinds_M_eq2_h3[simplified]
node_ptr_kinds_eq2_h2[simplified] node_ptr_kinds_eq2_h3[simplified])[1]
apply(auto simp add: disconnected_nodes_eq2_h3[symmetric])[1]
by (smt children_eq2_h3 children_h' children_h3 disconnected_nodes_eq2_h2 disconnected_nodes_h2 disconnected_nodes_h3 finite_set_in in_set_remove1 insert_before_list_in_set object_ptr_kinds_M_eq3_h' ptr_in_heap select_result_I2)
@ -6180,7 +6180,9 @@ proof -
by auto
obtain parent_opt where
parent_opt: "h \<turnstile> get_parent child \<rightarrow>\<^sub>r parent_opt"
by (meson assms(2) assms(3) is_OK_returns_result_I l_get_owner_document.get_owner_document_ptr_in_heap local.get_parent_ok local.l_get_owner_document_axioms node_ptr_kinds_commutes old_document returns_result_select_result)
by (meson assms(2) assms(3) is_OK_returns_result_I l_get_owner_document.get_owner_document_ptr_in_heap
local.get_parent_ok local.l_get_owner_document_axioms node_ptr_kinds_commutes old_document
returns_result_select_result)
then have "h \<turnstile> ok (get_parent child)"
by auto
@ -6407,7 +6409,8 @@ proof -
obtain h2 where
h2: "h \<turnstile> adopt_node owner_document node \<rightarrow>\<^sub>h h2"
by (meson assms(1) assms(2) assms(3) assms(5) is_OK_returns_heap_E adopt_node_ok l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms local.get_owner_document_owner_document_in_heap owner_document)
by (meson assms(1) assms(2) assms(3) assms(5) is_OK_returns_heap_E adopt_node_ok l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms
local.get_owner_document_owner_document_in_heap owner_document)
then have "h \<turnstile> ok (adopt_node owner_document node)"
by auto
have "object_ptr_kinds h = object_ptr_kinds h2"
@ -6970,24 +6973,18 @@ proof -
ultimately show "False"
apply(-)
apply(cases "x = document_ptr")
apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M
\<open>a_all_ptrs_in_heap h\<close>
\<open>cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
a_all_ptrs_in_heap_def assms(3) disc_nodes_h3 disconnected_nodes_eq2_h
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal
document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 fset_mp fset_of_list_elem
get_disconnected_nodes_ok h' returns_result_select_result select_result_I2
set_ConsD set_disconnected_nodes_get_disconnected_nodes)
apply(cases "y = document_ptr" )
apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M
\<open>a_all_ptrs_in_heap h\<close>
\<open>cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
a_all_ptrs_in_heap_def assms(3) disc_nodes_h3 disconnected_nodes_eq2_h
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal
document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 fset_mp fset_of_list_elem
get_disconnected_nodes_ok h' returns_result_select_result select_result_I2
set_ConsD set_disconnected_nodes_get_disconnected_nodes)
using disconnected_nodes_eq2_h3 by auto
apply (smt NodeMonad.ptr_kinds_ptr_kinds_M \<open>cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> \<open>local.a_all_ptrs_in_heap h\<close>
disc_nodes_h3 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3
disjoint_iff_not_equal document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h'
l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes
local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms
select_result_I2 set_ConsD subsetD)
by (smt NodeMonad.ptr_kinds_ptr_kinds_M \<open>cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_element_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close> \<open>local.a_all_ptrs_in_heap h\<close>
disc_nodes_document_ptr_h2 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3
disjoint_iff_not_equal document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h'
l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes
local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms
select_result_I2 set_ConsD subsetD)
next
fix x xa xb
assume 2: "(\<Union>x\<in>fset (object_ptr_kinds h3). set |h' \<turnstile> get_child_nodes x|\<^sub>r)
@ -7352,20 +7349,23 @@ proof -
apply(auto simp add: a_all_ptrs_in_heap_def)[1]
using node_ptr_kinds_eq_h \<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
\<open>h2 \<turnstile> get_child_nodes (cast new_character_data_ptr) \<rightarrow>\<^sub>r []\<close>
apply (metis (no_types, hide_lams) children_eq_h fempty_iff fset_mp fset_of_list_simps(1)
funionCI select_result_I2)
by (simp add: disconnected_nodes_eq_h fset_rev_mp node_ptr_kinds_eq_h)
apply (metis (no_types, lifting) NodeMonad.ptr_kinds_ptr_kinds_M \<open>parent_child_rel h = parent_child_rel h2\<close>
children_eq2_h finite_set_in finsert_iff funion_finsert_right local.parent_child_rel_child
local.parent_child_rel_parent_in_heap node_ptr_kinds_commutes object_ptr_kinds_eq_h
select_result_I2 subsetD sup_bot.right_neutral)
by (metis assms(1) assms(3) disconnected_nodes_eq2_h document_ptr_kinds_eq_h funionI1
local.get_disconnected_nodes_ok local.heap_is_wellformed_disc_nodes_in_heap
node_ptr_kinds_eq_h returns_result_select_result)
then have "a_all_ptrs_in_heap h3"
by(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_eq_h2 node_ptr_kinds_def
children_eq_h2 disconnected_nodes_eq_h2)
by (simp add: children_eq2_h2 disconnected_nodes_eq2_h2 document_ptr_kinds_eq_h2
local.a_all_ptrs_in_heap_def node_ptr_kinds_eq_h2 object_ptr_kinds_eq_h2)
then have "a_all_ptrs_in_heap h'"
apply(auto simp add: a_all_ptrs_in_heap_def object_ptr_kinds_eq_h3 node_ptr_kinds_def
children_eq_h3 )[1]
using disconnected_nodes_eq_h3 object_ptr_kinds_eq_h object_ptr_kinds_eq_h2
by (metis (no_types, lifting) disc_nodes_h3 finsertCI fset.map_comp fset_mp fset_of_list_elem
funion_finsert_right h' local.set_disconnected_nodes_get_disconnected_nodes
node_ptr_kinds_def node_ptr_kinds_eq_h select_result_I2 set_ConsD)
by (smt character_data_ptr_kinds_commutes children_eq2_h3 disc_nodes_document_ptr_h2
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h3
finite_set_in h' h2 local.a_all_ptrs_in_heap_def
local.set_disconnected_nodes_get_disconnected_nodes new_character_data_ptr
new_character_data_ptr_in_heap node_ptr_kinds_eq_h2 node_ptr_kinds_eq_h3
object_ptr_kinds_eq_h3 select_result_I2 set_ConsD subset_code(1))
have "\<And>p. p |\<in>| object_ptr_kinds h \<Longrightarrow> cast new_character_data_ptr \<notin> set |h \<turnstile> get_child_nodes p|\<^sub>r"
using \<open>heap_is_wellformed h\<close> \<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
heap_is_wellformed_children_in_heap
@ -7428,25 +7428,13 @@ proof -
moreover have "set |h3 \<turnstile> get_disconnected_nodes x|\<^sub>r \<inter> set |h3 \<turnstile> get_disconnected_nodes y|\<^sub>r = {}"
using calculation by(auto dest: distinct_concat_map_E(1))
ultimately show "False"
apply(cases "x = document_ptr")
apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M \<open>a_all_ptrs_in_heap h\<close>
\<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
a_all_ptrs_in_heap_def assms(3) disc_nodes_h3
disconnected_nodes_eq2_h disconnected_nodes_eq2_h2
disconnected_nodes_eq2_h3 disjoint_iff_not_equal
document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 fset_mp
fset_of_list_elem get_disconnected_nodes_ok h'
returns_result_select_result select_result_I2 set_ConsD
set_disconnected_nodes_get_disconnected_nodes)
apply(cases "y = document_ptr" )
apply (metis (no_types) NodeMonad.ptr_kinds_ptr_kinds_M
\<open>a_all_ptrs_in_heap h\<close> \<open>cast new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
a_all_ptrs_in_heap_def assms(3) disc_nodes_h3 disconnected_nodes_eq2_h
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal
document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 fset_mp fset_of_list_elem
get_disconnected_nodes_ok h' returns_result_select_result select_result_I2 set_ConsD
set_disconnected_nodes_get_disconnected_nodes)
using disconnected_nodes_eq2_h3 by auto
by (smt NodeMonad.ptr_kinds_ptr_kinds_M \<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>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_character_data_ptr \<notin> set |h \<turnstile> node_ptr_kinds_M|\<^sub>r\<close>
\<open>local.a_all_ptrs_in_heap h\<close> disc_nodes_document_ptr_h2 disconnected_nodes_eq2_h
disconnected_nodes_eq2_h2 disconnected_nodes_eq2_h3 disjoint_iff_not_equal
document_ptr_kinds_eq_h document_ptr_kinds_eq_h2 finite_set_in h'
l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes
local.a_all_ptrs_in_heap_def local.l_set_disconnected_nodes_get_disconnected_nodes_axioms
select_result_I2 set_ConsD subsetD)
next
fix x xa xb
assume 2: "(\<Union>x\<in>fset (object_ptr_kinds h3). set |h' \<turnstile> get_child_nodes x|\<^sub>r)
@ -7482,10 +7470,25 @@ proof -
apply (metis (no_types, lifting) document_ptr_kinds_eq_h h' list.set_intros(1)
local.set_disconnected_nodes_get_disconnected_nodes select_result_I2)
apply(simp add: object_ptr_kinds_eq_h)
by (metis (no_types, lifting) ObjectMonad.ptr_kinds_ptr_kinds_M
\<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 h' list.set_intros(2)
local.set_disconnected_nodes_get_disconnected_nodes 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'"
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>
@ -7595,7 +7598,7 @@ proof -
"\<And>doc_ptr disc_nodes. doc_ptr \<noteq> new_document_ptr
\<Longrightarrow> h \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes = h' \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes"
using get_disconnected_nodes_reads h' get_disconnected_nodes_new_document_different_pointers new_document_ptr
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
by (metis(full_types) \<open>\<And>thesis. (\<And>new_document_ptr.
\<lbrakk>h \<turnstile> new_document \<rightarrow>\<^sub>r new_document_ptr; h \<turnstile> new_document \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>
local.get_disconnected_nodes_new_document_different_pointers new_document_ptr)+
@ -7645,22 +7648,20 @@ proof -
have "a_all_ptrs_in_heap h"
using \<open>heap_is_wellformed h\<close> by (simp add: heap_is_wellformed_def)
then have "a_all_ptrs_in_heap h'"
then have "a_all_ptrs_in_heap h'"
apply(auto simp add: a_all_ptrs_in_heap_def)[1]
apply (metis ObjectMonad.ptr_kinds_ptr_kinds_M
\<open>cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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_document_ptr \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close>
\<open>parent_child_rel h = parent_child_rel h'\<close> assms(1) children_eq fset_of_list_elem
local.heap_is_wellformed_children_in_heap local.parent_child_rel_child
local.parent_child_rel_parent_in_heap node_ptr_kinds_eq)
by (metis (no_types, lifting) ObjectMonad.ptr_kinds_ptr_kinds_M
\<open>cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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_document_ptr \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close>
\<open>h' \<turnstile> get_child_nodes (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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_document_ptr) \<rightarrow>\<^sub>r []\<close>
\<open>parent_child_rel h = parent_child_rel h'\<close> assms(1) disconnected_nodes_eq_h
fset_of_list_elem h' local.heap_is_wellformed_disc_nodes_in_heap
local.new_document_no_disconnected_nodes local.parent_child_rel_child
local.parent_child_rel_parent_in_heap new_document_ptr node_ptr_kinds_eq
select_result_I2)
using ObjectMonad.ptr_kinds_ptr_kinds_M
\<open>cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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_document_ptr \<notin> set |h \<turnstile> object_ptr_kinds_M|\<^sub>r\<close>
\<open>parent_child_rel h = parent_child_rel h'\<close> assms(1) children_eq fset_of_list_elem
local.heap_is_wellformed_children_in_heap local.parent_child_rel_child
local.parent_child_rel_parent_in_heap node_ptr_kinds_eq
apply (metis (no_types, lifting) \<open>h' \<turnstile> get_child_nodes (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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_document_ptr) \<rightarrow>\<^sub>r []\<close>
children_eq2 finite_set_in finsert_iff funion_finsert_right object_ptr_kinds_eq select_result_I2 subsetD sup_bot.right_neutral)
by (metis (no_types, lifting) \<open>cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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_document_ptr |\<notin>| object_ptr_kinds h\<close>
\<open>h' \<turnstile> get_child_nodes (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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_document_ptr) \<rightarrow>\<^sub>r []\<close>
\<open>h' \<turnstile> get_disconnected_nodes new_document_ptr \<rightarrow>\<^sub>r []\<close> \<open>parent_child_rel h = parent_child_rel h'\<close> \<open>type_wf h'\<close> assms(1) disconnected_nodes_eq_h local.get_disconnected_nodes_ok
local.heap_is_wellformed_disc_nodes_in_heap local.parent_child_rel_child local.parent_child_rel_parent_in_heap
node_ptr_kinds_eq returns_result_select_result select_result_I2)
have "a_distinct_lists h"
using \<open>heap_is_wellformed h\<close>
by (simp add: heap_is_wellformed_def)
@ -7729,12 +7730,7 @@ proof -
then have "a_owner_document_valid h'"
apply(auto simp add: a_owner_document_valid_def)[1]
by (metis \<open>cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^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_document_ptr |\<notin>| object_ptr_kinds h\<close>
\<open>new_document_ptr |\<notin>| document_ptr_kinds h\<close> assms(3) assms(4) children_eq
children_eq2 disconnected_nodes_eq2_h disconnected_nodes_eq_h
is_OK_returns_result_E is_OK_returns_result_I local.get_child_nodes_ok
local.get_child_nodes_ptr_in_heap local.get_disconnected_nodes_ok
local.get_disconnected_nodes_ptr_in_heap local.known_ptrs_known_ptr node_ptr_kinds_eq)
children_eq2 disconnected_nodes_eq2_h document_ptr_kinds_commutes finite_set_in funion_iff node_ptr_kinds_eq object_ptr_kinds_eq)
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>
by(simp add: heap_is_wellformed_def)

2
Core_DOM/Core_DOM/standard/classes/ElementClass.thy
View File

@ -156,7 +156,7 @@ lemma get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_type_wf:
using l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_axioms assms
apply(simp add: type_wf_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
by (metis NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf bind_eq_None_conv element_ptr_kinds_commutes notin_fset
option.distinct(1))
option.distinct(1))
end
global_interpretation l_get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas type_wf