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