--- a/Nominal/Abs.thy Mon Mar 15 08:39:23 2010 +0100
+++ b/Nominal/Abs.thy Mon Mar 15 17:51:35 2010 +0100
@@ -2,45 +2,145 @@
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
begin
-(* the next three lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
+lemma permute_boolI:
+ fixes P::"bool"
+ shows "p \<bullet> P \<Longrightarrow> P"
+apply(simp add: permute_bool_def)
+done
+
+lemma permute_boolE:
+ fixes P::"bool"
+ shows "P \<Longrightarrow> p \<bullet> P"
+apply(simp add: permute_bool_def)
+done
+fun
+ alpha_tst
+where
+ alpha_tst[simp del]:
+ "alpha_tst (bs, x) R bv bv' fv p (cs, y) \<longleftrightarrow>
+ fv x - bv bs = fv y - bv' cs \<and>
+ (fv x - bv bs) \<sharp>* p \<and>
+ R (p \<bullet> x) y \<and>
+ (p \<bullet> bv bs) = bv' cs"
+
+notation
+ alpha_tst ("_ \<approx>tst _ _ _ _ _ _" [100, 100, 100, 100, 100, 100] 100)
+
+(*
+fun
+ alpha_tst_rec
+where
+ alpha_tst_rec[simp del]:
+ "alpha_tst_rec (bs, x) R1 R2 bv fv p (cs, y) \<longleftrightarrow>
+ fv x - bv bs = fv y - bv cs \<and>
+ (fv x - bv bs) \<sharp>* p \<and>
+ R1 (p \<bullet> x) y \<and>
+ R2 (p \<bullet> bs) cs \<and>
+ (p \<bullet> bv bs) = bv cs"
+
+notation
+ alpha_tst_rec ("_ \<approx>tstrec _ _ _ _ _ _" [100, 100, 100, 100, 100, 100] 100)
+*)
fun
alpha_gen
where
alpha_gen[simp del]:
- "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
- f x - bs = f y - cs \<and> (f x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y \<and> pi \<bullet> bs = cs"
+ "alpha_gen (bs, x) R fv pi (cs, y) \<longleftrightarrow>
+ fv x - bs = fv y - cs \<and> (fv x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y \<and> pi \<bullet> bs = cs"
notation
alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
-lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
- by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps)
+fun
+ alpha_res
+where
+ alpha_res[simp del]:
+ "alpha_res (bs, x) R fv pi (cs, y) \<longleftrightarrow>
+ fv x - bs = fv y - cs \<and> (fv x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y"
+
+notation
+ alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100)
+
+fun
+ alpha_lst
+where
+ alpha_lst[simp del]:
+ "alpha_lst (bs, x) R fv pi (cs, y) \<longleftrightarrow>
+ fv x - set bs = fv y - set cs \<and> (fv x - set bs) \<sharp>* pi \<and> R (pi \<bullet> x) y"
+
+notation
+ alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100)
+
+
+lemma [mono]:
+ shows "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
+ and "R1 \<le> R2 \<Longrightarrow> alpha_res x R1 \<le> alpha_res x R2"
+apply(case_tac [!] x)
+apply(auto simp add: le_fun_def le_bool_def alpha_gen.simps alpha_res.simps)
+done
lemma alpha_gen_refl:
assumes a: "R x x"
- shows "(bs, x) \<approx>gen R f 0 (bs, x)"
+ shows "(bs, x) \<approx>gen R fv 0 (bs, x)"
using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm)
+lemma alpha_gen_refl_tst:
+ assumes a: "R1 x x" "bv bs = bv' bs"
+ shows "(bs, x) \<approx>tst R1 bv bv' fv 0 (bs, x)"
+ using a
+ apply (simp add: alpha_tst fresh_star_def fresh_zero_perm)
+ done
+
+
lemma alpha_gen_sym:
- assumes a: "(bs, x) \<approx>gen R f p (cs, y)"
+ assumes a: "(bs, x) \<approx>gen R fv p (cs, y)"
and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
- shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
- using a b
- by (auto simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
+ shows "(cs, y) \<approx>gen R fv (- p) (bs, x)"
+ using a
+ apply(auto simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
+ apply(simp add: b)
+ done
+
+lemma alpha_gen_sym_tst:
+ assumes a: "(bs, x) \<approx>tst R1 bv bv' fv p (cs, y)"
+ and b: "R1 (p \<bullet> x) y \<Longrightarrow> R1 (- p \<bullet> y) x"
+ shows "(cs, y) \<approx>tst R1 bv' bv fv (- p) (bs, x)"
+ using a
+ apply(auto simp add: alpha_tst fresh_star_def fresh_def supp_minus_perm)
+ apply(simp add: b)
+ apply(rule_tac p="p" in permute_boolI)
+ apply(simp add: mem_eqvt)
+ apply(rule_tac p="- p" in permute_boolI)
+ apply(simp add: mem_eqvt)
+ apply(rotate_tac 3)
+ apply(drule sym)
+ apply(simp)
+ done
lemma alpha_gen_trans:
- assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
- and b: "(cs, y) \<approx>gen R f p2 (ds, z)"
- and c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"
- shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)"
+ assumes a: "(bs, x) \<approx>gen R fv p (cs, y)"
+ and b: "(cs, y) \<approx>gen R fv q (ds, z)"
+ and c: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
+ shows "(bs, x) \<approx>gen R fv (q + p) (ds, z)"
using a b c
using supp_plus_perm
apply(simp add: alpha_gen fresh_star_def fresh_def)
apply(blast)
done
+lemma alpha_gen_trans_tst:
+ assumes a: "(bs, x) \<approx>tst R1 bv bv' fv p (cs, y)"
+ and b: "(cs, y) \<approx>tst R1 bv' bv'' fv q (ds, z)"
+ and c: "\<lbrakk>R1 (p \<bullet> x) y; R1 (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R1 ((q + p) \<bullet> x) z"
+ shows "(bs, x) \<approx>tst R1 bv bv'' fv (q + p) (ds, z)"
+ using a b c
+ using supp_plus_perm
+ apply(simp add: alpha_tst fresh_star_def fresh_def)
+ apply(blast)
+ done
+
lemma alpha_gen_eqvt:
assumes a: "(bs, x) \<approx>gen R f q (cs, y)"
and b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
@@ -54,72 +154,40 @@
apply(clarsimp)
done
-lemma alpha_gen_compose_sym:
- fixes pi
- assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
- and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
- using b apply -
- apply(simp add: alpha_gen.simps)
- apply(erule conjE)+
- apply(rule conjI)
- apply(simp add: fresh_star_def fresh_minus_perm)
- apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
- apply simp
- apply(clarify)
- apply(simp)
- apply(rule a)
- apply assumption
+lemma alpha_gen_eqvt_tst:
+ assumes a: "(bs, x) \<approx>tst R1 bv bv' fv q (cs, y)"
+ and b1: "R1 (q \<bullet> x) y \<Longrightarrow> R1 (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
+ and c: "p \<bullet> (fv x) = fv (p \<bullet> x)"
+ and d: "p \<bullet> (fv y) = fv (p \<bullet> y)"
+ and e: "p \<bullet> (bv bs) = bv (p \<bullet> bs)"
+ and f: "p \<bullet> (bv cs) = bv (p \<bullet> cs)"
+ and e': "p \<bullet> (bv' bs) = bv' (p \<bullet> bs)"
+ and f': "p \<bullet> (bv' cs) = bv' (p \<bullet> cs)"
+ shows "(p \<bullet> bs, p \<bullet> x) \<approx>tst R1 bv bv' fv (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+ using a b1
+ apply(simp add: alpha_tst c[symmetric] d[symmetric]
+ e'[symmetric] f'[symmetric] e[symmetric] f[symmetric] Diff_eqvt[symmetric])
+ apply(simp add: permute_eqvt[symmetric])
+ apply(simp add: fresh_star_permute_iff)
+ apply(clarsimp)
done
-lemma alpha_gen_compose_trans:
- fixes pi pia
- 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)"
- and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
- and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
- using b c apply -
- apply(simp add: alpha_gen.simps)
- apply(erule conjE)+
- apply(simp add: fresh_star_plus)
- apply(drule_tac x="- pia \<bullet> sa" in spec)
- apply(drule mp)
- apply(rotate_tac 5)
- apply(drule_tac pi="- pia" in a)
- apply(simp)
- apply(rotate_tac 7)
- apply(drule_tac pi="pia" in a)
- apply(simp)
- done
-
-lemma alpha_gen_compose_eqvt:
- fixes pia
- assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
- and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
- and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
- shows "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)"
- using b
- apply -
- apply(simp add: alpha_gen.simps)
- apply(erule conjE)+
- apply(rule conjI)
- apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
- apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
- apply(rule conjI)
- apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
- apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
- apply(subst permute_eqvt[symmetric])
- apply(simp)
- oops
-
fun
alpha_abs
where
- "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
+ "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
notation
alpha_abs ("_ \<approx>abs _")
+fun
+ alpha_abs_tst
+where
+ "alpha_abs_tst (bv, bs, x) (bv',cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>tst (op=) bv bv' supp p (cs, y))"
+
+notation
+ alpha_abs_tst ("_ \<approx>abstst _")
+
lemma alpha_abs_swap:
assumes a1: "a \<notin> (supp x) - bs"
and a2: "b \<notin> (supp x) - bs"
@@ -137,14 +205,15 @@
apply(simp add: supp_swap)
done
-lemma alpha_gen_swap_fun:
- assumes f_eqvt: "\<And>pi. (pi \<bullet> (f x)) = f (pi \<bullet> x)"
- assumes a1: "a \<notin> (f x) - bs"
- and a2: "b \<notin> (f x) - bs"
- shows "\<exists>pi. (bs, x) \<approx>gen (op=) f pi ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
+lemma alpha_abs_tst_swap:
+ assumes a1: "a \<notin> (supp x) - bv bs"
+ and a2: "b \<notin> (supp x) - bv bs"
+ shows "(bv, bs, x) \<approx>abstst ((a \<rightleftharpoons> b) \<bullet> bv, (a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
+ apply(simp)
apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
- apply(simp add: alpha_gen)
- apply(simp add: f_eqvt[symmetric] Diff_eqvt[symmetric])
+ unfolding alpha_tst
+ apply(simp)
+ apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric] eqvt_apply[symmetric])
apply(simp add: swap_set_not_in[OF a1 a2])
apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
using a1 a2
@@ -155,9 +224,14 @@
fun
supp_abs_fun
-where
+ where
"supp_abs_fun (bs, x) = (supp x) - bs"
+fun
+ supp_abstst_fun::"('b::pt \<Rightarrow> atom set) \<times> 'b \<times> ('a::pt) \<Rightarrow> atom set"
+ where
+ "supp_abstst_fun (bv, bs, x) = (supp x - bv bs)"
+
lemma supp_abs_fun_lemma:
assumes a: "x \<approx>abs y"
shows "supp_abs_fun x = supp_abs_fun y"
@@ -165,6 +239,14 @@
apply(induct rule: alpha_abs.induct)
apply(simp add: alpha_gen)
done
+
+lemma supp_abstst_fun_lemma:
+ assumes a: "(bv, bs, x) \<approx>abstst (bv', cs, y)"
+ shows "supp_abstst_fun (bv, bs, x) = supp_abstst_fun (bv', cs, y)"
+ using a
+ apply(induct x\<equiv>"(bv, bs, x)" y\<equiv>"(bv', cs, y)" rule: alpha_abs_tst.induct)
+ apply(simp add: alpha_tst)
+ done
quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs"
apply(rule equivpI)
@@ -190,11 +272,49 @@
apply(simp)
done
+term "alpha_abs_tst"
+
+quotient_type ('a,'b) abs_tst = "(('a \<Rightarrow>atom set) \<times> 'a::pt \<times> 'b::pt)" / "alpha_abs_tst"
+ apply(rule equivpI)
+ unfolding reflp_def symp_def transp_def
+ apply(simp_all)
+ (* refl *)
+ apply(clarify)
+ apply(rule exI)
+ apply(rule alpha_gen_refl_tst)
+ apply(simp)
+ apply(simp)
+ (* symm *)
+ apply(clarify)
+ apply(rule exI)
+ apply(rule alpha_gen_sym_tst)
+ apply(assumption)
+ apply(clarsimp)
+ (* trans *)
+ apply(clarify)
+ apply(rule exI)
+ apply(rule alpha_gen_trans_tst)
+ apply(assumption)
+ apply(assumption)
+ apply(simp)
+ done
+
+
quotient_definition
"Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
is
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+fun
+ Pair_tst
+where
+ "Pair_tst a b c = (a, b, c)"
+
+quotient_definition
+ "Abs_tst::('b::pt \<Rightarrow> atom set) \<Rightarrow> 'b \<Rightarrow> ('a::pt) \<Rightarrow> ('b, 'a) abs_tst"
+is
+ "Pair_tst::('b::pt \<Rightarrow> atom set) \<Rightarrow> 'b \<Rightarrow> ('a::pt) \<Rightarrow> (('b \<Rightarrow> atom set) \<times> 'b \<times> 'a)"
+
lemma [quot_respect]:
shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair"
apply(clarsimp)
@@ -204,6 +324,22 @@
done
lemma [quot_respect]:
+ shows "((op =) ===> (op =) ===> (op =) ===> alpha_abs_tst) Pair_tst Pair_tst"
+ apply(clarsimp)
+ apply(rule exI)
+ apply(rule alpha_gen_refl_tst)
+ apply(simp_all)
+ done
+
+lemma [quot_respect]:
+ shows "((op =) ===> (op =) ===> (op =) ===> alpha_abs_tst) Pair_tst Pair_tst"
+ apply(clarsimp)
+ apply(rule exI)
+ apply(rule alpha_gen_refl_tst)
+ apply(simp_all)
+ done
+
+lemma [quot_respect]:
shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"
apply(clarsimp)
apply(rule exI)
@@ -217,11 +353,23 @@
apply(simp add: supp_abs_fun_lemma)
done
+lemma [quot_respect]:
+ shows "(alpha_abs_tst ===> (op =)) supp_abstst_fun supp_abstst_fun"
+ apply(simp)
+ apply(clarify)
+ apply(simp add: alpha_tst.simps)
+ sorry
+
+
lemma abs_induct:
"\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t"
apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
done
+lemma abs_tst_induct:
+ "\<lbrakk>\<And>bv as (x::'a::pt). P (Abs_tst bv as x)\<rbrakk> \<Longrightarrow> P t"
+ sorry
+
(* TEST case *)
lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]
thm abs_induct abs_induct2
@@ -247,14 +395,56 @@
end
+instantiation abs_tst :: (pt, pt) pt
+begin
+
+quotient_definition
+ "permute_abs_tst::perm \<Rightarrow> (('a::pt, 'b::pt) abs_tst) \<Rightarrow> ('a, 'b) abs_tst"
+is
+ "permute:: perm \<Rightarrow> ((('a::pt) \<Rightarrow> atom set) \<times> 'a \<times> 'b::pt) \<Rightarrow> (('a \<Rightarrow> atom set) \<times> 'a \<times> 'b)"
+
+lemma permute_ABS_tst [simp]:
+ fixes x::"'a::pt"
+ shows "(p \<bullet> (Abs_tst bv as x)) = Abs_tst (p \<bullet> bv) (p \<bullet> as) (p \<bullet> x)"
+ sorry
+
+instance
+ apply(default)
+ apply(induct_tac [!] x rule: abs_tst_induct)
+ apply(simp_all)
+ done
+
+end
+
quotient_definition
"supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool"
is
"supp_abs_fun"
+term supp_abstst_fun
+
+quotient_definition
+ "supp_Abstst_fun :: ('a::pt, 'b::pt) abs_tst \<Rightarrow> atom \<Rightarrow> bool"
+is
+ "supp_abstst_fun :: (('a::pt \<Rightarrow> atom \<Rightarrow> bool) \<times> 'a \<times> 'b::pt) \<Rightarrow> atom \<Rightarrow> bool"
+(* leave out type *)
+
lemma supp_Abs_fun_simp:
shows "supp_Abs_fun (Abs bs x) = (supp x) - bs"
by (lifting supp_abs_fun.simps(1))
+thm supp_abs_fun.simps(1)
+
+term supp_Abs_fun
+term supp_Abstst_fun
+
+lemma supp_Abs_tst_fun_simp:
+ fixes bv::"'b::pt \<Rightarrow> atom set"
+ shows "supp_Abstst_fun (Abs_tst bv bs x) = (supp x) - (bv bs)"
+sorry
+(* PROBLEM: regularisation fails
+ by (lifting supp_abstst_fun.simps(1))
+*)
+
lemma supp_Abs_fun_eqvt [eqvt]:
shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)"
@@ -262,6 +452,13 @@
apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt)
done
+lemma supp_Abs_test_fun_eqvt [eqvt]:
+ shows "(p \<bullet> supp_Abstst_fun x) = supp_Abstst_fun (p \<bullet> x)"
+ apply(induct_tac x rule: abs_tst_induct)
+ apply(simp add: supp_Abs_tst_fun_simp supp_eqvt Diff_eqvt)
+ apply(simp add: eqvt_apply)
+ done
+
lemma supp_Abs_fun_fresh:
shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)"
apply(rule fresh_fun_eqvt_app)
@@ -269,14 +466,36 @@
apply(simp)
done
+
+lemma supp_Abs_tst_fun_fresh:
+ shows "a \<sharp> Abs_tst bv bs x \<Longrightarrow> a \<sharp> supp_Abstst_fun (Abs_tst bv bs x)"
+ apply(rule fresh_fun_eqvt_app)
+ apply(simp add: eqvts_raw)
+ apply(simp)
+ done
+
lemma Abs_swap:
assumes a1: "a \<notin> (supp x) - bs"
and a2: "b \<notin> (supp x) - bs"
shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
- using a1 a2 by (lifting alpha_abs_swap)
+ using a1 a2
+ by (lifting alpha_abs_swap)
+
+thm alpha_abs_swap
+thm alpha_abs_tst_swap
+
+lemma Abs_tst_swap:
+ assumes a1: "a \<notin> (supp x) - bv bs"
+ and a2: "b \<notin> (supp x) - bv bs"
+ shows "(Abs_tst bv bs x) = (Abs_tst ((a \<rightleftharpoons> b) \<bullet> bv) ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
+ using a1 a2
+ sorry
+(* PROBLEM
+ by (lifting alpha_abs_tst_swap)
+*)
lemma Abs_supports:
- shows "((supp x) - as) supports (Abs as x)"
+ shows "(supp x - as) supports (Abs as x)"
unfolding supports_def
apply(clarify)
apply(simp (no_asm))
@@ -284,6 +503,15 @@
apply(simp_all)
done
+lemma Abs_tst_supports:
+ shows "(supp x - bv as) supports (Abs_tst bv as x)"
+ unfolding supports_def
+ apply(clarify)
+ apply(simp (no_asm))
+ apply(subst Abs_tst_swap[symmetric])
+ apply(simp_all)
+ done
+
lemma supp_Abs_subset1:
fixes x::"'a::fs"
shows "(supp x) - as \<subseteq> supp (Abs as x)"
@@ -295,6 +523,17 @@
apply(simp add: supp_finite_atom_set finite_supp)
done
+lemma supp_Abs_tst_subset1:
+ fixes x::"'a::fs"
+ shows "(supp x - bv as) \<subseteq> supp (Abs_tst bv as x)"
+ apply(simp add: supp_conv_fresh)
+ apply(auto)
+ apply(drule_tac supp_Abs_tst_fun_fresh)
+ apply(simp only: supp_Abs_tst_fun_simp)
+ apply(simp add: fresh_def)
+ apply(simp add: supp_finite_atom_set finite_supp)
+ done
+
lemma supp_Abs_subset2:
fixes x::"'a::fs"
shows "supp (Abs as x) \<subseteq> (supp x) - as"
@@ -303,6 +542,14 @@
apply(simp add: finite_supp)
done
+lemma supp_Abs_tst_subset2:
+ fixes x::"'a::fs"
+ shows "supp (Abs_tst bv as x) \<subseteq> (supp x - bv as)"
+ apply(rule supp_is_subset)
+ apply(rule Abs_tst_supports)
+ apply(simp add: finite_supp)
+ done
+
lemma supp_Abs:
fixes x::"'a::fs"
shows "supp (Abs as x) = (supp x) - as"
@@ -311,6 +558,14 @@
apply(rule supp_Abs_subset1)
done
+lemma supp_Abs_tst:
+ fixes x::"'a::fs"
+ shows "supp (Abs_tst bv as x) = (supp x - bv as)"
+ apply(rule_tac subset_antisym)
+ apply(rule supp_Abs_tst_subset2)
+ apply(rule supp_Abs_tst_subset1)
+ done
+
instance abs :: (fs) fs
apply(default)
apply(induct_tac x rule: abs_induct)
@@ -318,6 +573,13 @@
apply(simp add: finite_supp)
done
+instance abs_tst :: (pt, fs) fs
+ apply(default)
+ apply(induct_tac x rule: abs_tst_induct)
+ apply(simp add: supp_Abs_tst)
+ apply(simp add: finite_supp)
+ done
+
lemma Abs_fresh_iff:
fixes x::"'a::fs"
shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
@@ -326,10 +588,26 @@
apply(auto)
done
+lemma Abs_tst_fresh_iff:
+ fixes x::"'a::fs"
+ shows "a \<sharp> Abs_tst bv bs x \<longleftrightarrow> a \<in> bv bs \<or> (a \<notin> bv bs \<and> a \<sharp> x)"
+ apply(simp add: fresh_def)
+ apply(simp add: supp_Abs_tst)
+ apply(auto)
+ done
+
lemma Abs_eq_iff:
shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
by (lifting alpha_abs.simps(1))
+term alpha_tst
+
+lemma Abs_tst_eq_iff:
+ 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))"
+sorry
+(* PROBLEM
+by (lifting alpha_abs_tst.simps(1))
+*)
(*
@@ -346,15 +624,6 @@
notation
alpha1 ("_ \<approx>abs1 _")
-fun
- alpha2
-where
- "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))"
-
-notation
- alpha2 ("_ \<approx>abs2 _")
-
-
lemma
assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
shows "({a}, x) \<approx>abs ({b}, y)"
@@ -365,11 +634,12 @@
apply(rule exI)
apply(rule alpha_gen_refl)
apply(simp)
+apply(simp)
apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
apply(simp add: alpha_gen)
apply(simp add: fresh_def)
apply(rule conjI)
-apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1])
+apply(rule_tac p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1])
apply(rule trans)
apply(simp add: Diff_eqvt supp_eqvt)
apply(subst swap_set_not_in)
@@ -378,7 +648,7 @@
apply(simp)
apply(simp add: permute_set_eq)
apply(simp add: eqvts)
-apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
+apply(rule_tac p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
apply(simp add: permute_self)
apply(simp add: Diff_eqvt supp_eqvt)
apply(simp add: permute_set_eq)
@@ -533,18 +803,6 @@
apply (metis insert_Diff_single insert_absorb)
done
-lemma permute_boolI:
- fixes P::"bool"
- shows "p \<bullet> P \<Longrightarrow> P"
-apply(simp add: permute_bool_def)
-done
-
-lemma permute_boolE:
- fixes P::"bool"
- shows "P \<Longrightarrow> p \<bullet> P"
-apply(simp add: permute_bool_def)
-done
-
lemma kk:
assumes a: "p \<bullet> x = y"
shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"
@@ -673,12 +931,6 @@
apply(simp)
done
-fun
- distinct_perms
-where
- "distinct_perms [] = True"
-| "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
-
(* support of concrete atom sets *)
lemma atom_eqvt_raw:
@@ -701,11 +953,52 @@
apply(simp add: atom_image_cong)
done
-lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
- apply (simp add: fresh_def)
- apply (simp add: supp_atom_image)
- apply (fold fresh_def)
- apply (simp add: swap_fresh_fresh)
+lemma swap_atom_image_fresh:
+ "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
+apply (simp add: fresh_def)
+apply (simp add: supp_atom_image)
+apply (fold fresh_def)
+apply (simp add: swap_fresh_fresh)
+done
+
+
+(******************************************************)
+lemma alpha_gen_compose_sym:
+ fixes pi
+ assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
+ and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+ shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
+ using b
+ apply -
+ apply(simp add: alpha_gen.simps)
+ apply(erule conjE)+
+ apply(rule conjI)
+ apply(simp add: fresh_star_def fresh_minus_perm)
+ apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
+ apply simp
+ apply(clarsimp)
+ apply(rule a)
+ apply assumption
+ done
+
+lemma alpha_gen_compose_trans:
+ fixes pi pia
+ 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)"
+ and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
+ and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+ shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
+ using b c apply -
+ apply(simp add: alpha_gen.simps)
+ apply(erule conjE)+
+ apply(simp add: fresh_star_plus)
+ apply(drule_tac x="- pia \<bullet> sa" in spec)
+ apply(drule mp)
+ apply(rotate_tac 5)
+ apply(drule_tac pi="- pia" in a)
+ apply(simp)
+ apply(rotate_tac 7)
+ apply(drule_tac pi="pia" in a)
+ apply(simp)
done