Bug.thy

theory Bug
  imports HOL.Argo HOL.Metis ― ‹A minimalistic import for faster propagation of changes in Argo›
begin

lemma
  "¬ subseteq
     (Field (image (apsnd Container) (rel (upd h_ent (Object ob) (single (pair c n))))))
     s'_entities ⟶
   member 
     (w
       (Field (image (apsnd Container)
       (rel (upd h_ent (Object ob) (single (pair c n))))))
       s'_entities)
     (Field (image (apsnd Container) (rel (upd h_ent (Object ob) (single (pair c n)))))) ∧
   ¬ member
       (w 
         (Field (image (apsnd Container)
         (rel (upd h_ent (Object ob) (single (pair c n))))))
         s'_entities)
       s'_entities ⟹
   s'_entities =
     insert (Object ob) (union (image Object objects) (image Container containers)) ⟹
   subseteq
     (Field (image (apsnd Container) (rel (upd h_ent (Object ob) (single (pair c n))))))
     (insert (Object ob) (union (image Object objects) (image Container containers)))"
  apply argo
  oops

― ‹In case only \<^theory>‹HOL.Argo› is imported
⬚‹
typedecl 'a set
consts member :: "'a ⇒ 'a set ⇒ bool" ("_ ∈ _" [51, 51] 50)
consts image :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set" (infixr "`" 90)
›
›

lemma
 "w⇩i = 𝗐⇩i (Object ob) Container containers ⟹
  w⇩i⇩0 = 𝗐⇩i (Object ob) Object objects ⟹
  Object ob ∈ Object ` objects ⟶
    Object ob = Object (𝗐⇩i (Object ob) Object objects) ∧
    𝗐⇩i (Object ob) Object objects ∈ objects ⟹
  Object ob ∈ Container ` containers ⟶
    Object ob = Container (𝗐⇩i (Object ob) Container containers) ∧
    𝗐⇩i (Object ob) Container containers ∈ containers ⟹
  𝗍⇩e (Object ob) = zero ⟹
  𝗍⇩e (Container w⇩i) = one ⟹
  zero ≠ one ⟹
  object (Object w⇩i⇩0) = w⇩i⇩0 ⟹
  object (Object ob) = ob ⟹
  ¬(ob ∈ objects) ⟹
  ¬(Object ob ∈ Object ` objects) ∧ ¬(Object ob ∈ Container ` containers)"
  apply argo apply metis
  oops
end