src/HOL/Main.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (22 months ago)
changeset 66816 212a3334e7da
parent 66614 1f1c5d85d232
child 66817 0b12755ccbb2
permissions -rw-r--r--
more fundamental definition of div and mod on int
wenzelm@65553
     1
section \<open>Main HOL\<close>
wenzelm@65553
     2
wenzelm@65553
     3
text \<open>
wenzelm@65553
     4
  Classical Higher-order Logic -- only ``Main'', excluding real and
wenzelm@65553
     5
  complex numbers etc.
wenzelm@65553
     6
\<close>
wenzelm@65553
     7
wenzelm@65553
     8
theory Main
blanchet@66614
     9
imports Predicate_Compile Quickcheck_Narrowing Extraction Nunchaku BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD
wenzelm@65553
    10
begin
wenzelm@65553
    11
wenzelm@65814
    12
text \<open>
wenzelm@65814
    13
  Classical Higher-order Logic -- only ``Main'', excluding real and
wenzelm@65814
    14
  complex numbers etc.
wenzelm@65814
    15
\<close>
wenzelm@65814
    16
wenzelm@65814
    17
no_notation
wenzelm@65814
    18
  bot ("\<bottom>") and
wenzelm@65814
    19
  top ("\<top>") and
wenzelm@65814
    20
  inf (infixl "\<sqinter>" 70) and
wenzelm@65814
    21
  sup (infixl "\<squnion>" 65) and
wenzelm@65814
    22
  Inf ("\<Sqinter>_" [900] 900) and
wenzelm@65814
    23
  Sup ("\<Squnion>_" [900] 900) and
wenzelm@65814
    24
  ordLeq2 (infix "<=o" 50) and
wenzelm@65814
    25
  ordLeq3 (infix "\<le>o" 50) and
wenzelm@65814
    26
  ordLess2 (infix "<o" 50) and
wenzelm@65814
    27
  ordIso2 (infix "=o" 50) and
wenzelm@65814
    28
  card_of ("|_|") and
wenzelm@65814
    29
  csum (infixr "+c" 65) and
wenzelm@65814
    30
  cprod (infixr "*c" 80) and
wenzelm@65814
    31
  cexp (infixr "^c" 90) and
wenzelm@65814
    32
  convol ("\<langle>(_,/ _)\<rangle>")
wenzelm@65814
    33
wenzelm@65814
    34
hide_const (open)
wenzelm@65814
    35
  czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
wenzelm@65814
    36
  fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
wenzelm@65814
    37
  shift proj id_bnf
wenzelm@65814
    38
wenzelm@65814
    39
hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
wenzelm@65814
    40
wenzelm@65814
    41
no_syntax
wenzelm@65814
    42
  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
wenzelm@65814
    43
  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
wenzelm@65814
    44
  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
wenzelm@65814
    45
  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
wenzelm@65814
    46
wenzelm@65553
    47
end