diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/Nominal2_Base_Exec.thy
--- 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