Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Test.thy
changeset 1498 2ff84b1f551f
parent 1496 fd483d8f486b
child 1499 21dda372fb11 
--- a/Nominal/Test.thy	Thu Mar 18 08:03:42 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 18 08:32:55 2010 +0100
@@ -43,7 +43,7 @@
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(simp only: supp_def[symmetric])
-apply(rule_tac t="supp (Lm name lm_raw)" and s="supp (Abs {atom name} lm_raw)" in subst)
+apply(rule_tac t="supp (Lm name lm)" and s="supp (Abs {atom name} lm)" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lm_perm)
 apply(simp only: permute_ABS)
@@ -68,8 +68,8 @@
 lemma
   assumes a0: "finite (supp c)"
   and     a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm_raw1 lm_raw2 c. \<lbrakk>\<And>d. P d lm_raw1; \<And>d. P d lm_raw2\<rbrakk> \<Longrightarrow> P c (Ap lm_raw1 lm_raw2)"
-  and     a3: "\<And>name lm_raw c. \<lbrakk>\<And>d. P d lm_raw\<rbrakk> \<Longrightarrow> P c (Lm name lm_raw)"
+  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
+  and     a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
   shows "P c lm"
 proof -
   have "\<And>p c. P c (p \<bullet> lm)"
@@ -80,11 +80,11 @@
     apply(rule a2)
     apply(assumption)
     apply(assumption)
-    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm_raw)) 
+    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm)) 
                           \<and> sort_of (atom new) = sort_of (atom name)")
     apply(erule exE)
-    apply(rule_tac t="(p \<bullet> Lm name lm_raw)" and 
-                   s="((((atom (p \<bullet> name)) \<rightleftharpoons> (atom new)) + p) \<bullet> Lm name lm_raw)" in subst)
+    apply(rule_tac t="(p \<bullet> Lm name lm)" and 
+                   s="((((atom (p \<bullet> name)) \<rightleftharpoons> (atom new)) + p) \<bullet> Lm name lm)" in subst)
     apply(simp)
     apply(subst lm_perm)
     apply(subst (2) lm_perm)
@@ -150,7 +150,7 @@
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
-apply(rule_tac t="supp (LAM name lam_raw)" and s="supp (Abs {atom name} lam_raw)" in subst)
+apply(rule_tac t="supp (LAM name lam)" and s="supp (Abs {atom name} lam)" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
 apply(simp only: permute_ABS)
@@ -162,7 +162,7 @@
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 (* LET case *)
-apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \<union> fv_bi bp_raw" in subst)
+apply(rule_tac t="supp (LET bp lam)" and s="supp (Abs (bi bp) lam) \<union> fv_bi bp" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
 apply(simp only: permute_ABS)
@@ -239,7 +239,7 @@
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
-apply(rule_tac t="supp (LAM' name lam'_raw)" and s="supp (Abs {atom name} lam'_raw)" in subst)
+apply(rule_tac t="supp (LAM' name lam')" and s="supp (Abs {atom name} lam')" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam'_bp'_perm)
 apply(simp only: permute_ABS)
@@ -251,8 +251,8 @@
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 (* LET case *)
-apply(rule_tac t="supp (LET' bp'_raw lam'_raw)" and 
-               s="supp (Abs (bi' bp'_raw) (bp'_raw, lam'_raw))" in subst)
+apply(rule_tac t="supp (LET' bp' lam')" and 
+               s="supp (Abs (bi' bp') (bp', lam'))" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam'_bp'_perm)
 apply(simp only: permute_ABS)
@@ -325,7 +325,7 @@
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* LAM case *)
-apply(rule_tac t="supp (Lam name trm'_raw)" and s="supp (Abs {atom name} trm'_raw)" in subst)
+apply(rule_tac t="supp (Lam name trm')" and s="supp (Abs {atom name} trm')" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: trm'_pat'_perm)
 apply(simp only: permute_ABS)
@@ -337,8 +337,8 @@
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 (* LET case *)
-apply(rule_tac t="supp (Let pat'_raw trm'_raw1 trm'_raw2)" 
-           and s="supp (Abs (f pat'_raw) trm'_raw2) \<union> supp trm'_raw1 \<union> fv_f pat'_raw" in subst)
+apply(rule_tac t="supp (Let pat' trm'1 trm'2)" 
+           and s="supp (Abs (f pat') trm'2) \<union> supp trm'1 \<union> fv_f pat'" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: trm'_pat'_perm)
 apply(simp only: permute_ABS)
@@ -460,7 +460,7 @@
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* All case *)
-apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst)
+apply(rule_tac t="supp (All fun t)" and s="supp (Abs (atom ` fun) t)" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: t_tyS_perm)
 apply(simp only: permute_ABS)
nominal2