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

1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	1	theory SingleLet
2474 6e37bfb62474 generated inducts rule by Project_Rule.projections Christian Urban <urbanc@in.tum.de> parents: 2473 diff changeset	2	imports "../Nominal2"
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
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	7	declare [[STEPS = 100]]
2294 72ad4e766acf properly exported bn_descr Christian Urban <urbanc@in.tum.de> parents: 2293 diff changeset	8
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	9	nominal_datatype single_let: trm =
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	10	Var "name"
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	11	\| App "trm" "trm"
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	12	\| Lam x::"name" t::"trm" bind x in t
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	13	\| Let a::"assg" t::"trm" bind "bn a" in t
2424 621ebd8b13c4 changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default Christian Urban <urbanc@in.tum.de> parents: 2410 diff changeset	14	\| 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	15	\| Bar x::"name" y::"name" t::"trm" bind y x in t x y
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	16	\| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set) x in t2
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	17	and assg =
2320 d835a2771608 prove that alpha implies alpha_bn (needed for rsp proofs) Christian Urban <urbanc@in.tum.de> parents: 2318 diff changeset	18	As "name" x::"name" t::"trm" bind x in t
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	binder
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	20	bn::"assg \<Rightarrow> atom list"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	where
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	22	"bn (As x y t) = [atom x]"
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	23
2448 b9d9c4540265 proved supports lemmas Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	24
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	25	thm single_let.distinct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	26	thm single_let.induct
2474 6e37bfb62474 generated inducts rule by Project_Rule.projections Christian Urban <urbanc@in.tum.de> parents: 2473 diff changeset	27	thm single_let.inducts
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	28	thm single_let.exhaust
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	29	thm single_let.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	30	thm single_let.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	31	thm single_let.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	32	thm single_let.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	33	thm single_let.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	34	thm single_let.size_eqvt
2448 b9d9c4540265 proved supports lemmas Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	35	thm single_let.supports
2450 217ef3e4282e added proofs for fsupp properties Christian Urban <urbanc@in.tum.de> parents: 2449 diff changeset	36	thm single_let.fsupp
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	37	thm single_let.supp
2430 a746d49b0240 updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2428 diff changeset	38
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	39	lemma test2:
86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	40	assumes "fv_trm t = supp t"
86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	41	shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)"
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	42	apply(rule allI)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	43	apply(rule_tac p="-p" in permute_boolE)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	44	apply(perm_simp add: single_let.fv_bn_eqvt permute_minus_cancel)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	45	apply(rule assms)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	46	done
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	47
2361 d73d4d151cce more on the paper Christian Urban <urbanc@in.tum.de> parents: 2359 diff changeset	48	lemma supp_fv:
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	49	"fv_trm x = supp x"
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	50	"fv_assg xa = supp xa"
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	51	"fv_bn xa = supp_rel alpha_bn xa"
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	52	apply(induct rule: single_let.inducts)
2473 a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	53	-- " 0A "
a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	54	apply(simp only: single_let.fv_defs supp_Pair[symmetric])
a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	55	apply(simp (no_asm) only: supp_def)
a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	56	apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	57	apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	58	-- " 0B"
a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	59	apply(simp only: single_let.fv_defs supp_Pair[symmetric])
a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	60	apply(simp (no_asm) only: supp_def)
a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	61	apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	62	apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	63	apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	64	--" 1 "
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	65	apply(simp only: single_let.fv_defs supp_Pair[symmetric])
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	66	apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *})
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	67	apply(simp (no_asm) only: supp_def)
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	68	apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	69	apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	70	apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	71	apply(drule test2)
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	72	apply(simp only:)
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	73	-- " 2 "
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	74	apply(simp only: single_let.fv_defs supp_Pair[symmetric])
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	75	apply(subst supp_abs(3)[symmetric])
2473 a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	76	apply(simp (no_asm) only: supp_def supp_rel_def)
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	77	apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	78	apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	79	apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	80	apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	81	apply(drule test2)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	82	apply(simp only:)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	83	-- " 3 "
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	84	apply(simp only: single_let.fv_defs supp_Pair[symmetric])
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	85	apply(subst supp_abs(1)[symmetric])
2473 a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	86	apply(simp (no_asm) only: supp_def supp_rel_def)
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	87	apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	88	apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	89	apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	90	apply(drule test2)+
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	91	apply(simp only: supp_Pair Un_assoc conj_assoc)
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	92	-- " Bar "
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	93	apply(simp only: single_let.fv_defs supp_Pair[symmetric])
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	94	apply(subst supp_abs(3)[symmetric])
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	95	apply(simp (no_asm) only: supp_def)
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	96	apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	97	apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	98	apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	99	apply(drule test2)+
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	100	apply(simp only: supp_Pair Un_assoc conj_assoc)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	101	-- " Baz "
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	102	apply(simp only: single_let.fv_defs supp_Pair[symmetric])
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	103	apply(subst supp_abs(1)[symmetric])
486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	104	apply(subst supp_abs(1)[symmetric])
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	105	apply(simp (no_asm) only: supp_def)
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	106	apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	107	apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	108	apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	109	apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	110	apply(drule test2)+
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	111	apply(simp only: supp_Pair Un_assoc conj_assoc)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	112	-- "last"
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	113	apply(simp only: single_let.fv_defs supp_Pair[symmetric])
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	114	apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *})
2473 a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	115	apply(simp (no_asm) only: supp_def supp_rel_def)
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	116	apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	117	apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	118	apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	119	apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	120	apply(drule test2)+
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	121	apply(simp only: supp_Pair Un_assoc conj_assoc)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	122	-- "other case"
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	123	apply(simp only: single_let.fv_defs supp_Pair[symmetric])
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	124	apply(simp only: supp_abs(3)[symmetric])
2473 a3711f07449b added the definition supp_rel (support w.r.t. a relation) Christian Urban <urbanc@in.tum.de> parents: 2468 diff changeset	125	apply(simp (no_asm) only: supp_def supp_rel_def)
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	126	apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	127	apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	128	apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	129	apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)?
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	130	apply(drule test2)+
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	131	apply(simp only: supp_Pair Un_assoc conj_assoc)
f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	132	done
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	133
86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	134
86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	135
86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	136
86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	137
86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	138	text {* *}
86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	139
2448 b9d9c4540265 proved supports lemmas Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	140	(*
2365 467123396e5a tests Christian Urban <urbanc@in.tum.de> parents: 2361 diff changeset	141	consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm"
467123396e5a tests Christian Urban <urbanc@in.tum.de> parents: 2361 diff changeset	142	consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"
467123396e5a tests Christian Urban <urbanc@in.tum.de> parents: 2361 diff changeset	143
467123396e5a tests Christian Urban <urbanc@in.tum.de> parents: 2361 diff changeset	144	lemma y:
467123396e5a tests Christian Urban <urbanc@in.tum.de> parents: 2361 diff changeset	145	"perm_bn_trm p (Var x) = (Var x)"
467123396e5a tests Christian Urban <urbanc@in.tum.de> parents: 2361 diff changeset	146	"perm_bn_trm p (App t1 t2) = (App t1 t2)"
467123396e5a tests Christian Urban <urbanc@in.tum.de> parents: 2361 diff changeset	147	"perm_bn_trm p ("
467123396e5a tests Christian Urban <urbanc@in.tum.de> parents: 2361 diff changeset	148
467123396e5a tests Christian Urban <urbanc@in.tum.de> parents: 2361 diff changeset	149
2361 d73d4d151cce more on the paper Christian Urban <urbanc@in.tum.de> parents: 2359 diff changeset	150
2336 f2d545b77b31 added definition of the quotient types Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	151	typ trm
f2d545b77b31 added definition of the quotient types Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	152	typ assg
f2d545b77b31 added definition of the quotient types Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	153
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	154	thm trm_assg.fv
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	155	thm trm_assg.supp
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	156	thm trm_assg.eq_iff
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	157	thm trm_assg.bn
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	158	thm trm_assg.perm
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	159	thm trm_assg.induct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	160	thm trm_assg.inducts
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	161	thm trm_assg.distinct
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	162	ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	163	*)
2024 d974059827ad Equivariance fails for single let? Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	164
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	165
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	166
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	167	end
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	168
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	169
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	170

author	Christian Urban <urbanc@in.tum.de>
	Sat, 18 Sep 2010 06:09:43 +0800
changeset 2479	a9b6a00b1ba0
parent 2477	2f289c1f6cf1
child 2486	b4ea19604b0b
permissions	-rw-r--r--