src/HOL/Prolog/Type.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (20 months ago) changeset 67022 49309fe530fd parent 63167 0909deb8059b child 67613 ce654b0e6d69 permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
```     1 (*  Title:    HOL/Prolog/Type.thy
```
```     2     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
```
```     3 *)
```
```     4
```
```     5 section \<open>Type inference\<close>
```
```     6
```
```     7 theory Type
```
```     8 imports Func
```
```     9 begin
```
```    10
```
```    11 typedecl ty
```
```    12
```
```    13 axiomatization
```
```    14   bool    :: ty and
```
```    15   nat     :: ty and
```
```    16   arrow   :: "ty => ty => ty"       (infixr "->" 20) and
```
```    17   typeof  :: "[tm, ty] => bool" and
```
```    18   anyterm :: tm
```
```    19 where common_typeof:   "
```
```    20 typeof (app M N) B       :- typeof M (A -> B) & typeof N A..
```
```    21
```
```    22 typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
```
```    23 typeof (fix F)   A       :- (!x. typeof x A => typeof (F  x) A)..
```
```    24
```
```    25 typeof true  bool..
```
```    26 typeof false bool..
```
```    27 typeof (M and N) bool :- typeof M bool & typeof N bool..
```
```    28
```
```    29 typeof (M eq  N) bool :- typeof M T    & typeof N T   ..
```
```    30
```
```    31 typeof  Z    nat..
```
```    32 typeof (S N) nat :- typeof N nat..
```
```    33 typeof (M + N) nat :- typeof M nat & typeof N nat..
```
```    34 typeof (M - N) nat :- typeof M nat & typeof N nat..
```
```    35 typeof (M * N) nat :- typeof M nat & typeof N nat"
```
```    36
```
```    37 axiomatization where good_typeof:     "
```
```    38 typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
```
```    39
```
```    40 axiomatization where bad1_typeof:     "
```
```    41 typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
```
```    42
```
```    43 axiomatization where bad2_typeof:     "
```
```    44 typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
```
```    45
```
```    46
```
```    47 lemmas prog_Type = prog_Func good_typeof common_typeof
```
```    48
```
```    49 schematic_goal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
```
```    50   apply (prolog prog_Type)
```
```    51   done
```
```    52
```
```    53 schematic_goal "typeof (fix (%x. x)) ?T"
```
```    54   apply (prolog prog_Type)
```
```    55   done
```
```    56
```
```    57 schematic_goal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
```
```    58   apply (prolog prog_Type)
```
```    59   done
```
```    60
```
```    61 schematic_goal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
```
```    62   (n * (app fact (n - (S Z))))))) ?T"
```
```    63   apply (prolog prog_Type)
```
```    64   done
```
```    65
```
```    66 schematic_goal "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
```
```    67   apply (prolog prog_Type)
```
```    68   done
```
```    69
```
```    70 schematic_goal "typeof (abs(%v. Z)) ?T"
```
```    71   apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
```
```    72   done
```
```    73
```
```    74 schematic_goal "typeof (abs(%v. Z)) ?T"
```
```    75   apply (prolog bad1_typeof common_typeof)
```
```    76   back (* 2nd result (?A1 -> ?A1) wrong *)
```
```    77   done
```
```    78
```
```    79 schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T"
```
```    80   apply (prolog prog_Type)?  (*correctly fails*)
```
```    81   oops
```
```    82
```
```    83 schematic_goal "typeof (abs(%v. abs(%v. app v v))) ?T"
```
```    84   apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
```
```    85   done
```
```    86
```
```    87 end
```