Object

definition abbreviation theorem
legend
Object.{u_1, u_2} {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value)
  {L : FirstOrder.Language} [L.Structure ↑h.reachable] {I : Interface ↑h.reachable}
  (C : Class (↑h.reachable) L I) : Type
Show details 
| Object.mk : {Place Value : Type} →
  [inst : TopologicalSpace Place] →
    {h : Heap Place Value} →
      {L : FirstOrder.Language} →
        [inst_1 : L.Structure ↑h.reachable] →
          {I : Interface ↑h.reachable} →
            {C : Class (↑h.reachable) L I} →
              (place : Place) →
                (resides : place ∈ Heap.domain Value) →
                  ⟨Heap.at_ place resides, ⋯⟩ ∈ C.State →
                    (behavior :
                        (m : I.Method) → Behavior L ↑h.reachable ↑(I.input m) ↑(I.output m)) →
                      (∀ (m : I.Method) (pre : Option ↑h.reachable) (i : Option ↑(I.input m))
                          (post : Option ↑h.reachable) (o : Option ↑(I.output m)),
                          Behavior.relation L pre i post o → Behavior.relation L pre i post o) →
                        Object h C

Outer dependencies: Class, Heap, Heap.reachable, Interface

Inner dependencies: Behavior, Heap.mem_reachable

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure, Set, Set.Elem, TopologicalSpace

Lean core dependencies: Eq, HEq, Nat, Option, SizeOf, Subtype, eq_of_heq

Used by: Object.state, doorObject

Object.state.{u_1, u_2} {Place Value : Type} [TopologicalSpace Place] {h : Heap Place Value}
  {L : FirstOrder.Language} [L.Structure ↑h.reachable] {I : Interface ↑h.reachable}
  {C : Class (↑h.reachable) L I} (o : Object h C) : ↑C.State
Show details 
fun {Place Value} [TopologicalSpace Place] {h} {L} [L.Structure ↑h.reachable] {I} {C} o =>
  ⟨⟨Heap.at_ o.place ⋯, ⋯⟩, ⋯⟩

Complexity: 315 (size of the value term)

Outer dependencies: Class, Heap, Heap.reachable, Interface, Object

Inner dependencies: Heap.mem_reachable

Mathlib dependencies: FirstOrder.Language, FirstOrder.Language.Structure, Set, Set.Elem, TopologicalSpace

Used by: (none)

instNonemptyDoorState : Nonempty DoorState
Show details 
Nonempty.intro DoorState.opened

Complexity: 5 (size of the value term)

Outer dependencies: DoorState

Lean core dependencies: Nonempty

Used by: (none)

doorHeap : Heap Bool DoorState
Show details 
{ domain := Set.univ,
  at_ := fun p x =>
    match p, x with
    | true, x => DoorState.opened
    | false, x => DoorState.closed }

Complexity: 99 (size of the value term)

Outer dependencies: DoorState, Heap

Mathlib dependencies: Set, Set.univ

Lean core dependencies: Bool

Used by: doorBehavior, doorClass, doorHeap.closedVal, doorHeap.closed_reachable, doorHeap.openedVal, doorHeap.opened_reachable, doorInterface, doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

doorHeap.opened_reachable : DoorState.opened ∈ doorHeap.reachable
Show details 
Exists.intro true (Exists.intro trivial rfl)

Complexity: 167 (size of the value term)

Dependencies: DoorState, Heap.reachable, doorHeap

Mathlib dependencies: Set

Lean core dependencies: Bool, Eq, Exists, rfl, trivial

Used by: doorHeap.openedVal

doorHeap.closed_reachable : DoorState.closed ∈ doorHeap.reachable
Show details 
Exists.intro false (Exists.intro trivial rfl)

Complexity: 167 (size of the value term)

Dependencies: DoorState, Heap.reachable, doorHeap

Mathlib dependencies: Set

Lean core dependencies: Bool, Eq, Exists, rfl, trivial

Used by: doorHeap.closedVal

doorHeap.openedVal : ↑doorHeap.reachable
Show details 
⟨DoorState.opened, doorHeap.opened_reachable⟩

Complexity: 33 (size of the value term)

Outer dependencies: DoorState, Heap.reachable, doorHeap

Inner dependencies: doorHeap.opened_reachable

Mathlib dependencies: Set, Set.Elem

Lean core dependencies: Bool

Used by: instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass

doorHeap.closedVal : ↑doorHeap.reachable
Show details 
⟨DoorState.closed, doorHeap.closed_reachable⟩

Complexity: 33 (size of the value term)

Outer dependencies: DoorState, Heap.reachable, doorHeap

Inner dependencies: doorHeap.closed_reachable

Mathlib dependencies: Set, Set.Elem

Lean core dependencies: Bool

Used by: (none)

The language of a single unary relation, “is open”.

doorLanguage : FirstOrder.Language
Show details 
{ Functions := fun x => Empty,
  Relations := fun x =>
    match x with
    | 1 => Unit
    | x => Empty }

Complexity: 23 (size of the value term)

Outer dependencies: (none)

Mathlib dependencies: FirstOrder.Language

Lean core dependencies: Empty, Eq, Eq.ndrec_symm, Nat, Not, Unit, Unit.unit, dite

Used by: doorBehavior, doorClass, doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap :
  doorLanguage.Structure ↑doorHeap.reachable
Show details 
{ funMap := fun {x} f x_1 => Empty.elim f,
  RelMap := fun {n} r x =>
    match n, r, x with
    | 1, x, x_1 => ↑(x_1 0) = DoorState.opened
    | 0, r, x => Empty.elim r
    | n.succ.succ, r, x => Empty.elim r }

Complexity: 359 (size of the value term)

Outer dependencies: DoorState, Heap.reachable, doorHeap, doorLanguage

Mathlib dependencies: FirstOrder.Language.Structure, Set, Set.Elem

Lean core dependencies: Bool, Empty.elim, Eq, Fin, Nat

Used by: doorBehavior, doorClass, doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass

doorInterface : Interface ↑doorHeap.reachable
Show details 
{ Method := Unit, input := fun x => {v | ↑v = DoorState.opened},
  output := fun x => {v | ↑v = DoorState.opened} }

Complexity: 157 (size of the value term)

Outer dependencies: DoorState, Heap.reachable, Interface, doorHeap

Mathlib dependencies: Set, Set.Elem, setOf

Lean core dependencies: Bool, Eq, Unit

Used by: doorClass, doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass

doorBehavior :
  Behavior doorLanguage ↑doorHeap.reachable ↑{v | ↑v = DoorState.opened}
    ↑{v | ↑v = DoorState.opened}
Show details 
{
  relation := fun pre x post x_1 =>
    ∃ ps po,
      pre = some ps ∧
        post = some po ∧
          (↑ps = DoorState.opened ∧ ↑po = DoorState.closed ∨
            ↑ps = DoorState.closed ∧ ↑po = DoorState.opened) }

Complexity: 689 (size of the value term)

Outer dependencies: Behavior, DoorState, Heap.reachable, doorHeap, doorLanguage, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

Mathlib dependencies: Set, Set.Elem, setOf

Lean core dependencies: And, Bool, Eq, Exists, Option, Or

Used by: doorClass, doorObject

doorClass : Class (↑doorHeap.reachable) doorLanguage doorInterface
Show details 
{ State := Set.univ, operation := fun x => doorBehavior, autonomous := fun x x_1 => False }

Complexity: 123 (size of the value term)

Outer dependencies: Class, DoorState, Heap.reachable, doorHeap, doorInterface, doorLanguage, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

Inner dependencies: doorBehavior

Mathlib dependencies: Set.Elem, Set.univ

Lean core dependencies: Bool, False

Used by: doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass

instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass : Nonempty ↑doorClass.State
Show details 
Nonempty.intro ⟨doorHeap.openedVal, trivial⟩

Complexity: 149 (size of the value term)

Outer dependencies: DoorState, Heap.reachable, doorClass, doorHeap, doorInterface, doorLanguage, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

Inner dependencies: doorHeap.openedVal

Mathlib dependencies: Set, Set.Elem

Lean core dependencies: Bool, Nonempty, trivial

Used by: (none)

doorObject : Object doorHeap doorClass
Show details 
{ place := true, resides := trivial, member := trivial, behavior := fun x => doorBehavior,
  compatible := ⋯ }

Complexity: 273 (size of the value term)

Outer dependencies: DoorState, Object, doorClass, doorHeap, doorInterface, doorLanguage, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

Inner dependencies: Heap.reachable, doorBehavior

Mathlib dependencies: Set.Elem

Lean core dependencies: Bool, Option, trivial

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionabbreviationtheoremexampledeclared elsewheredependencyproof dependency
legend