# 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"