Theory vertex_example_simps

theory vertex_example_simps
imports "Lib/FiniteGraph" TopoS_Vertices
begin
(*<*)
― ‹The follwoing lemmata are used in the @{text "∃"}-style uniqueness proof›
lemma False_set: "{(e1, e2). False} = {}" by blast
lemma succ_tran_empty: "(succ_tran ⦇nodes = V, edges = {}⦈ v) = {}"
  by(simp add: succ_tran_def)
lemma vertex_1_vertex_2_set_simp: "{vertex_1, vertex_2, vertex_1, vertex_2} = {vertex_1, vertex_2}" by blast
lemma unique_default_example1: "succ_tran ⦇nodes = {vertex_1, vertex_2}, edges = {(vertex_1, vertex_2)}⦈ vertex_1 = {vertex_2}"
apply (simp add: succ_tran_def)
by (metis (lifting, no_types) Collect_cong Range.intros Range_empty Range_insert mem_Collect_eq singleton_conv singleton_iff trancl.r_into_trancl trancl_range)
lemma unique_default_example2: "succ_tran ⦇nodes = {vertex_1, vertex_2}, edges = {(vertex_2, vertex_1)}⦈ vertex_1 = {}"
apply (simp add: succ_tran_def)
by (metis Domain.DomainI Domain_empty Domain_insert distinct_vertices12 singleton_iff trancl_domain)
lemma unique_default_example3: "succ_tran ⦇nodes = {vertex_1, vertex_2}, edges = {(vertex_2, vertex_1)}⦈ vertex_2 = {vertex_1}"
apply (simp add: succ_tran_def)
by (metis (lifting, no_types) Collect_cong Range.intros Range_empty Range_insert mem_Collect_eq singleton_conv singleton_iff trancl.r_into_trancl trancl_range)
lemma unique_default_example_simp1: "{(e1, e2). e1 = vertex_1 ∧ e2 = vertex_2 ∧ (e1 = vertex_1 ⟶ e2 ≠ vertex_2)} = {}" by blast
lemma unique_default_example_simp2: "{(vertex_1, vertex_2)}⇧+ = {(vertex_1, vertex_2)}"
  apply(rule)
   apply(rule)
   apply(clarify)
   apply(rule_tac P="λ a b. a = vertex_1 ∧ b = vertex_2" in trancl.induct)
     apply auto
done
lemma unique_default_example_simp3: "{(e1, e2). e1 = vertex_2 ∧ e2 = vertex_1 ∧ (e1 = vertex_2 ⟶ e2 ≠ vertex_1)} = {}" 
  by(blast)
lemma vertex_set_simp2: "{vertex_2, vertex_1, vertex_2} = {vertex_1, vertex_2}" by blast
lemma canAccessThis_simp1: "canAccessThis ≠ vertex_1 ⟹ succ_tran ⦇nodes = {vertex_1, canAccessThis}, edges = {(vertex_1, canAccessThis)}⦈ vertex_1 = {canAccessThis}"
apply (simp add: succ_tran_def)
by (metis (lifting, no_types) Collect_cong Range.intros Range_empty Range_insert mem_Collect_eq singleton_conv singleton_iff trancl.r_into_trancl trancl_range)
lemma canAccessThis_simp2: "canAccessThis ≠ vertex_1 ⟹ succ_tran ⦇nodes = {vertex_1, canAccessThis}, edges = {(vertex_1, canAccessThis)}⦈ canAccessThis = {}"
apply (simp add: succ_tran_def)
by (metis Domain.DomainI Domain_empty Domain_insert singleton_iff trancl_domain)
lemma canAccessThis_simp3: 
  "canAccessThis ≠ vertex_1 ⟹ {(e1, e2). e1 = vertex_1 ∧ e2 = canAccessThis ∧ (e1 = vertex_1 ⟶ e2 ≠ canAccessThis)} = {}" by blast
lemma canAccessThis_simp4: 
  "canAccessThis ≠ vertex_1 ⟹ {vertex_1, canAccessThis, vertex_1, canAccessThis} = {vertex_1, canAccessThis}" by blast
lemmas example_simps = unique_default_example_simp1 unique_default_example2 unique_default_example3 
    unique_default_example_simp2 unique_default_example1 succ_tran_empty vertex_1_vertex_2_set_simp
    unique_default_example_simp3 vertex_set_simp2 canAccessThis_simp1 canAccessThis_simp2 canAccessThis_simp3
    canAccessThis_simp4
(*>*)
end