--- a/Attic/Quot/quotient_term.ML Mon Mar 15 17:42:17 2010 +0100
+++ b/Attic/Quot/quotient_term.ML Mon Mar 15 23:42:56 2010 +0100
@@ -7,8 +7,6 @@
signature QUOTIENT_TERM =
sig
- exception LIFT_MATCH of string
-
datatype flag = AbsF | RepF
val absrep_fun: flag -> Proof.context -> typ * typ -> term
@@ -65,7 +63,7 @@
fun get_mapfun ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
+ val exn = error ("No map function for type " ^ quote s ^ " found.")
val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
in
Const (mapfun, dummyT)
@@ -91,7 +89,7 @@
TVar _ => mk_Free rty
| Type (_, []) => mk_identity rty
| Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
- | _ => raise LIFT_MATCH "mk_mapfun (default)"
+ | _ => raise (error "mk_mapfun (default)")
in
fold_rev Term.lambda vs' (mk_mapfun_aux rty)
end
@@ -102,7 +100,7 @@
fun get_rty_qty ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
+ val exn = error ("No quotient type " ^ quote s ^ " found.")
val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
in
(#rtyp qdata, #qtyp qdata)
@@ -148,7 +146,7 @@
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
val ty_str = Syntax.string_of_typ ctxt ty
in
- raise LIFT_MATCH (space_implode " "
+ raise error (cat_lines
["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
end
@@ -233,9 +231,9 @@
| (TFree x, TFree x') =>
if x = x'
then mk_identity rty
- else raise (LIFT_MATCH "absrep_fun (frees)")
+ else raise (error "absrep_fun (frees)")
| (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
- | _ => raise (LIFT_MATCH "absrep_fun (default)")
+ | _ => raise (error "absrep_fun (default)")
fun absrep_fun_chk flag ctxt (rty, qty) =
absrep_fun flag ctxt (rty, qty)
@@ -270,7 +268,7 @@
fun get_relmap ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
+ val exn = error ("get_relmap (no relation map function found for type " ^ s ^ ")")
val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
in
Const (relmap, dummyT)
@@ -285,7 +283,7 @@
TVar _ => mk_Free rty
| Type (_, []) => HOLogic.eq_const rty
| Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
- | _ => raise LIFT_MATCH ("mk_relmap (default)")
+ | _ => raise (error "mk_relmap (default)")
in
fold_rev Term.lambda vs' (mk_relmap_aux rty)
end
@@ -293,7 +291,7 @@
fun get_equiv_rel ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
+ val exn = error ("get_quotdata (no quotient found for type " ^ s ^ ")")
in
#equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
end
@@ -303,7 +301,7 @@
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
val ty_str = Syntax.string_of_typ ctxt ty
in
- raise LIFT_MATCH (space_implode " "
+ raise error (space_implode " "
["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
end
@@ -410,7 +408,7 @@
val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
in
- raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
+ raise error (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
end
(* the major type of All and Ex quantifiers *)
@@ -573,14 +571,14 @@
| (Bound i, Bound i') =>
if i = i' then rtrm
- else raise (LIFT_MATCH "regularize (bounds mismatch)")
+ else raise (error "regularize (bounds mismatch)")
| _ =>
let
val rtrm_str = Syntax.string_of_term ctxt rtrm
val qtrm_str = Syntax.string_of_term ctxt qtrm
in
- raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
+ raise (error ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
end
fun regularize_trm_chk ctxt (rtrm, qtrm) =
@@ -628,7 +626,7 @@
val rtrm_str = Syntax.string_of_term ctxt rtrm
val qtrm_str = Syntax.string_of_term ctxt qtrm
in
- raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
+ raise error (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
end
--- a/Nominal/Abs.thy Mon Mar 15 17:42:17 2010 +0100
+++ b/Nominal/Abs.thy Mon Mar 15 23:42:56 2010 +0100
@@ -1,46 +1,146 @@
theory Abs
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
+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,75 +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
- 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)
- apply(simp add: c[symmetric])
- apply(subst permute_eqvt[symmetric])
- apply simp
+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
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"
@@ -140,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
@@ -158,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"
@@ -168,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)
@@ -193,11 +272,46 @@
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)
@@ -207,6 +321,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)
@@ -220,11 +350,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
@@ -250,14 +392,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)"
@@ -265,6 +449,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)
@@ -272,14 +463,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))
@@ -287,6 +500,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)"
@@ -298,6 +520,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"
@@ -306,6 +539,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"
@@ -314,6 +555,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)
@@ -321,6 +570,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)"
@@ -329,10 +585,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))
+*)
(*
@@ -349,15 +621,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)"
@@ -368,11 +631,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)
@@ -381,7 +645,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)
@@ -536,18 +800,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"
@@ -676,12 +928,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:
@@ -704,11 +950,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