isabelle: src/HOL/Subst/UTerm.thy@dfb8d2977263 (annotated)

3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 2903 diff changeset	1	(* Title: Subst/UTerm.thy
3268 012c43174664 Mostly cosmetic changes: updated headers, ID lines, etc. paulson parents: 3192 diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1381 diff changeset	3	Author: Martin Coen, Cambridge University Computer Laboratory
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	5
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1381 diff changeset	6	Simple term structure for unification.
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	7	Binary trees with leaves that are constants or variables.
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	8	*)
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	9
12406 c9775847ed66 use Main; wenzelm parents: 5184 diff changeset	10	UTerm = Main +
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	11
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 2903 diff changeset	12	datatype 'a uterm = Var ('a)
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 2903 diff changeset	13	\| Const ('a)
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 2903 diff changeset	14	\| Comb ('a uterm) ('a uterm)
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	15
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	16	consts
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 2903 diff changeset	17	vars_of :: 'a uterm => 'a set
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 2903 diff changeset	18	"<:" :: 'a uterm => 'a uterm => bool (infixl 54)
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 2903 diff changeset	19	uterm_size :: 'a uterm => nat
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 2903 diff changeset	20
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	21
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	22	primrec
9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	23	vars_of_Var "vars_of (Var v) = {v}"
9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	24	vars_of_Const "vars_of (Const c) = {}"
9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	25	vars_of_Comb "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	26
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	27
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	28	primrec
9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	29	occs_Var "u <: (Var v) = False"
9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	30	occs_Const "u <: (Const c) = False"
9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	31	occs_Comb "u <: (Comb M N) = (u=M \| u=N \| u <: M \| u <: N)"
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	32
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	33	primrec
9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	34	uterm_size_Var "uterm_size (Var v) = 0"
9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	35	uterm_size_Const "uterm_size (Const c) = 0"
9b8547a9496a Adapted to new datatype package. berghofe parents: 3268 diff changeset	36	uterm_size_Comb "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	37
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	38	end

author	kleing
	Mon, 19 Apr 2004 09:31:00 +0200
changeset 14626	dfb8d2977263
parent 12406	c9775847ed66
child 15635	8408a06590a6
permissions	-rw-r--r--