# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1283557178 -28800
# Node ID 894599a50af3c42dfb27970d76a2473ef80d4ec5
# Parent  bdb1eab471619cafc5d5005a98d750759e9755ef
got rid of Nominal2_Supp (is now in Nomina2_Base)

diff -r bdb1eab47161 -r 894599a50af3 Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Sat Sep 04 07:28:35 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(*  Title:      Nominal2_Supp
-    Authors:    Brian Huffman, Christian Urban
-
-    Supplementary Lemmas and Definitions for 
-    Nominal Isabelle. 
-*)
-theory Nominal2_Supp
-imports Nominal2_Base Nominal2_Eqvt 
-begin
-
-section {* Induction principle for permutations *}
-
-
-lemma perm_struct_induct[consumes 1, case_names zero swap]:
-  assumes S: "supp p \<subseteq> S"
-  and zero: "P 0"
-  and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
-  shows "P p"
-proof -
-  have "finite (supp p)" by (simp add: finite_supp)
-  then show "P p" using S
-  proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)
-    case (psubset p)
-    then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto
-    have as: "supp p \<subseteq> S" by fact
-    { assume "supp p = {}"
-      then have "p = 0" by (simp add: supp_perm expand_perm_eq)
-      then have "P p" using zero by simp
-    }
-    moreover
-    { assume "supp p \<noteq> {}"
-      then obtain a where a0: "a \<in> supp p" by blast
-      then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a"
-        using as by (auto simp add: supp_atom supp_perm swap_atom)
-      let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
-      have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
-      moreover
-      have "a \<notin> supp ?q" by (simp add: supp_perm)
-      then have "supp ?q \<noteq> supp p" using a0 by auto
-      ultimately have "supp ?q \<subset> supp p" using a2 by auto
-      then have "P ?q" using ih by simp
-      moreover
-      have "supp ?q \<subseteq> S" using as a2 by simp
-      ultimately  have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp 
-      moreover 
-      have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)
-      ultimately have "P p" by simp
-    }
-    ultimately show "P p" by blast
-  qed
-qed
-
-lemma perm_simple_struct_induct[case_names zero swap]:
-  assumes zero: "P 0"
-  and     swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
-  shows "P p"
-by (rule_tac S="supp p" in perm_struct_induct)
-   (auto intro: zero swap)
-
-lemma perm_subset_induct[consumes 1, case_names zero swap plus]:
-  assumes S: "supp p \<subseteq> S"
-  assumes zero: "P 0"
-  assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
-  assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
-  shows "P p"
-using S
-by (induct p rule: perm_struct_induct)
-   (auto intro: zero plus swap simp add: supp_swap)
-
-lemma supp_perm_eq:
-  assumes "(supp x) \<sharp>* p"
-  shows "p \<bullet> x = x"
-proof -
-  from assms have "supp p \<subseteq> {a. a \<sharp> x}"
-    unfolding supp_perm fresh_star_def fresh_def by auto
-  then show "p \<bullet> x = x"
-  proof (induct p rule: perm_struct_induct)
-    case zero
-    show "0 \<bullet> x = x" by simp
-  next
-    case (swap p a b)
-    then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all
-    then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)
-  qed
-qed
-
-lemma supp_perm_eq_test:
-  assumes "(supp x) \<sharp>* p"
-  shows "p \<bullet> x = x"
-proof -
-  from assms have "supp p \<subseteq> {a. a \<sharp> x}"
-    unfolding supp_perm fresh_star_def fresh_def by auto
-  then show "p \<bullet> x = x"
-  proof (induct p rule: perm_subset_induct)
-    case zero
-    show "0 \<bullet> x = x" by simp
-  next
-    case (swap a b)
-    then have "a \<sharp> x" "b \<sharp> x" by simp_all
-    then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
-  next
-    case (plus p1 p2)
-    have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+
-    then show "(p1 + p2) \<bullet> x = x" by simp
-  qed
-qed
-
-
-end
diff -r bdb1eab47161 -r 894599a50af3 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sat Sep 04 07:28:35 2010 +0800
+++ b/Nominal/Abs.thy	Sat Sep 04 07:39:38 2010 +0800
@@ -1,7 +1,6 @@
 theory Abs
 imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
-        "../Nominal-General/Nominal2_Supp" 
         "Quotient" 
         "Quotient_List"
         "Quotient_Product" 
diff -r bdb1eab47161 -r 894599a50af3 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sat Sep 04 07:28:35 2010 +0800
+++ b/Nominal/Nominal2.thy	Sat Sep 04 07:39:38 2010 +0800
@@ -2,7 +2,6 @@
 imports 
   "../Nominal-General/Nominal2_Base" 
   "../Nominal-General/Nominal2_Eqvt" 
-  "../Nominal-General/Nominal2_Supp" 
   "Nominal2_FSet"
   "Abs"
 uses ("nominal_dt_rawperm.ML")
diff -r bdb1eab47161 -r 894599a50af3 Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Sat Sep 04 07:28:35 2010 +0800
+++ b/Nominal/Nominal2_FSet.thy	Sat Sep 04 07:39:38 2010 +0800
@@ -1,6 +1,5 @@
 theory Nominal2_FSet
 imports "../Nominal-General/Nominal2_Base"
-        "../Nominal-General/Nominal2_Supp"
         "../Nominal-General/Nominal2_Eqvt" 
         FSet 
 begin
diff -r bdb1eab47161 -r 894599a50af3 Paper/Paper.thy
--- a/Paper/Paper.thy	Sat Sep 04 07:28:35 2010 +0800
+++ b/Paper/Paper.thy	Sat Sep 04 07:39:38 2010 +0800
@@ -21,21 +21,21 @@
   supp ("supp _" [78] 73) and
   uminus ("-_" [78] 73) and
   If  ("if _ then _ else _" 10) and
-  alpha_gen ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
+  alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
   alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
   alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
   fv ("fa'(_')" [100] 100) and
   equal ("=") and
-  alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
-  Abs ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
+  alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
+  Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
   Abs_lst ("[_]\<^bsub>list\<^esub>._") and
   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
   Abs_res ("[_]\<^bsub>res\<^esub>._") and
   Abs_print ("_\<^bsub>set\<^esub>._") and
   Cons ("_::_" [78,77] 73) and
-  supp_gen ("aux _" [1000] 10) and
+  supp_set ("aux _" [1000] 10) and
   alpha_bn ("_ \<approx>bn _")
 
 consts alpha_trm ::'a
@@ -647,7 +647,7 @@
   %
   \begin{equation}\label{alphaset}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
-  \multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+  \multicolumn{3}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
               & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
   @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
   @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
@@ -730,7 +730,7 @@
   types. For this we define 
   %
   \begin{equation}
-  @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
+  @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
   \end{equation}
   
   \noindent
@@ -762,7 +762,7 @@
   The elements in these types will be, respectively, written as:
 
   \begin{center}
-  @{term "Abs as x"} \hspace{5mm} 
+  @{term "Abs_set as x"} \hspace{5mm} 
   @{term "Abs_res as x"} \hspace{5mm}
   @{term "Abs_lst as x"} 
   \end{center}
@@ -832,7 +832,7 @@
   function @{text aux}, taking an abstraction as argument:
   %
   \begin{center}
-  @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
+  @{thm supp_set.simps[THEN eq_reflection, no_vars]}
   \end{center}
   
   \noindent
@@ -842,7 +842,7 @@
   This in turn means
   %
   \begin{center}
-  @{term "supp (supp_gen (Abs as x)) \<subseteq> supp (Abs as x)"}
+  @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
   \end{center}
 
   \noindent
@@ -860,7 +860,7 @@
   Theorem~\ref{suppabs}. 
 
   The method of first considering abstractions of the
-  form @{term "Abs as x"} etc is motivated by the fact that 
+  form @{term "Abs_set as x"} etc is motivated by the fact that 
   we can conveniently establish  at the Isabelle/HOL level
   properties about them.  It would be
   laborious to write custom ML-code that derives automatically such properties 
@@ -1489,7 +1489,7 @@
   lets us formally define the premise @{text P} for a non-empty binding clause as:
   %
   \begin{center}
-  \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>gen R fa p (B', D')"}}\;.
+  \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.
   \end{center}
 
   \noindent
diff -r bdb1eab47161 -r 894599a50af3 Pearl-jv/ROOT.ML
--- a/Pearl-jv/ROOT.ML	Sat Sep 04 07:28:35 2010 +0800
+++ b/Pearl-jv/ROOT.ML	Sat Sep 04 07:39:38 2010 +0800
@@ -1,7 +1,5 @@
 no_document use_thys ["../Nominal-General/Nominal2_Base", 
-                      "../Nominal-General/Nominal2_Atoms", 
                       "../Nominal-General/Nominal2_Eqvt",
-                      "../Nominal-General/Nominal2_Supp",
                       "../Nominal-General/Atoms", 
                       "LaTeXsugar"];
 
diff -r bdb1eab47161 -r 894599a50af3 Pearl/ROOT.ML
--- a/Pearl/ROOT.ML	Sat Sep 04 07:28:35 2010 +0800
+++ b/Pearl/ROOT.ML	Sat Sep 04 07:39:38 2010 +0800
@@ -1,5 +1,4 @@
 no_document use_thys ["../Nominal-General/Nominal2_Base", 
-                      "../Nominal-General/Nominal2_Atoms", 
                       "../Nominal-General/Nominal2_Eqvt",
                       "../Nominal-General/Atoms", 
                       "LaTeXsugar"];