src/HOL/Prolog/Type.thy
author wenzelm
Tue, 03 Sep 2013 01:12:40 +0200
changeset 53374 a14d2a854c02
parent 51311 337cfc42c9c8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
tuned proofs -- clarified flow of facts wrt. calculation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13208
965f95a3abd9 added the usual file headers
oheimb
parents: 12338
diff changeset
     1
(*  Title:    HOL/Prolog/Type.thy
965f95a3abd9 added the usual file headers
oheimb
parents: 12338
diff changeset
     2
    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
965f95a3abd9 added the usual file headers
oheimb
parents: 12338
diff changeset
     3
*)
9015
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
     4
17311
5b1d47d920ce converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     5
header {* Type inference *}
9015
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
     6
17311
5b1d47d920ce converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     7
theory Type
5b1d47d920ce converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     8
imports Func
5b1d47d920ce converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     9
begin
9015
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    10
17311
5b1d47d920ce converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    11
typedecl ty
9015
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    12
51311
337cfc42c9c8 eliminated legacy 'axioms';
wenzelm
parents: 36319
diff changeset
    13
axiomatization
337cfc42c9c8 eliminated legacy 'axioms';
wenzelm
parents: 36319
diff changeset
    14
  bool    :: ty and
337cfc42c9c8 eliminated legacy 'axioms';
wenzelm
parents: 36319
diff changeset
    15
  nat     :: ty and
337cfc42c9c8 eliminated legacy 'axioms';
wenzelm
parents: 36319
diff changeset
    16
  arrow   :: "ty => ty => ty"       (infixr "->" 20) and
337cfc42c9c8 eliminated legacy 'axioms';
wenzelm
parents: 36319
diff changeset
    17
  typeof  :: "[tm, ty] => bool" and
17311
5b1d47d920ce converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    18
  anyterm :: tm
51311
337cfc42c9c8 eliminated legacy 'axioms';
wenzelm
parents: 36319
diff changeset
    19
where common_typeof:   "
9015
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    20
typeof (app M N) B       :- typeof M (A -> B) & typeof N A..
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    21
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    22
typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    23
typeof (fix F)   A       :- (!x. typeof x A => typeof (F  x) A)..
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    24
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    25
typeof true  bool..
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    26
typeof false bool..
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    27
typeof (M and N) bool :- typeof M bool & typeof N bool..
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    28
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    29
typeof (M eq  N) bool :- typeof M T    & typeof N T   ..
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    30
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    31
typeof  Z    nat..
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    32
typeof (S N) nat :- typeof N nat..
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    33
typeof (M + N) nat :- typeof M nat & typeof N nat..
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    34
typeof (M - N) nat :- typeof M nat & typeof N nat..
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    35
typeof (M * N) nat :- typeof M nat & typeof N nat"
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    36
51311
337cfc42c9c8 eliminated legacy 'axioms';
wenzelm
parents: 36319
diff changeset
    37
axiomatization where good_typeof:     "
9015
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    38
typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    39
51311
337cfc42c9c8 eliminated legacy 'axioms';
wenzelm
parents: 36319
diff changeset
    40
axiomatization where bad1_typeof:     "
9015
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    41
typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    42
51311
337cfc42c9c8 eliminated legacy 'axioms';
wenzelm
parents: 36319
diff changeset
    43
axiomatization where bad2_typeof:     "
9015
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    44
typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    45
21425
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    46
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    47
lemmas prog_Type = prog_Func good_typeof common_typeof
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    48
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 34974
diff changeset
    49
schematic_lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
21425
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    50
  apply (prolog prog_Type)
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    51
  done
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    52
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 34974
diff changeset
    53
schematic_lemma "typeof (fix (%x. x)) ?T"
21425
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    54
  apply (prolog prog_Type)
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    55
  done
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    56
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 34974
diff changeset
    57
schematic_lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
21425
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    58
  apply (prolog prog_Type)
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    59
  done
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    60
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 34974
diff changeset
    61
schematic_lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
21425
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    62
  (n * (app fact (n - (S Z))))))) ?T"
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    63
  apply (prolog prog_Type)
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    64
  done
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    65
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 34974
diff changeset
    66
schematic_lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
21425
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    67
  apply (prolog prog_Type)
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    68
  done
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    69
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 34974
diff changeset
    70
schematic_lemma "typeof (abs(%v. Z)) ?T"
21425
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    71
  apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    72
  done
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    73
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 34974
diff changeset
    74
schematic_lemma "typeof (abs(%v. Z)) ?T"
21425
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    75
  apply (prolog bad1_typeof common_typeof)
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    76
  back (* 2nd result (?A1 -> ?A1) wrong *)
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    77
  done
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    78
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 34974
diff changeset
    79
schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
21425
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    80
  apply (prolog prog_Type)?  (*correctly fails*)
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    81
  oops
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    82
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 34974
diff changeset
    83
schematic_lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
21425
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    84
  apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 17311
diff changeset
    85
  done
17311
5b1d47d920ce converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    86
9015
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
    87
end