Code

Implement the algorithm#4

Code

Draft

jeltsch wants to merge 32 commits intomasterjeltsch/order-maintenance-correctness:masterfrom enhancement/algorithmjeltsch/order-maintenance-correctness:enhancement/algorithmCopy head branch name to clipboard

+293

Commits

Commits on Feb 9, 2021

• Add first bits of core data structure support

  jeltsch

  committed
  11134e2

• Simplify the non-emptiness proof for element_labeling

  Show description for 082ec01
  jeltsch

  committed
  082ec01

• Switch to using the Lifting and the Transfer package

  Show description for 5d8199a
  jeltsch

  committed
  5d8199a

• Prove that element_of and label_of are mutual inverses

  jeltsch

  committed
  d741d76

• Fix index calculation in lowest_common_ancestor

  jeltsch

  committed
  7adae88

• Simplify the definition of lowest_common_ancestor

  Show description for 63c4d68
  jeltsch

  committed
  63c4d68

• Switch to consistent use of Isar syntax

  Show description for 4cefdbd
  jeltsch

  committed
  4cefdbd

• Move index to a better position

  jeltsch

  committed
  958c0f9

• Fix the naming of labels in the definition of index

  jeltsch

  committed
  d43377f

• Rename index index_at_height

  jeltsch

  committed
  444a16b

Commits on Feb 10, 2021

• Introduce vertex type

  Show description for e8d7c99
  jeltsch

  committed
  e8d7c99

• Fix parent_graph_is_acyclic

  Show description for 2e39598
  jeltsch

  committed
  2e39598

• Fix mix-up of i₁ with h₂ in lowest_common_ancestor

  jeltsch

  committed
  92744fd

Commits on Feb 14, 2021

• Improve proof for lowest_common_ancestor

  jeltsch

  committed
  549b333

• Add is_child_of

  jeltsch

  committed
  0eca301

• Replace parent lemma by is_child_of lemmas

  jeltsch

  committed
  d58e4e5

• Make vertex an instance of semilattice_sup

  jeltsch

  committed
  652c99a

• Make totality of sup_vertex explicit

  jeltsch

  committed
  8c1da1c

• Improve names of some is_child_of lemmas

  jeltsch

  committed
  b05bea7

Commits on Feb 15, 2021

• Remove the domintros option for sup_vertex

  Show description for c7a0b17
  jeltsch

  committed
  c7a0b17

Commits on Feb 24, 2021

• Add leaves

  jeltsch

  committed
  d390026

Commits on Mar 2, 2021

• Add support for fresh element generation

  jeltsch

  committed
  560a7eb

• Add support for relabeling states

  jeltsch

  committed
  0583194

• Add support for states

  jeltsch

  committed
  729365a

Commits on Mar 8, 2021

• Rename Foundations to Data_Structure

  jeltsch

  committed
  8596aaf

• Improve the proof of fresh_element_is_fresh

  jeltsch

  committed
  8eb4438

Commits on Mar 9, 2021

• Merge branch 'enhancement/data-structure' into enhancement/algorithm

  jeltsch

  committed
  51cd480

• Add first bits of the algorithm implementation

  jeltsch

  committed
  fbc289a

Commits on Mar 12, 2021

• Replace fun by primrec

  jeltsch

  committed
  adb4e7d

• Merge branch 'enhancement/core-data-structures' into enhancement/algorithm

  jeltsch

  committed
  177f52c

• Replace fun by primrec

  jeltsch

  committed
  af8736d

Commits on Apr 25, 2021

• Merge branch 'master' into enhancement/algorithm

  jeltsch

  committed
  0463001