nominal2: Nominal/Test.thy@74888979e9cd (annotated)

954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Test
1335 c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	2	imports "Parser" "../Attic/Prove"
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	5	text {* example 1, equivalent to example 2 from Terms *}
1316 0577afdb1732 Porting from Lift to Parser; until defining the Quotient type. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1309 diff changeset	6
1428 4029105011ca Show that the new types are in finite support typeclass. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1418 diff changeset	7	atom_decl name
4029105011ca Show that the new types are in finite support typeclass. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1418 diff changeset	8
1454 7c8cd6eae8e2 FV_bn generated for recursive functions as well, and used in main fv for bindings. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1453 diff changeset	9	ML {* val _ = recursive := false *}
1445 3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1441 diff changeset	10
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	11	nominal_datatype lm =
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	12	Vr "name"
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	13	\| Ap "lm" "lm"
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	14	\| Lm x::"name" l::"lm" bind x in l
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	15
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	16	lemma finite_fv:
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	17	shows "finite (fv_lm t)"
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	18	apply(induct t rule: lm.induct)
1510 be911e869fde Added fv,bn,distinct,perm to the simplifier. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	19	apply(simp_all)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	20	done
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	21
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	22	lemma supp_fn:
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	23	shows "supp t = fv_lm t"
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	24	apply(induct t rule: lm.induct)
1510 be911e869fde Added fv,bn,distinct,perm to the simplifier. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	25	apply(simp_all)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	26	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	27	apply(simp only: lm.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	28	apply(simp only: lm.eq_iff)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	29	apply(simp only: supp_def[symmetric])
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	30	apply(simp only: supp_at_base)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	31	apply(simp (no_asm) only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	32	apply(simp only: lm.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	33	apply(simp only: lm.eq_iff)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	34	apply(simp only: de_Morgan_conj)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	35	apply(simp only: Collect_disj_eq)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	36	apply(simp only: infinite_Un)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	37	apply(simp only: Collect_disj_eq)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	38	apply(simp only: supp_def[symmetric])
1498 2ff84b1f551f Rename bound variables + minor cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1496 diff changeset	39	apply(rule_tac t="supp (Lm name lm)" and s="supp (Abs {atom name} lm)" in subst)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	40	apply(simp (no_asm) only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	41	apply(simp only: lm.perm)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	42	apply(simp only: permute_ABS)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	43	apply(simp only: lm.eq_iff)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	44	apply(simp only: Abs_eq_iff)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	45	apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	46	apply(simp only: alpha_gen)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	47	apply(simp only: supp_eqvt[symmetric])
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	48	apply(simp only: eqvts)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	49	apply(simp only: supp_Abs)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	50	done
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	51
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	52	lemmas supp_fn' = lm.fv[simplified supp_fn[symmetric]]
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	53
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	54	lemma
1499 21dda372fb11 simplified strong induction proof by using flip Christian Urban <urbanc@in.tum.de> parents: 1498 diff changeset	55	fixes c::"'a::fs"
21dda372fb11 simplified strong induction proof by using flip Christian Urban <urbanc@in.tum.de> parents: 1498 diff changeset	56	assumes a1: "\<And>name c. P c (Vr name)"
1500 212e7a3494eb vixed variable names Christian Urban <urbanc@in.tum.de> parents: 1499 diff changeset	57	and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
1517 62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	58	and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	59	shows "P c lm"
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	60	proof -
1499 21dda372fb11 simplified strong induction proof by using flip Christian Urban <urbanc@in.tum.de> parents: 1498 diff changeset	61	have "\<And>p. P c (p \<bullet> lm)"
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	62	apply(induct lm arbitrary: c rule: lm.induct)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	63	apply(simp only: lm.perm)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	64	apply(rule a1)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	65	apply(simp only: lm.perm)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	66	apply(rule a2)
1499 21dda372fb11 simplified strong induction proof by using flip Christian Urban <urbanc@in.tum.de> parents: 1498 diff changeset	67	apply(blast)[1]
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	68	apply(assumption)
1500 212e7a3494eb vixed variable names Christian Urban <urbanc@in.tum.de> parents: 1499 diff changeset	69	apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))")
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	70	apply(erule exE)
1500 212e7a3494eb vixed variable names Christian Urban <urbanc@in.tum.de> parents: 1499 diff changeset	71	apply(rule_tac t="p \<bullet> Lm name lm" and
212e7a3494eb vixed variable names Christian Urban <urbanc@in.tum.de> parents: 1499 diff changeset	72	s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	73	apply(simp del: lm.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	74	apply(subst lm.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	75	apply(subst (2) lm.perm)
1499 21dda372fb11 simplified strong induction proof by using flip Christian Urban <urbanc@in.tum.de> parents: 1498 diff changeset	76	apply(rule flip_fresh_fresh)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	77	apply(simp add: fresh_def)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	78	apply(simp only: supp_fn')
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	79	apply(simp)
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	80	apply(simp add: fresh_Pair)
1510 be911e869fde Added fv,bn,distinct,perm to the simplifier. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	81	apply(simp)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	82	apply(rule a3)
1517 62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	83	apply(simp add: fresh_Pair)
1499 21dda372fb11 simplified strong induction proof by using flip Christian Urban <urbanc@in.tum.de> parents: 1498 diff changeset	84	apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	85	apply(simp)
1499 21dda372fb11 simplified strong induction proof by using flip Christian Urban <urbanc@in.tum.de> parents: 1498 diff changeset	86	apply(simp add: fresh_def)
1500 212e7a3494eb vixed variable names Christian Urban <urbanc@in.tum.de> parents: 1499 diff changeset	87	apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
1499 21dda372fb11 simplified strong induction proof by using flip Christian Urban <urbanc@in.tum.de> parents: 1498 diff changeset	88	apply(simp add: supp_Pair finite_supp)
21dda372fb11 simplified strong induction proof by using flip Christian Urban <urbanc@in.tum.de> parents: 1498 diff changeset	89	apply(blast)
21dda372fb11 simplified strong induction proof by using flip Christian Urban <urbanc@in.tum.de> parents: 1498 diff changeset	90	done
1483 2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	91	then have "P c (0 \<bullet> lm)" by blast
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	92	then show "P c lm" by simp
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	93	qed
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	94
2ca8e43b53c5 added partial proof for the strong induction principle Christian Urban <urbanc@in.tum.de> parents: 1478 diff changeset	95
1517 62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	96	lemma
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	97	fixes c::"'a::fs"
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	98	assumes a1: "\<And>name c. P c (Vr name)"
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	99	and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	100	and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	101	shows "P c lm"
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	102	proof -
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	103	have "\<And>p. P c (p \<bullet> lm)"
1522 4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	104	apply(induct lm arbitrary: c rule: lm.induct)
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	105	apply(simp only: lm.perm)
1517 62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	106	apply(rule a1)
1522 4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	107	apply(simp only: lm.perm)
1517 62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	108	apply(rule a2)
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	109	apply(blast)[1]
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	110	apply(assumption)
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	111	thm at_set_avoiding
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	112	apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	113	apply(erule exE)
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	114	apply(rule_tac t="p \<bullet> Lm name lm" and
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	115	s="q \<bullet> p \<bullet> Lm name lm" in subst)
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	116	defer
1522 4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	117	apply(simp add: lm.perm)
1517 62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	118	apply(rule a3)
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	119	apply(simp add: eqvts fresh_star_def)
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	120	apply(drule_tac x="q + p" in meta_spec)
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	121	apply(simp)
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	122	sorry
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	123	then have "P c (0 \<bullet> lm)" by blast
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	124	then show "P c lm" by simp
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	125	qed
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	126
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	127
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	nominal_datatype lam =
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	VAR "name"
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	130	\| APP "lam" "lam"
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	131	\| LAM x::"name" t::"lam" bind x in t
1287 8557af71724e slight simplification of the raw-decl generation Christian Urban <urbanc@in.tum.de> parents: 1285 diff changeset	132	\| LET bp::"bp" t::"lam" bind "bi bp" in t
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	133	and bp =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	134	BP "name" "lam"
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	135	binder
1295 0ecc775e5fce Link calls to Raw permutations, FV definition and alpha_definition into the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1290 diff changeset	136	bi::"bp \<Rightarrow> atom set"
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	137	where
1295 0ecc775e5fce Link calls to Raw permutations, FV definition and alpha_definition into the parser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1290 diff changeset	138	"bi (BP x t) = {atom x}"
1228 c179ad9d2446 declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types Christian Urban <urbanc@in.tum.de> parents: 1223 diff changeset	139
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	140	thm lam_bp.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	141	thm lam_bp.eq_iff
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	142	thm lam_bp.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	143	thm lam_bp.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	144	thm lam_bp.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	145	thm lam_bp.inducts
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	146	thm lam_bp.distinct
1428 4029105011ca Show that the new types are in finite support typeclass. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1418 diff changeset	147	ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
4029105011ca Show that the new types are in finite support typeclass. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1418 diff changeset	148
4029105011ca Show that the new types are in finite support typeclass. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1418 diff changeset	149	term "supp (x :: lam)"
1418 632b08744613 With the 4 cheats, all examples fully lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1416 diff changeset	150
1436 04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	151	lemma bi_eqvt:
04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	152	shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
1441 14b850159df1 Use eqvt. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1439 diff changeset	153	by (rule eqvts)
1436 04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	154
04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	155	lemma supp_fv:
1461 c79bcbe1983d added the final unfolded result Christian Urban <urbanc@in.tum.de> parents: 1460 diff changeset	156	shows "supp t = fv_lam t"
c79bcbe1983d added the final unfolded result Christian Urban <urbanc@in.tum.de> parents: 1460 diff changeset	157	and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	158	apply(induct t and bp rule: lam_bp.inducts)
1510 be911e869fde Added fv,bn,distinct,perm to the simplifier. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	159	apply(simp_all)
1436 04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	160	(* VAR case *)
04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	161	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	162	apply(simp only: lam_bp.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	163	apply(simp only: lam_bp.eq_iff)
1436 04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	164	apply(simp only: supp_def[symmetric])
04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	165	apply(simp only: supp_at_base)
04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	166	(* APP case *)
04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	167	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	168	apply(simp only: lam_bp.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	169	apply(simp only: lam_bp.eq_iff)
1436 04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	170	apply(simp only: de_Morgan_conj)
04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	171	apply(simp only: Collect_disj_eq)
04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	172	apply(simp only: infinite_Un)
04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	173	apply(simp only: Collect_disj_eq)
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	174	(* LAM case *)
1498 2ff84b1f551f Rename bound variables + minor cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1496 diff changeset	175	apply(rule_tac t="supp (LAM name lam)" and s="supp (Abs {atom name} lam)" in subst)
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	176	apply(simp (no_asm) only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	177	apply(simp only: lam_bp.perm)
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	178	apply(simp only: permute_ABS)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	179	apply(simp only: lam_bp.eq_iff)
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	180	apply(simp only: Abs_eq_iff)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	181	apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	182	apply(simp only: alpha_gen)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	183	apply(simp only: supp_eqvt[symmetric])
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	184	apply(simp only: eqvts)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	185	apply(simp only: supp_Abs)
1436 04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	186	(* LET case *)
1498 2ff84b1f551f Rename bound variables + minor cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1496 diff changeset	187	apply(rule_tac t="supp (LET bp lam)" and s="supp (Abs (bi bp) lam) \<union> fv_bi bp" in subst)
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	188	apply(simp (no_asm) only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	189	apply(simp only: lam_bp.perm)
1460 0fd03936dedb merge and proof of support for non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1457 diff changeset	190	apply(simp only: permute_ABS)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	191	apply(simp only: lam_bp.eq_iff)
1460 0fd03936dedb merge and proof of support for non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1457 diff changeset	192	apply(simp only: eqvts)
0fd03936dedb merge and proof of support for non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1457 diff changeset	193	apply(simp only: Abs_eq_iff)
0fd03936dedb merge and proof of support for non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1457 diff changeset	194	apply(simp only: ex_simps)
0fd03936dedb merge and proof of support for non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1457 diff changeset	195	apply(simp only: de_Morgan_conj)
0fd03936dedb merge and proof of support for non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1457 diff changeset	196	apply(simp only: Collect_disj_eq)
0fd03936dedb merge and proof of support for non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1457 diff changeset	197	apply(simp only: infinite_Un)
0fd03936dedb merge and proof of support for non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1457 diff changeset	198	apply(simp only: Collect_disj_eq)
1436 04dad9b0136d started supp-fv proofs (is going to work) Christian Urban <urbanc@in.tum.de> parents: 1428 diff changeset	199	apply(simp only: alpha_gen)
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	200	apply(simp only: supp_eqvt[symmetric])
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	201	apply(simp only: eqvts)
1460 0fd03936dedb merge and proof of support for non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1457 diff changeset	202	apply(blast)
0fd03936dedb merge and proof of support for non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1457 diff changeset	203	apply(simp add: supp_Abs)
0fd03936dedb merge and proof of support for non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1457 diff changeset	204	apply(blast)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	205	(* BP case *)
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	206	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	207	apply(simp only: lam_bp.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	208	apply(simp only: lam_bp.eq_iff)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	209	apply(simp only: de_Morgan_conj)
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	210	apply(simp only: Collect_disj_eq)
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	211	apply(simp only: infinite_Un)
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	212	apply(simp only: Collect_disj_eq)
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	213	apply(simp only: supp_def[symmetric])
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	214	apply(simp only: supp_at_base)
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	215	apply(simp)
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1439 diff changeset	216	done
1367 9bbf56cdeb88 added compat definitions to some examples Christian Urban <urbanc@in.tum.de> parents: 1365 diff changeset	217
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	218	thm lam_bp.fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
1461 c79bcbe1983d added the final unfolded result Christian Urban <urbanc@in.tum.de> parents: 1460 diff changeset	219
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	220	ML {* val _ = recursive := true *}
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	221
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	222	nominal_datatype lam' =
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	223	VAR' "name"
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	224	\| APP' "lam'" "lam'"
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	225	\| LAM' x::"name" t::"lam'" bind x in t
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	226	\| LET' bp::"bp'" t::"lam'" bind "bi' bp" in t
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	227	and bp' =
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	228	BP' "name" "lam'"
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	229	binder
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	230	bi'::"bp' \<Rightarrow> atom set"
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	231	where
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	232	"bi' (BP' x t) = {atom x}"
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	233
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	234	thm lam'_bp'.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	235	thm lam'_bp'.eq_iff[no_vars]
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	236	thm lam'_bp'.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	237	thm lam'_bp'.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	238	thm lam'_bp'.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	239	thm lam'_bp'.inducts
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	240	thm lam'_bp'.distinct
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	241	ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	242
1549 74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	243	lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	244	apply (simp add: supp_Abs supp_Pair)
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	245	apply blast
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	246	done
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	247
1472 4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	248	lemma supp_fv':
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	249	shows "supp t = fv_lam' t"
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	250	and "supp bp = fv_bp' bp"
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	251	apply(induct t and bp rule: lam'_bp'.inducts)
1510 be911e869fde Added fv,bn,distinct,perm to the simplifier. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	252	apply(simp_all)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	253	(* VAR case *)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	254	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	255	apply(simp only: lam'_bp'.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	256	apply(simp only: lam'_bp'.eq_iff)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	257	apply(simp only: supp_def[symmetric])
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	258	apply(simp only: supp_at_base)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	259	(* APP case *)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	260	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	261	apply(simp only: lam'_bp'.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	262	apply(simp only: lam'_bp'.eq_iff)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	263	apply(simp only: de_Morgan_conj)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	264	apply(simp only: Collect_disj_eq)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	265	apply(simp only: infinite_Un)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	266	apply(simp only: Collect_disj_eq)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	267	(* LAM case *)
1498 2ff84b1f551f Rename bound variables + minor cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1496 diff changeset	268	apply(rule_tac t="supp (LAM' name lam')" and s="supp (Abs {atom name} lam')" in subst)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	269	apply(simp (no_asm) only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	270	apply(simp only: lam'_bp'.perm)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	271	apply(simp only: permute_ABS)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	272	apply(simp only: lam'_bp'.eq_iff)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	273	apply(simp only: Abs_eq_iff)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	274	apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	275	apply(simp only: alpha_gen)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	276	apply(simp only: supp_eqvt[symmetric])
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	277	apply(simp only: eqvts)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	278	apply(simp only: supp_Abs)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	279	(* LET case *)
1498 2ff84b1f551f Rename bound variables + minor cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1496 diff changeset	280	apply(rule_tac t="supp (LET' bp' lam')" and
2ff84b1f551f Rename bound variables + minor cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1496 diff changeset	281	s="supp (Abs (bi' bp') (bp', lam'))" in subst)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	282	apply(simp (no_asm) only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	283	apply(simp only: lam'_bp'.perm)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	284	apply(simp only: permute_ABS)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	285	apply(simp only: lam'_bp'.eq_iff)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	286	apply(simp only: Abs_eq_iff)
1471 7fe643ad19e4 The recursive supp just has one equation too much. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1466 diff changeset	287	apply(simp only: alpha_gen)
7fe643ad19e4 The recursive supp just has one equation too much. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1466 diff changeset	288	apply(simp only: eqvts split_def fst_conv snd_conv)
7fe643ad19e4 The recursive supp just has one equation too much. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1466 diff changeset	289	apply(simp only: eqvts[symmetric] supp_Pair)
7fe643ad19e4 The recursive supp just has one equation too much. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1466 diff changeset	290	apply(simp only: eqvts Pair_eq)
1472 4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	291	apply(simp add: supp_Abs supp_Pair)
4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	292	apply blast
4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	293	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	294	apply(simp only: lam'_bp'.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	295	apply(simp only: lam'_bp'.eq_iff)
1472 4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	296	apply(simp only: de_Morgan_conj)
4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	297	apply(simp only: Collect_disj_eq)
4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	298	apply(simp only: infinite_Un)
4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	299	apply(simp only: Collect_disj_eq)
4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	300	apply(simp only: supp_def[symmetric])
4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	301	apply(simp only: supp_at_base supp_atom)
4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	302	apply simp
4fa5365cd871 Fix in alpha; support of the recursive Let works :) Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1471 diff changeset	303	done
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	304
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	305	thm lam'_bp'.fv[simplified supp_fv'[symmetric]]
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	306
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	307
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: 1258 diff changeset	308	text {* example 2 *}
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: 1258 diff changeset	309
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	310	ML {* val _ = recursive := false *}
1265 fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	311	nominal_datatype trm' =
961 0f88e04eb486 Variable takes a 'name'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 954 diff changeset	312	Var "name"
1265 fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	313	\| App "trm'" "trm'"
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	314	\| Lam x::"name" t::"trm'" bind x in t
1265 fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	315	\| Let p::"pat'" "trm'" t::"trm'" bind "f p" in t
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	316	and pat' =
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	317	PN
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	318	\| PS "name"
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	319	\| PD "name" "name"
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	320	binder
1299 cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	321	f::"pat' \<Rightarrow> atom set"
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	322	where
978 b44592adf235 Improper interface for datatype and function packages and proper interface lateron. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 973 diff changeset	323	"f PN = {}"
1380 dab8d99b37c1 added bn-information, but it is not yet ordered according to the dts Christian Urban <urbanc@in.tum.de> parents: 1378 diff changeset	324	\| "f (PD x y) = {atom x, atom y}"
1299 cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	325	\| "f (PS x) = {atom x}"
1380 dab8d99b37c1 added bn-information, but it is not yet ordered according to the dts Christian Urban <urbanc@in.tum.de> parents: 1378 diff changeset	326
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	327	thm trm'_pat'.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	328	thm trm'_pat'.eq_iff
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	329	thm trm'_pat'.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	330	thm trm'_pat'.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	331	thm trm'_pat'.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	332	thm trm'_pat'.distinct
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	333
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	334	lemma supp_fv_trm'_pat':
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	335	shows "supp t = fv_trm' t"
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	336	and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp"
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	337	apply(induct t and bp rule: trm'_pat'.inducts)
1510 be911e869fde Added fv,bn,distinct,perm to the simplifier. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	338	apply(simp_all)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	339	(* VAR case *)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	340	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	341	apply(simp only: trm'_pat'.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	342	apply(simp only: trm'_pat'.eq_iff)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	343	apply(simp only: supp_def[symmetric])
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	344	apply(simp only: supp_at_base)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	345	(* APP case *)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	346	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	347	apply(simp only: trm'_pat'.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	348	apply(simp only: trm'_pat'.eq_iff)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	349	apply(simp only: de_Morgan_conj)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	350	apply(simp only: Collect_disj_eq)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	351	apply(simp only: infinite_Un)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	352	apply(simp only: Collect_disj_eq)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	353	(* LAM case *)
1498 2ff84b1f551f Rename bound variables + minor cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1496 diff changeset	354	apply(rule_tac t="supp (Lam name trm')" and s="supp (Abs {atom name} trm')" in subst)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	355	apply(simp (no_asm) only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	356	apply(simp only: trm'_pat'.perm)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	357	apply(simp only: permute_ABS)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	358	apply(simp only: trm'_pat'.eq_iff)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	359	apply(simp only: Abs_eq_iff)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	360	apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	361	apply(simp only: alpha_gen)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	362	apply(simp only: supp_eqvt[symmetric])
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	363	apply(simp only: eqvts)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	364	apply(simp only: supp_Abs)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	365	(* LET case *)
1498 2ff84b1f551f Rename bound variables + minor cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1496 diff changeset	366	apply(rule_tac t="supp (Let pat' trm'1 trm'2)"
2ff84b1f551f Rename bound variables + minor cleaning. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1496 diff changeset	367	and s="supp (Abs (f pat') trm'2) \<union> supp trm'1 \<union> fv_f pat'" in subst)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	368	apply(simp (no_asm) only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	369	apply(simp only: trm'_pat'.perm)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	370	apply(simp only: permute_ABS)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	371	apply(simp only: trm'_pat'.eq_iff)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	372	apply(simp only: eqvts)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	373	apply(simp only: Abs_eq_iff)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	374	apply(simp only: ex_simps)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	375	apply(simp only: de_Morgan_conj)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	376	apply(simp only: Collect_disj_eq)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	377	apply(simp only: infinite_Un)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	378	apply(simp only: Collect_disj_eq)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	379	apply(simp only: alpha_gen)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	380	apply(simp only: supp_eqvt[symmetric])
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	381	apply(simp only: eqvts)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	382	apply(blast)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	383	apply(simp add: supp_Abs)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	384	apply(blast)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	385	(* PN case *)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	386	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	387	apply(simp only: trm'_pat'.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	388	apply(simp only: trm'_pat'.eq_iff)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	389	apply(simp)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	390	(* PS case *)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	391	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	392	apply(simp only: trm'_pat'.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	393	apply(simp only: trm'_pat'.eq_iff)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	394	apply(simp only: supp_def[symmetric])
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	395	apply(simp only: supp_at_base)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	396	apply(simp)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	397	(* PD case *)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	398	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	399	apply(simp only: trm'_pat'.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	400	apply(simp only: trm'_pat'.eq_iff)
1465 4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	401	apply(simp only: de_Morgan_conj)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	402	apply(simp only: Collect_disj_eq)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	403	apply(simp only: infinite_Un)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	404	apply(simp only: Collect_disj_eq)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	405	apply(simp only: supp_def[symmetric])
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	406	apply(simp add: supp_at_base)
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	407	done
4de35639fef0 added another supp-proof for the non-recursive case Christian Urban <urbanc@in.tum.de> parents: 1461 diff changeset	408
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	409	thm trm'_pat'.fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]]
1367 9bbf56cdeb88 added compat definitions to some examples Christian Urban <urbanc@in.tum.de> parents: 1365 diff changeset	410
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	411	nominal_datatype trm0 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	412	Var0 "name"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	413	\| App0 "trm0" "trm0"
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	414	\| Lam0 x::"name" t::"trm0" bind x in t
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	415	\| Let0 p::"pat0" "trm0" t::"trm0" bind "f0 p" in t
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	416	and pat0 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	417	PN0
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	418	\| PS0 "name"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	419	\| PD0 "pat0" "pat0"
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	420	binder
1299 cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	421	f0::"pat0 \<Rightarrow> atom set"
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	422	where
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	423	"f0 PN0 = {}"
1299 cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	424	\| "f0 (PS0 x) = {atom x}"
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	425	\| "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	426
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	427	thm trm0_pat0.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	428	thm trm0_pat0.eq_iff
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	429	thm trm0_pat0.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	430	thm trm0_pat0.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	431	thm trm0_pat0.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	432	thm trm0_pat0.distinct
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	433
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	434	text {* example type schemes *}
1285 e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	435
1302 d3101a5b9c4d Length fix for nested recursions. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1299 diff changeset	436	nominal_datatype t =
1416 947e5f772a9c Lifting constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1398 diff changeset	437	VarTS "name"
947e5f772a9c Lifting constants. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1398 diff changeset	438	\| FunTS "t" "t"
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	439	and tyS =
1549 74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	440	All xs::"name fset" ty::"t" bind xs in ty
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	441
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	442	thm t_tyS.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	443	thm t_tyS.eq_iff
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	444	thm t_tyS.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	445	thm t_tyS.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	446	thm t_tyS.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	447	thm t_tyS.distinct
1418 632b08744613 With the 4 cheats, all examples fully lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1416 diff changeset	448
1473 b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	449	ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	450	ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	451
1478 1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	452	lemma finite_fv_t_tyS:
1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	453	fixes T::"t"
1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	454	and S::"tyS"
1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	455	shows "finite (fv_t T)"
1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	456	and "finite (fv_tyS S)"
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	457	apply(induct T and S rule: t_tyS.inducts)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	458	apply(simp_all add: t_tyS.fv)
1478 1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	459	done
1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	460
1473 b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	461	lemma supp_fv_t_tyS:
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	462	shows "supp T = fv_t T"
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	463	and "supp S = fv_tyS S"
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	464	apply(induct T and S rule: t_tyS.inducts)
1510 be911e869fde Added fv,bn,distinct,perm to the simplifier. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	465	apply(simp_all)
1473 b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	466	(* VarTS case *)
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	467	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	468	apply(simp only: t_tyS.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	469	apply(simp only: t_tyS.eq_iff)
1473 b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	470	apply(simp only: supp_def[symmetric])
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	471	apply(simp only: supp_at_base)
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	472	(* FunTS case *)
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	473	apply(simp only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	474	apply(simp only: t_tyS.perm)
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	475	apply(simp only: t_tyS.eq_iff)
1473 b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	476	apply(simp only: de_Morgan_conj)
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	477	apply(simp only: Collect_disj_eq)
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	478	apply(simp only: infinite_Un)
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	479	apply(simp only: Collect_disj_eq)
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	480	(* All case *)
1549 74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	481	apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst)
1473 b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	482	apply(simp (no_asm) only: supp_def)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	483	apply(simp only: t_tyS.perm)
1473 b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	484	apply(simp only: permute_ABS)
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	485	apply(simp only: t_tyS.eq_iff)
1473 b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	486	apply(simp only: Abs_eq_iff)
1549 74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	487	apply(simp only: eqvts)
1473 b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	488	apply(simp only: alpha_gen)
b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	489	apply(simp only: supp_eqvt[symmetric])
1549 74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	490	apply(simp only: eqvts eqvts_raw)
1478 1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	491	apply(rule trans)
1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	492	apply(rule finite_supp_Abs)
1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	493	apply(simp add: finite_fv_t_tyS)
1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	494	apply(simp)
1ea4ca823266 added proof of supp/fv for type schemes Christian Urban <urbanc@in.tum.de> parents: 1473 diff changeset	495	done
1473 b4216d0e109a added partial proof of supp for type schemes Christian Urban <urbanc@in.tum.de> parents: 1472 diff changeset	496
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	497	(* example 1 from Terms.thy *)
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	498
1517 62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	499
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	500
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	501
62d6f7acc110 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant Christian Urban <urbanc@in.tum.de> parents: 1515 diff changeset	502
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	503	nominal_datatype trm1 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	504	Vr1 "name"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	505	\| Ap1 "trm1" "trm1"
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	506	\| Lm1 x::"name" t::"trm1" bind x in t
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	507	\| Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	508	and bp1 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	509	BUnit1
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	510	\| BV1 "name"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	511	\| BP1 "bp1" "bp1"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	512	binder
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	513	bv1
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	514	where
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	515	"bv1 (BUnit1) = {}"
1392 baa67b07f436 parser produces ordered bn-fun information Christian Urban <urbanc@in.tum.de> parents: 1380 diff changeset	516	\| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	517	\| "bv1 (BV1 x) = {atom x}"
1392 baa67b07f436 parser produces ordered bn-fun information Christian Urban <urbanc@in.tum.de> parents: 1380 diff changeset	518
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	519	thm trm1_bp1.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	520	thm trm1_bp1.eq_iff
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	521	thm trm1_bp1.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	522	thm trm1_bp1.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	523	thm trm1_bp1.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	524	thm trm1_bp1.distinct
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	525
1367 9bbf56cdeb88 added compat definitions to some examples Christian Urban <urbanc@in.tum.de> parents: 1365 diff changeset	526	text {* example 3 from Terms.thy *}
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	527
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	528	nominal_datatype trm3 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	529	Vr3 "name"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	530	\| Ap3 "trm3" "trm3"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	531	\| Lm3 x::"name" t::"trm3" bind x in t
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	532	\| Lt3 r::"rassigns3" t::"trm3" bind "bv3 r" in t
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	533	and rassigns3 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	534	ANil
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	535	\| ACons "name" "trm3" "rassigns3"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	536	binder
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	537	bv3
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	538	where
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	539	"bv3 ANil = {}"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	540	\| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	541
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	542	thm trm3_rassigns3.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	543	thm trm3_rassigns3.eq_iff
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	544	thm trm3_rassigns3.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	545	thm trm3_rassigns3.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	546	thm trm3_rassigns3.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	547	thm trm3_rassigns3.distinct
1367 9bbf56cdeb88 added compat definitions to some examples Christian Urban <urbanc@in.tum.de> parents: 1365 diff changeset	548
1251 11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	549	(* example 5 from Terms.thy *)
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	550
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	551	nominal_datatype trm5 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	552	Vr5 "name"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	553	\| Ap5 "trm5" "trm5"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	554	\| Lt5 l::"lts" t::"trm5" bind "bv5 l" in t
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	555	and lts =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	556	Lnil
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	557	\| Lcons "name" "trm5" "lts"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	558	binder
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	559	bv5
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	560	where
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	561	"bv5 Lnil = {}"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	562	\| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	563
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	564	thm trm5_lts.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	565	thm trm5_lts.eq_iff
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	566	thm trm5_lts.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	567	thm trm5_lts.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	568	thm trm5_lts.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	569	thm trm5_lts.distinct
1418 632b08744613 With the 4 cheats, all examples fully lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1416 diff changeset	570
1549 74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	571	lemma
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	572	shows "fv_trm5 t = supp t"
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	573	and "fv_lts l = supp l \<and> fv_bv5 l = {a. infinite {b. \<not>alpha_bv5 ((a \<rightleftharpoons> b) \<bullet> l) l}}"
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	574	apply(induct t and l rule: trm5_lts.inducts)
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	575	apply(simp_all only: trm5_lts.fv)
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	576	apply(simp_all only: supp_Abs[symmetric])
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	577	(apply(simp_all only: supp_abs_sum))
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	578	apply(simp_all (no_asm) only: supp_def)
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	579	apply(simp_all only: trm5_lts.perm)
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	580	apply(simp_all only: permute_ABS)
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	581	apply(simp_all only: trm5_lts.eq_iff Abs_eq_iff)
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	582	(apply(simp_all only: alpha_gen2))
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	583	apply(simp_all only: alpha_gen)
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	584	apply(simp_all only: eqvts[symmetric] supp_Pair)
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	585	apply(simp_all only: eqvts Pair_eq)
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	586	apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	587	apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	588	apply(simp_all only: de_Morgan_conj[symmetric])
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	589	apply simp_all
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	590	done
74888979e9cd Update Test to use fset. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1522 diff changeset	591
1285 e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	592	(* example from my PHD *)
e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	593
e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	594	atom_decl coname
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	595
1341 c25f797c7e6e Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1340 diff changeset	596	nominal_datatype phd =
1290 a7e7ffb7f362 modified for new binding format - hope it is the intended one Christian Urban <urbanc@in.tum.de> parents: 1287 diff changeset	597	Ax "name" "coname"
a7e7ffb7f362 modified for new binding format - hope it is the intended one Christian Urban <urbanc@in.tum.de> parents: 1287 diff changeset	598	\| Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2
a7e7ffb7f362 modified for new binding format - hope it is the intended one Christian Urban <urbanc@in.tum.de> parents: 1287 diff changeset	599	\| AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2
a7e7ffb7f362 modified for new binding format - hope it is the intended one Christian Urban <urbanc@in.tum.de> parents: 1287 diff changeset	600	\| AndL1 n::"name" t::"phd" "name" bind n in t
a7e7ffb7f362 modified for new binding format - hope it is the intended one Christian Urban <urbanc@in.tum.de> parents: 1287 diff changeset	601	\| AndL2 n::"name" t::"phd" "name" bind n in t
a7e7ffb7f362 modified for new binding format - hope it is the intended one Christian Urban <urbanc@in.tum.de> parents: 1287 diff changeset	602	\| ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2
1319 d793ce9cd06f potential problem with the phd-example, where two permutations are generated, but only one is used Christian Urban <urbanc@in.tum.de> parents: 1313 diff changeset	603	\| ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t
d793ce9cd06f potential problem with the phd-example, where two permutations are generated, but only one is used Christian Urban <urbanc@in.tum.de> parents: 1313 diff changeset	604
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	605	thm phd.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	606	thm phd.eq_iff
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	607	thm phd.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	608	thm phd.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	609	thm phd.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	610	thm phd.distinct
1285 e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	611
e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	612	(* example form Leroy 96 about modules; OTT *)
1284 212f3ab40cc2 streamlined parser Christian Urban <urbanc@in.tum.de> parents: 1283 diff changeset	613
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	614	nominal_datatype mexp =
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	615	Acc "path"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	616	\| Stru "body"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	617	\| Funct x::"name" "sexp" m::"mexp" bind x in m
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	618	\| FApp "mexp" "path"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	619	\| Ascr "mexp" "sexp"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	620	and body =
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	621	Empty
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	622	\| Seq c::defn d::"body" bind "cbinders c" in d
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	623	and defn =
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	624	Type "name" "tyty"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	625	\| Dty "name"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	626	\| DStru "name" "mexp"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	627	\| Val "name" "trmtrm"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	628	and sexp =
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	629	Sig sbody
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	630	\| SFunc "name" "sexp" "sexp"
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	631	and sbody =
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	632	SEmpty
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	633	\| SSeq C::spec D::sbody bind "Cbinders C" in D
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	634	and spec =
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	635	Type1 "name"
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	636	\| Type2 "name" "tyty"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	637	\| SStru "name" "sexp"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	638	\| SVal "name" "tyty"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	639	and tyty =
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	640	Tyref1 "name"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	641	\| Tyref2 "path" "tyty"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	642	\| Fun "tyty" "tyty"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	643	and path =
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	644	Sref1 "name"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	645	\| Sref2 "path" "name"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	646	and trmtrm =
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	647	Tref1 "name"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	648	\| Tref2 "path" "name"
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	649	\| Lam' v::"name" "tyty" M::"trmtrm" bind v in M
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	650	\| App' "trmtrm" "trmtrm"
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	651	\| Let' "body" "trmtrm"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	652	binder
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	653	cbinders :: "defn \<Rightarrow> atom set"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	654	and Cbinders :: "spec \<Rightarrow> atom set"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	655	where
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	656	"cbinders (Type t T) = {atom t}"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	657	\| "cbinders (Dty t) = {atom t}"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	658	\| "cbinders (DStru x s) = {atom x}"
1396 08294f4d6c08 Linked parser to fv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1392 diff changeset	659	\| "cbinders (Val v M) = {atom v}"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	660	\| "Cbinders (Type1 t) = {atom t}"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	661	\| "Cbinders (Type2 t T) = {atom t}"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	662	\| "Cbinders (SStru x S) = {atom x}"
1396 08294f4d6c08 Linked parser to fv and alpha. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1392 diff changeset	663	\| "Cbinders (SVal v T) = {atom v}"
1265 fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	664
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	665	thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	666	thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	667	thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	668	thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	669	thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	670	thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	671	thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
1392 baa67b07f436 parser produces ordered bn-fun information Christian Urban <urbanc@in.tum.de> parents: 1380 diff changeset	672
1522 4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	673	lemma
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	674	"fv_mexp j = supp j \<and> fv_body k = supp k \<and>
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	675	(fv_defn c = supp c \<and> fv_cbinders c = {a. infinite {b. \<not>alpha_cbinders ((a \<rightleftharpoons> b) \<bullet> c) c}}) \<and>
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	676	fv_sexp d = supp d \<and> fv_sbody e = supp e \<and>
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	677	(fv_spec l = supp l \<and> fv_Cbinders l = {a. infinite {b. \<not>alpha_Cbinders ((a \<rightleftharpoons> b) \<bullet> l) l}}) \<and>
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	678	fv_tyty g = supp g \<and> fv_path h = supp h \<and> fv_trmtrm i = supp i"
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	679	apply(induct rule: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct)
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	680	apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv)
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	681	apply(simp_all only: supp_Abs[symmetric])
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	682	apply(simp_all (no_asm) only: supp_def)
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	683	apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm)
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	684	apply(simp_all only: permute_ABS)
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	685	apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff Abs_eq_iff)
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	686	apply(simp_all only: alpha_gen)
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	687	apply(simp_all only: eqvts[symmetric] supp_Pair)
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	688	apply(simp_all only: eqvts Pair_eq)
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	689	apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	690	apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	691	apply(simp_all only: de_Morgan_conj[symmetric])
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	692	apply simp_all
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	693	done
4f8bab472a83 Leroy96 supp=fv and fixes to make it compile Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1517 diff changeset	694
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	695	(* example 3 from Peter Sewell's bestiary *)
1418 632b08744613 With the 4 cheats, all examples fully lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1416 diff changeset	696
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	697	nominal_datatype exp =
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	698	VarP "name"
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	699	\| AppP "exp" "exp"
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	700	\| LamP x::"name" e::"exp" bind x in e
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	701	\| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1
1378 5c6c950812b1 All examples should work. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1368 diff changeset	702	and pat3 =
1319 d793ce9cd06f potential problem with the phd-example, where two permutations are generated, but only one is used Christian Urban <urbanc@in.tum.de> parents: 1313 diff changeset	703	PVar "name"
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	704	\| PUnit
1378 5c6c950812b1 All examples should work. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1368 diff changeset	705	\| PPair "pat3" "pat3"
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	706	binder
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	707	bp'' :: "pat3 \<Rightarrow> atom set"
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	708	where
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	709	"bp'' (PVar x) = {atom x}"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	710	\| "bp'' (PUnit) = {}"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	711	\| "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
1418 632b08744613 With the 4 cheats, all examples fully lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1416 diff changeset	712
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	713	thm exp_pat3.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	714	thm exp_pat3.eq_iff
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	715	thm exp_pat3.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	716	thm exp_pat3.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	717	thm exp_pat3.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	718	thm exp_pat3.distinct
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	719
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	720	(* example 6 from Peter Sewell's bestiary *)
1341 c25f797c7e6e Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1340 diff changeset	721	nominal_datatype exp6 =
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	722	EVar name
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	723	\| EPair exp6 exp6
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	724	\| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	725	and pat6 =
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	726	PVar' name
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	727	\| PUnit'
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	728	\| PPair' pat6 pat6
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	729	binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	730	bp6 :: "pat6 \<Rightarrow> atom set"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	731	where
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	732	"bp6 (PVar' x) = {atom x}"
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	733	\| "bp6 (PUnit') = {}"
1341 c25f797c7e6e Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1340 diff changeset	734	\| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
1418 632b08744613 With the 4 cheats, all examples fully lift. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1416 diff changeset	735
1515 76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	736	thm exp6_pat6.fv
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	737	thm exp6_pat6.eq_iff
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	738	thm exp6_pat6.bn
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	739	thm exp6_pat6.perm
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	740	thm exp6_pat6.induct
76fa21f27f22 Rename "_property" to ".property" Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1510 diff changeset	741	thm exp6_pat6.distinct
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	742
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	743	(* THE REST ARE NOT SUPPOSED TO WORK YET *)
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	744
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	745	(* example 7 from Peter Sewell's bestiary *)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	746	(* dest_Const raised
1341 c25f797c7e6e Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1340 diff changeset	747	nominal_datatype exp7 =
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	748	EVar' name
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	749	\| EUnit'
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	750	\| EPair' exp7 exp7
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	751	\| ELetRec' l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	752	and lrb =
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	753	Assign' name exp7
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	754	and lrbs =
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	755	Single' lrb
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	756	\| More' lrb lrbs
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	757	binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	758	b7 :: "lrb \<Rightarrow> atom set" and
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	759	b7s :: "lrbs \<Rightarrow> atom set"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	760	where
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	761	"b7 (Assign x e) = {atom x}"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	762	\| "b7s (Single a) = b7 a"
1341 c25f797c7e6e Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1340 diff changeset	763	\| "b7s (More a as) = (b7 a) \<union> (b7s as)"
1361 1e811e3424f3 With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1355 diff changeset	764	thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	765	*)
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	766
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	767	(* example 8 from Peter Sewell's bestiary *)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	768	(*
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	769	*** fv_bn: recursive argument, but wrong datatype.
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	770	*** At command "nominal_datatype".
1341 c25f797c7e6e Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1340 diff changeset	771	nominal_datatype exp8 =
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	772	EVar' name
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	773	\| EUnit'
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	774	\| EPair' exp8 exp8
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	775	\| ELetRec' l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	776	and fnclause =
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	777	K' x::name p::pat8 e::exp8 bind "b_pat p" in e
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	778	and fnclauses =
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	779	S' fnclause
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	780	\| ORs' fnclause fnclauses
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	781	and lrb8 =
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	782	Clause' fnclauses
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	783	and lrbs8 =
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	784	Single' lrb8
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	785	\| More' lrb8 lrbs8
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	786	and pat8 =
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	787	PVar'' name
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	788	\| PUnit''
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	789	\| PPair'' pat8 pat8
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	790	binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	791	b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	792	b_pat :: "pat8 \<Rightarrow> atom set" and
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	793	b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	794	b_fnclause :: "fnclause \<Rightarrow> atom set" and
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	795	b_lrb8 :: "lrb8 \<Rightarrow> atom set"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	796	where
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	797	"b_lrbs8 (Single' l) = b_lrb8 l"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	798	\| "b_lrbs8 (More' l ls) = b_lrb8 l \<union> b_lrbs8 ls"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	799	\| "b_pat (PVar'' x) = {atom x}"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	800	\| "b_pat (PUnit'') = {}"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	801	\| "b_pat (PPair'' p1 p2) = b_pat p1 \<union> b_pat p2"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	802	\| "b_fnclauses (S' fc) = (b_fnclause fc)"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	803	\| "b_fnclauses (ORs' fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	804	\| "b_lrb8 (Clause' fcs) = (b_fnclauses fcs)"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	805	\| "b_fnclause (K' x pat exp8) = {atom x}"
1361 1e811e3424f3 With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1355 diff changeset	806	thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	807	*)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	808	(* example 4 from Terms.thy *)
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	809	(* fv_eqvt does not work, we need to repaire defined permute functions
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	810	defined fv and defined alpha... *)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	811	(* lists-datastructure does not work yet
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	812	nominal_datatype trm4 =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	813	Vr4 "name"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	814	\| Ap4 "trm4" "trm4 list"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	815	\| Lm4 x::"name" t::"trm4" bind x in t
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	816
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	817	thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	818	thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	819	*)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	820	(* core haskell *)
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	821	atom_decl var
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	822	atom_decl tvar
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	823
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	824	(* there are types, coercion types and regular types *)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	825	(* list-data-structure
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	826	nominal_datatype tkind =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	827	KStar
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	828	\| KFun "tkind" "tkind"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	829	and ckind =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	830	CKEq "ty" "ty"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	831	and ty =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	832	TVar "tvar"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	833	\| TC "string"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	834	\| TApp "ty" "ty"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	835	\| TFun "string" "ty list"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	836	\| TAll tv::"tvar" "tkind" T::"ty" bind tv in T
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	837	\| TEq "ty" "ty" "ty"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	838	and co =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	839	CC "string"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	840	\| CApp "co" "co"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	841	\| CFun "string" "co list"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	842	\| CAll tv::"tvar" "ckind" C::"co" bind tv in C
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	843	\| CEq "co" "co" "co"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	844	\| CSym "co"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	845	\| CCir "co" "co"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	846	\| CLeft "co"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	847	\| CRight "co"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	848	\| CSim "co"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	849	\| CRightc "co"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	850	\| CLeftc "co"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	851	\| CCoe "co" "co"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	852
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	853	abbreviation
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	854	"atoms A \<equiv> atom ` A"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	855
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	856	nominal_datatype trm =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	857	Var "var"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	858	\| C "string"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	859	\| LAM tv::"tvar" "kind" t::"trm" bind tv in t
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	860	\| APP "trm" "ty"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	861	\| Lam v::"var" "ty" t::"trm" bind v in t
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	862	\| App "trm" "trm"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	863	\| Let x::"var" "ty" "trm" t::"trm" bind x in t
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	864	\| Case "trm" "assoc list"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	865	\| Cast "trm" "ty" --"ty is supposed to be a coercion type only"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	866	and assoc =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	867	A p::"pat" t::"trm" bind "bv p" in t
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	868	and pat =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	869	K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	870	binder
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	871	bv :: "pat \<Rightarrow> atom set"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	872	where
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	873	"bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	874	*)
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	875
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	876	text {* weirdo example from Peter Sewell's bestiary *}
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	877
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	878	nominal_datatype weird =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	879	WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	880	bind x in p1, bind x in p2, bind y in p2, bind y in p3
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	881	\| WV "name"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	882	\| WP "weird" "weird"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	883
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	884	thm permute_weird_raw.simps[no_vars]
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	885	thm alpha_weird_raw.intros[no_vars]
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	886	thm fv_weird_raw.simps[no_vars]
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	887
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	888	(* example 6 from Terms.thy *)
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	889
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	890	(* BV is not respectful, needs to fail*)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	891	(*
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	892	nominal_datatype trm6 =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	893	Vr6 "name"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	894	\| Lm6 x::"name" t::"trm6" bind x in t
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	895	\| Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	896	binder
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	897	bv6
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	898	where
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	899	"bv6 (Vr6 n) = {}"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	900	\| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	901	\| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	902	*)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	903
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	904	(* example 7 from Terms.thy *)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	905	(* BV is not respectful, needs to fail*)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	906	(*
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	907	nominal_datatype trm7 =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	908	Vr7 "name"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	909	\| Lm7 l::"name" r::"trm7" bind l in r
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	910	\| Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	911	binder
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	912	bv7
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	913	where
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	914	"bv7 (Vr7 n) = {atom n}"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	915	\| "bv7 (Lm7 n t) = bv7 t - {atom n}"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	916	\| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	917	*)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	918
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	919	(* example 8 from Terms.thy *)
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	920
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	921	(* Binding in a term under a bn, needs to fail *)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	922	(*
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	923	nominal_datatype foo8 =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	924	Foo0 "name"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	925	\| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	926	and bar8 =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	927	Bar0 "name"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	928	\| Bar1 "name" s::"name" b::"bar8" bind s in b
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	929	binder
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	930	bv8
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	931	where
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	932	"bv8 (Bar0 x) = {}"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	933	\| "bv8 (Bar1 v x b) = {atom v}"
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	934	*)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	935	(* example 9 from Terms.thy *)
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	936
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	937	(* BV is not respectful, needs to fail*)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	938	(*
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	939	nominal_datatype lam9 =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	940	Var9 "name"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	941	\| Lam9 n::"name" l::"lam9" bind n in l
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	942	and bla9 =
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	943	Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	944	binder
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	945	bv9
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	946	where
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	947	"bv9 (Var9 x) = {}"
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	948	\| "bv9 (Lam9 x b) = {atom x}"
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	949	*)
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	950
1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	951	(* Type schemes with separate datatypes *)
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	952	nominal_datatype T =
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	953	TVar "name"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	954	\| TFun "T" "T"
1398 1f3c01345c9e Reordered examples in Test. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1396 diff changeset	955
1466 d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	956	(* PROBLEM:
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	957	*** exception Datatype raised
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	958	*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	959	*** At command "nominal_datatype".
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	960	nominal_datatype TyS =
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	961	TAll xs::"name list" ty::"T" bind xs in ty
d18defacda25 commented out examples that should not work; but for example type-scheme example should work Christian Urban <urbanc@in.tum.de> parents: 1465 diff changeset	962	*)
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	963
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	964	(* example 9 from Peter Sewell's bestiary *)
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	965	(* run out of steam at the moment *)
1265 fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	966
961 0f88e04eb486 Variable takes a 'name'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 954 diff changeset	967	end
1223 160343d86a6f "raw"-ified the term-constructors and types given in the specification Christian Urban <urbanc@in.tum.de> parents: 1194 diff changeset	968
160343d86a6f "raw"-ified the term-constructors and types given in the specification Christian Urban <urbanc@in.tum.de> parents: 1194 diff changeset	969
1228 c179ad9d2446 declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types Christian Urban <urbanc@in.tum.de> parents: 1223 diff changeset	970

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Fri, 19 Mar 2010 15:01:01 +0100
changeset 1549	74888979e9cd
parent 1522	4f8bab472a83
child 1553	4355eb3b7161
permissions	-rw-r--r--