nominal2: Nominal/Ex/Multi_Recs.thy@592d17e26e09 (annotated)

2481 3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	1	theory Multi_Recs
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	2	imports "../Nominal2"
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
2481 3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	5	(*
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	6	multiple recursive binders
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	7
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	8	example 7 from Peter Sewell's bestiary
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	9
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	10	*)
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	atom_decl name
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13
2481 3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	14	nominal_datatype multi_recs: exp =
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	15	Var name
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	16	\| Unit
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	17	\| Pair exp exp
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	18	\| LetRec l::"lrbs" e::"exp" bind (set) "bs l" in l e
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	and lrb =
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	20	Assign name exp
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	21	and lrbs =
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	22	Single lrb
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	23	\| More lrb lrbs
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24	binder
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	25	b :: "lrb \<Rightarrow> atom set" and
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	26	bs :: "lrbs \<Rightarrow> atom set"
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	27	where
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	28	"b (Assign x e) = {atom x}"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	29	\| "bs (Single a) = b a"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	30	\| "bs (More a as) = (b a) \<union> (bs as)"
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2043 diff changeset	31
2481 3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	32	thm multi_recs.distinct
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	33	thm multi_recs.induct
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	34	thm multi_recs.inducts
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	35	thm multi_recs.exhaust
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	36	thm multi_recs.fv_defs
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	37	thm multi_recs.bn_defs
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	38	thm multi_recs.perm_simps
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	39	thm multi_recs.eq_iff
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	40	thm multi_recs.fv_bn_eqvt
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	41	thm multi_recs.size_eqvt
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	42	thm multi_recs.supports
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	43	thm multi_recs.fsupp
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	44	thm multi_recs.supp
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	45
2615 d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	46	thm multi_recs.bn_defs
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	47	thm multi_recs.permute_bn
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	48	thm multi_recs.perm_bn_alpha
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	49	thm multi_recs.perm_bn_simps
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	50	thm multi_recs.bn_finite
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	51
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	52
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	53	lemma at_set_avoiding5:
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	54	assumes "finite xs"
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	55	and "finite (supp c)"
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	56	shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs"
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	57	using assms
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	58	apply(erule_tac c="c" in at_set_avoiding)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	59	apply(auto)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	60	done
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	61
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	62	lemma
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	63	fixes c::"'a::fs"
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	64	assumes a: "\<And>lrbs exp. \<lbrakk>bs lrbs \<sharp>* c; y = LetRec lrbs exp\<rbrakk> \<Longrightarrow> P"
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	65	shows "y = LetRec lrbs exp \<Longrightarrow> P"
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	66	apply -
2616 dd7490fdd998 all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code Christian Urban <urbanc@in.tum.de> parents: 2615 diff changeset	67	apply(subgoal_tac "\<exists>p. ((p \<bullet> (bs lrbs)) \<sharp>* (c, bs lrbs, lrbs, exp))")
2615 d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	68	apply(erule exE)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	69	apply(simp add: fresh_star_Pair)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	70	apply(erule conjE)+
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	71	apply(simp add: multi_recs.fv_bn_eqvt)
2616 dd7490fdd998 all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code Christian Urban <urbanc@in.tum.de> parents: 2615 diff changeset	72	using Abs_rename_set'
2615 d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	73	apply -
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	74	apply(drule_tac x="p" in meta_spec)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	75	apply(drule_tac x="bs lrbs" in meta_spec)
2616 dd7490fdd998 all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code Christian Urban <urbanc@in.tum.de> parents: 2615 diff changeset	76	apply(drule_tac x="(lrbs, exp)" in meta_spec)
2615 d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	77	apply(drule meta_mp)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	78	apply(simp add: multi_recs.fv_bn_eqvt fresh_star_Pair)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	79	apply(drule meta_mp)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	80	apply(simp add: multi_recs.bn_finite)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	81	apply(erule exE)
2616 dd7490fdd998 all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code Christian Urban <urbanc@in.tum.de> parents: 2615 diff changeset	82	apply(erule conjE)
dd7490fdd998 all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code Christian Urban <urbanc@in.tum.de> parents: 2615 diff changeset	83	apply(rotate_tac 6)
dd7490fdd998 all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code Christian Urban <urbanc@in.tum.de> parents: 2615 diff changeset	84	apply(drule sym)
2615 d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	85	apply(simp add: multi_recs.fv_bn_eqvt)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	86	apply(rule a)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	87	apply(assumption)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	88	apply(clarify)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	89	apply(simp (no_asm) only: multi_recs.eq_iff)
2616 dd7490fdd998 all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code Christian Urban <urbanc@in.tum.de> parents: 2615 diff changeset	90	apply(rule at_set_avoiding1)
2615 d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	91	apply(simp add: multi_recs.bn_finite)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	92	apply(simp add: supp_Pair finite_supp)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	93	apply(rule finite_sets_supp)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	94	apply(simp add: multi_recs.bn_finite)
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	95	done
d5713db7e146 one interesting case done Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	96
1655 9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	97	end
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	98
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	99
9cec4269b7f9 Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	100

author	Christian Urban <urbanc@in.tum.de>
	Thu, 06 Jan 2011 13:28:04 +0000 (2011-01-06)
changeset 2641	592d17e26e09
parent 2616	dd7490fdd998
child 2950	0911cb7bf696
permissions	-rw-r--r--