nominal2: Nominal/Manual/Term3.thy@c39d4fe31100 (annotated)

1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Term3
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	section {* lets with many assignments *}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	datatype rtrm3 =
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	rVr3 "name"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11	\| rAp3 "rtrm3" "rtrm3"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	\| rLm3 "name" "rtrm3" --"bind (name) in (trm3)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	\| rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	and rassigns =
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	rANil
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	\| rACons "name" "rtrm3" "rassigns"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	(* to be given by the user *)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	primrec
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	bv3
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	where
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	"bv3 rANil = {}"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	\| "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24
1277 6eacf60ce41d Permutation and FV_Alpha interface change. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1270 diff changeset	25	setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term3.rtrm3") 2 *}
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26
1277 6eacf60ce41d Permutation and FV_Alpha interface change. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1270 diff changeset	27	local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term3.rtrm3")
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28	[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29	[[], [[], [], []]]] *}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	print_theorems
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32	notation
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	33	alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34	alpha_rassigns ("_ \<approx>3a _" [100, 100] 100)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35	thm alpha_rtrm3_alpha_rassigns.intros
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37	local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38	thm alpha3_inj
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40	lemma alpha3_eqvt:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	"t \<approx>3 s \<Longrightarrow> (pi \<bullet> t) \<approx>3 (pi \<bullet> s)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42	"a \<approx>3a b \<Longrightarrow> (pi \<bullet> a) \<approx>3a (pi \<bullet> b)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	43	sorry
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	44
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	45	local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []),
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	46	(build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	47	thm alpha3_equivp
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	48
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	49	quotient_type
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	50	trm3 = rtrm3 / alpha_rtrm3
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	51	and
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	52	assigns = rassigns / alpha_rassigns
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	53	by (rule alpha3_equivp(1)) (rule alpha3_equivp(2))
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	54
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	55	end

author	Christian Urban <urbanc@in.tum.de>
	Sun, 16 May 2010 12:41:27 +0100 (2010-05-16)
changeset 2142	c39d4fe31100
parent 1592	b679900fa5f6
permissions	-rw-r--r--