nominal2: Nominal/Ex/SingleLet.thy@08bbde090a17 (annotated)

1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	1	theory SingleLet
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	2	imports "../NewParser"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
2316 08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	7	declare [[STEPS = 12]]
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	8
2294 72ad4e766acf properly exported bn_descr Christian Urban <urbanc@in.tum.de> parents: 2293 diff changeset	9
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	10	nominal_datatype trm =
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	11	Var "name"
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	12	\| App "trm" "trm"
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	13	\| Lam x::"name" t::"trm" bind_set x in t
d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	14	\| Let a::"assg" t::"trm" bind_set "bn a" in t
2311 4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2308 diff changeset	15	\| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2
2296 45a69c9cc4cc alpha works now Christian Urban <urbanc@in.tum.de> parents: 2295 diff changeset	16	\| Bar x::"name" y::"name" t::"trm" bind y x in t x y
2316 08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	17	\| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	18	and assg =
2308 387fcbd33820 fixed problem with bn_info Christian Urban <urbanc@in.tum.de> parents: 2306 diff changeset	19	As "name" "name" "trm" "name"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	binder
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	21	bn::"assg \<Rightarrow> atom set"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	where
2308 387fcbd33820 fixed problem with bn_info Christian Urban <urbanc@in.tum.de> parents: 2306 diff changeset	23	"bn (As x y t z) = {atom x}"
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	24
2311 4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2308 diff changeset	25
2316 08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	26	lemma
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	27	shows "alpha_trm_raw x x"
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	28	and "alpha_assg_raw y y"
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	29	and "alpha_bn_raw y y"
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	30	apply(induct rule: trm_raw_assg_raw.inducts)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	31	apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	32	apply(rule refl)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	33	apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	34	apply(assumption)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	35	apply(assumption)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	36	apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	37	apply(rule_tac x="0" in exI)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	38	apply(rule alpha_gen_refl)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	39	apply(assumption)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	40	apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	41	apply(rule_tac x="0" in exI)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	42	apply(rule alpha_gen_refl)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	43	apply(assumption)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	44	apply(assumption)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	45	apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	46	apply(rule_tac x="0" in exI)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	47	apply(rule alpha_gen_refl)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	48	apply(simp only: prod_alpha_def split_conv prod_rel.simps)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	49	apply(simp)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	50	apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	51	apply(rule_tac x="0" in exI)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	52	apply(rule alpha_gen_refl)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	53	apply(simp only: prod_alpha_def split_conv prod_rel.simps)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	54	apply(simp)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	55	apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	56	apply(rule refl)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	57	apply(rule refl)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	58	apply(assumption)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	59	apply(rule refl)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	60	apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	61	apply(rule refl)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	62	apply(assumption)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	63	apply(rule refl)
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	64	done
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	65
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	66
08bbde090a17 also symmetry Christian Urban <urbanc@in.tum.de> parents: 2313 diff changeset	67
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	68	thm trm_assg.fv
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	69	thm trm_assg.supp
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	70	thm trm_assg.eq_iff
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	71	thm trm_assg.bn
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	72	thm trm_assg.perm
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	73	thm trm_assg.induct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	74	thm trm_assg.inducts
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	75	thm trm_assg.distinct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	76	ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
2288 3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 2146 diff changeset	77
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 2146 diff changeset	78	(* TEMPORARY
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	79	thm trm_assg.fv[simplified trm_assg.supp(1-2)]
2288 3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 2146 diff changeset	80	*)
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	81
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	82	end
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	83
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	84
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	85

author	Christian Urban <urbanc@in.tum.de>
	Fri, 11 Jun 2010 03:02:42 +0200
changeset 2316	08bbde090a17
parent 2313	25d2cdf7d7e4
child 2318	49cc1af89de9
permissions	-rw-r--r--