--- a/src/HOL/Decision_Procs/MIR.thy Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Wed Nov 28 15:59:18 2012 +0100
@@ -1947,7 +1947,7 @@
text{* plusinf : Virtual substitution of @{text "+\<infinity>"}
minusinf: Virtual substitution of @{text "-\<infinity>"}
@{text "\<delta>"} Compute lcm @{text "d| Dvd d c*x+t \<in> p"}
- @{text "d\<delta>"} checks if a given l divides all the ds above*}
+ @{text "d_\<delta>"} checks if a given l divides all the ds above*}
fun minusinf:: "fm \<Rightarrow> fm" where
"minusinf (And p q) = conj (minusinf p) (minusinf q)"
@@ -1981,18 +1981,18 @@
| "\<delta> (NDvd i (CN 0 c e)) = i"
| "\<delta> p = 1"
-fun d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where
- "d\<delta> (And p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)"
-| "d\<delta> (Or p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)"
-| "d\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
-| "d\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
-| "d\<delta> p = (\<lambda> d. True)"
+fun d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where
+ "d_\<delta> (And p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)"
+| "d_\<delta> (Or p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)"
+| "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
+| "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
+| "d_\<delta> p = (\<lambda> d. True)"
lemma delta_mono:
assumes lin: "iszlfm p bs"
and d: "d dvd d'"
- and ad: "d\<delta> p d"
- shows "d\<delta> p d'"
+ and ad: "d_\<delta> p d"
+ shows "d_\<delta> p d'"
using lin ad d
proof(induct p rule: iszlfm.induct)
case (9 i c e) thus ?case using d
@@ -2003,26 +2003,26 @@
qed simp_all
lemma \<delta> : assumes lin:"iszlfm p bs"
- shows "d\<delta> p (\<delta> p) \<and> \<delta> p >0"
+ shows "d_\<delta> p (\<delta> p) \<and> \<delta> p >0"
using lin
proof (induct p rule: iszlfm.induct)
case (1 p q)
let ?d = "\<delta> (And p q)"
from 1 lcm_pos_int have dp: "?d >0" by simp
have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp
- hence th: "d\<delta> p ?d"
+ hence th: "d_\<delta> p ?d"
using delta_mono 1 by (simp only: iszlfm.simps) blast
have "\<delta> q dvd \<delta> (And p q)" using 1 by simp
- hence th': "d\<delta> q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast
+ hence th': "d_\<delta> q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast
from th th' dp show ?case by simp
next
case (2 p q)
let ?d = "\<delta> (And p q)"
from 2 lcm_pos_int have dp: "?d >0" by simp
have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
- hence th: "d\<delta> p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
+ hence th: "d_\<delta> p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
have "\<delta> q dvd \<delta> (And p q)" using 2 by simp
- hence th': "d\<delta> q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
+ hence th': "d_\<delta> q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
from th th' dp show ?case by simp
qed simp_all
@@ -2152,7 +2152,7 @@
qed simp_all
lemma minusinf_repeats:
- assumes d: "d\<delta> p d" and linp: "iszlfm p (a # bs)"
+ assumes d: "d_\<delta> p d" and linp: "iszlfm p (a # bs)"
shows "Ifm ((real(x - k*d))#bs) (minusinf p) = Ifm (real x #bs) (minusinf p)"
using linp d
proof(induct p rule: iszlfm.induct)
@@ -2218,7 +2218,7 @@
proof-
let ?d = "\<delta> p"
from \<delta> [OF lin] have dpos: "?d >0" by simp
- from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
+ from \<delta> [OF lin] have alld: "d_\<delta> p ?d" by simp
from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P1 x = ?P1 (x - (k * ?d))" by simp
from minusinf_inf[OF lin] have th2:"\<exists> z. \<forall> x. x<z \<longrightarrow> (?P x = ?P1 x)" by blast
from minusinfinity [OF dpos th1 th2] exmi show ?thesis by blast
@@ -2232,7 +2232,7 @@
proof-
let ?d = "\<delta> p"
from \<delta> [OF lin] have dpos: "?d >0" by simp
- from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
+ from \<delta> [OF lin] have alld: "d_\<delta> p ?d" by simp
from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp
from periodic_finite_ex[OF dpos th1] show ?thesis by blast
qed
@@ -2240,37 +2240,37 @@
lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto
consts
- a\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
- d\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
+ a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
+ d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
\<zeta> :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
\<beta> :: "fm \<Rightarrow> num list"
\<alpha> :: "fm \<Rightarrow> num list"
-recdef a\<beta> "measure size"
- "a\<beta> (And p q) = (\<lambda> k. And (a\<beta> p k) (a\<beta> q k))"
- "a\<beta> (Or p q) = (\<lambda> k. Or (a\<beta> p k) (a\<beta> q k))"
- "a\<beta> (Eq (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
- "a\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
- "a\<beta> (Lt (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
- "a\<beta> (Le (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
- "a\<beta> (Gt (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
- "a\<beta> (Ge (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
- "a\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
- "a\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
- "a\<beta> p = (\<lambda> k. p)"
-
-recdef d\<beta> "measure size"
- "d\<beta> (And p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))"
- "d\<beta> (Or p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))"
- "d\<beta> (Eq (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d\<beta> (Lt (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d\<beta> (Le (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d\<beta> (Gt (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d\<beta> (Ge (CN 0 c e)) = (\<lambda> k. c dvd k)"
- "d\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
- "d\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
- "d\<beta> p = (\<lambda> k. True)"
+recdef a_\<beta> "measure size"
+ "a_\<beta> (And p q) = (\<lambda> k. And (a_\<beta> p k) (a_\<beta> q k))"
+ "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))"
+ "a_\<beta> (Eq (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
+ "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
+ "a_\<beta> (Lt (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
+ "a_\<beta> (Le (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
+ "a_\<beta> (Gt (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
+ "a_\<beta> (Ge (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
+ "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
+ "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
+ "a_\<beta> p = (\<lambda> k. p)"
+
+recdef d_\<beta> "measure size"
+ "d_\<beta> (And p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
+ "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
+ "d_\<beta> (Eq (CN 0 c e)) = (\<lambda> k. c dvd k)"
+ "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
+ "d_\<beta> (Lt (CN 0 c e)) = (\<lambda> k. c dvd k)"
+ "d_\<beta> (Le (CN 0 c e)) = (\<lambda> k. c dvd k)"
+ "d_\<beta> (Gt (CN 0 c e)) = (\<lambda> k. c dvd k)"
+ "d_\<beta> (Ge (CN 0 c e)) = (\<lambda> k. c dvd k)"
+ "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
+ "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
+ "d_\<beta> p = (\<lambda> k. True)"
recdef \<zeta> "measure size"
"\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
@@ -2320,7 +2320,7 @@
"mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
"mirror p = p"
-lemma mirror\<alpha>\<beta>:
+lemma mirror_\<alpha>_\<beta>:
assumes lp: "iszlfm p (a#bs)"
shows "(Inum (real (i::int)#bs)) ` set (\<alpha> p) = (Inum (real i#bs)) ` set (\<beta> (mirror p))"
using lp
@@ -2351,8 +2351,8 @@
lemma mirror_l: "iszlfm p (a#bs) \<Longrightarrow> iszlfm (mirror p) (a#bs)"
by (induct p rule: mirror.induct, auto simp add: isint_neg)
-lemma mirror_d\<beta>: "iszlfm p (a#bs) \<and> d\<beta> p 1
- \<Longrightarrow> iszlfm (mirror p) (a#bs) \<and> d\<beta> (mirror p) 1"
+lemma mirror_d_\<beta>: "iszlfm p (a#bs) \<and> d_\<beta> p 1
+ \<Longrightarrow> iszlfm (mirror p) (a#bs) \<and> d_\<beta> (mirror p) 1"
by (induct p rule: mirror.induct, auto simp add: isint_neg)
lemma mirror_\<delta>: "iszlfm p (a#bs) \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
@@ -2376,11 +2376,11 @@
shows "\<forall> b\<in> set (\<beta> p). numbound0 b"
using lp by (induct p rule: \<beta>.induct,auto)
-lemma d\<beta>_mono:
+lemma d_\<beta>_mono:
assumes linp: "iszlfm p (a #bs)"
- and dr: "d\<beta> p l"
+ and dr: "d_\<beta> p l"
and d: "l dvd l'"
- shows "d\<beta> p l'"
+ shows "d_\<beta> p l'"
using dr linp dvd_trans[of _ "l" "l'", simplified d]
by (induct p rule: iszlfm.induct) simp_all
@@ -2391,26 +2391,26 @@
lemma \<zeta>:
assumes linp: "iszlfm p (a #bs)"
- shows "\<zeta> p > 0 \<and> d\<beta> p (\<zeta> p)"
+ shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)"
using linp
proof(induct p rule: iszlfm.induct)
case (1 p q)
then have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
- from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
- d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
+ from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
+ d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
next
case (2 p q)
then have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
- from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
- d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
+ from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
+ d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
qed (auto simp add: lcm_pos_int)
-lemma a\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0"
- shows "iszlfm (a\<beta> p l) (a #bs) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a\<beta> p l) = Ifm ((real x)#bs) p)"
+lemma a_\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d_\<beta> p l" and lp: "l > 0"
+ shows "iszlfm (a_\<beta> p l) (a #bs) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a_\<beta> p l) = Ifm ((real x)#bs) p)"
using linp d
proof (induct p rule: iszlfm.induct)
case (5 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+
@@ -2556,20 +2556,20 @@
finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def be isint_Mul[OF ei] mult_strict_mono[OF ldcp jp ldcp ] by simp
qed (simp_all add: numbound0_I[where bs="bs" and b="real (l * x)" and b'="real x"] isint_Mul del: real_of_int_mult)
-lemma a\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d\<beta> p l" and lp: "l>0"
- shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)"
+lemma a_\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d_\<beta> p l" and lp: "l>0"
+ shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a_\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)"
(is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)")
proof-
have "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> (x::int). ?P (l*x))"
using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
- also have "\<dots> = (\<exists> (x::int). ?P' x)" using a\<beta>[OF linp d lp] by simp
+ also have "\<dots> = (\<exists> (x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp
finally show ?thesis .
qed
lemma \<beta>:
assumes lp: "iszlfm p (a#bs)"
- and u: "d\<beta> p 1"
- and d: "d\<delta> p d"
+ and u: "d_\<beta> p 1"
+ and d: "d_\<delta> p d"
and dp: "d > 0"
and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). real x = b + real j)"
and p: "Ifm (real x#bs) p" (is "?P x")
@@ -2705,8 +2705,8 @@
lemma \<beta>':
assumes lp: "iszlfm p (a #bs)"
- and u: "d\<beta> p 1"
- and d: "d\<delta> p d"
+ and u: "d_\<beta> p 1"
+ and d: "d_\<delta> p d"
and dp: "d > 0"
shows "\<forall> x. \<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> set(\<beta> p). Ifm ((Inum (a#bs) b + real j) #bs) p) \<longrightarrow> Ifm (real x#bs) p \<longrightarrow> Ifm (real (x - d)#bs) p" (is "\<forall> x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
proof(clarify)
@@ -2746,8 +2746,8 @@
theorem cp_thm:
assumes lp: "iszlfm p (a #bs)"
- and u: "d\<beta> p 1"
- and d: "d\<delta> p d"
+ and u: "d_\<beta> p 1"
+ and d: "d_\<delta> p d"
and dp: "d > 0"
shows "(\<exists> (x::int). Ifm (real x #bs) p) = (\<exists> j\<in> {1.. d}. Ifm (real j #bs) (minusinf p) \<or> (\<exists> b \<in> set (\<beta> p). Ifm ((Inum (a#bs) b + real j) #bs) p))"
(is "(\<exists> (x::int). ?P (real x)) = (\<exists> j\<in> ?D. ?M j \<or> (\<exists> b\<in> ?B. ?P (?I b + real j)))")
@@ -2775,9 +2775,9 @@
consts
\<rho> :: "fm \<Rightarrow> (num \<times> int) list" (* Compute the Reddy and Loveland Bset*)
- \<sigma>\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
- \<alpha>\<rho> :: "fm \<Rightarrow> (num\<times>int) list"
- a\<rho> :: "fm \<Rightarrow> int \<Rightarrow> fm"
+ \<sigma>_\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
+ \<alpha>_\<rho> :: "fm \<Rightarrow> (num\<times>int) list"
+ a_\<rho> :: "fm \<Rightarrow> int \<Rightarrow> fm"
recdef \<rho> "measure size"
"\<rho> (And p q) = (\<rho> p @ \<rho> q)"
"\<rho> (Or p q) = (\<rho> p @ \<rho> q)"
@@ -2789,52 +2789,52 @@
"\<rho> (Ge (CN 0 c e)) = [(Sub (C (-1)) e, c)]"
"\<rho> p = []"
-recdef \<sigma>\<rho> "measure size"
- "\<sigma>\<rho> (And p q) = (\<lambda> (t,k). And (\<sigma>\<rho> p (t,k)) (\<sigma>\<rho> q (t,k)))"
- "\<sigma>\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>\<rho> p (t,k)) (\<sigma>\<rho> q (t,k)))"
- "\<sigma>\<rho> (Eq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e))
+recdef \<sigma>_\<rho> "measure size"
+ "\<sigma>_\<rho> (And p q) = (\<lambda> (t,k). And (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
+ "\<sigma>_\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
+ "\<sigma>_\<rho> (Eq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e))
else (Eq (Add (Mul c t) (Mul k e))))"
- "\<sigma>\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e))
+ "\<sigma>_\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e))
else (NEq (Add (Mul c t) (Mul k e))))"
- "\<sigma>\<rho> (Lt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e))
+ "\<sigma>_\<rho> (Lt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e))
else (Lt (Add (Mul c t) (Mul k e))))"
- "\<sigma>\<rho> (Le (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e))
+ "\<sigma>_\<rho> (Le (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e))
else (Le (Add (Mul c t) (Mul k e))))"
- "\<sigma>\<rho> (Gt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e))
+ "\<sigma>_\<rho> (Gt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e))
else (Gt (Add (Mul c t) (Mul k e))))"
- "\<sigma>\<rho> (Ge (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e))
+ "\<sigma>_\<rho> (Ge (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e))
else (Ge (Add (Mul c t) (Mul k e))))"
- "\<sigma>\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e))
+ "\<sigma>_\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e))
else (Dvd (i*k) (Add (Mul c t) (Mul k e))))"
- "\<sigma>\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e))
+ "\<sigma>_\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e))
else (NDvd (i*k) (Add (Mul c t) (Mul k e))))"
- "\<sigma>\<rho> p = (\<lambda> (t,k). p)"
-
-recdef \<alpha>\<rho> "measure size"
- "\<alpha>\<rho> (And p q) = (\<alpha>\<rho> p @ \<alpha>\<rho> q)"
- "\<alpha>\<rho> (Or p q) = (\<alpha>\<rho> p @ \<alpha>\<rho> q)"
- "\<alpha>\<rho> (Eq (CN 0 c e)) = [(Add (C -1) e,c)]"
- "\<alpha>\<rho> (NEq (CN 0 c e)) = [(e,c)]"
- "\<alpha>\<rho> (Lt (CN 0 c e)) = [(e,c)]"
- "\<alpha>\<rho> (Le (CN 0 c e)) = [(Add (C -1) e,c)]"
- "\<alpha>\<rho> p = []"
+ "\<sigma>_\<rho> p = (\<lambda> (t,k). p)"
+
+recdef \<alpha>_\<rho> "measure size"
+ "\<alpha>_\<rho> (And p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
+ "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
+ "\<alpha>_\<rho> (Eq (CN 0 c e)) = [(Add (C -1) e,c)]"
+ "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
+ "\<alpha>_\<rho> (Lt (CN 0 c e)) = [(e,c)]"
+ "\<alpha>_\<rho> (Le (CN 0 c e)) = [(Add (C -1) e,c)]"
+ "\<alpha>_\<rho> p = []"
(* Simulates normal substituion by modifying the formula see correctness theorem *)
definition \<sigma> :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where
- "\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>\<rho> p (t,k))"
-
-lemma \<sigma>\<rho>:
+ "\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>_\<rho> p (t,k))"
+
+lemma \<sigma>_\<rho>:
assumes linp: "iszlfm p (real (x::int)#bs)"
and kpos: "real k > 0"
and tnb: "numbound0 t"
and tint: "isint t (real x#bs)"
and kdt: "k dvd floor (Inum (b'#bs) t)"
- shows "Ifm (real x#bs) (\<sigma>\<rho> p (t,k)) =
+ shows "Ifm (real x#bs) (\<sigma>_\<rho> p (t,k)) =
(Ifm ((real ((floor (Inum (b'#bs) t)) div k))#bs) p)"
(is "?I (real x) (?s p) = (?I (real ((floor (?N b' t)) div k)) p)" is "_ = (?I ?tk p)")
using linp kpos tnb
-proof(induct p rule: \<sigma>\<rho>.induct)
+proof(induct p rule: \<sigma>_\<rho>.induct)
case (3 c e)
from 3 have cp: "c > 0" and nb: "numbound0 e" by auto
{ assume kdc: "k dvd c"
@@ -3033,8 +3033,8 @@
numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"])
-lemma \<sigma>\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
- shows "bound0 (\<sigma>\<rho> p (t,k))"
+lemma \<sigma>_\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
+ shows "bound0 (\<sigma>_\<rho> p (t,k))"
using lp
by (induct p rule: iszlfm.induct, auto simp add: nb)
@@ -3043,15 +3043,15 @@
shows "\<forall> (b,k) \<in> set (\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)"
using lp by (induct p rule: \<rho>.induct, auto simp add: isint_sub isint_neg)
-lemma \<alpha>\<rho>_l:
+lemma \<alpha>_\<rho>_l:
assumes lp: "iszlfm p (real (i::int)#bs)"
- shows "\<forall> (b,k) \<in> set (\<alpha>\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)"
+ shows "\<forall> (b,k) \<in> set (\<alpha>_\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)"
using lp isint_add [OF isint_c[where j="- 1"],where bs="real i#bs"]
- by (induct p rule: \<alpha>\<rho>.induct, auto)
+ by (induct p rule: \<alpha>_\<rho>.induct, auto)
lemma \<rho>: assumes lp: "iszlfm p (real (i::int) #bs)"
and pi: "Ifm (real i#bs) p"
- and d: "d\<delta> p d"
+ and d: "d_\<delta> p d"
and dp: "d > 0"
and nob: "\<forall>(e,c) \<in> set (\<rho> p). \<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> Inum (real i#bs) e + real j"
(is "\<forall>(e,c) \<in> set (\<rho> p). \<forall> j\<in> {1 .. c*d}. _ \<noteq> ?N i e + _")
@@ -3187,10 +3187,10 @@
lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t"
shows "bound0 (\<sigma> p k t)"
- using \<sigma>\<rho>_nb[OF lp nb] nb by (simp add: \<sigma>_def)
+ using \<sigma>_\<rho>_nb[OF lp nb] nb by (simp add: \<sigma>_def)
lemma \<rho>': assumes lp: "iszlfm p (a #bs)"
- and d: "d\<delta> p d"
+ and d: "d_\<delta> p d"
and dp: "d > 0"
shows "\<forall> x. \<not>(\<exists> (e,c) \<in> set(\<rho> p). \<exists>(j::int) \<in> {1 .. c*d}. Ifm (a #bs) (\<sigma> p c (Add e (C j)))) \<longrightarrow> Ifm (real x#bs) p \<longrightarrow> Ifm (real (x - d)#bs) p" (is "\<forall> x. ?b x \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
proof(clarify)
@@ -3219,8 +3219,8 @@
from nb have nb': "numbound0 (Add e (C j))" by simp
have ji: "isint (C j) (real x#bs)" by (simp add: isint_def)
from isint_add[OF ei ji] have ei':"isint (Add e (C j)) (real x#bs)" .
- from th \<sigma>\<rho>[where b'="real x", OF lp' cp' nb' ei' cdej',symmetric]
- have "Ifm (real x#bs) (\<sigma>\<rho> p (Add e (C j), c))" by simp
+ from th \<sigma>_\<rho>[where b'="real x", OF lp' cp' nb' ei' cdej',symmetric]
+ have "Ifm (real x#bs) (\<sigma>_\<rho> p (Add e (C j), c))" by simp
with rcdej have th: "Ifm (real x#bs) (\<sigma> p c (Add e (C j)))" by (simp add: \<sigma>_def)
from th bound0_I[OF \<sigma>_nb[OF lp nb', where k="c"],where bs="bs" and b="real x" and b'="a"]
have "Ifm (a#bs) (\<sigma> p c (Add e (C j)))" by blast
@@ -3237,7 +3237,7 @@
is "?lhs = (?MD \<or> ?RD)" is "?lhs = ?rhs")
proof-
let ?d= "\<delta> p"
- from \<delta>[OF lp] have d:"d\<delta> p ?d" and dp: "?d > 0" by auto
+ from \<delta>[OF lp] have d:"d_\<delta> p ?d" and dp: "?d > 0" by auto
{ assume H:"?MD" hence th:"\<exists> (x::int). ?MP x" by blast
from H minusinf_ex[OF lp th] have ?thesis by blast}
moreover
@@ -3251,12 +3251,12 @@
from spx bound0_I[OF \<sigma>_nb[OF lp nb', where k="c"], where bs="bs" and b="a" and b'="real i"]
have spx': "Ifm (real i # bs) (\<sigma> p c (Add e (C j)))" by blast
from spx' have rcdej:"real c rdvd (Inum (real i#bs) (Add e (C j)))"
- and sr:"Ifm (real i#bs) (\<sigma>\<rho> p (Add e (C j),c))" by (simp add: \<sigma>_def)+
+ and sr:"Ifm (real i#bs) (\<sigma>_\<rho> p (Add e (C j),c))" by (simp add: \<sigma>_def)+
from rcdej eji[simplified isint_iff]
have "real c rdvd real (floor (Inum (real i#bs) (Add e (C j))))" by simp
hence cdej:"c dvd floor (Inum (real i#bs) (Add e (C j)))" by (simp only: int_rdvd_iff)
from cp have cp': "real c > 0" by simp
- from \<sigma>\<rho>[OF lp cp' nb' eji cdej] spx' have "?P (\<lfloor>Inum (real i # bs) (Add e (C j))\<rfloor> div c)"
+ from \<sigma>_\<rho>[OF lp cp' nb' eji cdej] spx' have "?P (\<lfloor>Inum (real i # bs) (Add e (C j))\<rfloor> div c)"
by (simp add: \<sigma>_def)
hence ?lhs by blast
with exR jD spx have ?thesis by blast}
@@ -3272,8 +3272,8 @@
ultimately show ?thesis by blast
qed
-lemma mirror_\<alpha>\<rho>: assumes lp: "iszlfm p (a#bs)"
- shows "(\<lambda> (t,k). (Inum (a#bs) t, k)) ` set (\<alpha>\<rho> p) = (\<lambda> (t,k). (Inum (a#bs) t,k)) ` set (\<rho> (mirror p))"
+lemma mirror_\<alpha>_\<rho>: assumes lp: "iszlfm p (a#bs)"
+ shows "(\<lambda> (t,k). (Inum (a#bs) t, k)) ` set (\<alpha>_\<rho> p) = (\<lambda> (t,k). (Inum (a#bs) t,k)) ` set (\<rho> (mirror p))"
using lp
by (induct p rule: mirror.induct, simp_all add: split_def image_Un )
@@ -4714,7 +4714,7 @@
qed
-lemma fr_eq\<upsilon>:
+lemma fr_eq_\<upsilon>:
assumes lp: "isrlfm p"
shows "(\<exists> x. Ifm (x#bs) p) = ((Ifm (x#bs) (minusinf p)) \<or> (Ifm (x#bs) (plusinf p)) \<or> (\<exists> (t,k) \<in> set (\<Upsilon> p). \<exists> (s,l) \<in> set (\<Upsilon> p). Ifm (x#bs) (\<upsilon> p (Add(Mul l t) (Mul k s) , 2*k*l))))"
(is "(\<exists> x. ?I x p) = (?M \<or> ?P \<or> ?F)" is "?E = ?D")
@@ -4856,7 +4856,7 @@
hence lqx: "?I x ?rq " using simpfm[where p="?rq" and bs="x#bs"] by auto
from qf have qfq:"isrlfm ?rq"
by (auto simp add: rsplit_def lt_def ge_def rlfm_I[OF qf xp x1])
- with lqx fr_eq\<upsilon>[OF qfq] show "?M \<or> ?P \<or> ?F" by blast
+ with lqx fr_eq_\<upsilon>[OF qfq] show "?M \<or> ?P \<or> ?F" by blast
next
assume D: "?D"
let ?U = "set (\<Upsilon> ?rq )"
@@ -5066,27 +5066,27 @@
lemma cp_thm':
assumes lp: "iszlfm p (real (i::int)#bs)"
- and up: "d\<beta> p 1" and dd: "d\<delta> p d" and dp: "d > 0"
+ and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0"
shows "(\<exists> (x::int). Ifm (real x#bs) p) = ((\<exists> j\<in> {1 .. d}. Ifm (real j#bs) (minusinf p)) \<or> (\<exists> j\<in> {1.. d}. \<exists> b\<in> (Inum (real i#bs)) ` set (\<beta> p). Ifm ((b+real j)#bs) p))"
using cp_thm[OF lp up dd dp] by auto
definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int" where
- "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a\<beta> p' l); d = \<delta> q;
+ "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l); d = \<delta> q;
B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
lemma unit: assumes qf: "qfree p"
- shows "\<And> q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> (Inum (real i#bs)) ` set B = (Inum (real i#bs)) ` set (\<beta> q) \<and> d\<beta> q 1 \<and> d\<delta> q d \<and> d >0 \<and> iszlfm q (real (i::int)#bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
+ shows "\<And> q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> (Inum (real i#bs)) ` set B = (Inum (real i#bs)) ` set (\<beta> q) \<and> d_\<beta> q 1 \<and> d_\<delta> q d \<and> d >0 \<and> iszlfm q (real (i::int)#bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
proof-
fix q B d
assume qBd: "unit p = (q,B,d)"
let ?thes = "((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and>
Inum (real i#bs) ` set B = Inum (real i#bs) ` set (\<beta> q) \<and>
- d\<beta> q 1 \<and> d\<delta> q d \<and> 0 < d \<and> iszlfm q (real i # bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
+ d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q (real i # bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
let ?I = "\<lambda> (x::int) p. Ifm (real x#bs) p"
let ?p' = "zlfm p"
let ?l = "\<zeta> ?p'"
- let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a\<beta> ?p' ?l)"
+ let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\<beta> ?p' ?l)"
let ?d = "\<delta> ?q"
let ?B = "set (\<beta> ?q)"
let ?B'= "remdups (map simpnum (\<beta> ?q))"
@@ -5097,12 +5097,12 @@
from iszlfm_gen[OF conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]]
have lp': "\<forall> (i::int). iszlfm ?p' (real i#bs)" by simp
hence lp'': "iszlfm ?p' (real (i::int)#bs)" by simp
- from lp' \<zeta>[where p="?p'" and bs="bs"] have lp: "?l >0" and dl: "d\<beta> ?p' ?l" by auto
- from a\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp'' dl lp] pp'
+ from lp' \<zeta>[where p="?p'" and bs="bs"] have lp: "?l >0" and dl: "d_\<beta> ?p' ?l" by auto
+ from a_\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp'' dl lp] pp'
have pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by (simp add: int_rdvd_iff)
- from lp'' lp a\<beta>[OF lp'' dl lp] have lq:"iszlfm ?q (real i#bs)" and uq: "d\<beta> ?q 1"
+ from lp'' lp a_\<beta>[OF lp'' dl lp] have lq:"iszlfm ?q (real i#bs)" and uq: "d_\<beta> ?q 1"
by (auto simp add: isint_def)
- from \<delta>[OF lq] have dp:"?d >0" and dd: "d\<delta> ?q ?d" by blast+
+ from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
let ?N = "\<lambda> t. Inum (real (i::int)#bs) t"
have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by (simp add:image_compose)
also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="real i #bs"] by auto
@@ -5124,13 +5124,13 @@
{assume "\<not> (length ?B' \<le> length ?A')"
hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
using qBd by (auto simp add: Let_def unit_def)
- with AA' mirror\<alpha>\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
+ with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
and bn: "\<forall>b\<in> set B. numbound0 b" by simp+
from mirror_ex[OF lq] pq_ex q
have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp
- from lq uq q mirror_d\<beta> [where p="?q" and bs="bs" and a="real i"]
- have lq': "iszlfm q (real i#bs)" and uq: "d\<beta> q 1" by auto
- from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d\<delta> q d " by auto
+ from lq uq q mirror_d_\<beta> [where p="?q" and bs="bs" and a="real i"]
+ have lq': "iszlfm q (real i#bs)" and uq: "d_\<beta> q 1" by auto
+ from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto
from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp
}
ultimately show ?thes by blast
@@ -5168,7 +5168,7 @@
have qbf:"unit p = (?q,?B,?d)" by simp
from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and
B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and
- uq:"d\<beta> ?q 1" and dd: "d\<delta> ?q ?d" and dp: "?d > 0" and
+ uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and
lq: "iszlfm ?q (real i#bs)" and
Bn: "\<forall> b\<in> set ?B. numbound0 b" by auto
from zlin_qfree[OF lq] have qfq: "qfree ?q" .
@@ -5231,14 +5231,14 @@
(* Redy and Loveland *)
-lemma \<sigma>\<rho>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'"
- shows "Ifm (a#bs) (\<sigma>\<rho> p (t,c)) = Ifm (a#bs) (\<sigma>\<rho> p (t',c))"
+lemma \<sigma>_\<rho>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'"
+ shows "Ifm (a#bs) (\<sigma>_\<rho> p (t,c)) = Ifm (a#bs) (\<sigma>_\<rho> p (t',c))"
using lp
by (induct p rule: iszlfm.induct, auto simp add: tt')
lemma \<sigma>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'"
shows "Ifm (a#bs) (\<sigma> p c t) = Ifm (a#bs) (\<sigma> p c t')"
- by (simp add: \<sigma>_def tt' \<sigma>\<rho>_cong[OF lp tt'])
+ by (simp add: \<sigma>_def tt' \<sigma>_\<rho>_cong[OF lp tt'])
lemma \<rho>_cong: assumes lp: "iszlfm p (a#bs)"
and RR: "(\<lambda>(b,k). (Inum (a#bs) b,k)) ` R = (\<lambda>(b,k). (Inum (a#bs) b,k)) ` set (\<rho> p)"
@@ -5284,7 +5284,7 @@
definition chooset :: "fm \<Rightarrow> fm \<times> ((num\<times>int) list) \<times> int" where
"chooset p \<equiv> (let q = zlfm p ; d = \<delta> q;
B = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<rho> q)) ;
- a = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<alpha>\<rho> q))
+ a = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<alpha>_\<rho> q))
in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
lemma chooset: assumes qf: "qfree p"
@@ -5299,8 +5299,8 @@
let ?B = "set (\<rho> ?q)"
let ?f = "\<lambda> (t,k). (simpnum t,k)"
let ?B'= "remdups (map ?f (\<rho> ?q))"
- let ?A = "set (\<alpha>\<rho> ?q)"
- let ?A'= "remdups (map ?f (\<alpha>\<rho> ?q))"
+ let ?A = "set (\<alpha>_\<rho> ?q)"
+ let ?A'= "remdups (map ?f (\<alpha>_\<rho> ?q))"
from conjunct1[OF zlfm_I[OF qf, where bs="bs"]]
have pp': "\<forall> i. ?I i ?q = ?I i p" by auto
hence pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by simp
@@ -5318,7 +5318,7 @@
finally have AA': "?N ` set ?A' = ?N ` ?A" .
from \<rho>_l[OF lq] have B_nb:"\<forall> (e,c)\<in> set ?B'. numbound0 e \<and> c > 0"
by (simp add: simpnum_numbound0 split_def)
- from \<alpha>\<rho>_l[OF lq] have A_nb: "\<forall> (e,c)\<in> set ?A'. numbound0 e \<and> c > 0"
+ from \<alpha>_\<rho>_l[OF lq] have A_nb: "\<forall> (e,c)\<in> set ?A'. numbound0 e \<and> c > 0"
by (simp add: simpnum_numbound0 split_def)
{assume "length ?B' \<le> length ?A'"
hence q:"q=?q" and "B = ?B'" and d:"d = ?d"
@@ -5330,7 +5330,7 @@
{assume "\<not> (length ?B' \<le> length ?A')"
hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
using qBd by (auto simp add: Let_def chooset_def)
- with AA' mirror_\<alpha>\<rho>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<rho> q)"
+ with AA' mirror_\<alpha>_\<rho>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<rho> q)"
and bn: "\<forall>(e,c)\<in> set B. numbound0 e \<and> c > 0" by auto
from mirror_ex[OF lq] pq_ex q
have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp
--- a/src/HOL/Nominal/Examples/Class3.thy Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Nominal/Examples/Class3.thy Wed Nov 28 15:59:18 2012 +0100
@@ -3091,22 +3091,22 @@
findn :: "(name\<times>coname\<times>trm) list\<Rightarrow>name\<Rightarrow>(coname\<times>trm) option"
where
"findn [] x = None"
-| "findn ((y,c,P)#\<theta>n) x = (if y=x then Some (c,P) else findn \<theta>n x)"
+| "findn ((y,c,P)#\<theta>_n) x = (if y=x then Some (c,P) else findn \<theta>_n x)"
lemma findn_eqvt[eqvt]:
fixes pi1::"name prm"
and pi2::"coname prm"
- shows "(pi1\<bullet>findn \<theta>n x) = findn (pi1\<bullet>\<theta>n) (pi1\<bullet>x)"
- and "(pi2\<bullet>findn \<theta>n x) = findn (pi2\<bullet>\<theta>n) (pi2\<bullet>x)"
-apply(induct \<theta>n)
+ shows "(pi1\<bullet>findn \<theta>_n x) = findn (pi1\<bullet>\<theta>_n) (pi1\<bullet>x)"
+ and "(pi2\<bullet>findn \<theta>_n x) = findn (pi2\<bullet>\<theta>_n) (pi2\<bullet>x)"
+apply(induct \<theta>_n)
apply(auto simp add: perm_bij)
done
lemma findn_fresh:
- assumes a: "x\<sharp>\<theta>n"
- shows "findn \<theta>n x = None"
+ assumes a: "x\<sharp>\<theta>_n"
+ shows "findn \<theta>_n x = None"
using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: fresh_list_cons fresh_atm fresh_prod)
done
@@ -3114,38 +3114,38 @@
findc :: "(coname\<times>name\<times>trm) list\<Rightarrow>coname\<Rightarrow>(name\<times>trm) option"
where
"findc [] x = None"
-| "findc ((c,y,P)#\<theta>c) a = (if a=c then Some (y,P) else findc \<theta>c a)"
+| "findc ((c,y,P)#\<theta>_c) a = (if a=c then Some (y,P) else findc \<theta>_c a)"
lemma findc_eqvt[eqvt]:
fixes pi1::"name prm"
and pi2::"coname prm"
- shows "(pi1\<bullet>findc \<theta>c a) = findc (pi1\<bullet>\<theta>c) (pi1\<bullet>a)"
- and "(pi2\<bullet>findc \<theta>c a) = findc (pi2\<bullet>\<theta>c) (pi2\<bullet>a)"
-apply(induct \<theta>c)
+ shows "(pi1\<bullet>findc \<theta>_c a) = findc (pi1\<bullet>\<theta>_c) (pi1\<bullet>a)"
+ and "(pi2\<bullet>findc \<theta>_c a) = findc (pi2\<bullet>\<theta>_c) (pi2\<bullet>a)"
+apply(induct \<theta>_c)
apply(auto simp add: perm_bij)
done
lemma findc_fresh:
- assumes a: "a\<sharp>\<theta>c"
- shows "findc \<theta>c a = None"
+ assumes a: "a\<sharp>\<theta>_c"
+ shows "findc \<theta>_c a = None"
using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: fresh_list_cons fresh_atm fresh_prod)
done
abbreviation
nmaps :: "(name\<times>coname\<times>trm) list \<Rightarrow> name \<Rightarrow> (coname\<times>trm) option \<Rightarrow> bool" ("_ nmaps _ to _" [55,55,55] 55)
where
- "\<theta>n nmaps x to P \<equiv> (findn \<theta>n x) = P"
+ "\<theta>_n nmaps x to P \<equiv> (findn \<theta>_n x) = P"
abbreviation
cmaps :: "(coname\<times>name\<times>trm) list \<Rightarrow> coname \<Rightarrow> (name\<times>trm) option \<Rightarrow> bool" ("_ cmaps _ to _" [55,55,55] 55)
where
- "\<theta>c cmaps a to P \<equiv> (findc \<theta>c a) = P"
+ "\<theta>_c cmaps a to P \<equiv> (findc \<theta>_c a) = P"
lemma nmaps_fresh:
- shows "\<theta>n nmaps x to Some (c,P) \<Longrightarrow> a\<sharp>\<theta>n \<Longrightarrow> a\<sharp>(c,P)"
-apply(induct \<theta>n)
+ shows "\<theta>_n nmaps x to Some (c,P) \<Longrightarrow> a\<sharp>\<theta>_n \<Longrightarrow> a\<sharp>(c,P)"
+apply(induct \<theta>_n)
apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
apply(case_tac "aa=x")
apply(auto)
@@ -3154,8 +3154,8 @@
done
lemma cmaps_fresh:
- shows "\<theta>c cmaps a to Some (y,P) \<Longrightarrow> x\<sharp>\<theta>c \<Longrightarrow> x\<sharp>(y,P)"
-apply(induct \<theta>c)
+ shows "\<theta>_c cmaps a to Some (y,P) \<Longrightarrow> x\<sharp>\<theta>_c \<Longrightarrow> x\<sharp>(y,P)"
+apply(induct \<theta>_c)
apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
apply(case_tac "a=aa")
apply(auto)
@@ -3164,14 +3164,14 @@
done
lemma nmaps_false:
- shows "\<theta>n nmaps x to Some (c,P) \<Longrightarrow> x\<sharp>\<theta>n \<Longrightarrow> False"
-apply(induct \<theta>n)
+ shows "\<theta>_n nmaps x to Some (c,P) \<Longrightarrow> x\<sharp>\<theta>_n \<Longrightarrow> False"
+apply(induct \<theta>_n)
apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
done
lemma cmaps_false:
- shows "\<theta>c cmaps c to Some (x,P) \<Longrightarrow> c\<sharp>\<theta>c \<Longrightarrow> False"
-apply(induct \<theta>c)
+ shows "\<theta>_c cmaps c to Some (x,P) \<Longrightarrow> c\<sharp>\<theta>_c \<Longrightarrow> False"
+apply(induct \<theta>_c)
apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
done
@@ -3179,25 +3179,25 @@
lookupa :: "name\<Rightarrow>coname\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm"
where
"lookupa x a [] = Ax x a"
-| "lookupa x a ((c,y,P)#\<theta>c) = (if a=c then Cut <a>.Ax x a (y).P else lookupa x a \<theta>c)"
+| "lookupa x a ((c,y,P)#\<theta>_c) = (if a=c then Cut <a>.Ax x a (y).P else lookupa x a \<theta>_c)"
lemma lookupa_eqvt[eqvt]:
fixes pi1::"name prm"
and pi2::"coname prm"
- shows "(pi1\<bullet>(lookupa x a \<theta>c)) = lookupa (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>c)"
- and "(pi2\<bullet>(lookupa x a \<theta>c)) = lookupa (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>c)"
+ shows "(pi1\<bullet>(lookupa x a \<theta>_c)) = lookupa (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>_c)"
+ and "(pi2\<bullet>(lookupa x a \<theta>_c)) = lookupa (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>_c)"
apply -
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: eqvts)
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: eqvts)
done
lemma lookupa_fire:
- assumes a: "\<theta>c cmaps a to Some (y,P)"
- shows "(lookupa x a \<theta>c) = Cut <a>.Ax x a (y).P"
+ assumes a: "\<theta>_c cmaps a to Some (y,P)"
+ shows "(lookupa x a \<theta>_c) = Cut <a>.Ax x a (y).P"
using a
-apply(induct \<theta>c arbitrary: x a y P)
+apply(induct \<theta>_c arbitrary: x a y P)
apply(auto)
done
@@ -3205,35 +3205,35 @@
lookupb :: "name\<Rightarrow>coname\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>coname\<Rightarrow>trm\<Rightarrow>trm"
where
"lookupb x a [] c P = Cut <c>.P (x).Ax x a"
-| "lookupb x a ((d,y,N)#\<theta>c) c P = (if a=d then Cut <c>.P (y).N else lookupb x a \<theta>c c P)"
+| "lookupb x a ((d,y,N)#\<theta>_c) c P = (if a=d then Cut <c>.P (y).N else lookupb x a \<theta>_c c P)"
lemma lookupb_eqvt[eqvt]:
fixes pi1::"name prm"
and pi2::"coname prm"
- shows "(pi1\<bullet>(lookupb x a \<theta>c c P)) = lookupb (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>c) (pi1\<bullet>c) (pi1\<bullet>P)"
- and "(pi2\<bullet>(lookupb x a \<theta>c c P)) = lookupb (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>c) (pi2\<bullet>c) (pi2\<bullet>P)"
+ shows "(pi1\<bullet>(lookupb x a \<theta>_c c P)) = lookupb (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>_c) (pi1\<bullet>c) (pi1\<bullet>P)"
+ and "(pi2\<bullet>(lookupb x a \<theta>_c c P)) = lookupb (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>_c) (pi2\<bullet>c) (pi2\<bullet>P)"
apply -
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: eqvts)
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: eqvts)
done
fun
lookup :: "name\<Rightarrow>coname\<Rightarrow>(name\<times>coname\<times>trm) list\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm"
where
- "lookup x a [] \<theta>c = lookupa x a \<theta>c"
-| "lookup x a ((y,c,P)#\<theta>n) \<theta>c = (if x=y then (lookupb x a \<theta>c c P) else lookup x a \<theta>n \<theta>c)"
+ "lookup x a [] \<theta>_c = lookupa x a \<theta>_c"
+| "lookup x a ((y,c,P)#\<theta>_n) \<theta>_c = (if x=y then (lookupb x a \<theta>_c c P) else lookup x a \<theta>_n \<theta>_c)"
lemma lookup_eqvt[eqvt]:
fixes pi1::"name prm"
and pi2::"coname prm"
- shows "(pi1\<bullet>(lookup x a \<theta>n \<theta>c)) = lookup (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>n) (pi1\<bullet>\<theta>c)"
- and "(pi2\<bullet>(lookup x a \<theta>n \<theta>c)) = lookup (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>n) (pi2\<bullet>\<theta>c)"
+ shows "(pi1\<bullet>(lookup x a \<theta>_n \<theta>_c)) = lookup (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>_n) (pi1\<bullet>\<theta>_c)"
+ and "(pi2\<bullet>(lookup x a \<theta>_n \<theta>_c)) = lookup (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>_n) (pi2\<bullet>\<theta>_c)"
apply -
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: eqvts)
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: eqvts)
done
@@ -3241,17 +3241,17 @@
lookupc :: "name\<Rightarrow>coname\<Rightarrow>(name\<times>coname\<times>trm) list\<Rightarrow>trm"
where
"lookupc x a [] = Ax x a"
-| "lookupc x a ((y,c,P)#\<theta>n) = (if x=y then P[c\<turnstile>c>a] else lookupc x a \<theta>n)"
+| "lookupc x a ((y,c,P)#\<theta>_n) = (if x=y then P[c\<turnstile>c>a] else lookupc x a \<theta>_n)"
lemma lookupc_eqvt[eqvt]:
fixes pi1::"name prm"
and pi2::"coname prm"
- shows "(pi1\<bullet>(lookupc x a \<theta>n)) = lookupc (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>n)"
- and "(pi2\<bullet>(lookupc x a \<theta>n)) = lookupc (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>n)"
+ shows "(pi1\<bullet>(lookupc x a \<theta>_n)) = lookupc (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>_n)"
+ and "(pi2\<bullet>(lookupc x a \<theta>_n)) = lookupc (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>_n)"
apply -
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: eqvts)
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: eqvts)
done
@@ -3259,47 +3259,47 @@
lookupd :: "name\<Rightarrow>coname\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm"
where
"lookupd x a [] = Ax x a"
-| "lookupd x a ((c,y,P)#\<theta>c) = (if a=c then P[y\<turnstile>n>x] else lookupd x a \<theta>c)"
+| "lookupd x a ((c,y,P)#\<theta>_c) = (if a=c then P[y\<turnstile>n>x] else lookupd x a \<theta>_c)"
lemma lookupd_eqvt[eqvt]:
fixes pi1::"name prm"
and pi2::"coname prm"
- shows "(pi1\<bullet>(lookupd x a \<theta>n)) = lookupd (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>n)"
- and "(pi2\<bullet>(lookupd x a \<theta>n)) = lookupd (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>n)"
+ shows "(pi1\<bullet>(lookupd x a \<theta>_n)) = lookupd (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>_n)"
+ and "(pi2\<bullet>(lookupd x a \<theta>_n)) = lookupd (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>_n)"
apply -
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: eqvts)
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: eqvts)
done
lemma lookupa_fresh:
- assumes a: "a\<sharp>\<theta>c"
- shows "lookupa y a \<theta>c = Ax y a"
+ assumes a: "a\<sharp>\<theta>_c"
+ shows "lookupa y a \<theta>_c = Ax y a"
using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
done
lemma lookupa_csubst:
- assumes a: "a\<sharp>\<theta>c"
- shows "Cut <a>.Ax y a (x).P = (lookupa y a \<theta>c){a:=(x).P}"
+ assumes a: "a\<sharp>\<theta>_c"
+ shows "Cut <a>.Ax y a (x).P = (lookupa y a \<theta>_c){a:=(x).P}"
using a by (simp add: lookupa_fresh)
lemma lookupa_freshness:
fixes a::"coname"
and x::"name"
- shows "a\<sharp>(\<theta>c,c) \<Longrightarrow> a\<sharp>lookupa y c \<theta>c"
- and "x\<sharp>(\<theta>c,y) \<Longrightarrow> x\<sharp>lookupa y c \<theta>c"
-apply(induct \<theta>c)
+ shows "a\<sharp>(\<theta>_c,c) \<Longrightarrow> a\<sharp>lookupa y c \<theta>_c"
+ and "x\<sharp>(\<theta>_c,y) \<Longrightarrow> x\<sharp>lookupa y c \<theta>_c"
+apply(induct \<theta>_c)
apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
done
lemma lookupa_unicity:
- assumes a: "lookupa x a \<theta>c= Ax y b" "b\<sharp>\<theta>c" "y\<sharp>\<theta>c"
+ assumes a: "lookupa x a \<theta>_c= Ax y b" "b\<sharp>\<theta>_c" "y\<sharp>\<theta>_c"
shows "x=y \<and> a=b"
using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: trm.inject fresh_list_cons fresh_prod fresh_atm)
apply(case_tac "a=aa")
apply(auto)
@@ -3308,10 +3308,10 @@
done
lemma lookupb_csubst:
- assumes a: "a\<sharp>(\<theta>c,c,N)"
- shows "Cut <c>.N (x).P = (lookupb y a \<theta>c c N){a:=(x).P}"
+ assumes a: "a\<sharp>(\<theta>_c,c,N)"
+ shows "Cut <c>.N (x).P = (lookupb y a \<theta>_c c N){a:=(x).P}"
using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: fresh_list_cons fresh_atm fresh_prod)
apply(rule sym)
apply(generate_fresh "name")
@@ -3337,17 +3337,17 @@
lemma lookupb_freshness:
fixes a::"coname"
and x::"name"
- shows "a\<sharp>(\<theta>c,c,b,P) \<Longrightarrow> a\<sharp>lookupb y c \<theta>c b P"
- and "x\<sharp>(\<theta>c,y,P) \<Longrightarrow> x\<sharp>lookupb y c \<theta>c b P"
-apply(induct \<theta>c)
+ shows "a\<sharp>(\<theta>_c,c,b,P) \<Longrightarrow> a\<sharp>lookupb y c \<theta>_c b P"
+ and "x\<sharp>(\<theta>_c,y,P) \<Longrightarrow> x\<sharp>lookupb y c \<theta>_c b P"
+apply(induct \<theta>_c)
apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
done
lemma lookupb_unicity:
- assumes a: "lookupb x a \<theta>c c P = Ax y b" "b\<sharp>(\<theta>c,c,P)" "y\<sharp>\<theta>c"
+ assumes a: "lookupb x a \<theta>_c c P = Ax y b" "b\<sharp>(\<theta>_c,c,P)" "y\<sharp>\<theta>_c"
shows "x=y \<and> a=b"
using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
apply(case_tac "a=aa")
apply(auto)
@@ -3356,10 +3356,10 @@
done
lemma lookupb_lookupa:
- assumes a: "x\<sharp>\<theta>c"
- shows "lookupb x c \<theta>c a P = (lookupa x c \<theta>c){x:=<a>.P}"
+ assumes a: "x\<sharp>\<theta>_c"
+ shows "lookupb x c \<theta>_c a P = (lookupa x c \<theta>_c){x:=<a>.P}"
using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: fresh_list_cons fresh_prod)
apply(generate_fresh "coname")
apply(generate_fresh "name")
@@ -3383,10 +3383,10 @@
done
lemma lookup_csubst:
- assumes a: "a\<sharp>(\<theta>n,\<theta>c)"
- shows "lookup y c \<theta>n ((a,x,P)#\<theta>c) = (lookup y c \<theta>n \<theta>c){a:=(x).P}"
+ assumes a: "a\<sharp>(\<theta>_n,\<theta>_c)"
+ shows "lookup y c \<theta>_n ((a,x,P)#\<theta>_c) = (lookup y c \<theta>_n \<theta>_c){a:=(x).P}"
using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: fresh_prod fresh_list_cons)
apply(simp add: lookupa_csubst)
apply(simp add: lookupa_freshness forget fresh_atm fresh_prod)
@@ -3396,18 +3396,18 @@
done
lemma lookup_fresh:
- assumes a: "x\<sharp>(\<theta>n,\<theta>c)"
- shows "lookup x c \<theta>n \<theta>c = lookupa x c \<theta>c"
+ assumes a: "x\<sharp>(\<theta>_n,\<theta>_c)"
+ shows "lookup x c \<theta>_n \<theta>_c = lookupa x c \<theta>_c"
using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
done
lemma lookup_unicity:
- assumes a: "lookup x a \<theta>n \<theta>c= Ax y b" "b\<sharp>(\<theta>c,\<theta>n)" "y\<sharp>(\<theta>c,\<theta>n)"
+ assumes a: "lookup x a \<theta>_n \<theta>_c= Ax y b" "b\<sharp>(\<theta>_c,\<theta>_n)" "y\<sharp>(\<theta>_c,\<theta>_n)"
shows "x=y \<and> a=b"
using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: trm.inject fresh_list_cons fresh_prod fresh_atm)
apply(drule lookupa_unicity)
apply(simp)+
@@ -3430,9 +3430,9 @@
lemma lookup_freshness:
fixes a::"coname"
and x::"name"
- shows "a\<sharp>(c,\<theta>c,\<theta>n) \<Longrightarrow> a\<sharp>lookup y c \<theta>n \<theta>c"
- and "x\<sharp>(y,\<theta>c,\<theta>n) \<Longrightarrow> x\<sharp>lookup y c \<theta>n \<theta>c"
-apply(induct \<theta>n)
+ shows "a\<sharp>(c,\<theta>_c,\<theta>_n) \<Longrightarrow> a\<sharp>lookup y c \<theta>_n \<theta>_c"
+ and "x\<sharp>(y,\<theta>_c,\<theta>_n) \<Longrightarrow> x\<sharp>lookup y c \<theta>_n \<theta>_c"
+apply(induct \<theta>_n)
apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
apply(simp add: fresh_atm fresh_prod lookupa_freshness)
apply(simp add: fresh_atm fresh_prod lookupa_freshness)
@@ -3443,9 +3443,9 @@
lemma lookupc_freshness:
fixes a::"coname"
and x::"name"
- shows "a\<sharp>(\<theta>c,c) \<Longrightarrow> a\<sharp>lookupc y c \<theta>c"
- and "x\<sharp>(\<theta>c,y) \<Longrightarrow> x\<sharp>lookupc y c \<theta>c"
-apply(induct \<theta>c)
+ shows "a\<sharp>(\<theta>_c,c) \<Longrightarrow> a\<sharp>lookupc y c \<theta>_c"
+ and "x\<sharp>(\<theta>_c,y) \<Longrightarrow> x\<sharp>lookupc y c \<theta>_c"
+apply(induct \<theta>_c)
apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
apply(rule rename_fresh)
apply(simp add: fresh_atm)
@@ -3454,26 +3454,26 @@
done
lemma lookupc_fresh:
- assumes a: "y\<sharp>\<theta>n"
- shows "lookupc y a \<theta>n = Ax y a"
+ assumes a: "y\<sharp>\<theta>_n"
+ shows "lookupc y a \<theta>_n = Ax y a"
using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
done
lemma lookupc_nmaps:
- assumes a: "\<theta>n nmaps x to Some (c,P)"
- shows "lookupc x a \<theta>n = P[c\<turnstile>c>a]"
+ assumes a: "\<theta>_n nmaps x to Some (c,P)"
+ shows "lookupc x a \<theta>_n = P[c\<turnstile>c>a]"
using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto)
done
lemma lookupc_unicity:
- assumes a: "lookupc y a \<theta>n = Ax x b" "x\<sharp>\<theta>n"
+ assumes a: "lookupc y a \<theta>_n = Ax x b" "x\<sharp>\<theta>_n"
shows "y=x"
using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: trm.inject fresh_list_cons fresh_prod)
apply(case_tac "y=aa")
apply(auto)
@@ -3484,18 +3484,18 @@
done
lemma lookupd_fresh:
- assumes a: "a\<sharp>\<theta>c"
- shows "lookupd y a \<theta>c = Ax y a"
+ assumes a: "a\<sharp>\<theta>_c"
+ shows "lookupd y a \<theta>_c = Ax y a"
using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
done
lemma lookupd_unicity:
- assumes a: "lookupd y a \<theta>c = Ax y b" "b\<sharp>\<theta>c"
+ assumes a: "lookupd y a \<theta>_c = Ax y b" "b\<sharp>\<theta>_c"
shows "a=b"
using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto simp add: trm.inject fresh_list_cons fresh_prod)
apply(case_tac "a=aa")
apply(auto)
@@ -3508,9 +3508,9 @@
lemma lookupd_freshness:
fixes a::"coname"
and x::"name"
- shows "a\<sharp>(\<theta>c,c) \<Longrightarrow> a\<sharp>lookupd y c \<theta>c"
- and "x\<sharp>(\<theta>c,y) \<Longrightarrow> x\<sharp>lookupd y c \<theta>c"
-apply(induct \<theta>c)
+ shows "a\<sharp>(\<theta>_c,c) \<Longrightarrow> a\<sharp>lookupd y c \<theta>_c"
+ and "x\<sharp>(\<theta>_c,y) \<Longrightarrow> x\<sharp>lookupd y c \<theta>_c"
+apply(induct \<theta>_c)
apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
apply(rule rename_fresh)
apply(simp add: fresh_atm)
@@ -3519,49 +3519,49 @@
done
lemma lookupd_cmaps:
- assumes a: "\<theta>c cmaps a to Some (x,P)"
- shows "lookupd y a \<theta>c = P[x\<turnstile>n>y]"
+ assumes a: "\<theta>_c cmaps a to Some (x,P)"
+ shows "lookupd y a \<theta>_c = P[x\<turnstile>n>y]"
using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto)
done
-nominal_primrec (freshness_context: "\<theta>n::(name\<times>coname\<times>trm)")
+nominal_primrec (freshness_context: "\<theta>_n::(name\<times>coname\<times>trm)")
stn :: "trm\<Rightarrow>(name\<times>coname\<times>trm) list\<Rightarrow>trm"
where
- "stn (Ax x a) \<theta>n = lookupc x a \<theta>n"
-| "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,\<theta>n)\<rbrakk> \<Longrightarrow> stn (Cut <a>.M (x).N) \<theta>n = (Cut <a>.M (x).N)"
-| "x\<sharp>\<theta>n \<Longrightarrow> stn (NotR (x).M a) \<theta>n = (NotR (x).M a)"
-| "a\<sharp>\<theta>n \<Longrightarrow>stn (NotL <a>.M x) \<theta>n = (NotL <a>.M x)"
-| "\<lbrakk>a\<sharp>(N,d,b,\<theta>n);b\<sharp>(M,d,a,\<theta>n)\<rbrakk> \<Longrightarrow> stn (AndR <a>.M <b>.N d) \<theta>n = (AndR <a>.M <b>.N d)"
-| "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL1 (x).M z) \<theta>n = (AndL1 (x).M z)"
-| "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL2 (x).M z) \<theta>n = (AndL2 (x).M z)"
-| "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR1 <a>.M b) \<theta>n = (OrR1 <a>.M b)"
-| "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR2 <a>.M b) \<theta>n = (OrR2 <a>.M b)"
-| "\<lbrakk>x\<sharp>(N,z,u,\<theta>n);u\<sharp>(M,z,x,\<theta>n)\<rbrakk> \<Longrightarrow> stn (OrL (x).M (u).N z) \<theta>n = (OrL (x).M (u).N z)"
-| "\<lbrakk>a\<sharp>(b,\<theta>n);x\<sharp>\<theta>n\<rbrakk> \<Longrightarrow> stn (ImpR (x).<a>.M b) \<theta>n = (ImpR (x).<a>.M b)"
-| "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,z,\<theta>n)\<rbrakk> \<Longrightarrow> stn (ImpL <a>.M (x).N z) \<theta>n = (ImpL <a>.M (x).N z)"
+ "stn (Ax x a) \<theta>_n = lookupc x a \<theta>_n"
+| "\<lbrakk>a\<sharp>(N,\<theta>_n);x\<sharp>(M,\<theta>_n)\<rbrakk> \<Longrightarrow> stn (Cut <a>.M (x).N) \<theta>_n = (Cut <a>.M (x).N)"
+| "x\<sharp>\<theta>_n \<Longrightarrow> stn (NotR (x).M a) \<theta>_n = (NotR (x).M a)"
+| "a\<sharp>\<theta>_n \<Longrightarrow>stn (NotL <a>.M x) \<theta>_n = (NotL <a>.M x)"
+| "\<lbrakk>a\<sharp>(N,d,b,\<theta>_n);b\<sharp>(M,d,a,\<theta>_n)\<rbrakk> \<Longrightarrow> stn (AndR <a>.M <b>.N d) \<theta>_n = (AndR <a>.M <b>.N d)"
+| "x\<sharp>(z,\<theta>_n) \<Longrightarrow> stn (AndL1 (x).M z) \<theta>_n = (AndL1 (x).M z)"
+| "x\<sharp>(z,\<theta>_n) \<Longrightarrow> stn (AndL2 (x).M z) \<theta>_n = (AndL2 (x).M z)"
+| "a\<sharp>(b,\<theta>_n) \<Longrightarrow> stn (OrR1 <a>.M b) \<theta>_n = (OrR1 <a>.M b)"
+| "a\<sharp>(b,\<theta>_n) \<Longrightarrow> stn (OrR2 <a>.M b) \<theta>_n = (OrR2 <a>.M b)"
+| "\<lbrakk>x\<sharp>(N,z,u,\<theta>_n);u\<sharp>(M,z,x,\<theta>_n)\<rbrakk> \<Longrightarrow> stn (OrL (x).M (u).N z) \<theta>_n = (OrL (x).M (u).N z)"
+| "\<lbrakk>a\<sharp>(b,\<theta>_n);x\<sharp>\<theta>_n\<rbrakk> \<Longrightarrow> stn (ImpR (x).<a>.M b) \<theta>_n = (ImpR (x).<a>.M b)"
+| "\<lbrakk>a\<sharp>(N,\<theta>_n);x\<sharp>(M,z,\<theta>_n)\<rbrakk> \<Longrightarrow> stn (ImpL <a>.M (x).N z) \<theta>_n = (ImpL <a>.M (x).N z)"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh abs_supp fin_supp)+
apply(fresh_guess)+
done
-nominal_primrec (freshness_context: "\<theta>c::(coname\<times>name\<times>trm)")
+nominal_primrec (freshness_context: "\<theta>_c::(coname\<times>name\<times>trm)")
stc :: "trm\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm"
where
- "stc (Ax x a) \<theta>c = lookupd x a \<theta>c"
-| "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,\<theta>c)\<rbrakk> \<Longrightarrow> stc (Cut <a>.M (x).N) \<theta>c = (Cut <a>.M (x).N)"
-| "x\<sharp>\<theta>c \<Longrightarrow> stc (NotR (x).M a) \<theta>c = (NotR (x).M a)"
-| "a\<sharp>\<theta>c \<Longrightarrow> stc (NotL <a>.M x) \<theta>c = (NotL <a>.M x)"
-| "\<lbrakk>a\<sharp>(N,d,b,\<theta>c);b\<sharp>(M,d,a,\<theta>c)\<rbrakk> \<Longrightarrow> stc (AndR <a>.M <b>.N d) \<theta>c = (AndR <a>.M <b>.N d)"
-| "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL1 (x).M z) \<theta>c = (AndL1 (x).M z)"
-| "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL2 (x).M z) \<theta>c = (AndL2 (x).M z)"
-| "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR1 <a>.M b) \<theta>c = (OrR1 <a>.M b)"
-| "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR2 <a>.M b) \<theta>c = (OrR2 <a>.M b)"
-| "\<lbrakk>x\<sharp>(N,z,u,\<theta>c);u\<sharp>(M,z,x,\<theta>c)\<rbrakk> \<Longrightarrow> stc (OrL (x).M (u).N z) \<theta>c = (OrL (x).M (u).N z)"
-| "\<lbrakk>a\<sharp>(b,\<theta>c);x\<sharp>\<theta>c\<rbrakk> \<Longrightarrow> stc (ImpR (x).<a>.M b) \<theta>c = (ImpR (x).<a>.M b)"
-| "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,z,\<theta>c)\<rbrakk> \<Longrightarrow> stc (ImpL <a>.M (x).N z) \<theta>c = (ImpL <a>.M (x).N z)"
+ "stc (Ax x a) \<theta>_c = lookupd x a \<theta>_c"
+| "\<lbrakk>a\<sharp>(N,\<theta>_c);x\<sharp>(M,\<theta>_c)\<rbrakk> \<Longrightarrow> stc (Cut <a>.M (x).N) \<theta>_c = (Cut <a>.M (x).N)"
+| "x\<sharp>\<theta>_c \<Longrightarrow> stc (NotR (x).M a) \<theta>_c = (NotR (x).M a)"
+| "a\<sharp>\<theta>_c \<Longrightarrow> stc (NotL <a>.M x) \<theta>_c = (NotL <a>.M x)"
+| "\<lbrakk>a\<sharp>(N,d,b,\<theta>_c);b\<sharp>(M,d,a,\<theta>_c)\<rbrakk> \<Longrightarrow> stc (AndR <a>.M <b>.N d) \<theta>_c = (AndR <a>.M <b>.N d)"
+| "x\<sharp>(z,\<theta>_c) \<Longrightarrow> stc (AndL1 (x).M z) \<theta>_c = (AndL1 (x).M z)"
+| "x\<sharp>(z,\<theta>_c) \<Longrightarrow> stc (AndL2 (x).M z) \<theta>_c = (AndL2 (x).M z)"
+| "a\<sharp>(b,\<theta>_c) \<Longrightarrow> stc (OrR1 <a>.M b) \<theta>_c = (OrR1 <a>.M b)"
+| "a\<sharp>(b,\<theta>_c) \<Longrightarrow> stc (OrR2 <a>.M b) \<theta>_c = (OrR2 <a>.M b)"
+| "\<lbrakk>x\<sharp>(N,z,u,\<theta>_c);u\<sharp>(M,z,x,\<theta>_c)\<rbrakk> \<Longrightarrow> stc (OrL (x).M (u).N z) \<theta>_c = (OrL (x).M (u).N z)"
+| "\<lbrakk>a\<sharp>(b,\<theta>_c);x\<sharp>\<theta>_c\<rbrakk> \<Longrightarrow> stc (ImpR (x).<a>.M b) \<theta>_c = (ImpR (x).<a>.M b)"
+| "\<lbrakk>a\<sharp>(N,\<theta>_c);x\<sharp>(M,z,\<theta>_c)\<rbrakk> \<Longrightarrow> stc (ImpL <a>.M (x).N z) \<theta>_c = (ImpL <a>.M (x).N z)"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh abs_supp fin_supp)+
@@ -3571,33 +3571,33 @@
lemma stn_eqvt[eqvt]:
fixes pi1::"name prm"
and pi2::"coname prm"
- shows "(pi1\<bullet>(stn M \<theta>n)) = stn (pi1\<bullet>M) (pi1\<bullet>\<theta>n)"
- and "(pi2\<bullet>(stn M \<theta>n)) = stn (pi2\<bullet>M) (pi2\<bullet>\<theta>n)"
+ shows "(pi1\<bullet>(stn M \<theta>_n)) = stn (pi1\<bullet>M) (pi1\<bullet>\<theta>_n)"
+ and "(pi2\<bullet>(stn M \<theta>_n)) = stn (pi2\<bullet>M) (pi2\<bullet>\<theta>_n)"
apply -
-apply(nominal_induct M avoiding: \<theta>n rule: trm.strong_induct)
+apply(nominal_induct M avoiding: \<theta>_n rule: trm.strong_induct)
apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
-apply(nominal_induct M avoiding: \<theta>n rule: trm.strong_induct)
+apply(nominal_induct M avoiding: \<theta>_n rule: trm.strong_induct)
apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
done
lemma stc_eqvt[eqvt]:
fixes pi1::"name prm"
and pi2::"coname prm"
- shows "(pi1\<bullet>(stc M \<theta>c)) = stc (pi1\<bullet>M) (pi1\<bullet>\<theta>c)"
- and "(pi2\<bullet>(stc M \<theta>c)) = stc (pi2\<bullet>M) (pi2\<bullet>\<theta>c)"
+ shows "(pi1\<bullet>(stc M \<theta>_c)) = stc (pi1\<bullet>M) (pi1\<bullet>\<theta>_c)"
+ and "(pi2\<bullet>(stc M \<theta>_c)) = stc (pi2\<bullet>M) (pi2\<bullet>\<theta>_c)"
apply -
-apply(nominal_induct M avoiding: \<theta>c rule: trm.strong_induct)
+apply(nominal_induct M avoiding: \<theta>_c rule: trm.strong_induct)
apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
-apply(nominal_induct M avoiding: \<theta>c rule: trm.strong_induct)
+apply(nominal_induct M avoiding: \<theta>_c rule: trm.strong_induct)
apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
done
lemma stn_fresh:
fixes a::"coname"
and x::"name"
- shows "a\<sharp>(\<theta>n,M) \<Longrightarrow> a\<sharp>stn M \<theta>n"
- and "x\<sharp>(\<theta>n,M) \<Longrightarrow> x\<sharp>stn M \<theta>n"
-apply(nominal_induct M avoiding: \<theta>n a x rule: trm.strong_induct)
+ shows "a\<sharp>(\<theta>_n,M) \<Longrightarrow> a\<sharp>stn M \<theta>_n"
+ and "x\<sharp>(\<theta>_n,M) \<Longrightarrow> x\<sharp>stn M \<theta>_n"
+apply(nominal_induct M avoiding: \<theta>_n a x rule: trm.strong_induct)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)
apply(rule lookupc_freshness)
apply(simp add: fresh_atm)
@@ -3608,9 +3608,9 @@
lemma stc_fresh:
fixes a::"coname"
and x::"name"
- shows "a\<sharp>(\<theta>c,M) \<Longrightarrow> a\<sharp>stc M \<theta>c"
- and "x\<sharp>(\<theta>c,M) \<Longrightarrow> x\<sharp>stc M \<theta>c"
-apply(nominal_induct M avoiding: \<theta>c a x rule: trm.strong_induct)
+ shows "a\<sharp>(\<theta>_c,M) \<Longrightarrow> a\<sharp>stc M \<theta>_c"
+ and "x\<sharp>(\<theta>_c,M) \<Longrightarrow> x\<sharp>stc M \<theta>_c"
+apply(nominal_induct M avoiding: \<theta>_c a x rule: trm.strong_induct)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)
apply(rule lookupd_freshness)
apply(simp add: fresh_atm)
@@ -3652,58 +3652,58 @@
apply(perm_simp)
done
-nominal_primrec (freshness_context: "(\<theta>n::(name\<times>coname\<times>trm) list,\<theta>c::(coname\<times>name\<times>trm) list)")
+nominal_primrec (freshness_context: "(\<theta>_n::(name\<times>coname\<times>trm) list,\<theta>_c::(coname\<times>name\<times>trm) list)")
psubst :: "(name\<times>coname\<times>trm) list\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm\<Rightarrow>trm" ("_,_<_>" [100,100,100] 100)
where
- "\<theta>n,\<theta>c<Ax x a> = lookup x a \<theta>n \<theta>c"
-| "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c);x\<sharp>(M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> \<theta>n,\<theta>c<Cut <a>.M (x).N> =
- Cut <a>.(if \<exists>x. M=Ax x a then stn M \<theta>n else \<theta>n,\<theta>c<M>)
- (x).(if \<exists>a. N=Ax x a then stc N \<theta>c else \<theta>n,\<theta>c<N>)"
-| "x\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotR (x).M a> =
- (case (findc \<theta>c a) of
- Some (u,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.NotR (x).(\<theta>n,\<theta>c<M>) a' (u).P)
- | None \<Rightarrow> NotR (x).(\<theta>n,\<theta>c<M>) a)"
-| "a\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotL <a>.M x> =
- (case (findn \<theta>n x) of
- Some (c,P) \<Rightarrow> fresh_fun (\<lambda>x'. Cut <c>.P (x').(NotL <a>.(\<theta>n,\<theta>c<M>) x'))
- | None \<Rightarrow> NotL <a>.(\<theta>n,\<theta>c<M>) x)"
-| "\<lbrakk>a\<sharp>(N,c,\<theta>n,\<theta>c);b\<sharp>(M,c,\<theta>n,\<theta>c);b\<noteq>a\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<AndR <a>.M <b>.N c>) =
- (case (findc \<theta>c c) of
- Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.(\<theta>n,\<theta>c<M>) <b>.(\<theta>n,\<theta>c<N>) a') (x).P)
- | None \<Rightarrow> AndR <a>.(\<theta>n,\<theta>c<M>) <b>.(\<theta>n,\<theta>c<N>) c)"
-| "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL1 (x).M z>) =
- (case (findn \<theta>n z) of
- Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).(\<theta>n,\<theta>c<M>) z')
- | None \<Rightarrow> AndL1 (x).(\<theta>n,\<theta>c<M>) z)"
-| "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL2 (x).M z>) =
- (case (findn \<theta>n z) of
- Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).(\<theta>n,\<theta>c<M>) z')
- | None \<Rightarrow> AndL2 (x).(\<theta>n,\<theta>c<M>) z)"
-| "\<lbrakk>x\<sharp>(N,z,\<theta>n,\<theta>c);u\<sharp>(M,z,\<theta>n,\<theta>c);x\<noteq>u\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<OrL (x).M (u).N z>) =
- (case (findn \<theta>n z) of
- Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).(\<theta>n,\<theta>c<M>) (u).(\<theta>n,\<theta>c<N>) z')
- | None \<Rightarrow> OrL (x).(\<theta>n,\<theta>c<M>) (u).(\<theta>n,\<theta>c<N>) z)"
-| "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR1 <a>.M b>) =
- (case (findc \<theta>c b) of
- Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.(\<theta>n,\<theta>c<M>) a' (x).P)
- | None \<Rightarrow> OrR1 <a>.(\<theta>n,\<theta>c<M>) b)"
-| "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR2 <a>.M b>) =
- (case (findc \<theta>c b) of
- Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.(\<theta>n,\<theta>c<M>) a' (x).P)
- | None \<Rightarrow> OrR2 <a>.(\<theta>n,\<theta>c<M>) b)"
-| "\<lbrakk>a\<sharp>(b,\<theta>n,\<theta>c); x\<sharp>(\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpR (x).<a>.M b>) =
- (case (findc \<theta>c b) of
- Some (z,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(\<theta>n,\<theta>c<M>) a' (z).P)
- | None \<Rightarrow> ImpR (x).<a>.(\<theta>n,\<theta>c<M>) b)"
-| "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c); x\<sharp>(z,M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpL <a>.M (x).N z>) =
- (case (findn \<theta>n z) of
- Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.(\<theta>n,\<theta>c<M>) (x).(\<theta>n,\<theta>c<N>) z')
- | None \<Rightarrow> ImpL <a>.(\<theta>n,\<theta>c<M>) (x).(\<theta>n,\<theta>c<N>) z)"
+ "\<theta>_n,\<theta>_c<Ax x a> = lookup x a \<theta>_n \<theta>_c"
+| "\<lbrakk>a\<sharp>(N,\<theta>_n,\<theta>_c);x\<sharp>(M,\<theta>_n,\<theta>_c)\<rbrakk> \<Longrightarrow> \<theta>_n,\<theta>_c<Cut <a>.M (x).N> =
+ Cut <a>.(if \<exists>x. M=Ax x a then stn M \<theta>_n else \<theta>_n,\<theta>_c<M>)
+ (x).(if \<exists>a. N=Ax x a then stc N \<theta>_c else \<theta>_n,\<theta>_c<N>)"
+| "x\<sharp>(\<theta>_n,\<theta>_c) \<Longrightarrow> \<theta>_n,\<theta>_c<NotR (x).M a> =
+ (case (findc \<theta>_c a) of
+ Some (u,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.NotR (x).(\<theta>_n,\<theta>_c<M>) a' (u).P)
+ | None \<Rightarrow> NotR (x).(\<theta>_n,\<theta>_c<M>) a)"
+| "a\<sharp>(\<theta>_n,\<theta>_c) \<Longrightarrow> \<theta>_n,\<theta>_c<NotL <a>.M x> =
+ (case (findn \<theta>_n x) of
+ Some (c,P) \<Rightarrow> fresh_fun (\<lambda>x'. Cut <c>.P (x').(NotL <a>.(\<theta>_n,\<theta>_c<M>) x'))
+ | None \<Rightarrow> NotL <a>.(\<theta>_n,\<theta>_c<M>) x)"
+| "\<lbrakk>a\<sharp>(N,c,\<theta>_n,\<theta>_c);b\<sharp>(M,c,\<theta>_n,\<theta>_c);b\<noteq>a\<rbrakk> \<Longrightarrow> (\<theta>_n,\<theta>_c<AndR <a>.M <b>.N c>) =
+ (case (findc \<theta>_c c) of
+ Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.(\<theta>_n,\<theta>_c<M>) <b>.(\<theta>_n,\<theta>_c<N>) a') (x).P)
+ | None \<Rightarrow> AndR <a>.(\<theta>_n,\<theta>_c<M>) <b>.(\<theta>_n,\<theta>_c<N>) c)"
+| "x\<sharp>(z,\<theta>_n,\<theta>_c) \<Longrightarrow> (\<theta>_n,\<theta>_c<AndL1 (x).M z>) =
+ (case (findn \<theta>_n z) of
+ Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).(\<theta>_n,\<theta>_c<M>) z')
+ | None \<Rightarrow> AndL1 (x).(\<theta>_n,\<theta>_c<M>) z)"
+| "x\<sharp>(z,\<theta>_n,\<theta>_c) \<Longrightarrow> (\<theta>_n,\<theta>_c<AndL2 (x).M z>) =
+ (case (findn \<theta>_n z) of
+ Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).(\<theta>_n,\<theta>_c<M>) z')
+ | None \<Rightarrow> AndL2 (x).(\<theta>_n,\<theta>_c<M>) z)"
+| "\<lbrakk>x\<sharp>(N,z,\<theta>_n,\<theta>_c);u\<sharp>(M,z,\<theta>_n,\<theta>_c);x\<noteq>u\<rbrakk> \<Longrightarrow> (\<theta>_n,\<theta>_c<OrL (x).M (u).N z>) =
+ (case (findn \<theta>_n z) of
+ Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).(\<theta>_n,\<theta>_c<M>) (u).(\<theta>_n,\<theta>_c<N>) z')
+ | None \<Rightarrow> OrL (x).(\<theta>_n,\<theta>_c<M>) (u).(\<theta>_n,\<theta>_c<N>) z)"
+| "a\<sharp>(b,\<theta>_n,\<theta>_c) \<Longrightarrow> (\<theta>_n,\<theta>_c<OrR1 <a>.M b>) =
+ (case (findc \<theta>_c b) of
+ Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.(\<theta>_n,\<theta>_c<M>) a' (x).P)
+ | None \<Rightarrow> OrR1 <a>.(\<theta>_n,\<theta>_c<M>) b)"
+| "a\<sharp>(b,\<theta>_n,\<theta>_c) \<Longrightarrow> (\<theta>_n,\<theta>_c<OrR2 <a>.M b>) =
+ (case (findc \<theta>_c b) of
+ Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.(\<theta>_n,\<theta>_c<M>) a' (x).P)
+ | None \<Rightarrow> OrR2 <a>.(\<theta>_n,\<theta>_c<M>) b)"
+| "\<lbrakk>a\<sharp>(b,\<theta>_n,\<theta>_c); x\<sharp>(\<theta>_n,\<theta>_c)\<rbrakk> \<Longrightarrow> (\<theta>_n,\<theta>_c<ImpR (x).<a>.M b>) =
+ (case (findc \<theta>_c b) of
+ Some (z,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(\<theta>_n,\<theta>_c<M>) a' (z).P)
+ | None \<Rightarrow> ImpR (x).<a>.(\<theta>_n,\<theta>_c<M>) b)"
+| "\<lbrakk>a\<sharp>(N,\<theta>_n,\<theta>_c); x\<sharp>(z,M,\<theta>_n,\<theta>_c)\<rbrakk> \<Longrightarrow> (\<theta>_n,\<theta>_c<ImpL <a>.M (x).N z>) =
+ (case (findn \<theta>_n z) of
+ Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.(\<theta>_n,\<theta>_c<M>) (x).(\<theta>_n,\<theta>_c<N>) z')
+ | None \<Rightarrow> ImpL <a>.(\<theta>_n,\<theta>_c<M>) (x).(\<theta>_n,\<theta>_c<N>) z)"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh stc_fresh)
apply(simp add: abs_fresh stn_fresh)
-apply(case_tac "findc \<theta>c x3")
+apply(case_tac "findc \<theta>_c x3")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "coname")
@@ -3711,7 +3711,7 @@
apply(drule cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x3")
+apply(case_tac "findn \<theta>_n x3")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
@@ -3719,7 +3719,7 @@
apply(drule nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findc \<theta>c x5")
+apply(case_tac "findc \<theta>_c x5")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "coname")
@@ -3727,7 +3727,7 @@
apply(drule cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findc \<theta>c x5")
+apply(case_tac "findc \<theta>_c x5")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "coname")
@@ -3735,7 +3735,7 @@
apply(drule_tac x="x3" in cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x3")
+apply(case_tac "findn \<theta>_n x3")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
@@ -3743,7 +3743,7 @@
apply(drule nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x3")
+apply(case_tac "findn \<theta>_n x3")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
@@ -3751,7 +3751,7 @@
apply(drule nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findc \<theta>c x3")
+apply(case_tac "findc \<theta>_c x3")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "coname")
@@ -3759,7 +3759,7 @@
apply(drule cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findc \<theta>c x3")
+apply(case_tac "findc \<theta>_c x3")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "coname")
@@ -3767,7 +3767,7 @@
apply(drule cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x5")
+apply(case_tac "findn \<theta>_n x5")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
@@ -3775,7 +3775,7 @@
apply(drule nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x5")
+apply(case_tac "findn \<theta>_n x5")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
@@ -3783,7 +3783,7 @@
apply(drule_tac a="x3" in nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findc \<theta>c x4")
+apply(case_tac "findc \<theta>_c x4")
apply(simp add: abs_fresh abs_supp fin_supp)
apply(auto)[1]
apply(generate_fresh "coname")
@@ -3791,7 +3791,7 @@
apply(drule cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm abs_supp fin_supp)
-apply(case_tac "findc \<theta>c x4")
+apply(case_tac "findc \<theta>_c x4")
apply(simp add: abs_fresh abs_supp fin_supp)
apply(auto)[1]
apply(generate_fresh "coname")
@@ -3799,7 +3799,7 @@
apply(drule_tac x="x2" in cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm abs_supp fin_supp)
-apply(case_tac "findn \<theta>n x5")
+apply(case_tac "findn \<theta>_n x5")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
@@ -3807,7 +3807,7 @@
apply(drule nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x5")
+apply(case_tac "findn \<theta>_n x5")
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
@@ -3826,17 +3826,17 @@
done
lemma find_maps:
- shows "\<theta>c cmaps a to (findc \<theta>c a)"
- and "\<theta>n nmaps x to (findn \<theta>n x)"
+ shows "\<theta>_c cmaps a to (findc \<theta>_c a)"
+ and "\<theta>_n nmaps x to (findn \<theta>_n x)"
apply(auto)
done
lemma psubst_eqvt[eqvt]:
fixes pi1::"name prm"
and pi2::"coname prm"
- shows "pi1\<bullet>(\<theta>n,\<theta>c<M>) = (pi1\<bullet>\<theta>n),(pi1\<bullet>\<theta>c)<(pi1\<bullet>M)>"
- and "pi2\<bullet>(\<theta>n,\<theta>c<M>) = (pi2\<bullet>\<theta>n),(pi2\<bullet>\<theta>c)<(pi2\<bullet>M)>"
-apply(nominal_induct M avoiding: \<theta>n \<theta>c rule: trm.strong_induct)
+ shows "pi1\<bullet>(\<theta>_n,\<theta>_c<M>) = (pi1\<bullet>\<theta>_n),(pi1\<bullet>\<theta>_c)<(pi1\<bullet>M)>"
+ and "pi2\<bullet>(\<theta>_n,\<theta>_c<M>) = (pi2\<bullet>\<theta>_n),(pi2\<bullet>\<theta>_c)<(pi2\<bullet>M)>"
+apply(nominal_induct M avoiding: \<theta>_n \<theta>_c rule: trm.strong_induct)
apply(auto simp add: eq_bij fresh_bij eqvts perm_pi_simp)
apply(rule case_cong)
apply(rule find_maps)
@@ -3921,69 +3921,69 @@
done
lemma ax_psubst:
- assumes a: "\<theta>n,\<theta>c<M> = Ax x a"
- and b: "a\<sharp>(\<theta>n,\<theta>c)" "x\<sharp>(\<theta>n,\<theta>c)"
+ assumes a: "\<theta>_n,\<theta>_c<M> = Ax x a"
+ and b: "a\<sharp>(\<theta>_n,\<theta>_c)" "x\<sharp>(\<theta>_n,\<theta>_c)"
shows "M = Ax x a"
using a b
-apply(nominal_induct M avoiding: \<theta>n \<theta>c rule: trm.strong_induct)
+apply(nominal_induct M avoiding: \<theta>_n \<theta>_c rule: trm.strong_induct)
apply(auto)
apply(drule lookup_unicity)
apply(simp)+
-apply(case_tac "findc \<theta>c coname")
+apply(case_tac "findc \<theta>_c coname")
apply(simp)
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp)
-apply(case_tac "findn \<theta>n name")
+apply(case_tac "findn \<theta>_n name")
apply(simp)
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp)
-apply(case_tac "findc \<theta>c coname3")
+apply(case_tac "findc \<theta>_c coname3")
apply(simp)
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp)
-apply(case_tac "findn \<theta>n name3")
+apply(case_tac "findn \<theta>_n name3")
apply(simp)
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "name")
@@ -4113,10 +4113,10 @@
lemma psubst_fresh_name:
fixes x::"name"
- assumes a: "x\<sharp>\<theta>n" "x\<sharp>\<theta>c" "x\<sharp>M"
- shows "x\<sharp>\<theta>n,\<theta>c<M>"
+ assumes a: "x\<sharp>\<theta>_n" "x\<sharp>\<theta>_c" "x\<sharp>M"
+ shows "x\<sharp>\<theta>_n,\<theta>_c<M>"
using a
-apply(nominal_induct M avoiding: x \<theta>n \<theta>c rule: trm.strong_induct)
+apply(nominal_induct M avoiding: x \<theta>_n \<theta>_c rule: trm.strong_induct)
apply(simp add: lookup_freshness)
apply(auto simp add: abs_fresh)[1]
apply(simp add: lookupc_freshness)
@@ -4126,70 +4126,70 @@
apply(simp add: lookupd_freshness)
apply(simp add: lookupc_freshness)
apply(simp)
-apply(case_tac "findc \<theta>c coname")
+apply(case_tac "findc \<theta>_c coname")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
apply(simp)
-apply(case_tac "findn \<theta>n name")
+apply(case_tac "findn \<theta>_n name")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
apply(simp)
-apply(case_tac "findc \<theta>c coname3")
+apply(case_tac "findc \<theta>_c coname3")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
apply(simp)
-apply(case_tac "findn \<theta>n name3")
+apply(case_tac "findn \<theta>_n name3")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(auto simp add: abs_fresh abs_supp fin_supp)[1]
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp add: abs_fresh abs_supp fin_supp fresh_prod fresh_atm cmaps_fresh)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "name")
@@ -4199,10 +4199,10 @@
lemma psubst_fresh_coname:
fixes a::"coname"
- assumes a: "a\<sharp>\<theta>n" "a\<sharp>\<theta>c" "a\<sharp>M"
- shows "a\<sharp>\<theta>n,\<theta>c<M>"
+ assumes a: "a\<sharp>\<theta>_n" "a\<sharp>\<theta>_c" "a\<sharp>M"
+ shows "a\<sharp>\<theta>_n,\<theta>_c<M>"
using a
-apply(nominal_induct M avoiding: a \<theta>n \<theta>c rule: trm.strong_induct)
+apply(nominal_induct M avoiding: a \<theta>_n \<theta>_c rule: trm.strong_induct)
apply(simp add: lookup_freshness)
apply(auto simp add: abs_fresh)[1]
apply(simp add: lookupd_freshness)
@@ -4212,70 +4212,70 @@
apply(simp add: lookupc_freshness)
apply(simp add: lookupd_freshness)
apply(simp)
-apply(case_tac "findc \<theta>c coname")
+apply(case_tac "findc \<theta>_c coname")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
apply(simp)
-apply(case_tac "findn \<theta>n name")
+apply(case_tac "findn \<theta>_n name")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
apply(simp)
-apply(case_tac "findc \<theta>c coname3")
+apply(case_tac "findc \<theta>_c coname3")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
apply(simp)
-apply(case_tac "findn \<theta>n name3")
+apply(case_tac "findn \<theta>_n name3")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(auto simp add: abs_fresh abs_supp fin_supp)[1]
apply(auto)[1]
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(simp add: abs_fresh abs_supp fin_supp fresh_prod fresh_atm cmaps_fresh)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(auto simp add: abs_fresh)[1]
apply(auto)[1]
apply(generate_fresh "name")
@@ -4284,10 +4284,10 @@
done
lemma psubst_csubst:
- assumes a: "a\<sharp>(\<theta>n,\<theta>c)"
- shows "\<theta>n,((a,x,P)#\<theta>c)<M> = ((\<theta>n,\<theta>c<M>){a:=(x).P})"
+ assumes a: "a\<sharp>(\<theta>_n,\<theta>_c)"
+ shows "\<theta>_n,((a,x,P)#\<theta>_c)<M> = ((\<theta>_n,\<theta>_c<M>){a:=(x).P})"
using a
-apply(nominal_induct M avoiding: a x \<theta>n \<theta>c P rule: trm.strong_induct)
+apply(nominal_induct M avoiding: a x \<theta>_n \<theta>_c P rule: trm.strong_induct)
apply(auto simp add: fresh_list_cons fresh_prod)[1]
apply(simp add: lookup_csubst)
apply(simp add: fresh_list_cons fresh_prod)
@@ -4298,7 +4298,7 @@
apply(simp)
apply(simp add: abs_fresh fresh_atm)
apply(simp add: lookupd_fresh)
-apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>n")
+apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>_n")
apply(simp add: forget)
apply(simp add: trm.inject)
apply(rule sym)
@@ -4315,8 +4315,8 @@
apply(rule impI)
apply(simp add: lookupd_unicity)
apply(rule impI)
-apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>n")
-apply(subgoal_tac "a\<sharp>lookupd name aa \<theta>c")
+apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>_n")
+apply(subgoal_tac "a\<sharp>lookupd name aa \<theta>_c")
apply(simp add: forget)
apply(rule lookupd_freshness)
apply(simp add: fresh_atm)
@@ -4335,7 +4335,7 @@
apply(simp)
apply(blast)
apply(rule impI)
-apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>n")
+apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>_n")
apply(simp add: forget)
apply(rule lookupc_freshness)
apply(simp add: fresh_atm)
@@ -4362,7 +4362,7 @@
apply(rule impI)
apply(simp add: lookupd_unicity)
apply(rule impI)
-apply(subgoal_tac "a\<sharp>lookupd name aa \<theta>c")
+apply(subgoal_tac "a\<sharp>lookupd name aa \<theta>_c")
apply(simp add: forget)
apply(rule lookupd_freshness)
apply(simp add: fresh_atm)
@@ -4379,7 +4379,7 @@
apply(blast)
(* NotR *)
apply(simp)
-apply(case_tac "findc \<theta>c coname")
+apply(case_tac "findc \<theta>_c coname")
apply(simp)
apply(auto simp add: fresh_list_cons fresh_prod)[1]
apply(simp)
@@ -4398,7 +4398,7 @@
apply(auto simp add: fresh_prod fresh_atm)[1]
(* NotL *)
apply(simp)
-apply(case_tac "findn \<theta>n name")
+apply(case_tac "findn \<theta>_n name")
apply(simp)
apply(auto simp add: fresh_list_cons fresh_prod)[1]
apply(simp)
@@ -4417,7 +4417,7 @@
apply(simp)
(* AndR *)
apply(simp)
-apply(case_tac "findc \<theta>c coname3")
+apply(case_tac "findc \<theta>_c coname3")
apply(simp)
apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
apply(simp)
@@ -4436,7 +4436,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* AndL1 *)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(simp)
apply(auto simp add: fresh_list_cons fresh_prod)[1]
apply(simp)
@@ -4455,7 +4455,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* AndL2 *)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(simp)
apply(auto simp add: fresh_list_cons fresh_prod)[1]
apply(simp)
@@ -4474,7 +4474,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* OrR1 *)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(simp)
apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
apply(simp)
@@ -4493,7 +4493,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* OrR2 *)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(simp)
apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
apply(simp)
@@ -4512,7 +4512,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* OrL *)
apply(simp)
-apply(case_tac "findn \<theta>n name3")
+apply(case_tac "findn \<theta>_n name3")
apply(simp)
apply(auto simp add: fresh_list_cons psubst_fresh_name fresh_atm fresh_prod)[1]
apply(simp)
@@ -4531,7 +4531,7 @@
apply(auto simp add: psubst_fresh_name fresh_prod fresh_atm)[1]
(* ImpR *)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(simp)
apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
apply(simp)
@@ -4550,7 +4550,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* ImpL *)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(simp)
apply(auto simp add: fresh_list_cons psubst_fresh_coname psubst_fresh_name fresh_atm fresh_prod)[1]
apply(simp)
@@ -4571,10 +4571,10 @@
done
lemma psubst_nsubst:
- assumes a: "x\<sharp>(\<theta>n,\<theta>c)"
- shows "((x,a,P)#\<theta>n),\<theta>c<M> = ((\<theta>n,\<theta>c<M>){x:=<a>.P})"
+ assumes a: "x\<sharp>(\<theta>_n,\<theta>_c)"
+ shows "((x,a,P)#\<theta>_n),\<theta>_c<M> = ((\<theta>_n,\<theta>_c<M>){x:=<a>.P})"
using a
-apply(nominal_induct M avoiding: a x \<theta>n \<theta>c P rule: trm.strong_induct)
+apply(nominal_induct M avoiding: a x \<theta>_n \<theta>_c P rule: trm.strong_induct)
apply(auto simp add: fresh_list_cons fresh_prod)[1]
apply(simp add: lookup_fresh)
apply(rule lookupb_lookupa)
@@ -4591,7 +4591,7 @@
apply(simp add: abs_fresh)
apply(simp add: abs_fresh fresh_atm)
apply(simp add: lookupd_fresh)
-apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>c")
+apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>_c")
apply(simp add: forget)
apply(simp add: trm.inject)
apply(rule sym)
@@ -4608,8 +4608,8 @@
apply(rule impI)
apply(simp add: lookupc_unicity)
apply(rule impI)
-apply(subgoal_tac "x\<sharp>lookupc xa coname \<theta>n")
-apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>c")
+apply(subgoal_tac "x\<sharp>lookupc xa coname \<theta>_n")
+apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>_c")
apply(simp add: forget)
apply(rule lookupd_freshness)
apply(simp add: fresh_atm)
@@ -4638,7 +4638,7 @@
apply(rule impI)
apply(simp add: lookupc_unicity)
apply(rule impI)
-apply(subgoal_tac "x\<sharp>lookupc xa coname \<theta>n")
+apply(subgoal_tac "x\<sharp>lookupc xa coname \<theta>_n")
apply(simp add: forget)
apply(rule lookupc_freshness)
apply(simp add: fresh_prod fresh_atm)
@@ -4656,7 +4656,7 @@
apply(simp)
apply(blast)
apply(rule impI)
-apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>c")
+apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>_c")
apply(simp add: forget)
apply(rule lookupd_freshness)
apply(simp add: fresh_atm)
@@ -4673,7 +4673,7 @@
apply(blast)
(* NotR *)
apply(simp)
-apply(case_tac "findc \<theta>c coname")
+apply(case_tac "findc \<theta>_c coname")
apply(simp)
apply(auto simp add: fresh_list_cons fresh_prod)[1]
apply(simp)
@@ -4690,7 +4690,7 @@
apply(simp)
(* NotL *)
apply(simp)
-apply(case_tac "findn \<theta>n name")
+apply(case_tac "findn \<theta>_n name")
apply(simp)
apply(auto simp add: fresh_list_cons fresh_prod)[1]
apply(simp)
@@ -4709,7 +4709,7 @@
apply(simp add: fresh_prod fresh_atm)
(* AndR *)
apply(simp)
-apply(case_tac "findc \<theta>c coname3")
+apply(case_tac "findc \<theta>_c coname3")
apply(simp)
apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
apply(simp)
@@ -4726,7 +4726,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* AndL1 *)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(simp)
apply(auto simp add: fresh_list_cons fresh_prod)[1]
apply(simp)
@@ -4745,7 +4745,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* AndL2 *)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(simp)
apply(auto simp add: fresh_list_cons fresh_prod)[1]
apply(simp)
@@ -4764,7 +4764,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* OrR1 *)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(simp)
apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
apply(simp)
@@ -4781,7 +4781,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* OrR2 *)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(simp)
apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
apply(simp)
@@ -4798,7 +4798,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* OrL *)
apply(simp)
-apply(case_tac "findn \<theta>n name3")
+apply(case_tac "findn \<theta>_n name3")
apply(simp)
apply(auto simp add: fresh_list_cons psubst_fresh_name fresh_atm fresh_prod)[1]
apply(simp)
@@ -4817,7 +4817,7 @@
apply(auto simp add: psubst_fresh_name fresh_prod fresh_atm)[1]
(* ImpR *)
apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
apply(simp)
apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
apply(simp)
@@ -4834,7 +4834,7 @@
apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1]
(* ImpL *)
apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
apply(simp)
apply(auto simp add: fresh_list_cons psubst_fresh_coname psubst_fresh_name fresh_atm fresh_prod)[1]
apply(simp)
@@ -4856,35 +4856,35 @@
definition
ncloses :: "(name\<times>coname\<times>trm) list\<Rightarrow>(name\<times>ty) list \<Rightarrow> bool" ("_ ncloses _" [55,55] 55)
where
- "\<theta>n ncloses \<Gamma> \<equiv> \<forall>x B. ((x,B) \<in> set \<Gamma> \<longrightarrow> (\<exists>c P. \<theta>n nmaps x to Some (c,P) \<and> <c>:P \<in> (\<parallel><B>\<parallel>)))"
+ "\<theta>_n ncloses \<Gamma> \<equiv> \<forall>x B. ((x,B) \<in> set \<Gamma> \<longrightarrow> (\<exists>c P. \<theta>_n nmaps x to Some (c,P) \<and> <c>:P \<in> (\<parallel><B>\<parallel>)))"
definition
ccloses :: "(coname\<times>name\<times>trm) list\<Rightarrow>(coname\<times>ty) list \<Rightarrow> bool" ("_ ccloses _" [55,55] 55)
where
- "\<theta>c ccloses \<Delta> \<equiv> \<forall>a B. ((a,B) \<in> set \<Delta> \<longrightarrow> (\<exists>x P. \<theta>c cmaps a to Some (x,P) \<and> (x):P \<in> (\<parallel>(B)\<parallel>)))"
+ "\<theta>_c ccloses \<Delta> \<equiv> \<forall>a B. ((a,B) \<in> set \<Delta> \<longrightarrow> (\<exists>x P. \<theta>_c cmaps a to Some (x,P) \<and> (x):P \<in> (\<parallel>(B)\<parallel>)))"
lemma ncloses_elim:
assumes a: "(x,B) \<in> set \<Gamma>"
- and b: "\<theta>n ncloses \<Gamma>"
- shows "\<exists>c P. \<theta>n nmaps x to Some (c,P) \<and> <c>:P \<in> (\<parallel><B>\<parallel>)"
+ and b: "\<theta>_n ncloses \<Gamma>"
+ shows "\<exists>c P. \<theta>_n nmaps x to Some (c,P) \<and> <c>:P \<in> (\<parallel><B>\<parallel>)"
using a b by (auto simp add: ncloses_def)
lemma ccloses_elim:
assumes a: "(a,B) \<in> set \<Delta>"
- and b: "\<theta>c ccloses \<Delta>"
- shows "\<exists>x P. \<theta>c cmaps a to Some (x,P) \<and> (x):P \<in> (\<parallel>(B)\<parallel>)"
+ and b: "\<theta>_c ccloses \<Delta>"
+ shows "\<exists>x P. \<theta>_c cmaps a to Some (x,P) \<and> (x):P \<in> (\<parallel>(B)\<parallel>)"
using a b by (auto simp add: ccloses_def)
lemma ncloses_subset:
- assumes a: "\<theta>n ncloses \<Gamma>"
+ assumes a: "\<theta>_n ncloses \<Gamma>"
and b: "set \<Gamma>' \<subseteq> set \<Gamma>"
- shows "\<theta>n ncloses \<Gamma>'"
+ shows "\<theta>_n ncloses \<Gamma>'"
using a b by (auto simp add: ncloses_def)
lemma ccloses_subset:
- assumes a: "\<theta>c ccloses \<Delta>"
+ assumes a: "\<theta>_c ccloses \<Delta>"
and b: "set \<Delta>' \<subseteq> set \<Delta>"
- shows "\<theta>c ccloses \<Delta>'"
+ shows "\<theta>_c ccloses \<Delta>'"
using a b by (auto simp add: ccloses_def)
lemma validc_fresh:
@@ -4908,8 +4908,8 @@
done
lemma ccloses_extend:
- assumes a: "\<theta>c ccloses \<Delta>" "a\<sharp>\<Delta>" "a\<sharp>\<theta>c" "(x):P\<in>\<parallel>(B)\<parallel>"
- shows "(a,x,P)#\<theta>c ccloses (a,B)#\<Delta>"
+ assumes a: "\<theta>_c ccloses \<Delta>" "a\<sharp>\<Delta>" "a\<sharp>\<theta>_c" "(x):P\<in>\<parallel>(B)\<parallel>"
+ shows "(a,x,P)#\<theta>_c ccloses (a,B)#\<Delta>"
using a
apply(simp add: ccloses_def)
apply(drule validc_fresh)
@@ -4917,8 +4917,8 @@
done
lemma ncloses_extend:
- assumes a: "\<theta>n ncloses \<Gamma>" "x\<sharp>\<Gamma>" "x\<sharp>\<theta>n" "<a>:P\<in>\<parallel><B>\<parallel>"
- shows "(x,a,P)#\<theta>n ncloses (x,B)#\<Gamma>"
+ assumes a: "\<theta>_n ncloses \<Gamma>" "x\<sharp>\<Gamma>" "x\<sharp>\<theta>_n" "<a>:P\<in>\<parallel><B>\<parallel>"
+ shows "(x,a,P)#\<theta>_n ncloses (x,B)#\<Gamma>"
using a
apply(simp add: ncloses_def)
apply(drule validn_fresh)
@@ -5082,39 +5082,39 @@
done
lemma psubst_Ax_aux:
- assumes a: "\<theta>c cmaps a to Some (y,N)"
- shows "lookupb x a \<theta>c c P = Cut <c>.P (y).N"
+ assumes a: "\<theta>_c cmaps a to Some (y,N)"
+ shows "lookupb x a \<theta>_c c P = Cut <c>.P (y).N"
using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
apply(auto)
done
lemma psubst_Ax:
- assumes a: "\<theta>n nmaps x to Some (c,P)"
- and b: "\<theta>c cmaps a to Some (y,N)"
- shows "\<theta>n,\<theta>c<Ax x a> = Cut <c>.P (y).N"
+ assumes a: "\<theta>_n nmaps x to Some (c,P)"
+ and b: "\<theta>_c cmaps a to Some (y,N)"
+ shows "\<theta>_n,\<theta>_c<Ax x a> = Cut <c>.P (y).N"
using a b
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
apply(auto simp add: psubst_Ax_aux)
done
lemma psubst_Cut:
assumes a: "\<forall>x. M\<noteq>Ax x c"
and b: "\<forall>a. N\<noteq>Ax x a"
- and c: "c\<sharp>(\<theta>n,\<theta>c,N)" "x\<sharp>(\<theta>n,\<theta>c,M)"
- shows "\<theta>n,\<theta>c<Cut <c>.M (x).N> = Cut <c>.(\<theta>n,\<theta>c<M>) (x).(\<theta>n,\<theta>c<N>)"
+ and c: "c\<sharp>(\<theta>_n,\<theta>_c,N)" "x\<sharp>(\<theta>_n,\<theta>_c,M)"
+ shows "\<theta>_n,\<theta>_c<Cut <c>.M (x).N> = Cut <c>.(\<theta>_n,\<theta>_c<M>) (x).(\<theta>_n,\<theta>_c<N>)"
using a b c
apply(simp)
done
lemma all_CAND:
assumes a: "\<Gamma> \<turnstile> M \<turnstile> \<Delta>"
- and b: "\<theta>n ncloses \<Gamma>"
- and c: "\<theta>c ccloses \<Delta>"
- shows "SNa (\<theta>n,\<theta>c<M>)"
+ and b: "\<theta>_n ncloses \<Gamma>"
+ and c: "\<theta>_c ccloses \<Delta>"
+ shows "SNa (\<theta>_n,\<theta>_c<M>)"
using a b c
-proof(nominal_induct avoiding: \<theta>n \<theta>c rule: typing.strong_induct)
- case (TAx \<Gamma> \<Delta> x B a \<theta>n \<theta>c)
+proof(nominal_induct avoiding: \<theta>_n \<theta>_c rule: typing.strong_induct)
+ case (TAx \<Gamma> \<Delta> x B a \<theta>_n \<theta>_c)
then show ?case
apply -
apply(drule ncloses_elim)
@@ -5123,13 +5123,13 @@
apply(assumption)
apply(erule exE)+
apply(erule conjE)+
- apply(rule_tac s="Cut <c>.P (xa).Pa" and t="\<theta>n,\<theta>c<Ax x a>" in subst)
+ apply(rule_tac s="Cut <c>.P (xa).Pa" and t="\<theta>_n,\<theta>_c<Ax x a>" in subst)
apply(rule sym)
apply(simp only: psubst_Ax)
apply(simp add: CUT_SNa)
done
next
- case (TNotR x \<Gamma> B M \<Delta> \<Delta>' a \<theta>n \<theta>c)
+ case (TNotR x \<Gamma> B M \<Delta> \<Delta>' a \<theta>_n \<theta>_c)
then show ?case
apply(simp)
apply(subgoal_tac "(a,NOT B) \<in> set \<Delta>'")
@@ -5145,7 +5145,7 @@
apply(rule disjI2)
apply(rule_tac x="c" in exI)
apply(rule_tac x="x" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp)
apply(rule conjI)
apply(rule fic.intros)
@@ -5157,13 +5157,13 @@
apply(unfold BINDINGn_def)
apply(simp)
apply(rule_tac x="x" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp)
apply(rule allI)+
apply(rule impI)
apply(simp add: psubst_nsubst[symmetric])
- apply(drule_tac x="(x,aa,Pa)#\<theta>n" in meta_spec)
- apply(drule_tac x="\<theta>c" in meta_spec)
+ apply(drule_tac x="(x,aa,Pa)#\<theta>_n" in meta_spec)
+ apply(drule_tac x="\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_extend)
apply(assumption)
@@ -5179,7 +5179,7 @@
apply(blast)
done
next
- case (TNotL a \<Delta> \<Gamma> M B \<Gamma>' x \<theta>n \<theta>c)
+ case (TNotL a \<Delta> \<Gamma> M B \<Gamma>' x \<theta>_n \<theta>_c)
then show ?case
apply(simp)
apply(subgoal_tac "(x,NOT B) \<in> set \<Gamma>'")
@@ -5197,7 +5197,7 @@
apply(rule disjI2)
apply(rule_tac x="a" in exI)
apply(rule_tac x="ca" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp del: NEGc.simps)
apply(rule conjI)
apply(rule fin.intros)
@@ -5209,13 +5209,13 @@
apply(unfold BINDINGc_def)
apply(simp (no_asm))
apply(rule_tac x="a" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp (no_asm))
apply(rule allI)+
apply(rule impI)
apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
- apply(drule_tac x="\<theta>n" in meta_spec)
- apply(drule_tac x="(a,xa,Pa)#\<theta>c" in meta_spec)
+ apply(drule_tac x="\<theta>_n" in meta_spec)
+ apply(drule_tac x="(a,xa,Pa)#\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_subset)
apply(assumption)
@@ -5230,7 +5230,7 @@
apply(blast)
done
next
- case (TAndL1 x \<Gamma> y B1 M \<Delta> \<Gamma>' B2 \<theta>n \<theta>c)
+ case (TAndL1 x \<Gamma> y B1 M \<Delta> \<Gamma>' B2 \<theta>_n \<theta>_c)
then show ?case
apply(simp)
apply(subgoal_tac "(y,B1 AND B2) \<in> set \<Gamma>'")
@@ -5249,7 +5249,7 @@
apply(rule disjI1)
apply(rule_tac x="x" in exI)
apply(rule_tac x="ca" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp del: NEGc.simps)
apply(rule conjI)
apply(rule fin.intros)
@@ -5262,13 +5262,13 @@
apply(unfold BINDINGn_def)
apply(simp (no_asm))
apply(rule_tac x="x" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp (no_asm))
apply(rule allI)+
apply(rule impI)
apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
- apply(drule_tac x="(x,a,Pa)#\<theta>n" in meta_spec)
- apply(drule_tac x="\<theta>c" in meta_spec)
+ apply(drule_tac x="(x,a,Pa)#\<theta>_n" in meta_spec)
+ apply(drule_tac x="\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_extend)
apply(rule ncloses_subset)
@@ -5283,7 +5283,7 @@
apply(blast)
done
next
- case (TAndL2 x \<Gamma> y B2 M \<Delta> \<Gamma>' B1 \<theta>n \<theta>c)
+ case (TAndL2 x \<Gamma> y B2 M \<Delta> \<Gamma>' B1 \<theta>_n \<theta>_c)
then show ?case
apply(simp)
apply(subgoal_tac "(y,B1 AND B2) \<in> set \<Gamma>'")
@@ -5302,7 +5302,7 @@
apply(rule disjI2)
apply(rule_tac x="x" in exI)
apply(rule_tac x="ca" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp del: NEGc.simps)
apply(rule conjI)
apply(rule fin.intros)
@@ -5315,13 +5315,13 @@
apply(unfold BINDINGn_def)
apply(simp (no_asm))
apply(rule_tac x="x" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp (no_asm))
apply(rule allI)+
apply(rule impI)
apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
- apply(drule_tac x="(x,a,Pa)#\<theta>n" in meta_spec)
- apply(drule_tac x="\<theta>c" in meta_spec)
+ apply(drule_tac x="(x,a,Pa)#\<theta>_n" in meta_spec)
+ apply(drule_tac x="\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_extend)
apply(rule ncloses_subset)
@@ -5336,7 +5336,7 @@
apply(blast)
done
next
- case (TAndR a \<Delta> N c b M \<Gamma> B C \<Delta>' \<theta>n \<theta>c)
+ case (TAndR a \<Delta> N c b M \<Gamma> B C \<Delta>' \<theta>_n \<theta>_c)
then show ?case
apply(simp)
apply(subgoal_tac "(c,B AND C) \<in> set \<Delta>'")
@@ -5353,8 +5353,8 @@
apply(rule_tac x="ca" in exI)
apply(rule_tac x="a" in exI)
apply(rule_tac x="b" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
apply(simp)
apply(rule conjI)
apply(rule fic.intros)
@@ -5373,13 +5373,13 @@
apply(unfold BINDINGc_def)
apply(simp)
apply(rule_tac x="a" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp)
apply(rule allI)+
apply(rule impI)
apply(simp add: psubst_csubst[symmetric])
- apply(drule_tac x="\<theta>n" in meta_spec)
- apply(drule_tac x="(a,xa,Pa)#\<theta>c" in meta_spec)
+ apply(drule_tac x="\<theta>_n" in meta_spec)
+ apply(drule_tac x="(a,xa,Pa)#\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(assumption)
apply(drule meta_mp)
@@ -5395,14 +5395,14 @@
apply(unfold BINDINGc_def)
apply(simp)
apply(rule_tac x="b" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
apply(simp)
apply(rule allI)+
apply(rule impI)
apply(simp add: psubst_csubst[symmetric])
apply(rotate_tac 14)
- apply(drule_tac x="\<theta>n" in meta_spec)
- apply(drule_tac x="(b,xa,Pa)#\<theta>c" in meta_spec)
+ apply(drule_tac x="\<theta>_n" in meta_spec)
+ apply(drule_tac x="(b,xa,Pa)#\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(assumption)
apply(drule meta_mp)
@@ -5418,7 +5418,7 @@
apply(blast)
done
next
- case (TOrL x \<Gamma> N z y M B \<Delta> C \<Gamma>' \<theta>n \<theta>c)
+ case (TOrL x \<Gamma> N z y M B \<Delta> C \<Gamma>' \<theta>_n \<theta>_c)
then show ?case
apply(simp)
apply(subgoal_tac "(z,B OR C) \<in> set \<Gamma>'")
@@ -5437,8 +5437,8 @@
apply(rule_tac x="x" in exI)
apply(rule_tac x="y" in exI)
apply(rule_tac x="ca" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
apply(simp del: NEGc.simps)
apply(rule conjI)
apply(rule fin.intros)
@@ -5457,13 +5457,13 @@
apply(unfold BINDINGn_def)
apply(simp del: NEGc.simps)
apply(rule_tac x="x" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp del: NEGc.simps)
apply(rule allI)+
apply(rule impI)
apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
- apply(drule_tac x="(x,a,Pa)#\<theta>n" in meta_spec)
- apply(drule_tac x="\<theta>c" in meta_spec)
+ apply(drule_tac x="(x,a,Pa)#\<theta>_n" in meta_spec)
+ apply(drule_tac x="\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_extend)
apply(rule ncloses_subset)
@@ -5479,14 +5479,14 @@
apply(unfold BINDINGn_def)
apply(simp del: NEGc.simps)
apply(rule_tac x="y" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
apply(simp del: NEGc.simps)
apply(rule allI)+
apply(rule impI)
apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
apply(rotate_tac 14)
- apply(drule_tac x="(y,a,Pa)#\<theta>n" in meta_spec)
- apply(drule_tac x="\<theta>c" in meta_spec)
+ apply(drule_tac x="(y,a,Pa)#\<theta>_n" in meta_spec)
+ apply(drule_tac x="\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_extend)
apply(rule ncloses_subset)
@@ -5501,7 +5501,7 @@
apply(blast)
done
next
- case (TOrR1 a \<Delta> b \<Gamma> M B1 \<Delta>' B2 \<theta>n \<theta>c)
+ case (TOrR1 a \<Delta> b \<Gamma> M B1 \<Delta>' B2 \<theta>_n \<theta>_c)
then show ?case
apply(simp)
apply(subgoal_tac "(b,B1 OR B2) \<in> set \<Delta>'")
@@ -5518,7 +5518,7 @@
apply(rule disjI1)
apply(rule_tac x="a" in exI)
apply(rule_tac x="c" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp)
apply(rule conjI)
apply(rule fic.intros)
@@ -5531,13 +5531,13 @@
apply(unfold BINDINGc_def)
apply(simp (no_asm))
apply(rule_tac x="a" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp (no_asm))
apply(rule allI)+
apply(rule impI)
apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
- apply(drule_tac x="\<theta>n" in meta_spec)
- apply(drule_tac x="(a,xa,Pa)#\<theta>c" in meta_spec)
+ apply(drule_tac x="\<theta>_n" in meta_spec)
+ apply(drule_tac x="(a,xa,Pa)#\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(assumption)
apply(drule meta_mp)
@@ -5553,7 +5553,7 @@
apply(blast)
done
next
- case (TOrR2 a \<Delta> b \<Gamma> M B2 \<Delta>' B1 \<theta>n \<theta>c)
+ case (TOrR2 a \<Delta> b \<Gamma> M B2 \<Delta>' B1 \<theta>_n \<theta>_c)
then show ?case
apply(simp)
apply(subgoal_tac "(b,B1 OR B2) \<in> set \<Delta>'")
@@ -5570,7 +5570,7 @@
apply(rule disjI2)
apply(rule_tac x="a" in exI)
apply(rule_tac x="c" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp)
apply(rule conjI)
apply(rule fic.intros)
@@ -5583,13 +5583,13 @@
apply(unfold BINDINGc_def)
apply(simp (no_asm))
apply(rule_tac x="a" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp (no_asm))
apply(rule allI)+
apply(rule impI)
apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
- apply(drule_tac x="\<theta>n" in meta_spec)
- apply(drule_tac x="(a,xa,Pa)#\<theta>c" in meta_spec)
+ apply(drule_tac x="\<theta>_n" in meta_spec)
+ apply(drule_tac x="(a,xa,Pa)#\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(assumption)
apply(drule meta_mp)
@@ -5605,7 +5605,7 @@
apply(blast)
done
next
- case (TImpL a \<Delta> N x \<Gamma> M y B C \<Gamma>' \<theta>n \<theta>c)
+ case (TImpL a \<Delta> N x \<Gamma> M y B C \<Gamma>' \<theta>_n \<theta>_c)
then show ?case
apply(simp)
apply(subgoal_tac "(y,B IMP C) \<in> set \<Gamma>'")
@@ -5624,8 +5624,8 @@
apply(rule_tac x="x" in exI)
apply(rule_tac x="a" in exI)
apply(rule_tac x="ca" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
apply(simp del: NEGc.simps)
apply(rule conjI)
apply(rule fin.intros)
@@ -5643,13 +5643,13 @@
apply(unfold BINDINGc_def)
apply(simp del: NEGc.simps)
apply(rule_tac x="a" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp del: NEGc.simps)
apply(rule allI)+
apply(rule impI)
apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
- apply(drule_tac x="\<theta>n" in meta_spec)
- apply(drule_tac x="(a,xa,Pa)#\<theta>c" in meta_spec)
+ apply(drule_tac x="\<theta>_n" in meta_spec)
+ apply(drule_tac x="(a,xa,Pa)#\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_subset)
apply(assumption)
@@ -5665,14 +5665,14 @@
apply(unfold BINDINGn_def)
apply(simp del: NEGc.simps)
apply(rule_tac x="x" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
apply(simp del: NEGc.simps)
apply(rule allI)+
apply(rule impI)
apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
apply(rotate_tac 12)
- apply(drule_tac x="(x,aa,Pa)#\<theta>n" in meta_spec)
- apply(drule_tac x="\<theta>c" in meta_spec)
+ apply(drule_tac x="(x,aa,Pa)#\<theta>_n" in meta_spec)
+ apply(drule_tac x="\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_extend)
apply(rule ncloses_subset)
@@ -5687,7 +5687,7 @@
apply(blast)
done
next
- case (TImpR a \<Delta> b x \<Gamma> B M C \<Delta>' \<theta>n \<theta>c)
+ case (TImpR a \<Delta> b x \<Gamma> B M C \<Delta>' \<theta>_n \<theta>_c)
then show ?case
apply(simp)
apply(subgoal_tac "(b,B IMP C) \<in> set \<Delta>'")
@@ -5704,7 +5704,7 @@
apply(rule_tac x="x" in exI)
apply(rule_tac x="a" in exI)
apply(rule_tac x="c" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp)
apply(rule conjI)
apply(rule fic.intros)
@@ -5721,16 +5721,16 @@
apply(unfold BINDINGn_def)
apply(simp)
apply(rule_tac x="x" in exI)
- apply(rule_tac x="\<theta>n,((a,z,Pa)#\<theta>c)<M>" in exI)
+ apply(rule_tac x="\<theta>_n,((a,z,Pa)#\<theta>_c)<M>" in exI)
apply(simp)
apply(rule allI)+
apply(rule impI)
- apply(rule_tac t="\<theta>n,((a,z,Pa)#\<theta>c)<M>{x:=<aa>.Pb}" and
- s="((x,aa,Pb)#\<theta>n),((a,z,Pa)#\<theta>c)<M>" in subst)
+ apply(rule_tac t="\<theta>_n,((a,z,Pa)#\<theta>_c)<M>{x:=<aa>.Pb}" and
+ s="((x,aa,Pb)#\<theta>_n),((a,z,Pa)#\<theta>_c)<M>" in subst)
apply(rule psubst_nsubst)
apply(simp add: fresh_prod fresh_atm fresh_list_cons)
- apply(drule_tac x="(x,aa,Pb)#\<theta>n" in meta_spec)
- apply(drule_tac x="(a,z,Pa)#\<theta>c" in meta_spec)
+ apply(drule_tac x="(x,aa,Pb)#\<theta>_n" in meta_spec)
+ apply(drule_tac x="(a,z,Pa)#\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_extend)
apply(assumption)
@@ -5753,16 +5753,16 @@
apply(unfold BINDINGc_def)
apply(simp)
apply(rule_tac x="a" in exI)
- apply(rule_tac x="((x,ca,Q)#\<theta>n),\<theta>c<M>" in exI)
+ apply(rule_tac x="((x,ca,Q)#\<theta>_n),\<theta>_c<M>" in exI)
apply(simp)
apply(rule allI)+
apply(rule impI)
- apply(rule_tac t="((x,ca,Q)#\<theta>n),\<theta>c<M>{a:=(xaa).Pa}" and
- s="((x,ca,Q)#\<theta>n),((a,xaa,Pa)#\<theta>c)<M>" in subst)
+ apply(rule_tac t="((x,ca,Q)#\<theta>_n),\<theta>_c<M>{a:=(xaa).Pa}" and
+ s="((x,ca,Q)#\<theta>_n),((a,xaa,Pa)#\<theta>_c)<M>" in subst)
apply(rule psubst_csubst)
apply(simp add: fresh_prod fresh_atm fresh_list_cons)
- apply(drule_tac x="(x,ca,Q)#\<theta>n" in meta_spec)
- apply(drule_tac x="(a,xaa,Pa)#\<theta>c" in meta_spec)
+ apply(drule_tac x="(x,ca,Q)#\<theta>_n" in meta_spec)
+ apply(drule_tac x="(a,xaa,Pa)#\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_extend)
apply(assumption)
@@ -5782,7 +5782,7 @@
apply(blast)
done
next
- case (TCut a \<Delta> N x \<Gamma> M B \<theta>n \<theta>c)
+ case (TCut a \<Delta> N x \<Gamma> M B \<theta>_n \<theta>_c)
then show ?case
apply -
apply(case_tac "\<forall>y. M\<noteq>Ax y a")
@@ -5793,14 +5793,14 @@
apply(unfold BINDINGc_def)
apply(simp)
apply(rule_tac x="a" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp)
apply(rule allI)
apply(rule allI)
apply(rule impI)
apply(simp add: psubst_csubst[symmetric]) (*?*)
- apply(drule_tac x="\<theta>n" in meta_spec)
- apply(drule_tac x="(a,xa,P)#\<theta>c" in meta_spec)
+ apply(drule_tac x="\<theta>_n" in meta_spec)
+ apply(drule_tac x="(a,xa,P)#\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(assumption)
apply(drule meta_mp)
@@ -5814,15 +5814,15 @@
apply(unfold BINDINGn_def)
apply(simp)
apply(rule_tac x="x" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
apply(simp)
apply(rule allI)
apply(rule allI)
apply(rule impI)
apply(simp add: psubst_nsubst[symmetric]) (*?*)
apply(rotate_tac 11)
- apply(drule_tac x="(x,aa,P)#\<theta>n" in meta_spec)
- apply(drule_tac x="\<theta>c" in meta_spec)
+ apply(drule_tac x="(x,aa,P)#\<theta>_n" in meta_spec)
+ apply(drule_tac x="\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_extend)
apply(assumption)
@@ -5844,12 +5844,12 @@
apply(unfold BINDINGc_def)
apply(simp)
apply(rule_tac x="a" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
apply(simp)
apply(rule allI)+
apply(rule impI)
- apply(drule_tac x="\<theta>n" in meta_spec)
- apply(drule_tac x="(a,xa,P)#\<theta>c" in meta_spec)
+ apply(drule_tac x="\<theta>_n" in meta_spec)
+ apply(drule_tac x="(a,xa,P)#\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(assumption)
apply(drule meta_mp)
@@ -5935,15 +5935,15 @@
apply(unfold BINDINGn_def)
apply(simp)
apply(rule_tac x="x" in exI)
- apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+ apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
apply(simp)
apply(rule allI)
apply(rule allI)
apply(rule impI)
apply(simp add: psubst_nsubst[symmetric]) (*?*)
apply(rotate_tac 10)
- apply(drule_tac x="(x,aa,P)#\<theta>n" in meta_spec)
- apply(drule_tac x="\<theta>c" in meta_spec)
+ apply(drule_tac x="(x,aa,P)#\<theta>_n" in meta_spec)
+ apply(drule_tac x="\<theta>_c" in meta_spec)
apply(drule meta_mp)
apply(rule ncloses_extend)
apply(assumption)
@@ -6038,7 +6038,7 @@
lemma lookup1:
assumes a: "x\<sharp>(idn \<Gamma> b)"
- shows "lookup x a (idn \<Gamma> b) \<theta>c = lookupa x a \<theta>c"
+ shows "lookup x a (idn \<Gamma> b) \<theta>_c = lookupa x a \<theta>_c"
using a
apply(induct \<Gamma>)
apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
@@ -6046,7 +6046,7 @@
lemma lookup2:
assumes a: "\<not>(x\<sharp>(idn \<Gamma> b))"
- shows "lookup x a (idn \<Gamma> b) \<theta>c = lookupb x a \<theta>c b (Ax x b)"
+ shows "lookup x a (idn \<Gamma> b) \<theta>_c = lookupb x a \<theta>_c b (Ax x b)"
using a
apply(induct \<Gamma>)
apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil)