hatsugai

open Ddsv

type shared_vars = {
    m : int;
    t1 : int;
    t2 : int;
}

let show_sv r =
  Printf.sprintf "m=%d t1=%d t2=%d" r.m r.t1 r.t2

hatsugai

open Printf
open Ddsv

type shared_vars = {
    mutex : int;
    cv_bits : int;
    cv_state : int;
    cv_old : int list;
    count : int;
}

hatsugai

#include "ddsv.h"

#define NUM_PROCESSES 2

#define MAX_COUNT 1

typedef unsigned prop_t;     /* process id bit */

typedef struct shared_vars {
    int mutex;

hatsugai

import java.util.*;
import java.io.*;

public class Ddsv
{
    abstract class Transition
    {
        int target;
        String label;
        abstract boolean guard(SharedVars s);

hatsugai

theory CoindStudy imports Main begin

codatatype (sset:'a) stream = SCons (shd:'a) (stl:"'a stream")

coinductive_set
  cle :: "(('a::order) stream * 'a stream) set"
where
  cle: "shd s <= shd t & (shd s = shd t --> (stl s, stl t) : cle) ==> (s, t) : cle"

definition

hatsugai

theory IndStudy imports Main begin

codatatype (sset:'a) stream = SCons (shd:'a) (stl:"'a stream")

inductive_set
  nle :: "(('a::order) stream * 'a stream) set"
where
  nle1: "~ shd s <= shd t ==> (s, t) : nle" |
  nle2: "(s, t) : nle ==> (SCons x s, SCons x t) : nle"

hatsugai

theory Stream7 imports Main begin

codatatype (sset:'a) stream = SCons (shd:'a) (stl:"'a stream")

coinductive_set
  cle :: "(('a::order) stream * 'a stream) set"
where
  cle: "shd s <= shd t & (shd s = shd t --> (stl s, stl t) : cle) ==> (s, t) : cle"

inductive_set

hatsugai

(*
  SICP 3.5.2

  Isabele 2014
*)
theory Stream4 imports Main begin

codatatype 'a stream = SCons (shd:'a) (stl:"'a stream")

primcorec

hatsugai

theory Stream3 imports Main begin

codatatype 'a stream = SCons (shd:'a) (stl:"'a stream")

primcorec
  sadd :: "nat stream => nat stream => nat stream"
where
  "sadd s t = SCons (shd s + shd t) (sadd (stl s) (stl t))"

primcorec zeros :: "nat stream" where

hatsugai

(* Isabelle 2014 *)

theory Stream imports Main begin

codatatype 'a stream = SCons (shd:'a) (stl:"'a stream")

coinductive_set
  sle :: "(('a::order) stream * 'a stream) set"
where
  sle: "shd s <= shd t &