nominal2: Nominal/Ex/Ex3.thy@56b849d348ae (annotated)

1597 af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	1	theory Ex3
2028 15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	2	imports "../NewParser"
1597 af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	begin
af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
1598 2406350c358f Term1 is identical to Example 3 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1597 diff changeset	5	(* Example 3, identical to example 1 from Terms.thy *)
2406350c358f Term1 is identical to Example 3 Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1597 diff changeset	6
1597 af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	atom_decl name
af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8
2028 15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	9	nominal_datatype trm =
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	10	Var "name"
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	11	\| App "trm" "trm"
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	12	\| Lam x::"name" t::"trm" bind_set x in t
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	13	\| Let p::"pat" "trm" t::"trm" bind_set "f p" in t
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	14	and pat =
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	15	PN
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	16	\| PS "name"
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	17	\| PD "pat" "pat"
1597 af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	binder
2028 15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	19	f::"pat \<Rightarrow> atom set"
1597 af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	20	where
2028 15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	21	"f PN = {}"
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	22	\| "f (PS x) = {atom x}"
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	23	\| "f (PD p1 p2) = (f p1) \<union> (f p2)"
1597 af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24
2028 15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	25	thm trm_pat.fv
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	26	thm trm_pat.eq_iff
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	27	thm trm_pat.bn
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	28	thm trm_pat.perm
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	29	thm trm_pat.induct
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	30	thm trm_pat.distinct
15c5a2926622 SingleLet and Ex3 work with NewParser. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1773 diff changeset	31	thm trm_pat.fv[simplified trm_pat.supp(1-2)]
1597 af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	32
2082 0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	33
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	34	declare permute_trm_raw_permute_pat_raw.simps[eqvt]
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	35	declare alpha_gen_eqvt[eqvt]
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	36
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	37	equivariance alpha_trm_raw
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	38
0854af516f14 cleaned up a bit the examples; added equivariance to all examples Christian Urban <urbanc@in.tum.de> parents: 2028 diff changeset	39
1597 af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	40	end
af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	41
af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	42
af34dd3418fe Move example3 out. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	43

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Mon, 10 May 2010 15:54:16 +0200
changeset 2094	56b849d348ae
parent 2082	0854af516f14
child 2104	2205b572bc9b
permissions	-rw-r--r--