src/HOL/Prolog/HOHH.thy
 author paulson 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!
```     1 (*  Title:    HOL/Prolog/HOHH.thy
```
```     2     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
```
```     3 *)
```
```     4
```
```     5 section {* Higher-order hereditary Harrop formulas *}
```
```     6
```
```     7 theory HOHH
```
```     8 imports HOL
```
```     9 begin
```
```    10
```
```    11 ML_file "prolog.ML"
```
```    12
```
```    13 method_setup ptac =
```
```    14   {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
```
```    15   "basic Lambda Prolog interpreter"
```
```    16
```
```    17 method_setup prolog =
```
```    18   {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
```
```    19   "Lambda Prolog interpreter"
```
```    20
```
```    21 consts
```
```    22
```
```    23 (* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A            *)
```
```    24   Dand        :: "[bool, bool] => bool"         (infixr ".." 28)
```
```    25   Dif        :: "[bool, bool] => bool"         (infixl ":-" 29)
```
```    26
```
```    27 (* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G
```
```    28                                | True | !x. G | D => G                  *)
```
```    29 (*Dand'         :: "[bool, bool] => bool"         (infixr "," 35)*)
```
```    30   Dimp          :: "[bool, bool] => bool"         (infixr "=>" 27)
```
```    31
```
```    32 translations
```
```    33
```
```    34   "D :- G"      =>      "G --> D"
```
```    35   "D1 .. D2"    =>      "D1 & D2"
```
```    36 (*"G1 , G2"     =>      "G1 & G2"*)
```
```    37   "D => G"      =>      "D --> G"
```
```    38
```
```    39 end
```