# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1313304723 -7200
# Node ID 847972b7b5ba3837f44940f7c8c9239cdbb6f39f
# Parent  05ccb61aa6287e365b114d1f717dbf0aaa6923f7# Parent  1b39ba5db2c11540e899a3949b4f0f5aa51b70a3
merged

diff -r 05ccb61aa628 -r 847972b7b5ba Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Fri Aug 12 22:37:41 2011 +0200
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Sun Aug 14 08:52:03 2011 +0200
@@ -155,8 +155,7 @@
 apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff)
 by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+
 
-termination
-  by (relation "measure size") (simp_all add: lt.size)
+termination (eqvt) by (relation "measure size") (simp_all)
 
 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim]
 
@@ -167,25 +166,6 @@
 lemma [simp]: "x \<sharp> M* = x \<sharp> M"
   unfolding fresh_def by simp
 
-(* Will be provided automatically by nominal_primrec *)
-lemma CPS_eqvt[eqvt]:
-  shows "p \<bullet> M* = (p \<bullet> M)*"
-  apply (induct M rule: lt.induct)
-  apply (rule_tac x="(name, p \<bullet> name, p)" and ?'a="name" in obtain_fresh)
-  apply simp
-  apply (simp add: Abs1_eq_iff lt.fresh flip_def[symmetric])
-  apply (metis atom_eqvt flip_fresh_fresh fresh_perm atom_eq_iff fresh_at_base)
-  apply (rule_tac x="(name, lt, p \<bullet> name, p \<bullet> lt, p)" and ?'a="name" in obtain_fresh)
-  apply simp
-  apply (metis atom_eqvt fresh_perm atom_eq_iff)
-  apply (rule_tac x="(lt1, p \<bullet> lt1, lt2, p \<bullet> lt2, p)" and ?'a="name" in obtain_fresh)
-  apply (rule_tac x="(a, lt2, p \<bullet> lt2, p)" and ?'a="name" in obtain_fresh)
-  apply (rule_tac x="(a, aa, p)" and ?'a="name" in obtain_fresh)
-  apply (simp)
-  apply (simp add: Abs1_eq_iff lt.fresh flip_def[symmetric])
-  apply (metis atom_eqvt fresh_perm atom_eq_iff)
-  done
-
 nominal_primrec
   convert:: "lt => lt" ("_+" [250] 250)
 where
@@ -197,11 +177,11 @@
   apply (erule lt.exhaust)
   apply (simp_all)
   apply blast
-  apply (simp add: Abs1_eq_iff CPS_eqvt)
+  apply (simp add: Abs1_eq_iff CPS.eqvt)
   by blast
 
-termination
-  by (relation "measure size") (simp_all add: lt.size)
+termination (eqvt)
+  by (relation "measure size") (simp_all)
 
 lemma convert_supp[simp]:
   shows "supp (M+) = supp M"
@@ -211,10 +191,6 @@
   shows "x \<sharp> (M+) = x \<sharp> M"
   unfolding fresh_def by simp
 
-lemma convert_eqvt[eqvt]:
-  shows "p \<bullet> (M+) = (p \<bullet> M)+"
-  by (nominal_induct M rule: lt.strong_induct, auto simp add: CPS_eqvt)
-
 lemma [simp]:
   shows "isValue (p \<bullet> (M::lt)) = isValue M"
   by (nominal_induct M rule: lt.strong_induct) auto
@@ -265,8 +241,8 @@
 apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+
 done
 
-termination
-  by (relation "measure (\<lambda>(t, _). size t)") (simp_all add: lt.size)
+termination (eqvt)
+  by (relation "measure (\<lambda>(t, _). size t)") (simp_all)
 
 section{* lemma related to Kapply *}
 
diff -r 05ccb61aa628 -r 847972b7b5ba Nominal/Ex/CPS/CPS3_DanvyFilinski.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Fri Aug 12 22:37:41 2011 +0200
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Sun Aug 14 08:52:03 2011 +0200
@@ -217,7 +217,7 @@
   apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 definition psi:: "lt => lt"
diff -r 05ccb61aa628 -r 847972b7b5ba Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Fri Aug 12 22:37:41 2011 +0200
+++ b/Nominal/Ex/CPS/Lt.thy	Sun Aug 14 08:52:03 2011 +0200
@@ -33,13 +33,7 @@
   apply (simp_all add: swap_fresh_fresh)
   done
 
-termination
-  by (relation "measure (\<lambda>(t, _, _). size t)")
-     (simp_all add: lt.size)
-
-lemma subst_eqvt[eqvt]:
-  shows "p\<bullet>(M[V/(x::name)]) = (p\<bullet>M)[(p\<bullet>V)/(p\<bullet>x)]"
-  by (induct M V x rule: subst.induct) (simp_all)
+termination (eqvt) by lexicographic_order
 
 lemma forget[simp]:
   shows "atom x \<sharp> M \<Longrightarrow> M[s/x] = M"
@@ -60,9 +54,8 @@
   by (perm_simp, auto)
      (erule lt.exhaust, auto)
 
-termination
-  by (relation "measure size")
-     (simp_all add: lt.size)
+termination (eqvt)
+  by (relation "measure size") (simp_all)
 
 lemma is_Value_eqvt[eqvt]:
   shows "p\<bullet>(isValue (M::lt)) = isValue (p\<bullet>M)"
diff -r 05ccb61aa628 -r 847972b7b5ba Nominal/Ex/SFT/Consts.thy
--- a/Nominal/Ex/SFT/Consts.thy	Fri Aug 12 22:37:41 2011 +0200
+++ b/Nominal/Ex/SFT/Consts.thy	Sun Aug 14 08:52:03 2011 +0200
@@ -94,13 +94,7 @@
     by (rule, perm_simp, rule)
 qed
 
-termination
-  by (relation "measure (\<lambda>(t). size t)")
-     (simp_all add: lam.size)
-
-lemma numeral_eqvt[eqvt]: "p \<bullet> \<lbrace>x\<rbrace> = \<lbrace>p \<bullet> x\<rbrace>"
-  by (induct x rule: lam.induct)
-     (simp_all add: Var_App_Abs_eqvt)
+termination (eqvt) by lexicographic_order
 
 lemma supp_numeral[simp]:
   "supp \<lbrace>x\<rbrace> = supp x"
@@ -145,27 +139,7 @@
   apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev)
   done
 
-termination
-  by (relation "measure (\<lambda>t. size t)")
-     (simp_all add: lam.size)
-
-lemma ltgt_eqvt[eqvt]:
-  "p \<bullet> \<guillemotleft>t\<guillemotright> = \<guillemotleft>p \<bullet> t\<guillemotright>"
-proof -
-  obtain x :: var where "atom x \<sharp> (t, p \<bullet> t)" using obtain_fresh by auto
-  then have *: "atom x \<sharp> t" "atom x \<sharp> (p \<bullet> t)" using fresh_Pair by simp_all
-  then show ?thesis using *[unfolded fresh_def]
-    apply (simp add: Abs1_eq_iff lam.fresh app_lst_eqvt Ltgt.simps)
-    apply (case_tac "p \<bullet> x = x")
-    apply (simp_all add: eqvts)
-    apply rule
-    apply (subst swap_fresh_fresh)
-    apply (simp_all add: fresh_at_base_permute_iff fresh_def[symmetric] fresh_at_base)
-    apply (subgoal_tac "eqvt app_lst")
-    apply (erule fresh_fun_eqvt_app2)
-    apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev)
-    done
-qed
+termination (eqvt) by lexicographic_order
 
 lemma ltgt_eq_iff[simp]:
   "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N"
@@ -240,7 +214,7 @@
   "F1 = \<integral>x. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V x))"
   "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> F2 = \<integral>a. \<integral>b. \<integral>c. ((App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (V c \<cdot> V a))) \<cdot> (V c \<cdot> V b))"
   "a \<noteq> b \<Longrightarrow> a \<noteq> x \<Longrightarrow> x \<noteq> b \<Longrightarrow> F3 = \<integral>a. \<integral>b. (App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (V b \<cdot> (V a \<cdot> V x)))))"
-  apply (simp_all add: F1_def F2_def F3_def Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt numeral_eqvt flip_def[symmetric] fresh_at_base)
+  apply (simp_all add: F1_def F2_def F3_def Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base)
   apply (smt cx_cy_cz permute_flip_at)+
   done
 
@@ -291,7 +265,7 @@
   "x \<noteq> y \<Longrightarrow> A1 = \<integral>x. \<integral>y. (F1 \<cdot> V x)"
   "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> A2 = \<integral>a. \<integral>b. \<integral>c. (F2 \<cdot> V a \<cdot> V b \<cdot> \<guillemotleft>[V c]\<guillemotright>)"
   "a \<noteq> b \<Longrightarrow> A3 = \<integral>a. \<integral>b. (F3 \<cdot> V a \<cdot> \<guillemotleft>[V b]\<guillemotright>)"
-  apply (simp_all add: Lam_A1_pre Lam_A2_pre Lam_A3_pre Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt numeral_eqvt flip_def[symmetric] fresh_at_base F_eqvt ltgt_eqvt)
+  apply (simp_all add: Lam_A1_pre Lam_A2_pre Lam_A3_pre Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base F_eqvt Ltgt.eqvt)
   apply (smt cx_cy_cz permute_flip_at)+
   done
 
diff -r 05ccb61aa628 -r 847972b7b5ba Nominal/Ex/SFT/Lambda.thy
--- a/Nominal/Ex/SFT/Lambda.thy	Fri Aug 12 22:37:41 2011 +0200
+++ b/Nominal/Ex/SFT/Lambda.thy	Sun Aug 14 08:52:03 2011 +0200
@@ -10,7 +10,7 @@
 nominal_datatype lam =
   V "var"
 | Ap "lam" "lam" (infixl "\<cdot>" 98)
-| Lm x::"var" l::"lam"  bind x in l ("\<integral> _. _" [97, 97] 99)
+| Lm x::"var" l::"lam"  binds x in l ("\<integral> _. _" [97, 97] 99)
 
 nominal_primrec
   subst :: "lam \<Rightarrow> var \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
@@ -48,13 +48,7 @@
     by (rule, perm_simp, rule)
 qed
 
-termination
-  by (relation "measure (\<lambda>(t,_,_). size t)")
-     (simp_all add: lam.size)
-
-lemma subst_eqvt[eqvt]:
-  shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
-  by (induct t x s rule: subst.induct) (simp_all)
+termination (eqvt) by lexicographic_order
 
 lemma forget[simp]:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"