--- a/Nominal/Nominal2_Base_Exec.thy Tue May 22 14:00:59 2012 +0200
+++ b/Nominal/Nominal2_Base_Exec.thy Tue May 22 14:55:58 2012 +0200
@@ -9,6 +9,12 @@
"~~/src/HOL/Library/Infinite_Set"
"~~/src/HOL/Quotient_Examples/FSet"
"GPerm"
+ "~~/src/HOL/Library/List_lexord"
+ "~~/src/HOL/Library/Product_ord"
+ "~~/src/HOL/Library/Efficient_Nat"
+ "~~/src/HOL/Library/Char_ord"
+ "~~/src/HOL/Library/Code_Char_chr"
+ "~~/src/HOL/Library/Code_Char_ord"
keywords
"atom_decl" "equivariance" :: thy_decl
uses ("nominal_basics.ML")
@@ -95,73 +101,70 @@
typedef (open) perm = "{p::atom gperm. sort_respecting p}"
by (auto intro: exI[of _ "0"])
+setup_lifting type_definition_perm
+
lemma perm_eq_rep:
"p = q \<longleftrightarrow> Rep_perm p = Rep_perm q"
by (simp add: Rep_perm_inject)
-definition mk_perm :: "atom gperm \<Rightarrow> perm" where
- "mk_perm p = Abs_perm (if sort_respecting p then p else 0)"
-
-lemma sort_respecting_Rep_perm [simp, intro]:
+lift_definition mk_perm :: "atom gperm \<Rightarrow> perm" is
+ "\<lambda>p. if sort_respecting p then p else 0" by simp
+
+(*lemma sort_respecting_Rep_perm [simp, intro]:
"sort_respecting (Rep_perm p)"
- using Rep_perm [of p] by simp
+ using Rep_perm [of p] by simp*)
lemma Rep_perm_mk_perm [simp]:
"Rep_perm (mk_perm p) = (if sort_respecting p then p else 0)"
by (simp add: mk_perm_def Abs_perm_inverse)
-lemma mk_perm_Rep_perm [simp, code abstype]:
+(*lemma mk_perm_Rep_perm [simp, code abstype]:
"mk_perm (Rep_perm dxs) = dxs"
- by (simp add: mk_perm_def Rep_perm_inverse)
+ by (simp add: mk_perm_def Rep_perm_inverse)*)
instance perm :: size ..
instantiation perm :: group_add
begin
-definition "(0 :: perm) = mk_perm 0"
-
-definition "uminus p = mk_perm (uminus (Rep_perm p))"
-
-definition "p + q = mk_perm ((Rep_perm p) + (Rep_perm q))"
+lift_definition zero_perm :: "perm" is "0" by simp
+
+lift_definition uminus_perm :: "perm \<Rightarrow> perm" is "uminus"
+ unfolding sort_respecting_def
+ by transfer (auto, metis perm_apply_minus)
+
+lift_definition plus_perm :: "perm \<Rightarrow> perm \<Rightarrow> perm" is "plus"
+ unfolding sort_respecting_def
+ by transfer (simp add: perm_add_apply)
definition "(p :: perm) - q = p + - q"
-lemma [simp]:
- "sort_respecting x \<Longrightarrow> sort_respecting y \<Longrightarrow> sort_respecting (x + y)"
- unfolding sort_respecting_def
- by descending (simp add: perm_add_apply)
-
-lemma [simp]:
- "sort_respecting y \<Longrightarrow> sort_respecting (- y)"
- unfolding sort_respecting_def
- by partiality_descending
- (auto, metis perm_apply_minus)
-
lemma Rep_perm_0 [simp, code abstract]:
"Rep_perm 0 = 0"
- by (simp add: zero_perm_def)
+ by (metis (mono_tags) zero_perm.rep_eq)
lemma Rep_perm_uminus [simp, code abstract]:
"Rep_perm (- p) = - (Rep_perm p)"
- by (simp add: uminus_perm_def)
+ by (metis uminus_perm.rep_eq)
lemma Rep_perm_add [simp, code abstract]:
"Rep_perm (p + q) = (Rep_perm p) + (Rep_perm q)"
- by (simp add: plus_perm_def)
+ by (simp add: plus_perm.rep_eq)
instance
- by default (auto simp add: perm_eq_rep add_assoc minus_perm_def)
+ apply default
+ unfolding minus_perm_def
+ by (transfer, simp add: add_assoc)+
end
-definition swap :: "atom \<Rightarrow> atom \<Rightarrow> perm" ("'(_ \<rightleftharpoons> _')")
-where "swap a b = (if sort_of a = sort_of b then mk_perm (gswap a b) else 0)"
+lift_definition swap :: "atom \<Rightarrow> atom \<Rightarrow> perm" ("'(_ \<rightleftharpoons> _')")
+ is "(\<lambda>a b. (if sort_of a = sort_of b then mk_perm (gswap a b) else 0))" .
lemma sort_respecting_swap [simp]:
"sort_of a = sort_of b \<Longrightarrow> sort_respecting (gswap a b)"
unfolding sort_respecting_def
- by descending auto
+ by transfer auto
lemma Rep_swap [simp, code abstract]:
"Rep_perm (swap a b) = (if sort_of a = sort_of b then gswap a b else 0)"
@@ -268,7 +271,7 @@
lemma sort_of_permute [simp]:
shows "sort_of (p \<bullet> a) = sort_of a"
- by (metis sort_respecting_Rep_perm sort_respecting_def permute_atom_def)
+ by (metis Rep_perm mem_Collect_eq sort_respecting_def permute_atom_def)
lemma swap_atom:
shows "(a \<rightleftharpoons> b) \<bullet> c =
@@ -542,11 +545,6 @@
subsection {* Permutations for @{typ "'a fset"} *}
-lemma permute_fset_rsp[quot_respect]:
- shows "(op = ===> list_eq ===> list_eq) permute permute"
- unfolding fun_rel_def
- by (simp add: set_eqvt[symmetric])
-
instantiation fset :: (pt) pt
begin
@@ -554,8 +552,9 @@
"permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
is
"permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-instance
+ by (simp add: set_eqvt[symmetric])
+
+instance
proof
fix x :: "'a fset" and p q :: "perm"
have lst: "\<And>l :: 'a list. 0 \<bullet> l = l" by simp
@@ -3167,7 +3166,86 @@
use "nominal_eqvt.ML"
-
-
+instantiation atom_sort :: ord begin
+
+fun less_atom_sort where
+ "less_atom_sort (Sort s1 l1) (Sort s2 []) \<longleftrightarrow> s1 < s2"
+| "less_atom_sort (Sort s1 []) (Sort s2 (h # t)) \<longleftrightarrow> s1 \<le> s2"
+| "less_atom_sort (Sort s1 (h1 # t1)) (Sort s2 (h2 # t2)) \<longleftrightarrow> s1 < s2 \<or> s1 \<le> s2 \<and> ((less_atom_sort h1 h2) \<or> (h1 = h2 \<and> less_atom_sort (Sort s1 t1) (Sort s2 t2)))"
+
+definition less_eq_atom_sort where
+ less_eq_atom_sort_def: "less_eq_atom_sort (x :: atom_sort) y \<longleftrightarrow> x < y \<or> x = y"
+
+instance ..
end
+
+lemma less_st_less: "(Sort s1 l1) < (Sort s2 l2) \<longleftrightarrow> s1 < s2 \<or> s1 \<le> s2 \<and> l1 < l2"
+ by (induct l1 l2 rule: list_induct2') auto
+
+lemma not_as_le_as: "\<not>((x :: atom_sort) < x)"
+ apply (rule less_atom_sort.induct[of "\<lambda>x y. x = y \<longrightarrow> \<not>x < y" "x" "x", simplified]) ..
+
+instance atom_sort :: linorder
+proof (default, auto simp add: less_eq_atom_sort_def not_as_le_as)
+ fix x y :: atom_sort
+ assume x: "x < y" "y < x"
+ then show False
+ by (induct x y rule: less_atom_sort.induct) (case_tac l1, auto)
+ with x show "x = y"
+ by (induct x y rule: less_atom_sort.induct) (case_tac l1, auto)
+next
+ fix x y z :: atom_sort
+ assume "x < y" "y < z"
+ then show "x < z"
+ apply (induct x z arbitrary: y rule: less_atom_sort.induct)
+ apply (case_tac [!] y) apply auto
+ apply (case_tac [!] list2) apply auto
+ apply (case_tac l1) apply auto[2]
+ done
+next
+ fix x y :: atom_sort
+ assume x: "\<not>x < y" "y \<noteq> x"
+ then show "y < x"
+ apply (induct x y rule: less_atom_sort.induct)
+ apply auto
+ apply (case_tac [!] l1)
+ apply auto
+ done
+qed
+
+instantiation atom :: linorder begin
+
+definition less_eq_atom where
+ [simp]: "less_eq_atom x y \<longleftrightarrow> sort_of x < sort_of y \<or> sort_of x \<le> sort_of y \<and> nat_of x \<le> nat_of y"
+
+definition less_atom where
+ [simp]: "less_atom x y \<longleftrightarrow> sort_of x < sort_of y \<or> sort_of x \<le> sort_of y \<and> nat_of x < nat_of y"
+
+instance apply default
+ apply auto
+ apply (case_tac x, case_tac y)
+ apply auto
+ done
+
+end
+
+lemma [code]:
+ "gpermute p = perm_apply (dest_perm p)"
+ apply transfer
+ unfolding Rel_def
+ by (auto, metis perm_eq_def valid_dest_perm_raw_eq(2))
+
+instantiation perm :: equal begin
+
+definition "equal_perm a b \<longleftrightarrow> Rep_perm a = Rep_perm b"
+
+instance
+ apply default
+ unfolding equal_perm_def perm_eq_rep ..
+
+end
+
+(* Test: export_code swap in SML *)
+
+end