nominal2: Nominal/Test.thy@3727e234fe6b (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
1320 447666754176 Another problem with permutations in alpha and possibly also in fv Christian Urban <urbanc@in.tum.de> parents: 1319 diff changeset	5	text {* weirdo example from Peter Sewell's bestiary *}
447666754176 Another problem with permutations in alpha and possibly also in fv Christian Urban <urbanc@in.tum.de> parents: 1319 diff changeset	6
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	7	nominal_datatype weird =
1320 447666754176 Another problem with permutations in alpha and possibly also in fv Christian Urban <urbanc@in.tum.de> parents: 1319 diff changeset	8	WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
447666754176 Another problem with permutations in alpha and possibly also in fv Christian Urban <urbanc@in.tum.de> parents: 1319 diff changeset	9	bind x in p1, bind x in p2, bind y in p2, bind y in p3
1321 bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	10	\| WV "name"
bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	11	\| WP "weird" "weird"
1320 447666754176 Another problem with permutations in alpha and possibly also in fv Christian Urban <urbanc@in.tum.de> parents: 1319 diff changeset	12
1321 bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	13	thm permute_weird_raw.simps[no_vars]
1320 447666754176 Another problem with permutations in alpha and possibly also in fv Christian Urban <urbanc@in.tum.de> parents: 1319 diff changeset	14	thm alpha_weird_raw.intros[no_vars]
447666754176 Another problem with permutations in alpha and possibly also in fv Christian Urban <urbanc@in.tum.de> parents: 1319 diff changeset	15	thm fv_weird_raw.simps[no_vars]
447666754176 Another problem with permutations in alpha and possibly also in fv Christian Urban <urbanc@in.tum.de> parents: 1319 diff changeset	16
1335 c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	17	thm eqvts
c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	18
c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	19	local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding weird_inj}, []), (build_alpha_inj @{thms alpha_weird_raw.intros} @{thms weird_raw.distinct weird_raw.inject} @{thms alpha_weird_raw.cases} ctxt)) ctxt)) *}
c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	20	thm weird_inj
c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	21
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	22	(local_setup {
1335 c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	23	(fn ctxt => snd (Local_Theory.note ((@{binding alpha_eqvt}, []),
c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	24	build_alpha_eqvts [@{term alpha_weird_raw}] [@{term "permute :: perm \<Rightarrow> weird_raw \<Rightarrow> weird_raw"}] @{thms permute_weird_raw.simps weird_inj} @{thm alpha_weird_raw.induct} ctxt) ctxt)) *}
c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	25
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	26	(prove { (snd o snd) (build_alpha_refl_gl [@{term alpha_weird_raw}] ("x","y","z")) *}
1335 c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	27
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	28	apply (tactic {* transp_tac @{context} @{thm alpha_weird_raw.induct} @{thms weird_inj} @{thms weird_raw.inject} @{thms weird_raw.distinct} @{thms alpha_weird_raw.cases} @{thms alpha_eqvt} 1 *})
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	29	*)
1337 7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	30	lemma "alpha_weird_raw x y \<longrightarrow> (\<forall>z. alpha_weird_raw y z \<longrightarrow> alpha_weird_raw x z)"
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	31	apply (rule impI)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	32	apply (erule alpha_weird_raw.induct)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	33	apply (simp_all add: weird_inj)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	34	defer
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	35	apply (rule allI)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	36	apply (rule impI)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	37	apply (erule alpha_weird_raw.cases)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	38	apply (simp_all add: weird_inj)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	39	apply (rule allI)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	40	apply (rule impI)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	41	apply (erule alpha_weird_raw.cases)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	42	apply (simp_all add: weird_inj)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	43	apply (erule conjE)+
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	44	apply (erule exE)+
1338 95fb422bbb2b A version that just leaves the supp/\supp goal. Obviously not true. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1337 diff changeset	45	apply (erule conjE)+
95fb422bbb2b A version that just leaves the supp/\supp goal. Obviously not true. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1337 diff changeset	46	apply (erule exE)+
1337 7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	47	apply (rule conjI)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	48	apply (rule_tac x="pica + pic" in exI)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	49	apply (erule alpha_gen_compose_trans)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	50	apply assumption
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	51	apply (simp add: alpha_eqvt)
1338 95fb422bbb2b A version that just leaves the supp/\supp goal. Obviously not true. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1337 diff changeset	52	apply (rule_tac x="pia + pib" in exI)
95fb422bbb2b A version that just leaves the supp/\supp goal. Obviously not true. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1337 diff changeset	53	apply (rule_tac x="piaa + piba" in exI)
95fb422bbb2b A version that just leaves the supp/\supp goal. Obviously not true. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1337 diff changeset	54	apply (rule conjI)
95fb422bbb2b A version that just leaves the supp/\supp goal. Obviously not true. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1337 diff changeset	55	apply (erule alpha_gen_compose_trans)
95fb422bbb2b A version that just leaves the supp/\supp goal. Obviously not true. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1337 diff changeset	56	apply assumption
95fb422bbb2b A version that just leaves the supp/\supp goal. Obviously not true. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1337 diff changeset	57	apply (simp add: alpha_eqvt)
1337 7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	58	apply (rule conjI)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	59	defer
1338 95fb422bbb2b A version that just leaves the supp/\supp goal. Obviously not true. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1337 diff changeset	60	apply (rule_tac x="pid + pi" in exI)
1335 c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	61	apply (erule alpha_gen_compose_trans)
c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	62	apply assumption
c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	63	apply (simp add: alpha_eqvt)
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	64	sorry
1335 c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	65
1337 7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	66	lemma "alpha_weird_raw x y \<Longrightarrow> alpha_weird_raw y x"
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	67	apply (erule alpha_weird_raw.induct)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	68	apply (simp_all add: weird_inj)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	69	apply (erule conjE)+
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	70	apply (erule exE)+
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	71	apply (erule conjE)+
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	72	apply (erule exE)+
1337 7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	73	apply (rule conjI)
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	74	apply (rule_tac x="- pic" in exI)
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	75	apply (erule alpha_gen_compose_sym)
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	76	apply (simp_all add: alpha_eqvt)
1337 7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	77	apply (rule_tac x="- pia" in exI)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	78	apply (rule_tac x="- pib" in exI)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	79	apply (simp add: minus_add[symmetric])
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	80	apply (rule conjI)
1337 7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	81	apply (erule alpha_gen_compose_sym)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	82	apply (simp_all add: alpha_eqvt)
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	83	apply (rule conjI)
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	84	apply (simp add: supp_minus_perm Int_commute)
1337 7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	85	apply (rule_tac x="- pi" in exI)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	86	apply (erule alpha_gen_compose_sym)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	87	apply (simp_all add: alpha_eqvt)
7ae031bd5d2f Prove symp and transp of weird without the supp /\ supp = {} assumption. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1336 diff changeset	88	done
1335 c3dfd4193b42 Experiments with proving weird transp Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1331 diff changeset	89
1332 103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	90
1321 bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	91	abbreviation "WBind \<equiv> WBind_raw"
bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	92	abbreviation "WP \<equiv> WP_raw"
bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	93	abbreviation "WV \<equiv> WV_raw"
bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	94
bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	95	lemma test:
bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	96	assumes a: "distinct [x, y, z]"
1332 103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	97	shows "alpha_weird_raw (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y)))
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	98	(WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))"
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	99	apply(rule_tac alpha_weird_raw.intros)
1321 bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	100	unfolding alpha_gen
bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	101	using a
1332 103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	102	apply(auto)
1321 bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	103	apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
1332 103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	104	apply(auto)
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	105	apply(simp add: fresh_star_def flip_def fresh_def supp_swap)
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	106	apply(rule alpha_weird_raw.intros)
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	107	apply(simp add: alpha_weird_raw.intros(2))
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	108	apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	109	apply(rule_tac x="0" in exI)
1321 bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	110	apply(simp add: fresh_star_def)
bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	111	apply(auto)
1332 103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	112	apply(rule alpha_weird_raw.intros)
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	113	apply(simp add: alpha_weird_raw.intros(2))
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	114	apply(simp add: flip_def supp_swap supp_perm)
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	115	apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
1321 bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	116	apply(simp)
1332 103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	117	apply(auto)
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	118	apply(simp add: flip_def fresh_def supp_swap)
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	119	apply(rule alpha_weird_raw.intros)
103eb390f1b1 fixed mess in Test.thy Christian Urban <urbanc@in.tum.de> parents: 1331 diff changeset	120	apply(simp add: alpha_weird_raw.intros(2))
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	121	done*)
1321 bfd9af005e23 preliinary test about alpha-weirdo Christian Urban <urbanc@in.tum.de> parents: 1320 diff changeset	122
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	123	text {* example 1 *}
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	124
1316 0577afdb1732 Porting from Lift to Parser; until defining the Quotient type. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1309 diff changeset	125	(* ML {* set show_hyps } )
0577afdb1732 Porting from Lift to Parser; until defining the Quotient type. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1309 diff changeset	126
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	127	nominal_datatype lam =
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	VAR "name"
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	\| APP "lam" "lam"
1287 8557af71724e slight simplification of the raw-decl generation Christian Urban <urbanc@in.tum.de> parents: 1285 diff changeset	130	\| LET bp::"bp" t::"lam" bind "bi bp" in t
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	131	and bp =
1287 8557af71724e slight simplification of the raw-decl generation Christian Urban <urbanc@in.tum.de> parents: 1285 diff changeset	132	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	133	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	134	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	135	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	136	"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	137
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	138	typ lam_raw
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	term VAR_raw
1283 6a133abb7633 generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders" Christian Urban <urbanc@in.tum.de> parents: 1272 diff changeset	140	term APP_raw
6a133abb7633 generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders" Christian Urban <urbanc@in.tum.de> parents: 1272 diff changeset	141	term LET_raw
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	142	term Test.BP_raw
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	143	thm bi_raw.simps
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	144	thm permute_lam_raw_permute_bp_raw.simps
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	145	thm alpha_lam_raw_alpha_bp_raw.intros[no_vars]
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	146	thm fv_lam_raw_fv_bp_raw.simps[no_vars]
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	147	(*thm lam_bp_induct
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	148	thm lam_bp_perm
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	149	thm lam_bp_fv
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	150	thm lam_bp_bn
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	151	thm lam_bp_inject*)
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	152
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: 1258 diff changeset	153	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	154
1265 fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	155	nominal_datatype trm' =
961 0f88e04eb486 Variable takes a 'name'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 954 diff changeset	156	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	157	\| App "trm'" "trm'"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	158	\| 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	159	\| 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	160	and pat' =
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	161	PN
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	162	\| 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	163	\| 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	164	binder
1299 cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	165	f::"pat' \<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	166	where
978 b44592adf235 Improper interface for datatype and function packages and proper interface lateron. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 973 diff changeset	167	"f PN = {}"
1299 cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	168	\| "f (PS x) = {atom x}"
cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	169	\| "f (PD x y) = {atom x, atom y}"
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	170
1320 447666754176 Another problem with permutations in alpha and possibly also in fv Christian Urban <urbanc@in.tum.de> parents: 1319 diff changeset	171
447666754176 Another problem with permutations in alpha and possibly also in fv Christian Urban <urbanc@in.tum.de> parents: 1319 diff changeset	172	thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]
447666754176 Another problem with permutations in alpha and possibly also in fv Christian Urban <urbanc@in.tum.de> parents: 1319 diff changeset	173	thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
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	174	thm f_raw.simps
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	175	(*thm trm'_pat'_induct
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	176	thm trm'_pat'_perm
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	177	thm trm'_pat'_fv
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	178	thm trm'_pat'_bn
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	179	thm trm'_pat'_inject*)
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	180
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	181	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	182	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	183	\| App0 "trm0" "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	184	\| Lam0 x::"name" t::"trm0" 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	185	\| 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	186	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	187	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	188	\| 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	189	\| 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	190	binder
1299 cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	191	f0::"pat0 \<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	192	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	193	"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	194	\| "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	195	\| "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	196
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	197	thm f0_raw.simps
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	198	(*thm trm0_pat0_induct
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	199	thm trm0_pat0_perm
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	200	thm trm0_pat0_fv
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	201	thm trm0_pat0_bn*)
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	202
c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	203	text {* example type schemes *}
1285 e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	204
1304 dc65319809cc Change type schemes to name set. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1302 diff changeset	205	(* does not work yet
1302 d3101a5b9c4d Length fix for nested recursions. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1299 diff changeset	206	nominal_datatype t =
d3101a5b9c4d Length fix for nested recursions. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1299 diff changeset	207	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	208	\| Fun "t" "t"
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	209
1302 d3101a5b9c4d Length fix for nested recursions. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1299 diff changeset	210	nominal_datatype tyS =
1299 cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	211	All xs::"name list" ty::"t_raw" bind xs in ty
cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	212	*)
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	213
1316 0577afdb1732 Porting from Lift to Parser; until defining the Quotient type. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1309 diff changeset	214
1299 cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	215	nominal_datatype t =
cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	216	Var "name"
cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	217	\| Fun "t" "t"
cbcd4997dac5 most tests work - the ones that do not I commented out Christian Urban <urbanc@in.tum.de> parents: 1298 diff changeset	218	and tyS =
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	219	All xs::"name set" 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	220
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	221	(* 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	222
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	223	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	224	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	225	\| Ap1 "trm1" "trm1"
1290 a7e7ffb7f362 modified for new binding format - hope it is the intended one Christian Urban <urbanc@in.tum.de> parents: 1287 diff changeset	226	\| Lm1 x::"name" t::"trm1" 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	227	\| Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 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	228	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	229	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	230	\| 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	231	\| 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	232	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	233	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	234	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	235	"bv1 (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	236	\| "bv1 (BV1 x) = {atom x}"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	237	\| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	238
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	239	thm bv1_raw.simps
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	240
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	241	(* example 2 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	242
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	243	nominal_datatype trm2 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	244	Vr2 "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	245	\| Ap2 "trm2" "trm2"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	246	\| Lm2 x::"name" t::"trm2" 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	247	\| Lt2 r::"rassign" t::"trm2" bind "bv2 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	248	and rassign =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	249	As "name" "trm2"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	250	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	251	bv2
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	252	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	253	"bv2 (As x t) = {atom x}"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	254
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	255	(* example 3 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	256
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	257	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	258	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	259	\| 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	260	\| 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	261	\| 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	262	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	263	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	264	\| 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	265	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	266	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	267	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	268	"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	269	\| "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	270
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	271	(* example 4 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	272
1326 4bc9278a808d weird eqvt Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1322 diff changeset	273	(* fv_eqvt does not work, we need to repaire defined permute functions
4bc9278a808d weird eqvt Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1322 diff changeset	274	defined fv and defined alpha... *)
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	275	nominal_datatype trm4 =
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	276	Vr4 "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	277	\| Ap4 "trm4" "trm4 list"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	278	\| Lm4 x::"name" t::"trm4" bind x in t
1302 d3101a5b9c4d Length fix for nested recursions. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1299 diff changeset	279
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	280	thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
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	281	thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
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	282
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	283	(* 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	284
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	285	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	286	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	287	\| 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	288	\| 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	289	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	290	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	291	\| 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	292	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	293	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	294	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	295	"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	296	\| "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	297
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	298	(* example 6 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	299
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	300	(* BV is not respectful, needs to fail*)
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	301	nominal_datatype trm6 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	302	Vr6 "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	303	\| Lm6 x::"name" t::"trm6" 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	304	\| Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	305	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	306	bv6
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	307	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	308	"bv6 (Vr6 n) = {}"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	309	\| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
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	310	\| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
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	311	(* example 7 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	312
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	313	(* BV is not respectful, needs to fail*)
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	314	nominal_datatype trm7 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	315	Vr7 "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	316	\| Lm7 l::"name" r::"trm7" bind l in r
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	317	\| Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	318	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	319	bv7
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	320	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	321	"bv7 (Vr7 n) = {atom n}"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	322	\| "bv7 (Lm7 n t) = bv7 t - {atom n}"
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	323	\| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
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	324
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	325	(* example 8 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	326
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	327	nominal_datatype foo8 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	328	Foo0 "name"
1283 6a133abb7633 generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders" Christian Urban <urbanc@in.tum.de> parents: 1272 diff changeset	329	\| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
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	330	and bar8 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	331	Bar0 "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	332	\| Bar1 "name" s::"name" b::"bar8" bind s in b
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	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	334	bv8
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	335	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	336	"bv8 (Bar0 x) = {}"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	337	\| "bv8 (Bar1 v x b) = {atom v}"
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	338
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	339	(* example 9 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	340
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	341	(* BV is not respectful, needs to fail*)
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	342	nominal_datatype lam9 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	343	Var9 "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	344	\| Lam9 n::"name" l::"lam9" bind n in l
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	345	and bla9 =
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	346	Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	347	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	348	bv9
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful) Christian Urban <urbanc@in.tum.de> parents: 1232 diff changeset	349	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	350	"bv9 (Var9 x) = {}"
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	351	\| "bv9 (Lam9 x b) = {atom x}"
954 c009d2535896 very rough example file for how nominal2 specification can be parsed Christian Urban <urbanc@in.tum.de> parents: diff changeset	352
1285 e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	353	(* example from my PHD *)
e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	354
e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	355	atom_decl coname
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	356
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	357	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	358	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	359	\| 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	360	\| 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	361	\| 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	362	\| 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	363	\| 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	364	\| 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	365
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	366	thm alpha_phd_raw.intros[no_vars]
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	367	thm fv_phd_raw.simps[no_vars]
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	368
1285 e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	369
e3ac56d3b7af added example from my phd Christian Urban <urbanc@in.tum.de> parents: 1284 diff changeset	370	(* example form Leroy 96 about modules; OTT *)
1284 212f3ab40cc2 streamlined parser Christian Urban <urbanc@in.tum.de> parents: 1283 diff changeset	371
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	372	nominal_datatype mexp =
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	373	Acc "path"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	374	\| Stru "body"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	375	\| Funct x::"name" "sexp" m::"mexp" bind x in m
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	376	\| FApp "mexp" "path"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	377	\| Ascr "mexp" "sexp"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	378	and body =
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	379	Empty
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	380	\| Seq c::defn d::"body" bind "cbinders c" in d
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	381	and defn =
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	382	Type "name" "tyty"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	383	\| Dty "name"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	384	\| DStru "name" "mexp"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	385	\| Val "name" "trmtrm"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	386	and sexp =
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	387	Sig sbody
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	388	\| SFunc "name" "sexp" "sexp"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	389	and sbody =
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	390	SEmpty
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	391	\| 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	392	and spec =
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	393	Type1 "name"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	394	\| Type2 "name" "tyty"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	395	\| SStru "name" "sexp"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	396	\| SVal "name" "tyty"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	397	and tyty =
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	398	Tyref1 "name"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	399	\| Tyref2 "path" "tyty"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	400	\| Fun "tyty" "tyty"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	401	and path =
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	402	Sref1 "name"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	403	\| Sref2 "path" "name"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	404	and trmtrm =
1296 790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	405	Tref1 "name"
790940e90db2 some tuning Christian Urban <urbanc@in.tum.de> parents: 1295 diff changeset	406	\| Tref2 "path" "name"
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	407	\| 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	408	\| App' "trmtrm" "trmtrm"
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	409	\| Let' "body" "trmtrm"
1272 6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	410	binder
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	411	cbinders :: "defn \<Rightarrow> atom set"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	412	and Cbinders :: "spec \<Rightarrow> atom set"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	413	where
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	414	"cbinders (Type t T) = {atom t}"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	415	\| "cbinders (Dty t) = {atom t}"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	416	\| "cbinders (DStru x s) = {atom x}"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	417	\| "cbinders (Val v M) = {atom v}"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	418	\| "Cbinders (Type1 t) = {atom t}"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	419	\| "Cbinders (Type2 t T) = {atom t}"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	420	\| "Cbinders (SStru x S) = {atom x}"
6d140b2c751f added ott-example about Leroy96 Christian Urban <urbanc@in.tum.de> parents: 1265 diff changeset	421	\| "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	422
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	423	(* core haskell *)
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	424	print_theorems
1265 fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	425
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	426	atom_decl var
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	427	atom_decl tvar
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	428
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	429
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	430	(* there are types, coercion types and regular types *)
1351 cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	431	nominal_datatype tkind =
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	432	KStar
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	433	\| KFun "tkind" "tkind"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	434	and ckind =
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	435	CKEq "ty" "ty"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	436	and ty =
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	437	TVar "tvar"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	438	\| TC "string"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	439	\| TApp "ty" "ty"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	440	\| TFun "string" "ty list"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	441	\| TAll tv::"tvar" "tkind" T::"ty" bind tv in T
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	442	\| TEq "ty" "ty" "ty"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	443	and co =
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	444	CC "string"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	445	\| CApp "co" "co"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	446	\| CFun "string" "co list"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	447	\| CAll tv::"tvar" "ckind" C::"co" bind tv in C
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	448	\| CEq "co" "co" "co"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	449	\| CSym "co"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	450	\| CCir "co" "co"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	451	\| CLeft "co"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	452	\| CRight "co"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	453	\| CSim "co"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	454	\| CRightc "co"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	455	\| CLeftc "co"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	456	\| CCoe "co" "co"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	457
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	458
1265 fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	459	typedecl ty --"hack since ty is not yet defined"
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	460
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	461	abbreviation
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	462	"atoms A \<equiv> atom ` A"
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	463
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	464	nominal_datatype trm =
1351 cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	465	Var "var"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	466	\| C "string"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	467	\| LAM tv::"tvar" "kind" t::"trm" bind tv in t
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	468	\| APP "trm" "ty"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	469	\| Lam v::"var" "ty" t::"trm" bind v in t
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	470	\| App "trm" "trm"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	471	\| Let x::"var" "ty" "trm" t::"trm" bind x in t
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	472	\| Case "trm" "assoc list"
cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	473	\| Cast "trm" "ty" --"ty is supposed to be a coercion type only"
1265 fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	474	and assoc =
1351 cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	475	A p::"pat" t::"trm" bind "bv p" 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	476	and pat =
1351 cffc5d78ab7f more proofs in Abs and work on Core Haskell Christian Urban <urbanc@in.tum.de> parents: 1332 diff changeset	477	K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
1265 fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	478	binder
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	479	bv :: "pat \<Rightarrow> atom set"
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	480	where
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	481	"bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
fc8f5897b00a first attempt to make sense out of the core-haskell definition Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	482
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	483	(thm bv_raw.simps)
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	484
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	485	(* example 3 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	486	nominal_datatype exp =
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	487	VarP "name"
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	488	\| AppP "exp" "exp"
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	489	\| LamP x::"name" e::"exp" bind x in e
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	490	\| LetP x::"name" p::"pat" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	491	and pat =
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	492	PVar "name"
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	493	\| PUnit
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	494	\| PPair "pat" "pat"
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	495	binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	496	bp :: "pat \<Rightarrow> atom set"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	497	where
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	498	"bp (PVar x) = {atom x}"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	499	\| "bp (PUnit) = {}"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	500	\| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	501
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	502	thm quot_respect
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	503	(* 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	504	nominal_datatype exp6 =
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	505	EVar name
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	506	\| EPair exp6 exp6
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	507	\| 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	508	and pat6 =
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	509	PVar' name
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	510	\| PUnit'
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	511	\| PPair' pat6 pat6
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	512	binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	513	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	514	where
1340 f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	515	"bp6 (PVar' x) = {atom x}"
f201eb6acafc Lift BV,FV,Permutations and injection :). Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1338 diff changeset	516	\| "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	517	\| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	518
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	519	(* example 7 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	520	nominal_datatype exp7 =
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	521	EVar name
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	522	\| EUnit
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	523	\| EPair exp7 exp7
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	524	\| ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	525	and lrb =
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	526	Assign name exp7
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	527	and lrbs =
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	528	Single lrb
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	529	\| More lrb lrbs
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	530	binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	531	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	532	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	533	where
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	534	"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	535	\| "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	536	\| "b7s (More a as) = (b7 a) \<union> (b7s as)"
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	537
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	538	(* example 8 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	539	nominal_datatype exp8 =
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	540	EVar name
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	541	\| EUnit
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	542	\| EPair exp8 exp8
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	543	\| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	544	and fnclause =
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	545	K x::name p::pat8 e::exp8 bind "b_pat p" in e
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	546	and fnclauses =
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	547	S fnclause
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	548	\| ORs fnclause fnclauses
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	549	and lrb8 =
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	550	Clause fnclauses
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	551	and lrbs8 =
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	552	Single lrb8
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	553	\| More lrb8 lrbs8
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	554	and pat8 =
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	555	PVar name
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	556	\| PUnit
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	557	\| PPair pat8 pat8
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	558	binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	559	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	560	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	561	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	562	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	563	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	564	where
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	565	"b_lrbs8 (Single l) = b_lrb8 l"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	566	\| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	567	\| "b_pat (PVar x) = {atom x}"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	568	\| "b_pat (PUnit) = {}"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	569	\| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	570	\| "b_fnclauses (S fc) = (b_fnclause fc)"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	571	\| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	572	\| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
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	573	\| "b_fnclause (K x pat exp8) = {atom x}"
1312 b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	574
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	575
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	576
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	577
b0eae8c93314 added some more examples from Peter Sewell's bestiary Christian Urban <urbanc@in.tum.de> parents: 1304 diff changeset	578	(* 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	579	(* 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	580
961 0f88e04eb486 Variable takes a 'name'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 954 diff changeset	581	end
1223 160343d86a6f "raw"-ified the term-constructors and types given in the specification Christian Urban <urbanc@in.tum.de> parents: 1194 diff changeset	582
160343d86a6f "raw"-ified the term-constructors and types given in the specification Christian Urban <urbanc@in.tum.de> parents: 1194 diff changeset	583
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	584

author	Christian Urban <urbanc@in.tum.de>
	Thu, 04 Mar 2010 15:56:58 +0100 (2010-03-04)
changeset 1353	3727e234fe6b
parent 1352	cad5f3851569
parent 1341	c25f797c7e6e
child 1355	7b0c6d07a24e
permissions	-rw-r--r--