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

(* 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 &

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

(*
  SICP 3.5.2

  Isabele 2014
*)
theory Stream4 imports Main begin

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

primcorec

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

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