Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated to Isabelle version April 1
authorChristian Urban <urbanc@in.tum.de>
Wed, 04 Apr 2012 06:19:38 +0100
changeset 3152 da59c94bed7e
parent 3151 16e6140225af
child 3153 fde87a11377c
updated to Isabelle version April 1
Nominal/Nominal2_Abs.thy file | annotate | diff | comparison | revisions
Nominal/Nominal2_Base.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Nominal2_Abs.thy	Tue Apr 03 23:09:13 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy	Wed Apr 04 06:19:38 2012 +0100
@@ -470,21 +470,21 @@
 where
   "Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set"
 is
-  "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+  "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" .
 
 quotient_definition
   Abs_res ("[_]res. _" [60, 60] 60)
 where
   "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"
 is
-  "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+  "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" .
 
 quotient_definition
   Abs_lst ("[_]lst. _" [60, 60] 60)
 where
   "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
 is
-  "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
+  "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)" .
 
 lemma [quot_respect]:
   shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"
@@ -540,7 +540,8 @@
 quotient_definition
   "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set"
 is
-  "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+  "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" 
+  by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
 lemma permute_Abs_set[simp]:
   fixes x::"'a::pt"  
@@ -562,6 +563,7 @@
   "permute_abs_res::perm \<Rightarrow> ('a::pt abs_res) \<Rightarrow> 'a abs_res"
 is
   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+  by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
 lemma permute_Abs_res[simp]:
   fixes x::"'a::pt"  
@@ -583,6 +585,7 @@
   "permute_abs_lst::perm \<Rightarrow> ('a::pt abs_lst) \<Rightarrow> 'a abs_lst"
 is
   "permute:: perm \<Rightarrow> (atom list \<times> 'a::pt) \<Rightarrow> (atom list \<times> 'a::pt)"
+  by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
 lemma permute_Abs_lst[simp]:
   fixes x::"'a::pt"  
--- a/Nominal/Nominal2_Base.thy	Tue Apr 03 23:09:13 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Apr 04 06:19:38 2012 +0100
@@ -629,6 +629,7 @@
   "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
   "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  by (simp add: set_eqvt[symmetric])
 
 instance 
 proof
nominal2