nominal2: Nominal/Ex/SystemFOmega.thy@af6eda1fb91f (annotated)

2581 3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory SystemFOmega
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports "../Nominal2"
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	text {*
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	System from the F-ing paper by Rossberg, Russo and
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	Dreyer, TLDI'10
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	*}
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	10
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	atom_decl var
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	atom_decl tvar
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	atom_decl label
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	14
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	nominal_datatype kind =
2622 e6e6a3da81aa tuned examples Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	16	\<Omega>
e6e6a3da81aa tuned examples Christian Urban <urbanc@in.tum.de> parents: 2617 diff changeset	17	\| KFun kind kind
2581 3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	nominal_datatype ty =
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	TVar tvar
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	\| TFun ty ty
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	22	\| TAll a::tvar kind t::ty binds a in t
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	23	\| TEx a::tvar kind t::ty binds a in t
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	24	\| TLam a::tvar kind t::ty binds a in t
2581 3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	\| TApp ty ty
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	\| TRec trec
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	and trec =
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	TRNil
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	\| TRCons label ty trec
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	30
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	nominal_datatype trm =
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	Var var
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	33	\| Lam x::var ty t::trm binds x in t
2581 3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	\| App trm trm
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	\| Dot trm label
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	36	\| LAM a::tvar kind t::trm binds a in t
2581 3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	\| APP trm ty
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	\| Pack ty trm
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2622 diff changeset	39	\| Unpack a::tvar x::var trm t::trm binds a x in t
2581 3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	\| Rec rec
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	and rec =
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	RNil
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	\| RCons label trm rec
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	44
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	45	thm ty_trec.distinct
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	46	thm ty_trec.induct
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	47	thm ty_trec.inducts
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	48	thm ty_trec.exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	49	thm ty_trec.strong_exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	50	thm ty_trec.fv_defs
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	51	thm ty_trec.bn_defs
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	52	thm ty_trec.perm_simps
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	53	thm ty_trec.eq_iff
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	54	thm ty_trec.fv_bn_eqvt
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	55	thm ty_trec.size_eqvt
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	56	thm ty_trec.supports
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	57	thm ty_trec.fsupp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	58	thm ty_trec.supp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	59	thm ty_trec.fresh
2581 3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	60
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	61	thm trm_rec.distinct
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	62	thm trm_rec.induct
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	63	thm trm_rec.inducts
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	64	thm trm_rec.exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	65	thm trm_rec.strong_exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	66	thm trm_rec.fv_defs
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	67	thm trm_rec.bn_defs
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	68	thm trm_rec.perm_simps
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	69	thm trm_rec.eq_iff
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	70	thm trm_rec.fv_bn_eqvt
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	71	thm trm_rec.size_eqvt
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	72	thm trm_rec.supports
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	73	thm trm_rec.fsupp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	74	thm trm_rec.supp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2581 diff changeset	75	thm trm_rec.fresh
2581 3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	76
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	77	end
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	78
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	79
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	80
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer Christian Urban <urbanc@in.tum.de> parents: diff changeset	81

author	Christian Urban <urbanc@in.tum.de>
	Wed, 21 Sep 2011 15:18:32 +0200
changeset 3038	af6eda1fb91f
parent 2950	0911cb7bf696
permissions	-rw-r--r--