src/HOL/Prolog/HOHH.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 58889 5b7a9633cfa8
child 63167 0909deb8059b
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
oheimb@13208
     1
(*  Title:    HOL/Prolog/HOHH.thy
oheimb@13208
     2
    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
oheimb@13208
     3
*)
oheimb@9015
     4
wenzelm@58889
     5
section {* Higher-order hereditary Harrop formulas *}
wenzelm@17311
     6
wenzelm@17311
     7
theory HOHH
wenzelm@17311
     8
imports HOL
wenzelm@17311
     9
begin
oheimb@9015
    10
wenzelm@48891
    11
ML_file "prolog.ML"
wenzelm@48891
    12
wenzelm@21425
    13
method_setup ptac =
wenzelm@30549
    14
  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
wenzelm@42814
    15
  "basic Lambda Prolog interpreter"
wenzelm@21425
    16
wenzelm@21425
    17
method_setup prolog =
wenzelm@30549
    18
  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
wenzelm@21425
    19
  "Lambda Prolog interpreter"
wenzelm@21425
    20
oheimb@9015
    21
consts
oheimb@9015
    22
wenzelm@17311
    23
(* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A            *)
wenzelm@21425
    24
  Dand        :: "[bool, bool] => bool"         (infixr ".." 28)
wenzelm@21425
    25
  Dif        :: "[bool, bool] => bool"         (infixl ":-" 29)
oheimb@9015
    26
wenzelm@17311
    27
(* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G
wenzelm@17311
    28
                               | True | !x. G | D => G                  *)
wenzelm@21425
    29
(*Dand'         :: "[bool, bool] => bool"         (infixr "," 35)*)
wenzelm@21425
    30
  Dimp          :: "[bool, bool] => bool"         (infixr "=>" 27)
oheimb@9015
    31
oheimb@9015
    32
translations
oheimb@9015
    33
wenzelm@17311
    34
  "D :- G"      =>      "G --> D"
wenzelm@17311
    35
  "D1 .. D2"    =>      "D1 & D2"
wenzelm@17311
    36
(*"G1 , G2"     =>      "G1 & G2"*)
wenzelm@17311
    37
  "D => G"      =>      "D --> G"
oheimb@9015
    38
oheimb@9015
    39
end