mbrcknl

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
 
{-# OPTIONS_GHC -Wall #-}
 
data HList f l where
  HNil :: HList f '[]

mbrcknl

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilyDependencies #-}

data Ty = IntTy | FunTy Ty Ty

mbrcknl

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}

data Ty = IntTy | FunTy Ty Ty

data Term :: (Ty -> *) -> Ty -> * where
  Lit :: Int -> Term var IntTy

mbrcknl

theory locale_experiment
imports Main
begin

section \<open>Algebraic formulation of a semilattice\<close>

locale semigroup =
  fixes ap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes assoc: "\<And>x y z. ap x (ap y z) = ap (ap x y) z"

mbrcknl

theory Scratch imports Main begin

locale Magma =
  fixes m :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

locale SemiGroup = Magma +
  assumes assoc: "\<And>x y z. m (m x y) z = m x (m y z)"

locale Commutative = Magma +
  assumes comm: "\<And>x y. m x y = m y x"

mbrcknl

Definition p5 : com :=
  WHILE (BNot (BEq (AId X) (ANum 1))) DO
    HAVOC X
  END.

Definition p6 : com :=
  X ::= ANum 1.

Lemma p5_may_terminate: forall s, p5 / s || update s X 1.
  intro s; destruct (eq_nat_dec (s X) 1).

mbrcknl

Require Import List.

Inductive type : Type :=
| base : type
| arr  : type -> type -> type.

Infix "==>" := arr (right associativity, at level 52).

Inductive elem {A: Type} (x: A): list A -> Type :=
| here  : forall xs, elem x (x :: xs)

mbrcknl

Require Import Sorted.
Require Import Permutation.

Definition isSortingFunction (A: Type) (R: A -> A -> Prop) (f: list A -> list A): Prop :=
  forall (xs: list A), Permutation xs (f xs) /\ Sorted R (f xs).

Check (isSortingFunction: forall (A: Type), (A -> A -> Prop) -> (list A -> list A) -> Prop).

mbrcknl

Require Import List.

Inductive type : Type :=
| base : type
| arr  : type -> type -> type.

Infix "==>" := arr (right associativity, at level 52).

Inductive elem {A: Type} (x: A): list A -> Type :=
| here  : forall xs, elem x (x :: xs)

mbrcknl

Fixpoint R (T:ty) (t:tm) {struct T} : Prop :=
  has_type empty t T /\ halts t /\
  match T with
    | TBool  => True
    | TArrow T1 T2 => (forall s, R T1 s -> R T2 (tapp t s))
    | TProd T1 T2 => exists t1, exists t2, t ==>* tpair t1 t2 /\ R T1 t1 /\ R T2 t2
  end.