isabelle: src/ZF/Coind/Language.thy@fec1504e5f03 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/Coind/Language.thy
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	2	Author: Jacob Frost, Cambridge University Computer Laboratory
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	3	Copyright 1995 University of Cambridge
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	4	*)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	5
65449 c82e63b11b8b clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy; wenzelm parents: 60770 diff changeset	6	theory Language imports ZF begin
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	7
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	8
60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 41779 diff changeset	9	text\<open>these really can't be definitions without losing the abstraction\<close>
41779 a68f503805ed modernized specifications; wenzelm parents: 35762 diff changeset	10
a68f503805ed modernized specifications; wenzelm parents: 35762 diff changeset	11	axiomatization
a68f503805ed modernized specifications; wenzelm parents: 35762 diff changeset	12	Const :: i and (* Abstract type of constants *)
a68f503805ed modernized specifications; wenzelm parents: 35762 diff changeset	13	c_app :: "[i,i] => i" (* Abstract constructor for fun application*)
a68f503805ed modernized specifications; wenzelm parents: 35762 diff changeset	14	where
a68f503805ed modernized specifications; wenzelm parents: 35762 diff changeset	15	constNEE: "c \<in> Const ==> c \<noteq> 0" and
12595 0480d02221b8 conversion to Isar paulson parents: 11354 diff changeset	16	c_appI: "[\| c1 \<in> Const; c2 \<in> Const \|] ==> c_app(c1,c2) \<in> Const"
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	17
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	18
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	19	consts
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	20	Exp :: i (* Datatype of expressions *)
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	21	ExVar :: i (* Abstract type of variables *)
6112 5e4871c5136b datatype package improvements paulson parents: 2874 diff changeset	22
5e4871c5136b datatype package improvements paulson parents: 2874 diff changeset	23	datatype
12595 0480d02221b8 conversion to Isar paulson parents: 11354 diff changeset	24	"Exp" = e_const ("c \<in> Const")
0480d02221b8 conversion to Isar paulson parents: 11354 diff changeset	25	\| e_var ("x \<in> ExVar")
0480d02221b8 conversion to Isar paulson parents: 11354 diff changeset	26	\| e_fn ("x \<in> ExVar","e \<in> Exp")
0480d02221b8 conversion to Isar paulson parents: 11354 diff changeset	27	\| e_fix ("x1 \<in> ExVar","x2 \<in> ExVar","e \<in> Exp")
0480d02221b8 conversion to Isar paulson parents: 11354 diff changeset	28	\| e_app ("e1 \<in> Exp","e2 \<in> Exp")
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	29
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	30	end

author	wenzelm
	Sun, 01 Oct 2017 20:50:26 +0200
changeset 66744	fec1504e5f03
parent 65449	c82e63b11b8b
child 76213	e44d86131648
permissions	-rw-r--r--