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

open Printf

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

module IntSetHash =

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

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