isabelle: src/HOL/W0/Type.thy@8b2eafed6183 (annotated)

2520 aecaa76e7eff Incorporated Larry's changes. nipkow parents: 2518 diff changeset	1	(* Title: HOL/W0/Type.thy
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	2	ID: $Id$
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	3	Author: Dieter Nazareth and Tobias Nipkow
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	4	Copyright 1995 TU Muenchen
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	5
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	6	MiniML-types and type substitutions.
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	7	*)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	8
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	9	Type = Maybe +
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	10
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	11	(* new class for structures containing type variables *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	12	classes
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	13	type_struct < term
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	14
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	15	(* type expressions *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	16	datatype
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	17	typ = TVar nat \| "->" typ typ (infixr 70)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	18
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	19	(* type variable substitution *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	20	types
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	21	subst = nat => typ
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	22
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	23	arities
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	24	typ::type_struct
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	25	list::(type_struct)type_struct
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	26	fun::(term,type_struct)type_struct
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	27
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	28	(* substitutions *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	29
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	30	(* identity *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	31	constdefs
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	32	id_subst :: subst
3842 b55686a7b22c fixed dots; wenzelm parents: 2520 diff changeset	33	"id_subst == (%n. TVar n)"
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	34
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	35	(* extension of substitution to type structures *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	36	consts
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	37	app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	38
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 3842 diff changeset	39	primrec
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	40	app_subst_TVar "$ s (TVar n) = s n"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	41	app_subst_Fun "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	42
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	43	defs
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	44	app_subst_list "$ s == map ($ s)"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	45
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	46	(* free_tv s: the type variables occuring freely in the type structure s *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	47	consts
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	48	free_tv :: ['a::type_struct] => nat set
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	49
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 3842 diff changeset	50	primrec
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	51	"free_tv (TVar m) = {m}"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	52	"free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	53
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 3842 diff changeset	54	primrec
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	55	"free_tv [] = {}"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	56	"free_tv (x#l) = (free_tv x) Un (free_tv l)"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	57
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	58	(* domain of a substitution *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	59	constdefs
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	60	dom :: subst => nat set
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	61	"dom s == {n. s n ~= TVar n}"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	62
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	63	(* codomain of a substitutions: the introduced variables *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	64	constdefs
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	65	cod :: subst => nat set
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	66	"cod s == (UN m:dom s. free_tv (s m))"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	67
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	68	defs
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	69	free_tv_subst "free_tv s == (dom s) Un (cod s)"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	70
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	71	(* new_tv s n computes whether n is a new type variable w.r.t. a type
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	72	structure s, i.e. whether n is greater than any type variable
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	73	occuring in the type structure *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	74	constdefs
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	75	new_tv :: [nat,'a::type_struct] => bool
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	76	"new_tv n ts == ! m. m:free_tv ts --> m<n"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	77
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	78	(* unification algorithm mgu *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	79	consts
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	80	mgu :: [typ,typ] => subst maybe
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	81	rules
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	82	mgu_eq "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	83	mgu_mg "[\| (mgu t1 t2) = Ok u; $s t1 = $s t2 \|] ==>
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	84	? r. s = $r o u"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	85	mgu_Ok "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	86	mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	87
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	88	end
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	89

author	wenzelm
	Sun, 07 Jan 2001 21:35:34 +0100
changeset 10816	8b2eafed6183
parent 5184	9b8547a9496a
child 12338	de0f4a63baa5
permissions	-rw-r--r--