--- 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
--- 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"
--- 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")
--- 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
--- 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
--- 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"];
--- 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"];