isabelle: src/ZF/Coind/Language.thy@0b3700d31758 (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 *)
76215 a642599ffdea More syntactic cleanup. LaTeX markup working paulson <lp15@cam.ac.uk> parents: 76213 diff changeset	13	c_app :: "[i,i] \<Rightarrow> i" (* Abstract constructor for fun application*)
41779 a68f503805ed modernized specifications; wenzelm parents: 35762 diff changeset	14	where
76213 e44d86131648 Removal of obsolete ASCII syntax paulson <lp15@cam.ac.uk> parents: 65449 diff changeset	15	constNEE: "c \<in> Const \<Longrightarrow> c \<noteq> 0" and
e44d86131648 Removal of obsolete ASCII syntax paulson <lp15@cam.ac.uk> parents: 65449 diff changeset	16	c_appI: "\<lbrakk>c1 \<in> Const; c2 \<in> Const\<rbrakk> \<Longrightarrow> 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
	Thu, 19 Oct 2023 17:06:39 +0200
changeset 78800	0b3700d31758
parent 76215	a642599ffdea
permissions	-rw-r--r--