nominal2: Nominal/Abs.thy@b66d754bf1c2 (annotated)

1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Abs
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	5	lemma permute_boolI:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	6	fixes P::"bool"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	7	shows "p \<bullet> P \<Longrightarrow> P"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	8	apply(simp add: permute_bool_def)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	9	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	10
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	11	lemma permute_boolE:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	12	fixes P::"bool"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	13	shows "P \<Longrightarrow> p \<bullet> P"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	14	apply(simp add: permute_bool_def)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	15	done
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	16
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	17	fun
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	18	alpha_tst
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	19	where
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	20	alpha_tst[simp del]:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	21	"alpha_tst (bs, x) R bv bv' fv p (cs, y) \<longleftrightarrow>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	22	fv x - bv bs = fv y - bv' cs \<and>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	23	(fv x - bv bs) \<sharp>* p \<and>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	24	R (p \<bullet> x) y \<and>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	25	(p \<bullet> bv bs) = bv' cs"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	26
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	27	notation
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	28	alpha_tst ("_ \<approx>tst _ _ _ _ _ _" [100, 100, 100, 100, 100, 100] 100)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	29
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	30	(*
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	31	fun
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	32	alpha_tst_rec
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	33	where
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	34	alpha_tst_rec[simp del]:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	35	"alpha_tst_rec (bs, x) R1 R2 bv fv p (cs, y) \<longleftrightarrow>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	36	fv x - bv bs = fv y - bv cs \<and>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	37	(fv x - bv bs) \<sharp>* p \<and>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	38	R1 (p \<bullet> x) y \<and>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	39	R2 (p \<bullet> bs) cs \<and>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	40	(p \<bullet> bv bs) = bv cs"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	41
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	42	notation
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	43	alpha_tst_rec ("_ \<approx>tstrec _ _ _ _ _ _" [100, 100, 100, 100, 100, 100] 100)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	44	*)
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	45
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	fun
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	alpha_gen
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	where
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	alpha_gen[simp del]:
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	50	"alpha_gen (bs, x) R fv pi (cs, y) \<longleftrightarrow>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	51	fv x - bs = fv y - cs \<and> (fv x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y \<and> pi \<bullet> bs = cs"
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	52
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	53	notation
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	54	alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	55
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	56	fun
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	57	alpha_res
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	58	where
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	59	alpha_res[simp del]:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	60	"alpha_res (bs, x) R fv pi (cs, y) \<longleftrightarrow>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	61	fv x - bs = fv y - cs \<and> (fv x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	62
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	63	notation
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	64	alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	65
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	66	fun
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	67	alpha_lst
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	68	where
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	69	alpha_lst[simp del]:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	70	"alpha_lst (bs, x) R fv pi (cs, y) \<longleftrightarrow>
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	71	fv x - set bs = fv y - set cs \<and> (fv x - set bs) \<sharp>* pi \<and> R (pi \<bullet> x) y"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	72
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	73	notation
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	74	alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	75
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	76
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	77	lemma [mono]:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	78	shows "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	79	and "R1 \<le> R2 \<Longrightarrow> alpha_res x R1 \<le> alpha_res x R2"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	80	apply(case_tac [!] x)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	81	apply(auto simp add: le_fun_def le_bool_def alpha_gen.simps alpha_res.simps)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	82	done
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	83
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	lemma alpha_gen_refl:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	85	assumes a: "R x x"
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	86	shows "(bs, x) \<approx>gen R fv 0 (bs, x)"
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	87	using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	88
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	89	lemma alpha_gen_refl_tst:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	90	assumes a: "R1 x x" "bv bs = bv' bs"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	91	shows "(bs, x) \<approx>tst R1 bv bv' fv 0 (bs, x)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	92	using a
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	93	apply (simp add: alpha_tst fresh_star_def fresh_zero_perm)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	94	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	95
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	96
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	97	lemma alpha_gen_sym:
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	98	assumes a: "(bs, x) \<approx>gen R fv p (cs, y)"
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	99	and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	100	shows "(cs, y) \<approx>gen R fv (- p) (bs, x)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	101	using a
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	102	apply(auto simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	103	apply(simp add: b)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	104	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	105
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	106	lemma alpha_gen_sym_tst:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	107	assumes a: "(bs, x) \<approx>tst R1 bv bv' fv p (cs, y)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	108	and b: "R1 (p \<bullet> x) y \<Longrightarrow> R1 (- p \<bullet> y) x"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	109	shows "(cs, y) \<approx>tst R1 bv' bv fv (- p) (bs, x)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	110	using a
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	111	apply(auto simp add: alpha_tst fresh_star_def fresh_def supp_minus_perm)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	112	apply(simp add: b)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	113	apply(rule_tac p="p" in permute_boolI)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	114	apply(simp add: mem_eqvt)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	115	apply(rule_tac p="- p" in permute_boolI)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	116	apply(simp add: mem_eqvt)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	117	apply(rotate_tac 3)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	118	apply(drule sym)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	119	apply(simp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	120	done
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	121
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	122	lemma alpha_gen_trans:
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	123	assumes a: "(bs, x) \<approx>gen R fv p (cs, y)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	124	and b: "(cs, y) \<approx>gen R fv q (ds, z)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	125	and c: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	126	shows "(bs, x) \<approx>gen R fv (q + p) (ds, z)"
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	127	using a b c
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	using supp_plus_perm
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	apply(simp add: alpha_gen fresh_star_def fresh_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	130	apply(blast)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	131	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	132
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	133	lemma alpha_gen_trans_tst:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	134	assumes a: "(bs, x) \<approx>tst R1 bv bv' fv p (cs, y)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	135	and b: "(cs, y) \<approx>tst R1 bv' bv'' fv q (ds, z)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	136	and c: "\<lbrakk>R1 (p \<bullet> x) y; R1 (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R1 ((q + p) \<bullet> x) z"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	137	shows "(bs, x) \<approx>tst R1 bv bv'' fv (q + p) (ds, z)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	138	using a b c
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	139	using supp_plus_perm
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	140	apply(simp add: alpha_tst fresh_star_def fresh_def)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	141	apply(blast)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	142	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	143
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	144	lemma alpha_gen_eqvt:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	145	assumes a: "(bs, x) \<approx>gen R f q (cs, y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	146	and b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	147	and c: "p \<bullet> (f x) = f (p \<bullet> x)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	148	and d: "p \<bullet> (f y) = f (p \<bullet> y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	149	shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	150	using a b
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	151	apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric])
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	152	apply(simp add: permute_eqvt[symmetric])
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	153	apply(simp add: fresh_star_permute_iff)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	154	apply(clarsimp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	155	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	156
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	157	lemma alpha_gen_eqvt_tst:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	158	assumes a: "(bs, x) \<approx>tst R1 bv bv' fv q (cs, y)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	159	and b1: "R1 (q \<bullet> x) y \<Longrightarrow> R1 (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	160	and c: "p \<bullet> (fv x) = fv (p \<bullet> x)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	161	and d: "p \<bullet> (fv y) = fv (p \<bullet> y)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	162	and e: "p \<bullet> (bv bs) = bv (p \<bullet> bs)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	163	and f: "p \<bullet> (bv cs) = bv (p \<bullet> cs)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	164	and e': "p \<bullet> (bv' bs) = bv' (p \<bullet> bs)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	165	and f': "p \<bullet> (bv' cs) = bv' (p \<bullet> cs)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	166	shows "(p \<bullet> bs, p \<bullet> x) \<approx>tst R1 bv bv' fv (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	167	using a b1
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	168	apply(simp add: alpha_tst c[symmetric] d[symmetric]
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	169	e'[symmetric] f'[symmetric] e[symmetric] f[symmetric] Diff_eqvt[symmetric])
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	170	apply(simp add: permute_eqvt[symmetric])
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	171	apply(simp add: fresh_star_permute_iff)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	172	apply(clarsimp)
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	173	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	174
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	175	fun
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	176	alpha_abs
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	177	where
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	178	"alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	179
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	180	notation
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	181	alpha_abs ("_ \<approx>abs _")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	182
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	183	fun
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	184	alpha_abs_tst
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	185	where
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	186	"alpha_abs_tst (bv, bs, x) (bv',cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>tst (op=) bv bv' supp p (cs, y))"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	187
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	188	notation
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	189	alpha_abs_tst ("_ \<approx>abstst _")
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	190
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	191	lemma alpha_abs_swap:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	192	assumes a1: "a \<notin> (supp x) - bs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	193	and a2: "b \<notin> (supp x) - bs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	194	shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	195	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	196	apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	197	unfolding alpha_gen
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	198	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	199	apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	200	apply(simp add: swap_set_not_in[OF a1 a2])
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	201	apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	202	using a1 a2
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	203	apply(simp add: fresh_star_def fresh_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	204	apply(blast)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	205	apply(simp add: supp_swap)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	206	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	207
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	208	lemma alpha_abs_tst_swap:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	209	assumes a1: "a \<notin> (supp x) - bv bs"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	210	and a2: "b \<notin> (supp x) - bv bs"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	211	shows "(bv, bs, x) \<approx>abstst ((a \<rightleftharpoons> b) \<bullet> bv, (a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	212	apply(simp)
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	213	apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	214	unfolding alpha_tst
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	215	apply(simp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	216	apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric] eqvt_apply[symmetric])
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	217	apply(simp add: swap_set_not_in[OF a1 a2])
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	218	apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	219	using a1 a2
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	220	apply(simp add: fresh_star_def fresh_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	221	apply(blast)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	222	apply(simp add: supp_swap)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	223	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	224
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	225	fun
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	226	supp_abs_fun
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	227	where
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	228	"supp_abs_fun (bs, x) = (supp x) - bs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	229
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	230	fun
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	231	supp_abstst_fun::"('b::pt \<Rightarrow> atom set) \<times> 'b \<times> ('a::pt) \<Rightarrow> atom set"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	232	where
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	233	"supp_abstst_fun (bv, bs, x) = (supp x - bv bs)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	234
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	235	lemma supp_abs_fun_lemma:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	236	assumes a: "x \<approx>abs y"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	237	shows "supp_abs_fun x = supp_abs_fun y"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	238	using a
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	239	apply(induct rule: alpha_abs.induct)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	240	apply(simp add: alpha_gen)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	241	done
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	242
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	243	lemma supp_abstst_fun_lemma:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	244	assumes a: "(bv, bs, x) \<approx>abstst (bv', cs, y)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	245	shows "supp_abstst_fun (bv, bs, x) = supp_abstst_fun (bv', cs, y)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	246	using a
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	247	apply(induct x\<equiv>"(bv, bs, x)" y\<equiv>"(bv', cs, y)" rule: alpha_abs_tst.induct)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	248	apply(simp add: alpha_tst)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	249	done
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	250
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	251	quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	252	apply(rule equivpI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	253	unfolding reflp_def symp_def transp_def
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	254	apply(simp_all)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	255	(* refl *)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	256	apply(clarify)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	257	apply(rule exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	258	apply(rule alpha_gen_refl)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	259	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	260	(* symm *)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	261	apply(clarify)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	262	apply(rule exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	263	apply(rule alpha_gen_sym)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	264	apply(assumption)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	265	apply(clarsimp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	266	(* trans *)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	267	apply(clarify)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	268	apply(rule exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	269	apply(rule alpha_gen_trans)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	270	apply(assumption)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	271	apply(assumption)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	272	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	273	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	274
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	275	term "alpha_abs_tst"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	276
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	277	quotient_type ('a,'b) abs_tst = "(('a \<Rightarrow>atom set) \<times> 'a::pt \<times> 'b::pt)" / "alpha_abs_tst"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	278	apply(rule equivpI)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	279	unfolding reflp_def symp_def transp_def
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	280	apply(simp_all)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	281	(* refl *)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	282	apply(clarify)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	283	apply(rule exI)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	284	apply(rule alpha_gen_refl_tst)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	285	apply(simp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	286	apply(simp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	287	(* symm *)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	288	apply(clarify)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	289	apply(rule exI)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	290	apply(rule alpha_gen_sym_tst)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	291	apply(assumption)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	292	apply(clarsimp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	293	(* trans *)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	294	apply(clarify)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	295	apply(rule exI)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	296	apply(rule alpha_gen_trans_tst)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	297	apply(assumption)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	298	apply(assumption)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	299	apply(simp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	300	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	301
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	302
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	303	quotient_definition
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	304	"Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	305	is
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	306	"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	307
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	308	fun
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	309	Pair_tst
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	310	where
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	311	"Pair_tst a b c = (a, b, c)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	312
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	313	quotient_definition
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	314	"Abs_tst::('b::pt \<Rightarrow> atom set) \<Rightarrow> 'b \<Rightarrow> ('a::pt) \<Rightarrow> ('b, 'a) abs_tst"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	315	is
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	316	"Pair_tst::('b::pt \<Rightarrow> atom set) \<Rightarrow> 'b \<Rightarrow> ('a::pt) \<Rightarrow> (('b \<Rightarrow> atom set) \<times> 'b \<times> 'a)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	317
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	318	lemma [quot_respect]:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	319	shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	320	apply(clarsimp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	321	apply(rule exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	322	apply(rule alpha_gen_refl)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	323	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	324	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	325
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	326	lemma [quot_respect]:
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	327	shows "((op =) ===> (op =) ===> (op =) ===> alpha_abs_tst) Pair_tst Pair_tst"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	328	apply(clarsimp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	329	apply(rule exI)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	330	apply(rule alpha_gen_refl_tst)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	331	apply(simp_all)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	332	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	333
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	334	lemma [quot_respect]:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	335	shows "((op =) ===> (op =) ===> (op =) ===> alpha_abs_tst) Pair_tst Pair_tst"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	336	apply(clarsimp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	337	apply(rule exI)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	338	apply(rule alpha_gen_refl_tst)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	339	apply(simp_all)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	340	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	341
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	342	lemma [quot_respect]:
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	343	shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	344	apply(clarsimp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	345	apply(rule exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	346	apply(rule alpha_gen_eqvt)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	347	apply(assumption)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	348	apply(simp_all add: supp_eqvt)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	349	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	350
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	351	lemma [quot_respect]:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	352	shows "(alpha_abs ===> (op =)) supp_abs_fun supp_abs_fun"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	353	apply(simp add: supp_abs_fun_lemma)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	354	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	355
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	356	lemma [quot_respect]:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	357	shows "(alpha_abs_tst ===> (op =)) supp_abstst_fun supp_abstst_fun"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	358	apply(simp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	359	apply(clarify)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	360	apply(simp add: alpha_tst.simps)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	361	sorry
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	362
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	363
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	364	lemma abs_induct:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	365	"\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	366	apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	367	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	368
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	369	lemma abs_tst_induct:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	370	"\<lbrakk>\<And>bv as (x::'a::pt). P (Abs_tst bv as x)\<rbrakk> \<Longrightarrow> P t"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	371	sorry
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	372
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	373	(* TEST case *)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	374	lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	375	thm abs_induct abs_induct2
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	376
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	377	instantiation abs :: (pt) pt
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	378	begin
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	379
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	380	quotient_definition
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	381	"permute_abs::perm \<Rightarrow> ('a::pt abs) \<Rightarrow> 'a abs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	382	is
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	383	"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	384
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	385	lemma permute_ABS [simp]:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	386	fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	387	shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	388	by (lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"])
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	389
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	390	instance
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	391	apply(default)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	392	apply(induct_tac [!] x rule: abs_induct)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	393	apply(simp_all)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	394	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	395
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	396	end
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	397
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	398	instantiation abs_tst :: (pt, pt) pt
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	399	begin
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	400
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	401	quotient_definition
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	402	"permute_abs_tst::perm \<Rightarrow> (('a::pt, 'b::pt) abs_tst) \<Rightarrow> ('a, 'b) abs_tst"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	403	is
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	404	"permute:: perm \<Rightarrow> ((('a::pt) \<Rightarrow> atom set) \<times> 'a \<times> 'b::pt) \<Rightarrow> (('a \<Rightarrow> atom set) \<times> 'a \<times> 'b)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	405
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	406	lemma permute_ABS_tst [simp]:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	407	fixes x::"'a::pt"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	408	shows "(p \<bullet> (Abs_tst bv as x)) = Abs_tst (p \<bullet> bv) (p \<bullet> as) (p \<bullet> x)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	409	sorry
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	410
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	411	instance
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	412	apply(default)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	413	apply(induct_tac [!] x rule: abs_tst_induct)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	414	apply(simp_all)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	415	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	416
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	417	end
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	418
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	419	quotient_definition
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	420	"supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	421	is
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	422	"supp_abs_fun"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	423
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	424	term supp_abstst_fun
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	425
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	426	quotient_definition
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	427	"supp_Abstst_fun :: ('a::pt, 'b::pt) abs_tst \<Rightarrow> atom \<Rightarrow> bool"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	428	is
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	429	"supp_abstst_fun :: (('a::pt \<Rightarrow> atom \<Rightarrow> bool) \<times> 'a \<times> 'b::pt) \<Rightarrow> atom \<Rightarrow> bool"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	430	(* leave out type *)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	431
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	432	lemma supp_Abs_fun_simp:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	433	shows "supp_Abs_fun (Abs bs x) = (supp x) - bs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	434	by (lifting supp_abs_fun.simps(1))
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	435	thm supp_abs_fun.simps(1)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	436
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	437	term supp_Abs_fun
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	438	term supp_Abstst_fun
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	439
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	440	lemma supp_Abs_tst_fun_simp:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	441	fixes bv::"'b::pt \<Rightarrow> atom set"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	442	shows "supp_Abstst_fun (Abs_tst bv bs x) = (supp x) - (bv bs)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	443	sorry
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	444	(* PROBLEM: regularisation fails
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	445	by (lifting supp_abstst_fun.simps(1))
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	446	*)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	447
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	448
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	449	lemma supp_Abs_fun_eqvt [eqvt]:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	450	shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	451	apply(induct_tac x rule: abs_induct)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	452	apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	453	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	454
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	455	lemma supp_Abs_test_fun_eqvt [eqvt]:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	456	shows "(p \<bullet> supp_Abstst_fun x) = supp_Abstst_fun (p \<bullet> x)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	457	apply(induct_tac x rule: abs_tst_induct)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	458	apply(simp add: supp_Abs_tst_fun_simp supp_eqvt Diff_eqvt)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	459	apply(simp add: eqvt_apply)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	460	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	461
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	462	lemma supp_Abs_fun_fresh:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	463	shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	464	apply(rule fresh_fun_eqvt_app)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	465	apply(simp add: eqvts_raw)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	466	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	467	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	468
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	469
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	470	lemma supp_Abs_tst_fun_fresh:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	471	shows "a \<sharp> Abs_tst bv bs x \<Longrightarrow> a \<sharp> supp_Abstst_fun (Abs_tst bv bs x)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	472	apply(rule fresh_fun_eqvt_app)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	473	apply(simp add: eqvts_raw)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	474	apply(simp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	475	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	476
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	477	lemma Abs_swap:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	478	assumes a1: "a \<notin> (supp x) - bs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	479	and a2: "b \<notin> (supp x) - bs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	480	shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	481	using a1 a2
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	482	by (lifting alpha_abs_swap)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	483
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	484	thm alpha_abs_swap
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	485	thm alpha_abs_tst_swap
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	486
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	487	lemma Abs_tst_swap:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	488	assumes a1: "a \<notin> (supp x) - bv bs"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	489	and a2: "b \<notin> (supp x) - bv bs"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	490	shows "(Abs_tst bv bs x) = (Abs_tst ((a \<rightleftharpoons> b) \<bullet> bv) ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	491	using a1 a2
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	492	sorry
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	493	(* PROBLEM
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	494	by (lifting alpha_abs_tst_swap)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	495	*)
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	496
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	497	lemma Abs_supports:
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	498	shows "(supp x - as) supports (Abs as x)"
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	499	unfolding supports_def
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	500	apply(clarify)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	501	apply(simp (no_asm))
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	502	apply(subst Abs_swap[symmetric])
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	503	apply(simp_all)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	504	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	505
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	506	lemma Abs_tst_supports:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	507	shows "(supp x - bv as) supports (Abs_tst bv as x)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	508	unfolding supports_def
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	509	apply(clarify)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	510	apply(simp (no_asm))
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	511	apply(subst Abs_tst_swap[symmetric])
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	512	apply(simp_all)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	513	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	514
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	515	lemma supp_Abs_subset1:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	516	fixes x::"'a::fs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	517	shows "(supp x) - as \<subseteq> supp (Abs as x)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	518	apply(simp add: supp_conv_fresh)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	519	apply(auto)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	520	apply(drule_tac supp_Abs_fun_fresh)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	521	apply(simp only: supp_Abs_fun_simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	522	apply(simp add: fresh_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	523	apply(simp add: supp_finite_atom_set finite_supp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	524	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	525
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	526	lemma supp_Abs_tst_subset1:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	527	fixes x::"'a::fs"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	528	shows "(supp x - bv as) \<subseteq> supp (Abs_tst bv as x)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	529	apply(simp add: supp_conv_fresh)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	530	apply(auto)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	531	apply(drule_tac supp_Abs_tst_fun_fresh)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	532	apply(simp only: supp_Abs_tst_fun_simp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	533	apply(simp add: fresh_def)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	534	apply(simp add: supp_finite_atom_set finite_supp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	535	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	536
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	537	lemma supp_Abs_subset2:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	538	fixes x::"'a::fs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	539	shows "supp (Abs as x) \<subseteq> (supp x) - as"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	540	apply(rule supp_is_subset)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	541	apply(rule Abs_supports)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	542	apply(simp add: finite_supp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	543	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	544
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	545	lemma supp_Abs_tst_subset2:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	546	fixes x::"'a::fs"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	547	shows "supp (Abs_tst bv as x) \<subseteq> (supp x - bv as)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	548	apply(rule supp_is_subset)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	549	apply(rule Abs_tst_supports)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	550	apply(simp add: finite_supp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	551	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	552
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	553	lemma supp_Abs:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	554	fixes x::"'a::fs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	555	shows "supp (Abs as x) = (supp x) - as"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	556	apply(rule_tac subset_antisym)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	557	apply(rule supp_Abs_subset2)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	558	apply(rule supp_Abs_subset1)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	559	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	560
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	561	lemma supp_Abs_tst:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	562	fixes x::"'a::fs"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	563	shows "supp (Abs_tst bv as x) = (supp x - bv as)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	564	apply(rule_tac subset_antisym)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	565	apply(rule supp_Abs_tst_subset2)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	566	apply(rule supp_Abs_tst_subset1)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	567	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	568
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	569	instance abs :: (fs) fs
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	570	apply(default)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	571	apply(induct_tac x rule: abs_induct)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	572	apply(simp add: supp_Abs)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	573	apply(simp add: finite_supp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	574	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	575
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	576	instance abs_tst :: (pt, fs) fs
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	577	apply(default)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	578	apply(induct_tac x rule: abs_tst_induct)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	579	apply(simp add: supp_Abs_tst)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	580	apply(simp add: finite_supp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	581	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	582
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	583	lemma Abs_fresh_iff:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	584	fixes x::"'a::fs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	585	shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	586	apply(simp add: fresh_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	587	apply(simp add: supp_Abs)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	588	apply(auto)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	589	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	590
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	591	lemma Abs_tst_fresh_iff:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	592	fixes x::"'a::fs"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	593	shows "a \<sharp> Abs_tst bv bs x \<longleftrightarrow> a \<in> bv bs \<or> (a \<notin> bv bs \<and> a \<sharp> x)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	594	apply(simp add: fresh_def)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	595	apply(simp add: supp_Abs_tst)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	596	apply(auto)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	597	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	598
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	599	lemma Abs_eq_iff:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	600	shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	601	by (lifting alpha_abs.simps(1))
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	602
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	603	term alpha_tst
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	604
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	605	lemma Abs_tst_eq_iff:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	606	shows "Abs_tst bv bs x = Abs_tst bv cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>tst (op =) bv bv supp p (cs, y))"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	607	sorry
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	608	(* PROBLEM
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	609	by (lifting alpha_abs_tst.simps(1))
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	610	*)
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	611
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	612
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	613	(*
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	614	below is a construction site for showing that in the
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	615	single-binder case, the old and new alpha equivalence
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	616	coincide
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	617	*)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	618
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	619	fun
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	620	alpha1
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	621	where
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	622	"alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	623
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	624	notation
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	625	alpha1 ("_ \<approx>abs1 _")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	626
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	627	lemma
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	628	assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	629	shows "({a}, x) \<approx>abs ({b}, y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	630	using a
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	631	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	632	apply(erule disjE)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	633	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	634	apply(rule exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	635	apply(rule alpha_gen_refl)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	636	apply(simp)
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	637	apply(simp)
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	638	apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	639	apply(simp add: alpha_gen)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	640	apply(simp add: fresh_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	641	apply(rule conjI)
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	642	apply(rule_tac p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1])
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	643	apply(rule trans)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	644	apply(simp add: Diff_eqvt supp_eqvt)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	645	apply(subst swap_set_not_in)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	646	back
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	647	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	648	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	649	apply(simp add: permute_set_eq)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	650	apply(simp add: eqvts)
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	651	apply(rule_tac p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	652	apply(simp add: permute_self)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	653	apply(simp add: Diff_eqvt supp_eqvt)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	654	apply(simp add: permute_set_eq)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	655	apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	656	apply(simp add: fresh_star_def fresh_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	657	apply(blast)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	658	apply(simp add: supp_swap)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	659	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	660
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	661	lemma perm_zero:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	662	assumes a: "\<forall>x::atom. p \<bullet> x = x"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	663	shows "p = 0"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	664	using a
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	665	by (simp add: expand_perm_eq)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	666
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	667	fun
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	668	add_perm
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	669	where
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	670	"add_perm [] = 0"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	671	\| "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	672
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	673	fun
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	674	elem_perm
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	675	where
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	676	"elem_perm [] = {}"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	677	\| "elem_perm ((a, b) # xs) = {a, b} \<union> elem_perm xs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	678
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	679
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	680	lemma add_perm_apend:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	681	shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	682	apply(induct xs arbitrary: ys)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	683	apply(auto simp add: add_assoc)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	684	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	685
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	686	lemma perm_list_exists:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	687	fixes p::perm
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	688	shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	689	apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	690	apply(rename_tac p)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	691	apply(case_tac "supp p = {}")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	692	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	693	apply(simp add: supp_perm)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	694	apply(drule perm_zero)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	695	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	696	apply(rule_tac x="[]" in exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	697	apply(simp add: supp_Nil)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	698	apply(subgoal_tac "\<exists>x. x \<in> supp p")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	699	defer
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	700	apply(auto)[1]
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	701	apply(erule exE)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	702	apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	703	apply(drule mp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	704	defer
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	705	apply(erule exE)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	706	apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	707	apply(simp add: add_perm_apend)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	708	apply(erule conjE)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	709	apply(drule sym)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	710	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	711	apply(simp add: expand_perm_eq)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	712	apply(simp add: supp_append)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	713	apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	714	apply(rule conjI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	715	prefer 2
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	716	apply(auto)[1]
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	717	apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2))
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	718	defer
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	719	apply(rule psubset_card_mono)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	720	apply(simp add: finite_supp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	721	apply(rule psubsetI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	722	defer
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	723	apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	724	apply(blast)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	725	apply(simp add: supp_perm)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	726	defer
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	727	apply(auto simp add: supp_perm)[1]
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	728	apply(case_tac "x = xa")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	729	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	730	apply(case_tac "((- p) \<bullet> x) = xa")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	731	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	732	apply(case_tac "sort_of xa = sort_of x")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	733	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	734	apply(auto)[1]
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	735	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	736	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	737	apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	738	apply(blast)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	739	apply(auto simp add: supp_perm)[1]
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	740	apply(case_tac "x = xa")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	741	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	742	apply(case_tac "((- p) \<bullet> x) = xa")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	743	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	744	apply(case_tac "sort_of xa = sort_of x")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	745	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	746	apply(auto)[1]
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	747	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	748	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	749	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	750
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	751	lemma tt0:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	752	fixes p::perm
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	753	shows "(supp x) \<sharp>* p \<Longrightarrow> \<forall>a \<in> supp p. a \<sharp> x"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	754	apply(auto simp add: fresh_star_def supp_perm fresh_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	755	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	756
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	757	lemma uu0:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	758	shows "(\<forall>a \<in> elem_perm xs. a \<sharp> x) \<Longrightarrow> (add_perm xs \<bullet> x) = x"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	759	apply(induct xs rule: add_perm.induct)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	760	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	761	apply(simp add: swap_fresh_fresh)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	762	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	763
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	764	lemma yy0:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	765	fixes xs::"(atom \<times> atom) list"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	766	shows "supp xs = elem_perm xs"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	767	apply(induct xs rule: elem_perm.induct)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	768	apply(auto simp add: supp_Nil supp_Cons supp_Pair supp_atom)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	769	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	770
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	771	lemma tt1:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	772	shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	773	apply(drule tt0)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	774	apply(subgoal_tac "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	775	prefer 2
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	776	apply(rule perm_list_exists)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	777	apply(erule exE)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	778	apply(simp only: yy0)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	779	apply(rule uu0)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	780	apply(auto)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	781	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	782
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	783
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	784	lemma perm_induct_test:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	785	fixes P :: "perm => bool"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	786	assumes fin: "finite (supp p)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	787	assumes zero: "P 0"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	788	assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	789	assumes plus: "\<And>p1 p2. \<lbrakk>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	790	shows "P p"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	791	using fin
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	792	apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	793	apply(simp add: supp_perm)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	794	apply(drule perm_zero)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	795	apply(simp add: zero)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	796	apply(rotate_tac 3)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	797	oops
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	798
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	799	lemma yy:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	800	assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	801	shows "S1 = S2"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	802	using assms
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	803	apply (metis insert_Diff_single insert_absorb)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	804	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	805
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	806	lemma kk:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	807	assumes a: "p \<bullet> x = y"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	808	shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	809	using a
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	810	apply(auto)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	811	apply(rule_tac p="- p" in permute_boolI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	812	apply(simp add: mem_eqvt supp_eqvt)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	813	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	814
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	815	lemma ww:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	816	assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	817	shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	818	apply(subgoal_tac "(supp x) supports x")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	819	apply(simp add: supports_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	820	using assms
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	821	apply -
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	822	apply(drule_tac x="a" in spec)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	823	defer
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	824	apply(rule supp_supports)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	825	apply(auto)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	826	apply(rotate_tac 1)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	827	apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	828	apply(simp add: mem_eqvt supp_eqvt)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	829	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	830
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	831	lemma alpha_abs_sym:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	832	assumes a: "({a}, x) \<approx>abs ({b}, y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	833	shows "({b}, y) \<approx>abs ({a}, x)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	834	using a
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	835	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	836	apply(erule exE)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	837	apply(rule_tac x="- p" in exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	838	apply(simp add: alpha_gen)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	839	apply(simp add: fresh_star_def fresh_minus_perm)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	840	apply (metis permute_minus_cancel(2))
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	841	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	842
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	843	lemma alpha_abs_trans:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	844	assumes a: "({a1}, x1) \<approx>abs ({a2}, x2)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	845	assumes b: "({a2}, x2) \<approx>abs ({a3}, x3)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	846	shows "({a1}, x1) \<approx>abs ({a3}, x3)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	847	using a b
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	848	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	849	apply(erule exE)+
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	850	apply(rule_tac x="pa + p" in exI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	851	apply(simp add: alpha_gen)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	852	apply(simp add: fresh_star_def fresh_plus_perm)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	853	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	854
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	855	lemma alpha_equal:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	856	assumes a: "({a}, x) \<approx>abs ({a}, y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	857	shows "(a, x) \<approx>abs1 (a, y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	858	using a
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	859	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	860	apply(erule exE)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	861	apply(simp add: alpha_gen)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	862	apply(erule conjE)+
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	863	apply(case_tac "a \<notin> supp x")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	864	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	865	apply(subgoal_tac "supp x \<sharp>* p")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	866	apply(drule tt1)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	867	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	868	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	869	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	870	apply(case_tac "a \<notin> supp y")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	871	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	872	apply(drule tt1)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	873	apply(clarify)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	874	apply(simp (no_asm_use))
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	875	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	876	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	877	apply(drule yy)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	878	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	879	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	880	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	881	apply(case_tac "a \<sharp> p")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	882	apply(subgoal_tac "supp y \<sharp>* p")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	883	apply(drule tt1)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	884	apply(clarify)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	885	apply(simp (no_asm_use))
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	886	apply(metis)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	887	apply(auto simp add: fresh_star_def)[1]
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	888	apply(frule_tac kk)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	889	apply(drule_tac x="a" in bspec)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	890	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	891	apply(simp add: fresh_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	892	apply(simp add: supp_perm)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	893	apply(subgoal_tac "((p \<bullet> a) \<sharp> p)")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	894	apply(simp add: fresh_def supp_perm)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	895	apply(simp add: fresh_star_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	896	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	897
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	898	lemma alpha_unequal:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	899	assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" "a \<noteq> b"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	900	shows "(a, x) \<approx>abs1 (b, y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	901	using a
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	902	apply -
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	903	apply(subgoal_tac "a \<notin> supp x - {a}")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	904	apply(subgoal_tac "b \<notin> supp x - {a}")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	905	defer
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	906	apply(simp add: alpha_gen)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	907	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	908	apply(drule_tac alpha_abs_swap)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	909	apply(assumption)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	910	apply(simp only: insert_eqvt empty_eqvt swap_atom_simps)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	911	apply(drule alpha_abs_sym)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	912	apply(rotate_tac 4)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	913	apply(drule_tac alpha_abs_trans)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	914	apply(assumption)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	915	apply(drule alpha_equal)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	916	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	917	apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	918	apply(simp add: fresh_eqvt)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	919	apply(simp add: fresh_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	920	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	921
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	922	lemma alpha_new_old:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	923	assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	924	shows "(a, x) \<approx>abs1 (b, y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	925	using a
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	926	apply(case_tac "a=b")
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	927	apply(simp only: alpha_equal)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	928	apply(drule alpha_unequal)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	929	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	930	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	931	apply(simp)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	932	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	933
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	934	(* support of concrete atom sets *)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	935
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	936	lemma atom_eqvt_raw:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	937	fixes p::"perm"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	938	shows "(p \<bullet> atom) = atom"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	939	by (simp add: expand_fun_eq permute_fun_def atom_eqvt)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	940
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	941	lemma atom_image_cong:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	942	shows "(atom ` X = atom ` Y) = (X = Y)"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	943	apply(rule inj_image_eq_iff)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	944	apply(simp add: inj_on_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	945	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	946
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	947	lemma supp_atom_image:
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	948	fixes as::"'a::at_base set"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	949	shows "supp (atom ` as) = supp as"
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	950	apply(simp add: supp_def)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	951	apply(simp add: image_eqvt)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	952	apply(simp add: atom_eqvt_raw)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	953	apply(simp add: atom_image_cong)
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	954	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	955
1449 b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	956	lemma swap_atom_image_fresh:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	957	"\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	958	apply (simp add: fresh_def)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	959	apply (simp add: supp_atom_image)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	960	apply (fold fresh_def)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	961	apply (simp add: swap_fresh_fresh)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	962	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	963
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	964
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	965	(******************************************************)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	966	lemma alpha_gen_compose_sym:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	967	fixes pi
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	968	assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	969	and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	970	shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	971	using b
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	972	apply -
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	973	apply(simp add: alpha_gen.simps)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	974	apply(erule conjE)+
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	975	apply(rule conjI)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	976	apply(simp add: fresh_star_def fresh_minus_perm)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	977	apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	978	apply simp
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	979	apply(clarsimp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	980	apply(rule a)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	981	apply assumption
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	982	done
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	983
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	984	lemma alpha_gen_compose_trans:
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	985	fixes pi pia
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	986	assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	987	and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	988	and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	989	shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	990	using b c apply -
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	991	apply(simp add: alpha_gen.simps)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	992	apply(erule conjE)+
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	993	apply(simp add: fresh_star_plus)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	994	apply(drule_tac x="- pia \<bullet> sa" in spec)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	995	apply(drule mp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	996	apply(rotate_tac 5)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	997	apply(drule_tac pi="- pia" in a)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	998	apply(simp)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	999	apply(rotate_tac 7)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	1000	apply(drule_tac pi="pia" in a)
b66d754bf1c2 proof for support when bn-function is present, but fb_function is empty Christian Urban <urbanc@in.tum.de> parents: 1440 diff changeset	1001	apply(simp)
1440 ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	1002	done
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	1003
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	1004
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	1005	end
ffd5540ac2e9 added preliminary test version....but Test works now Christian Urban <urbanc@in.tum.de> parents: diff changeset	1006

author	Christian Urban <urbanc@in.tum.de>
	Mon, 15 Mar 2010 17:51:35 +0100
changeset 1449	b66d754bf1c2
parent 1440	ffd5540ac2e9
child 1451	104bdc0757e9
permissions	-rw-r--r--