hatsugai

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

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

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

open Printf
open Ddsv

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

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 Ddsv

type shared_vars = {
    x : int;
    t1 : int;
    t2 : int;
    a1 : int;
    a2 : int;
}

hatsugai

(use gauche.threads)

(define (amb . xs)
  (call/cc
    (lambda (k)
      (if (null? xs)
          ((thread-specific (current-thread)) #f)
          (begin
            (for-each
              (lambda (x)

hatsugai

theory Dominators imports Main begin

typedecl node

axiomatization
  s0 :: "node" and
  R :: "node rel"
where
  reachable: "ALL n. (s0, n) : R^*"

hatsugai

theory X imports Complex_Main begin

consts a :: "nat => real"

theorem
  "k > 0 ==>
   (ALL e. e > 0 --> (EX N1. (ALL n. n > N1 --> abs (a n - b) < e)))
 = (ALL e. e > 0 --> (EX N2. (ALL n. n > N2 --> abs (a n - b) < k * e)))"
apply(rule iffI)
apply(rule allI)

hatsugai

(* Isabelle/HOL 2014 *)
theory "greedy_section" imports Main begin

definition sound :: "(nat * nat) set => bool" where
  "sound X = (ALL p. p : X --> fst p < snd p)"

inductive_set greedy :: "(nat * nat) set => (nat * nat) list set"
  for A :: "(nat * nat) set"
  where
  greedy_base:

hatsugai

theory subseq imports "~~/src/HOL/Hoare/Hoare_Logic" begin

definition is_subseq :: "'a list => 'a list => bool" where
  "is_subseq xs ys ==
    (\<exists>c.
      (\<forall>i. i + 1 < length ys --> c i < c (i + 1))
    \<and> (length ys > 0 \<longrightarrow> c (length ys - 1) < length xs)
    \<and> (\<forall>i. i < length ys \<longrightarrow> ys ! i = xs ! (c i)))"

fun is_subseq2 :: "'a list => 'a list => bool" where