isabelle: src/HOL/MiniML/MiniML.ML@946efd210837 (annotated)

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";

author	nipkow
	Mon, 20 May 1996 18:41:55 +0200
changeset 1751	946efd210837
parent 1743	f7feaacd33d3
child 2031	03a843f0f447
permissions	-rw-r--r--