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

Renamed use _step suffix rather than _thesis.

This commit is contained in:
Michael Herzberg 2020-05-12 16:16:03 +01:00
parent c044d5fd86
commit 4ed7af1ec9
2 changed files with 12 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -4239,7 +4239,7 @@ locale l_adopt_node_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\
l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin begin
lemma adopt_node_removes_child: lemma adopt_node_removes_child_step:
assumes wellformed: "heap_is_wellformed h" assumes wellformed: "heap_is_wellformed h"
and adopt_node: "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h2" and adopt_node: "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h2"
and children: "h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children" and children: "h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
@ -4286,12 +4286,12 @@ proof -
qed qed
qed qed
lemma adopt_node_removes_child_thesis: lemma adopt_node_removes_child:
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
assumes "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h'" assumes "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h'"
shows "\<And>ptr' children'. shows "\<And>ptr' children'.
h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children' \<Longrightarrow> node_ptr \<notin> set children'" h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children' \<Longrightarrow> node_ptr \<notin> set children'"
using adopt_node_removes_child assms by blast using adopt_node_removes_child_step assms by blast
lemma adopt_node_preserves_wellformedness: lemma adopt_node_preserves_wellformedness:
assumes "heap_is_wellformed h" assumes "heap_is_wellformed h"
@ -5035,7 +5035,7 @@ locale l_insert_before_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub
l_get_owner_document_wf l_get_owner_document_wf
begin begin
lemma insert_before_preserves_acyclitity_thesis: lemma insert_before_preserves_acyclitity:
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
assumes "h \<turnstile> insert_before ptr node child \<rightarrow>\<^sub>h h'" assumes "h \<turnstile> insert_before ptr node child \<rightarrow>\<^sub>h h'"
shows "acyclic (parent_child_rel h')" shows "acyclic (parent_child_rel h')"
@ -5736,7 +5736,7 @@ proof -
by (simp add: heap_is_wellformed_def) by (simp add: heap_is_wellformed_def)
qed qed
lemma adopt_node_children_remain_distinct_thesis: lemma adopt_node_children_remain_distinct:
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
assumes "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h'" assumes "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h'"
shows "\<And>ptr' children'. shows "\<And>ptr' children'.
@ -5745,7 +5745,7 @@ shows "\<And>ptr' children'.
by blast by blast
lemma insert_node_children_remain_distinct_thesis: lemma insert_node_children_remain_distinct:
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
assumes "h \<turnstile> a_insert_node ptr new_child reference_child_opt \<rightarrow>\<^sub>h h'" assumes "h \<turnstile> a_insert_node ptr new_child reference_child_opt \<rightarrow>\<^sub>h h'"
assumes "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children" assumes "h \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
@ -5768,7 +5768,7 @@ proof -
using assms(5) assms(6) insert_before_list_distinct returns_result_eq by fastforce using assms(5) assms(6) insert_before_list_distinct returns_result_eq by fastforce
qed qed
lemma insert_before_children_remain_distinct_thesis: lemma insert_before_children_remain_distinct:
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
assumes "h \<turnstile> insert_before ptr new_child child_opt \<rightarrow>\<^sub>h h'" assumes "h \<turnstile> insert_before ptr new_child child_opt \<rightarrow>\<^sub>h h'"
shows "\<And>ptr' children'. shows "\<And>ptr' children'.
@ -5795,7 +5795,7 @@ proof -
have "\<And>ptr children. h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children have "\<And>ptr children. h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
\<Longrightarrow> distinct children" \<Longrightarrow> distinct children"
using adopt_node_children_remain_distinct_thesis using adopt_node_children_remain_distinct
using assms(1) assms(2) assms(3) h2 using assms(1) assms(2) assms(3) h2
by blast by blast
moreover have "\<And>ptr children. h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children moreover have "\<And>ptr children. h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children
@ -5814,7 +5814,7 @@ proof -
qed qed
lemma insert_before_removes_child_thesis: lemma insert_before_removes_child:
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
assumes "h \<turnstile> insert_before ptr node child \<rightarrow>\<^sub>h h'" assumes "h \<turnstile> insert_before ptr node child \<rightarrow>\<^sub>h h'"
assumes "ptr \<noteq> ptr'" assumes "ptr \<noteq> ptr'"

6
Core_DOM/Core_SC_DOM/scope_components/Core_DOM_Heap_WF.thy
View File

@ -4242,7 +4242,7 @@ locale l_adopt_node_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\
l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin begin
lemma adopt_node_removes_child: lemma adopt_node_removes_child_step:
assumes wellformed: "heap_is_wellformed h" assumes wellformed: "heap_is_wellformed h"
and adopt_node: "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h2" and adopt_node: "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h2"
and children: "h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children" and children: "h2 \<turnstile> get_child_nodes ptr \<rightarrow>\<^sub>r children"
@ -4289,12 +4289,12 @@ proof -
qed qed
qed qed
lemma adopt_node_removes_child_thesis: lemma adopt_node_removes_child:
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h" assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
assumes "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h'" assumes "h \<turnstile> adopt_node owner_document node_ptr \<rightarrow>\<^sub>h h'"
shows "\<And>ptr' children'. shows "\<And>ptr' children'.
h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children' \<Longrightarrow> node_ptr \<notin> set children'" h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children' \<Longrightarrow> node_ptr \<notin> set children'"
using adopt_node_removes_child assms by blast using adopt_node_removes_child_step assms by blast
lemma adopt_node_preserves_wellformedness: lemma adopt_node_preserves_wellformedness:
assumes "heap_is_wellformed h" assumes "heap_is_wellformed h"