--- a/Nominal/Abs.thy Tue Mar 16 17:20:46 2010 +0100
+++ b/Nominal/Abs.thy Tue Mar 16 18:02:08 2010 +0100
@@ -1,146 +1,40 @@
theory Abs
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Quotient" "Quotient_Product"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
begin
-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 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"
+ "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"
notation
alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
-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 [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)
lemma alpha_gen_refl:
assumes a: "R x x"
- shows "(bs, x) \<approx>gen R fv 0 (bs, x)"
+ shows "(bs, x) \<approx>gen R f 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 fv p (cs, y)"
+ assumes a: "(bs, x) \<approx>gen R f p (cs, y)"
and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
- 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
+ shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
+ using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
lemma alpha_gen_trans:
- 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
+ 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)"
+ 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)"
@@ -154,48 +48,77 @@
apply(clarsimp)
done
-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)
+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(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 4)
+ apply(drule_tac pi="- pia" in a)
+ apply(simp)
+ apply(rotate_tac 6)
+ 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)
done
fun
alpha_abs
where
- "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
+ "alpha_abs (bs, x) (cs, y) = (\<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"
shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
apply(simp)
apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
- unfolding alpha_gen
- apply(simp)
+ apply(simp add: alpha_gen)
apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
apply(simp add: swap_set_not_in[OF a1 a2])
apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
@@ -205,15 +128,14 @@
apply(simp add: supp_swap)
done
-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)
+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)"
apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
- unfolding alpha_tst
- apply(simp)
- apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric] eqvt_apply[symmetric])
+ apply(simp add: alpha_gen)
+ apply(simp add: f_eqvt[symmetric] Diff_eqvt[symmetric])
apply(simp add: swap_set_not_in[OF a1 a2])
apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
using a1 a2
@@ -222,16 +144,12 @@
apply(simp add: supp_swap)
done
+
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"
@@ -239,14 +157,6 @@
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)
@@ -272,46 +182,11 @@
apply(simp)
done
-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)
@@ -321,22 +196,6 @@
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)
@@ -350,23 +209,11 @@
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
@@ -392,56 +239,14 @@
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)"
@@ -449,13 +254,6 @@
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)
@@ -463,36 +261,14 @@
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)
-
-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)
-*)
+ using a1 a2 by (lifting alpha_abs_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))
@@ -500,15 +276,6 @@
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)"
@@ -520,17 +287,6 @@
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"
@@ -539,14 +295,6 @@
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"
@@ -555,14 +303,6 @@
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)
@@ -570,13 +310,6 @@
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)"
@@ -585,26 +318,10 @@
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))
-*)
(*
@@ -621,7 +338,32 @@
notation
alpha1 ("_ \<approx>abs1 _")
-lemma
+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 qq:
+ fixes S::"atom set"
+ assumes a: "supp p \<inter> S = {}"
+ shows "p \<bullet> S = S"
+using a
+apply(simp add: supp_perm permute_set_eq)
+apply(auto)
+apply(simp only: disjoint_iff_not_equal)
+apply(simp)
+apply (metis permute_atom_def_raw)
+apply(rule_tac x="(- p) \<bullet> x" in exI)
+apply(simp)
+apply(simp only: disjoint_iff_not_equal)
+apply(simp)
+apply(metis permute_minus_cancel)
+done
+
+lemma alpha_old_new:
assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
shows "({a}, x) \<approx>abs ({b}, y)"
using a
@@ -631,12 +373,11 @@
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)
@@ -644,8 +385,7 @@
apply(simp)
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)
@@ -792,6 +532,9 @@
apply(simp add: zero)
apply(rotate_tac 3)
oops
+lemma tt:
+ "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
+oops
lemma yy:
assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
@@ -800,6 +543,18 @@
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"
@@ -928,6 +683,12 @@
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:
@@ -950,52 +711,11 @@
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)
-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)
+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