hatsugai

(* Isabelle 2014 *)

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

theorem "(ALL i j. i < length b & j < length b & i ~= j --> b!i ~= b!j)
= (ALL i. 1 <= i & i < length b --> (ALL j. j < i --> b!i ~= b!j))"
apply(auto)
by (metis Suc_le_eq gr0_conv_Suc linorder_neqE_nat old.nat.exhaust)

theorem "(ALL i j. i < length b & j < length b & i ~= j --> b!i ~= b!j)

hatsugai

(*
  Tarski's fixed-point theorem on sets (complete lattice)
  Isabelle 2014
*)
theory Tarski imports Main begin

lemma fp1: "mono F ==> F (Inter {X. F X <= X}) <= Inter {X. F X <= X}"
apply(rule subsetI)
apply(rule InterI)
apply(simp)

hatsugai

open Printf

module IntSet =
  Set.Make (
      struct
        type t = int
        let compare = compare
      end)

module IntSetHash =

hatsugai

(* Isabelle 2014 *)

theory RtranclInductRev imports Main begin

lemma rtrancl_induct2_sub: "(x, y) : r^* ==>
  (ALL a. P a a) --> (ALL a b c. (a, b) : r & (b, c) : r^* & P b c --> P a c) --> P x y"
apply(drule rtrancl_converseI)
apply(erule rtrancl.induct)
apply(auto)
apply(rotate_tac 3)

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)