nominal2: Nominal/Term4.thy@22a084c9316b (annotated)

1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Term4
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 {* lam with indirect list recursion *}
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 rtrm4 =
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	rVr4 "name"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11	\| rAp4 "rtrm4" "rtrm4 list"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	\| rLm4 "name" "rtrm4" --"bind (name) in (trm)"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	print_theorems
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	thm rtrm4.recs
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	(* there cannot be a clause for lists, as *)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	(* permutations are already defined in Nominal (also functions, options, and so on) *)
1277 6eacf60ce41d Permutation and FV_Alpha interface change. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1270 diff changeset	19	setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *}
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	(* "repairing" of the permute function *)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	lemma repaired:
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	fixes ts::"rtrm4 list"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24	shows "permute_rtrm4_list p ts = p \<bullet> ts"
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	25	apply(induct ts)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	26	apply(simp_all)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	done
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	28
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	29	thm permute_rtrm4_permute_rtrm4_list.simps
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	30	thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31
1277 6eacf60ce41d Permutation and FV_Alpha interface change. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1270 diff changeset	32	local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4")
1300 22a084c9316b Fixed eqvt code. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1277 diff changeset	33	[[[], [], [(NONE, 0,1)]], [[], []] ] *}
1270 8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	34	print_theorems
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	35
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	36	notation
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	37	alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	38	alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39	thm alpha_rtrm4_alpha_rtrm4_list.intros
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41	local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42	thm alpha4_inj
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	43	thm alpha_rtrm4_alpha_rtrm4_list.induct
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 {*
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	46	snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	47	*}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	48	print_theorems
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	49
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	50	local_setup {*
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	51	(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	52	build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	53	*}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	54	print_theorems
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	55
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	56	local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	57	(build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	58	thm alpha4_equivp
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	59
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	60	quotient_type
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	61	qrtrm4 = rtrm4 / alpha_rtrm4 and
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	62	qrtrm4list = "rtrm4 list" / alpha_rtrm4_list
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	63	by (simp_all add: alpha4_equivp)
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	64
8c3cf9f4f5f2 Split Terms into separate files and add them to tests. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	65	end

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Tue, 02 Mar 2010 11:04:49 +0100
changeset 1300	22a084c9316b
parent 1277	6eacf60ce41d
child 1318	cce1b6d1b761
permissions	-rw-r--r--