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