hatsugai

theory StrongInduction imports Main begin

inductive_set E where
  base: "0 \<in> E"
| step: "n \<in> E \<Longrightarrow> Suc (Suc n) \<in> E"

thm E.induct
(*
  \<lbrakk>?x \<in> E; ?P 0; \<And>n. \<lbrakk>n \<in> E; ?P n\<rbrakk> \<Longrightarrow> ?P (Suc (Suc n))\<rbrakk> \<Longrightarrow> ?P ?x
                      ~~~~~

hatsugai

theory MU_Puzzle imports Main begin

datatype miu = M | I | U

inductive_set S :: "miu list set" where
  "[M, I] : S" |
  "x @ [I] : S ==> x @ [I, U] : S" |
  "[M] @ x : S ==> [M] @ x @ x : S" |
  "x @ [I, I, I] @ y : S ==> x @ [U] @ y : S" |
  "x @ [U, U] @ y : S ==> x @ y : S"

hatsugai

nametype t = 0..1

event P_begin, P_end
event Q_begin, Q_end

channel rd_flag0, wr_flag0 : t
channel rd_flag1, wr_flag1 : t
channel rd_turn, wr_turn : t

VAR(rd, wr, m) =

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

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

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 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

theory Dominators imports Main begin

typedecl node

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

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

open Ddsv

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