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