src/HOL/MiniML/MiniML.ML
author paulson
Fri, 10 May 1996 17:03:17 +0200
changeset 1743 f7feaacd33d3
parent 1525 d127436567d0
child 2031 03a843f0f447
permissions -rw-r--r--
Updated for new form of induction rules
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     1
(* Title:     HOL/MiniML/MiniML.ML
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     2
   ID:        $Id$
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     3
   Author:    Dieter Nazareth and Tobias Nipkow
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     4
   Copyright  1995 TU Muenchen
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     5
*)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     6
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     7
open MiniML;
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     8
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     9
Addsimps has_type.intrs;
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    10
Addsimps [Un_upper1,Un_upper2];
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    11
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    12
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    13
(* has_type is closed w.r.t. substitution *)
1743
f7feaacd33d3 Updated for new form of induction rules
paulson
parents: 1525
diff changeset
    14
goal MiniML.thy "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
f7feaacd33d3 Updated for new form of induction rules
paulson
parents: 1525
diff changeset
    15
by (etac has_type.induct 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    16
(* case VarI *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    17
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    18
by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    19
by( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    20
(* case AbsI *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    21
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    22
(* case AppI *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    23
by (Asm_full_simp_tac 1);
1743
f7feaacd33d3 Updated for new form of induction rules
paulson
parents: 1525
diff changeset
    24
qed "has_type_cl_sub";