nominal2: Nominal/Ex/Classical.thy@36aeb97fabb0 (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
2008 1bddffddc03f attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing) Christian Urban <urbanc@in.tum.de> parents: 1866 diff changeset	2	imports "../NewParser"
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
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	5	(* example from my Urban's PhD *)
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
2308 387fcbd33820 fixed problem with bn_info Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	10	declare [[STEPS = 9]]
2031 d361a4699176 Added cheats to classical Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2008 diff changeset	11
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	12	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	13	Ax "name" "coname"
2311 4da5c5c29009 work on transitivity proof Christian Urban <urbanc@in.tum.de> parents: 2308 diff changeset	14	\| 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	15	\| 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	16	\| 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	17	\| 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	18	\| 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	19	\| 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	20
2308 387fcbd33820 fixed problem with bn_info Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	21	thm alpha_trm_raw.intros[no_vars]
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	22
2308 387fcbd33820 fixed problem with bn_info Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	23	(*
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	24	thm trm.fv
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	25	thm trm.eq_iff
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	26	thm trm.bn
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	27	thm trm.perm
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	28	thm trm.induct
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	29	thm trm.distinct
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	30	thm trm.fv[simplified trm.supp]
2308 387fcbd33820 fixed problem with bn_info Christian Urban <urbanc@in.tum.de> parents: 2120 diff changeset	31	*)
1866 6d4e4bf9bce6 automatic proofs for equivariance of alphas Christian Urban <urbanc@in.tum.de> parents: 1792 diff changeset	32
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	33
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	34	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	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
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

author	Christian Urban <urbanc@in.tum.de>
	Thu, 01 Jul 2010 14:18:36 +0100 (2010-07-01)
changeset 2343	36aeb97fabb0
parent 2311	4da5c5c29009
child 2434	92dc6cfa3a95
permissions	-rw-r--r--