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)

kyodaisuu

#!/usr/bin/python
# coding: utf-8
# Print Graham's number
# 
# Just a code for showing definition.
# It causes runtime error of maximum recursion.

def G(n):
    # G function of Graham's number
    if n == 0:

SekiT

data FizzDataType : Type where
  FizzData : FizzDataType

data BuzzDataType : Type where
  BuzzData : BuzzDataType

data FizzBuzzDataType : Type where
  FizzBuzzData : FizzBuzzDataType

data NatDataType : (n : Nat) -> Type where

egisatoshi

concat (matchAll (["akira", "susumu", "tamotsu", "tomo"], ["blue", "green", "red", "white"], [1, 2, 3, 4])
              as (list something, multiset something, multiset something) with
          | ([$x_1, $x_2, $x_3, $x_4], [$y_1, $y_2, $y_3, $y_4], [$z_1, $z_2, $z_3, $z_4])
          -> matchAll [(x_1, y_1, z_1), (x_2, y_2, z_2), (x_3, y_3, z_3), (x_4, y_4, z_4)]
                   as set (eq, eq, eq) with
               | (#"akira", #"blue", !#1) ::
                 (#"susumu", !#"green", !#4) ::
                 (_, #"red", #2) ::
                 (_, #"white", $n) ::
                 (#"tamotsu", _, #(n - 1)) :: _

ksk

(* Zagier's one-sentence proof for the two-square theorem in Coq (SSReflect) *)
(* - D. Zagier, "A One-Sentence Proof That Every Prime p \equiv 1 (\mod 4) Is a Sum of Two Squares", 
     The American Mathematical Monthly, Vol. 97, No. 2 (Feb., 1990), p. 144 *)

Set Implicit Arguments. Unset Strict Implicit.
From mathcomp Require Import all_ssreflect.

Lemma odd_fixedpoints {X:eqType} (f:X->X) (D:seq X):
  uniq D -> (forall x, x \in D -> (f x \in D) && (f (f x) == x)) ->
  odd (size D) <-> odd (count [pred x | f x == x] D).