src/Sequents/ILL/ILL_predlog.thy
author wenzelm
Sun, 18 Sep 2005 15:20:08 +0200
changeset 17481 75166ebb619b
parent 14854 61bdf2ae4dc5
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     1
(* $Id$ *)
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     2
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     3
theory ILL_predlog
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     4
imports ILL
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     5
begin
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     6
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     7
typedecl plf
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     8
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     9
consts
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    10
  "&"   :: "[plf,plf] => plf"   (infixr 35)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    11
  "|"   :: "[plf,plf] => plf"   (infixr 35)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    12
  ">"   :: "[plf,plf] => plf"   (infixr 35)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    13
  "="   :: "[plf,plf] => plf"   (infixr 35)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    14
  "@NG" :: "plf => plf"   ("- _ " [50] 55)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    15
  ff    :: "plf"
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    16
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    17
  PL    :: "plf => o"      ("[* / _ / *]" [] 100)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    18
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    19
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    20
translations
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    21
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    22
  "[* A & B *]" == "[*A*] && [*B*]"
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    23
  "[* A | B *]" == "![*A*] ++ ![*B*]"
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    24
  "[* - A *]"   == "[*A > ff*]"
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    25
  "[* ff *]"    == "0"
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    26
  "[* A = B *]" => "[* (A > B) & (B > A) *]"
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    27
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    28
  "[* A > B *]" == "![*A*] -o [*B*]"
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    29
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    30
(* another translations for linear implication:
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    31
  "[* A > B *]" == "!([*A*] -o [*B*])" *)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    32
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    33
end