nominal2: Nominal/Ex/Classical.thy@e44551d067e6 (annotated)

1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Classical
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2436 diff changeset	2	imports "../Nominal2"
1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	5	(* example from Urban's PhD *)
1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	atom_decl name
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	atom_decl coname
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	nominal_datatype trm =
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	Ax "name" "coname"
2311 4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2308 diff changeset	12	\| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2
4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2308 diff changeset	13	\| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2
4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2308 diff changeset	14	\| AndL1 n::"name" t::"trm" "name" bind n in t
4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2308 diff changeset	15	\| AndL2 n::"name" t::"trm" "name" bind n in t
4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2308 diff changeset	16	\| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2
4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2308 diff changeset	17	\| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t
1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	19	thm trm.distinct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	20	thm trm.induct
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	21	thm trm.exhaust
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	22	thm trm.strong_exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	23	thm trm.strong_exhaust[simplified]
2436 3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	24	thm trm.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	25	thm trm.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	26	thm trm.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	27	thm trm.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	28	thm trm.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples Christian Urban <urbanc@in.tum.de> parents: 2434 diff changeset	29	thm trm.size_eqvt
2617 e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	30	thm trm.supp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	31	thm trm.supp[simplified]
1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	32
2434 92dc6cfa3a95 automatic lifting Christian Urban <urbanc@in.tum.de> parents: 2311 diff changeset	33
1866 6d4e4bf9bce6 automatic proofs for equivariance of alphas Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	34
1792 c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	35
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	end
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	37
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	38
c29a139410d2 properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper) Christian Urban <urbanc@in.tum.de> parents: diff changeset	39

author	Christian Urban <urbanc@in.tum.de>
	Wed, 22 Dec 2010 09:13:25 +0000 (2010-12-22)
changeset 2617	e44551d067e6
parent 2454	9ffee4eb1ae1
child 2889	0435c4dfd6f6
permissions	-rw-r--r--