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

1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	1	theory SingleLet
2474 6e37bfb62474 generated inducts rule by Project_Rule.projections Christian Urban <urbanc@in.tum.de> parents: 2473 diff changeset	2	imports "../Nominal2"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	atom_decl name
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	7	nominal_datatype single_let: trm =
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	8	Var "name"
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	9	\| App "trm" "trm"
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	10	\| Lam x::"name" t::"trm" binds x in t
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	11	\| Let a::"assg" t::"trm" binds "bn a" in t
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	12	\| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" binds (set) x in y t t1 t2
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	13	\| Bar x::"name" y::"name" t::"trm" binds y x in t x y
0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	14	\| Baz x::"name" t1::"trm" t2::"trm" binds (set) x in t1, binds (set+) x in t2
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	15	and assg =
2950 0911cb7bf696 changed bind to binds in specifications; bind will cause trouble with Monad_Syntax Christian Urban <urbanc@in.tum.de> parents: 2634 diff changeset	16	As "name" x::"name" t::"trm" binds x in t
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	binder
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	18	bn::"assg \<Rightarrow> atom list"
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19	where
2464 f4eba60cbd69 made the fv-definition aggree more with alpha (needed in the support proofs) Christian Urban <urbanc@in.tum.de> parents: 2461 diff changeset	20	"bn (As x y t) = [atom x]"
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	21
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	22	thm single_let.distinct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	23	thm single_let.induct
2474 6e37bfb62474 generated inducts rule by Project_Rule.projections Christian Urban <urbanc@in.tum.de> parents: 2473 diff changeset	24	thm single_let.inducts
2622 e6e6a3da81aa tuned examples Christian Urban <urbanc@in.tum.de> parents: 2616 diff changeset	25	thm single_let.exhaust
e6e6a3da81aa tuned examples Christian Urban <urbanc@in.tum.de> parents: 2616 diff changeset	26	thm single_let.strong_exhaust
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	27	thm single_let.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	28	thm single_let.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	29	thm single_let.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	30	thm single_let.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	31	thm single_let.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	32	thm single_let.size_eqvt
2448 b9d9c4540265 proved supports lemmas Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	33	thm single_let.supports
2450 217ef3e4282e added proofs for fsupp properties Christian Urban <urbanc@in.tum.de> parents: 2449 diff changeset	34	thm single_let.fsupp
2475 486d4647bb37 supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) Christian Urban <urbanc@in.tum.de> parents: 2474 diff changeset	35	thm single_let.supp
2493 2e174807c891 added postprocessed fresh-lemmas for constructors Christian Urban <urbanc@in.tum.de> parents: 2492 diff changeset	36	thm single_let.fresh
2461 86028b2016bd some experiments with support Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	37
2064 2725853f43b9 solved the problem with equivariance by first eta-normalising the goal Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	38
1596 c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	39	end
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41
c69d9fb16785 Move Ex1 and Ex2 out of Test Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42

author	Cezary Kaliszyk <cezarykaliszyk@gmail.com>
	Thu, 29 Mar 2012 10:37:41 +0200 (2012-03-29)
changeset 3142	4d01d1056e22
parent 2950	0911cb7bf696
permissions	-rw-r--r--