src/HOL/Prolog/Type.thy
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 21425 c11ab38b78a7
child 34974 18b41bba42b5
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
     1 (*  Title:    HOL/Prolog/Type.thy
     2     ID:       $Id$
     3     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     4 *)
     5 
     6 header {* Type inference *}
     7 
     8 theory Type
     9 imports Func
    10 begin
    11 
    12 typedecl ty
    13 
    14 consts
    15   bool    :: ty
    16   nat     :: ty
    17   arrow   :: "ty => ty => ty"       (infixr "->" 20)
    18   typeof  :: "[tm, ty] => bool"
    19   anyterm :: tm
    20 
    21 axioms  common_typeof:   "
    22 typeof (app M N) B       :- typeof M (A -> B) & typeof N A..
    23 
    24 typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
    25 typeof (fix F)   A       :- (!x. typeof x A => typeof (F  x) A)..
    26 
    27 typeof true  bool..
    28 typeof false bool..
    29 typeof (M and N) bool :- typeof M bool & typeof N bool..
    30 
    31 typeof (M eq  N) bool :- typeof M T    & typeof N T   ..
    32 
    33 typeof  Z    nat..
    34 typeof (S N) nat :- typeof N nat..
    35 typeof (M + N) nat :- typeof M nat & typeof N nat..
    36 typeof (M - N) nat :- typeof M nat & typeof N nat..
    37 typeof (M * N) nat :- typeof M nat & typeof N nat"
    38 
    39 axioms good_typeof:     "
    40 typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
    41 
    42 axioms bad1_typeof:     "
    43 typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
    44 
    45 axioms bad2_typeof:     "
    46 typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
    47 
    48 
    49 lemmas prog_Type = prog_Func good_typeof common_typeof
    50 
    51 lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
    52   apply (prolog prog_Type)
    53   done
    54 
    55 lemma "typeof (fix (%x. x)) ?T"
    56   apply (prolog prog_Type)
    57   done
    58 
    59 lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
    60   apply (prolog prog_Type)
    61   done
    62 
    63 lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
    64   (n * (app fact (n - (S Z))))))) ?T"
    65   apply (prolog prog_Type)
    66   done
    67 
    68 lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
    69   apply (prolog prog_Type)
    70   done
    71 
    72 lemma "typeof (abs(%v. Z)) ?T"
    73   apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
    74   done
    75 
    76 lemma "typeof (abs(%v. Z)) ?T"
    77   apply (prolog bad1_typeof common_typeof)
    78   back (* 2nd result (?A1 -> ?A1) wrong *)
    79   done
    80 
    81 lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
    82   apply (prolog prog_Type)?  (*correctly fails*)
    83   oops
    84 
    85 lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
    86   apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
    87   done
    88 
    89 end