nominal2: comparison Nominal/GPerm.thy

equal deleted inserted replaced

-:4cf3a4d36799
+:9876d73adb2b
 by (metis uminus_perm_raw_def)
 lemma uminus_perm_raw_rsp[simp]:
 "x \<approx> y \<Longrightarrow> map swap_pair x \<approx> map swap_pair y"
 by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
-lemma [quot_respect]:
-"(op \<approx> ===> op \<approx>) uminus_perm_raw uminus_perm_raw"
-by (auto intro!: fun_relI simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
 lemma fst_snd_map_pair[simp]:
 "fst ` map_pair f g ` set l = f ` fst ` set l"
 "snd ` map_pair f g ` set l = g ` snd ` set l"
 by (induct l) auto
 lemma perm_add_raw_rsp[simp]:
 "x \<approx> y \<Longrightarrow> xa \<approx> ya \<Longrightarrow> perm_add_raw x xa \<approx> perm_add_raw y ya"
 by (simp add: fun_eq_iff perm_add_apply perm_eq_def)
-lemma [quot_respect]:
-"(op \<approx> ===> op \<approx> ===> op \<approx>) perm_add_raw perm_add_raw"
-by (auto intro!: fun_relI simp add: perm_add_raw_rsp)
 lemma [simp]:
 "a \<approx> a \<longleftrightarrow> valid_perm a"
 by (simp_all add: perm_eq_def)
-lemma [quot_respect]: "[] \<approx> []"
-by auto
-lemmas [simp] = in_respects
 instantiation gperm :: (type) group_add
 begin
-quotient_definition "0 :: 'a gperm" is "[] :: ('a \<times> 'a) list"
+lift_definition zero_gperm :: "'a gperm" is "[]" by simp
-quotient_definition "uminus :: 'a gperm \<Rightarrow> 'a gperm" is
+lift_definition uminus_gperm :: "'a gperm \<Rightarrow> 'a gperm" is uminus_perm_raw
-"uminus_perm_raw :: ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list"
+by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
-quotient_definition "(op +) :: 'a gperm \<Rightarrow> 'a gperm \<Rightarrow> 'a gperm" is
+lift_definition plus_gperm :: "'a gperm \<Rightarrow> 'a gperm \<Rightarrow> 'a gperm" is perm_add_raw
-"perm_add_raw :: ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list"
+by simp
 definition
 minus_perm_def: "(p1::'a gperm) - p2 = p1 + - p2"
 instance
 apply default
 unfolding minus_perm_def
-by (partiality_descending, simp add: perm_add_apply perm_eq_def fun_eq_iff valid_perm_add_minus)+
+by (transfer,simp add: perm_add_apply perm_eq_def fun_eq_iff valid_perm_add_minus)+
 end
 definition "mk_perm_raw l = (if valid_perm l then l else [])"
-quotient_definition "mk_perm :: ('a \<times> 'a) list \<Rightarrow> 'a gperm"
+lift_definition mk_perm :: "('a \<times> 'a) list \<Rightarrow> 'a gperm" is "mk_perm_raw"
-is "mk_perm_raw"
+by (simp add: mk_perm_raw_def)
 definition "dest_perm_raw p = sort [x\<leftarrow>p. fst x \<noteq> snd x]"
-quotient_definition "dest_perm :: ('a :: linorder) gperm \<Rightarrow> ('a \<times> 'a) list"
-is "dest_perm_raw"
-lemma [quot_respect]: "(op = ===> op \<approx>) mk_perm_raw mk_perm_raw"
-by (auto intro!: fun_relI simp add: mk_perm_raw_def)
 lemma distinct_fst_distinct[simp]: "distinct (map fst x) \<Longrightarrow> distinct x"
 by (induct x) auto
 lemma perm_apply_in_set:
 apply (metis in_set_in_dpr3 fun_eq_iff)
 unfolding dest_perm_raw_def
 by (rule sorted_distinct_set_unique)
 (simp_all add: distinct_filter valid_perm_def perm_eq_not_eq_same[simplified perm_eq_def, simplified])
-lemma [quot_respect]:
+lift_definition dest_perm :: "('a :: linorder) gperm \<Rightarrow> ('a \<times> 'a) list"
-"(op \<approx> ===> op =) dest_perm_raw dest_perm_raw"
+is "dest_perm_raw"
-by (auto intro!: fun_relI simp add: perm_eq_def)
+by (simp add: perm_eq_def)
 lemma dest_perm_mk_perm[simp]:
 "dest_perm (mk_perm xs) = sort [x\<leftarrow>mk_perm_raw xs. fst x \<noteq> snd x]"
-by (partiality_descending)
+by transfer (simp add: dest_perm_raw_def)
-(simp add: dest_perm_raw_def)
 lemma valid_perm_filter_id[simp]:
 "valid_perm p \<Longrightarrow> valid_perm [x\<leftarrow>p. fst x \<noteq> snd x]"
 proof (simp (no_asm) add: valid_perm_def, intro conjI)
 show "valid_perm p \<Longrightarrow> distinct (map fst [x\<Colon>'a \<times> 'a\<leftarrow>p . fst x \<noteq> snd x])"
 "valid_perm p \<Longrightarrow> p \<approx> dest_perm_raw p"
 by (simp_all add: dest_perm_raw_eq[symmetric])
 lemma mk_perm_dest_perm[code abstype]:
 "mk_perm (dest_perm p) = p"
-by (partiality_descending)
+by transfer
 (auto simp add: mk_perm_raw_def)
 instantiation gperm :: (linorder) equal begin
 definition equal_gperm_def: "equal_gperm a b \<longleftrightarrow> dest_perm a = dest_perm b"
 instance
 apply default
 unfolding equal_gperm_def
-by partiality_descending simp
+by transfer simp
 end
 lemma [code abstract]:
 "dest_perm 0 = []"
-by (partiality_descending) (simp add: dest_perm_raw_def)
+by transfer (simp add: dest_perm_raw_def)
 lemma [code abstract]:
 "dest_perm (-a) = dest_perm_raw (uminus_perm_raw (dest_perm a))"
-by (partiality_descending) (auto)
+by transfer auto
 lemma [code abstract]:
 "dest_perm (a + b) = dest_perm_raw (perm_add_raw (dest_perm a) (dest_perm b))"
-by (partiality_descending) auto
+by transfer auto
-quotient_definition "gpermute :: 'a gperm \<Rightarrow> 'a \<Rightarrow> 'a"
+lift_definition gpermute :: "'a gperm \<Rightarrow> 'a \<Rightarrow> 'a"
 is perm_apply
+by (simp add: perm_eq_def)
-lemma [quot_respect]: "(op \<approx> ===> op =) perm_apply perm_apply"
-by (auto intro!: fun_relI simp add: perm_eq_def)
 lemma gpermute_zero[simp]:
 "gpermute 0 x = x"
-by descending simp
+by transfer simp
 lemma gpermute_add[simp]:
 "gpermute (p + q) x = gpermute p (gpermute q x)"
-by descending (simp add: perm_add_apply)
+by transfer (simp add: perm_add_apply)
-definition [simp]:"swap_raw a b = (if a = b then [] else [(a, b), (b, a)])"
+definition [simp]: "swap_raw a b = (if a = b then [] else [(a, b), (b, a)])"
-lemma [quot_respect]: "(op = ===> op = ===> op \<approx>) swap_raw swap_raw"
+lift_definition gswap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a gperm" is swap_raw
-by (auto intro!: fun_relI simp add: valid_perm_def)
+by (auto simp add: valid_perm_def)
-quotient_definition "gswap :: 'a \<Rightarrow> 'a \<Rightarrow> 'a gperm"
-is swap_raw
 lemma [code abstract]:
 "dest_perm (gswap a b) = (if (a, b) \<le> (b, a) then swap_raw a b else swap_raw b a)"
-by (partiality_descending) (auto simp add: dest_perm_raw_def)
+by transfer (auto simp add: dest_perm_raw_def)
 lemma swap_self [simp]:
 "gswap a a = 0"
-by (partiality_descending, auto)
+by transfer simp
 lemma [simp]: "a \<noteq> b \<Longrightarrow> valid_perm [(a, b), (b, a)]"
 unfolding valid_perm_def by auto
 lemma swap_cancel [simp]:
 "gswap a b + gswap a b = 0"
 "gswap a b + gswap b a = 0"
-by (descending, auto simp add: perm_eq_def perm_add_apply)+
+by (transfer, auto simp add: perm_eq_def perm_add_apply)+
 lemma minus_swap [simp]:
 "- gswap a b = gswap a b"
-by (partiality_descending, auto simp add: perm_eq_def)
+by transfer (auto simp add: perm_eq_def)
 lemma swap_commute:
 "gswap a b = gswap b a"
-by (partiality_descending, auto simp add: perm_eq_def)
+by transfer (auto simp add: perm_eq_def)
 lemma swap_triple:
 assumes "a \<noteq> b" "c \<noteq> b"
 shows "gswap a c + gswap b c + gswap a c = gswap a b"
 using assms
-by descending (auto simp add: perm_eq_def fun_eq_iff perm_add_apply)
+by transfer (auto simp add: perm_eq_def fun_eq_iff perm_add_apply)
 lemma gpermute_gswap[simp]:
 "b \<noteq> a \<Longrightarrow> gpermute (gswap a b) b = a"
 "a \<noteq> b \<Longrightarrow> gpermute (gswap a b) a = b"
 "c \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> gpermute (gswap a b) c = c"
-by (descending, auto)+
+by (transfer, auto)+
 lemma gperm_eq:
 "(p = q) = (\<forall>a. gpermute p a = gpermute q a)"
-by (partiality_descending) (auto simp add: perm_eq_def)
+by transfer (auto simp add: perm_eq_def)
 lemma finite_gpermute_neq:
 "finite {a. gpermute p a \<noteq> a}"
-apply descending
+apply transfer
 apply (rule_tac B="fst ` set p" in finite_subset)
 apply auto
 by (metis perm_apply_outset)
 end

changeset 3173	9876d73adb2b
parent 3139	e05c033d69c1
child 3175	52730e5ec8cb