gernst

(declare-datatypes ((Nat 0)) (((Z) (S (proj1-S Nat)))))
(declare-datatypes ((list 0))
  (((nil) (cons (head Nat) (tail list)))))
(define-fun-rec
  ==
  ((x Nat) (y Nat)) Bool
  (match x
    ((Z
      (match y
        ((Z true)

gernst

begin

fun mult :: "nat ⇒ nat ⇒ nat" where
"mult x 0 = 0" |
"mult x y = x + mult x (y - 1)"

lemma mult_rec[simp]:
  "y ≠ 0 ⟹ mult x y = x + mult x (y - 1)"
  by (cases y) auto

gernst

theory RegularBehavioralHoareLogic
  imports Main
begin

(* Mechanization of

   Gidon Ernst, Alexander Knapp, and Toby Murray:
   A Hoare Logic with Regular Behavioral Specifications
   submitted to ISoLa 2022

gernst

class Expr:
  def eval(self, state):
    pass

class Var(Expr):
  def __init__(self, name):
    self.name = name

  def eval(self, state):
    return state[name]

gernst

(* using tactics *)
lemma "A ∧ B ⟶ B ∧ A"
  apply (rule impI)  (* A ∧ B ⟹ B ∧ A *)
  apply (rule conjI) (* 1: A ∧ B ⟹ B and 2: A ∧ B ⟹ A *)
(* goal 1 *)
   apply (erule conjE) (* A ⟹ B ⟹ B *)
   apply assumption
(* goal 2 *)
   apply (erule conjE) (* A ⟹ B ⟹ A *)
  apply assumption

gernst

theory Mergesort
  imports Main
begin

fun sorted :: "nat list ⇒ bool" where
"sorted [] = True" |
"sorted (x#[]) = True" |
"sorted (x#y#zs) = (x ≤ y ∧ sorted (y#zs))"

fun merge :: "nat list ⇒ nat list ⇒ nat list" where

gernst

type Elem = int

/*** Specification ***/

trait SpecSet {
  ghost var content: set<Elem>

  method insert(x: Elem)
    modifies this
    ensures content == old(content) + {x}

gernst

// Data types to model the domain
type Key(==) // Keys support equality
type Flags
type Time = nat
type Data

datatype option<T> =
  none | some(get: T)

datatype Entry