--- a/Nominal-General/Nominal2_Supp.thy Wed Apr 21 19:10:55 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy Wed Apr 21 19:11:51 2010 +0200
@@ -433,6 +433,13 @@
qed
qed
+lemma perm_struct_induct2[case_names zero swap]:
+ assumes zero: "P 0"
+ assumes 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"
--- a/Nominal/Abs.thy Wed Apr 21 19:10:55 2010 +0200
+++ b/Nominal/Abs.thy Wed Apr 21 19:11:51 2010 +0200
@@ -397,150 +397,6 @@
section {* BELOW is stuff that may or may not be needed *}
-lemma
- fixes t1 s1::"'a::fs"
- and t2 s2::"'b::fs"
- shows "Abs as (t1, t2) = Abs as (s1, s2) \<longrightarrow> (Abs as t1 = Abs as s1 \<and> Abs as t2 = Abs as s2)"
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE)
-apply(simp add: supp_Pair)
-apply(simp add: Un_Diff)
-apply(simp add: fresh_star_union)
-apply(erule conjE)+
-apply(rule conjI)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-done
-
-lemma
- fixes t1 s1::"'a::fs"
- and t2 s2::"'b::fs"
- shows "Abs as (t1, t2) = Abs bs (s1, s2) \<longrightarrow> (Abs as t1 = Abs bs s1 \<and> Abs as t2 = Abs bs s2)"
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE)
-apply(simp add: supp_Pair)
-apply(simp add: Un_Diff)
-apply(simp add: fresh_star_union)
-apply(erule conjE)+
-apply(rule conjI)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-done
-
-lemma fresh_star_eq:
- assumes a: "as \<sharp>* p"
- shows "\<forall>a \<in> as. p \<bullet> a = a"
-using a by (simp add: fresh_star_def fresh_def supp_perm)
-
-lemma fresh_star_set_eq:
- assumes a: "as \<sharp>* p"
- shows "p \<bullet> as = as"
-using a
-apply(simp add: fresh_star_def fresh_def supp_perm permute_set_eq)
-apply(auto)
-by (metis permute_atom_def)
-
-lemma
- fixes t1 s1::"'a::fs"
- and t2 s2::"'b::fs"
- shows "Abs as t1 = Abs bs s1 \<longrightarrow> Abs (as \<union> cs) t1 = Abs (bs \<union> cs) s1"
-apply(subst abs_eq_iff)
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE | erule conjE)+
-apply(rule_tac x="p" in exI)
-apply(simp)
-apply(rule conjI)
-apply(auto)[1]
-apply(rule conjI)
-apply(auto)[1]
-apply(simp add: fresh_star_def)
-apply(auto)[1]
-apply(simp add: union_eqvt)
-oops
-
-
-lemma
- fixes t1 s1::"'a::fs"
- and t2 s2::"'b::fs"
- shows "(Abs as t1 = Abs bs s1 \<and> Abs as t2 = Abs bs s2) \<longrightarrow> Abs as (t1, t2) = Abs bs (s1, s2)"
-apply(subst abs_eq_iff)
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE | erule conjE)+
-apply(simp add: abs_eq_iff)
-apply(simp add: alphas_abs)
-apply(simp add: alphas)
-apply(rule conjI)
-apply(simp add: supp_Pair Un_Diff)
-oops
-
-
-
-(* support of concrete atom sets *)
-
-lemma
- shows "Abs as t = Abs (supp t \<inter> as) t"
-apply(simp add: abs_eq_iff)
-apply(simp add: alphas_abs)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas)
-apply(auto)
-oops
-
-lemma
- assumes "finite S"
- shows "\<exists>q. supp q \<subseteq> S \<union> p \<bullet> S \<and> (\<forall>a \<in> S. q \<bullet> a = p \<bullet> a)"
-using assms
-apply(induct)
-apply(rule_tac x="0" in exI)
-apply(simp add: supp_zero_perm)
-apply(auto)
-apply(simp add: insert_eqvt)
-apply(rule_tac x="((p \<bullet> x) \<rightleftharpoons> x) + q" in exI)
-apply(rule conjI)
-apply(rule subset_trans)
-apply(rule supp_plus_perm)
-apply(simp add: supp_swap)
-apply(auto)[1]
-apply(simp)
-apply(rule conjI)
-apply(case_tac "q \<bullet> x = x")
-apply(simp)
-apply(simp add: supp_perm)
-apply(case_tac "x \<in> p \<bullet> F")
-sorry
-
lemma supp_atom_image:
fixes as::"'a::at_base set"
--- a/PAPER-TODO Wed Apr 21 19:10:55 2010 +0200
+++ b/PAPER-TODO Wed Apr 21 19:11:51 2010 +0200
@@ -12,9 +12,6 @@
I didn't quite get top of second column, p. 6
-"the problem Pottier and Cheney pointed out": I had forgotten it in the
-meantime
-
the equation in the first actuall bullet on p. 8 lacks it =?
missing v. spaces, top of 2nd col p. 8
\ No newline at end of file
--- a/Paper/Paper.thy Wed Apr 21 19:10:55 2010 +0200
+++ b/Paper/Paper.thy Wed Apr 21 19:11:51 2010 +0200
@@ -338,7 +338,7 @@
(Note that this means also the term-constructors for variables, applications
and lambda are lifted to the quotient level.) This construction, of course,
only works if alpha-equivalence is indeed an equivalence relation, and the
- lifted definitions and theorems are respectful w.r.t.~alpha-equivalence.
+ ``raw'' definitions and theorems are respectful w.r.t.~alpha-equivalence.
For example, we will not be able to lift a bound-variable function. Although
this function can be defined for raw terms, it does not respect
alpha-equivalence and therefore cannot be lifted. To sum up, every lifting
@@ -352,7 +352,7 @@
known as Core-Haskell (see Figure~\ref{corehas}). This term language
involves patterns that have lists of type-, coercion- and term-variables,
all of which are bound in @{text "\<CASE>"}-expressions. One
- difficulty is that we do not know in advance how many variables need to
+ feature is that we do not know in advance how many variables need to
be bound. Another is that each bound variable comes with a kind or type
annotation. Representing such binders with single binders and reasoning
about them in a theorem prover would be a major pain. \medskip
@@ -932,9 +932,9 @@
\begin{center}
\begin{tabular}{l}
- \isacommand{bind}\; {\it binder}\; \isacommand{in}\; {\it label}\\
- \isacommand{bind\_set}\; {\it binder}\; \isacommand{in}\; {\it label}\\
- \isacommand{bind\_res}\; {\it binder}\; \isacommand{in}\; {\it label}\\
+ \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
+ \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
+ \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
\end{tabular}
\end{center}
@@ -943,15 +943,15 @@
the second is for sets of binders (the order does not matter, but the
cardinality does) and the last is for sets of binders (with vacuous binders
preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding
- clause will be called the \emph{body}; the ``\isacommand{bind}-part'' will
- be called the \emph{binder}.
+ clause will be called \emph{body}; the ``\isacommand{bind}-part'' will
+ be called \emph{binder}.
In addition we distinguish between \emph{shallow} and \emph{deep}
- binders. Shallow binders are of the form \isacommand{bind}\; {\it label}\;
- \isacommand{in}\; {\it label'} (similar for the other two modes). The
- restriction we impose on shallow binders is that the {\it label} must either
- refer to a type that is an atom type or to a type that is a finite set or
- list of an atom type. Two examples for the use of shallow binders are the
+ binders. Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
+ \isacommand{in}\; {\it labels'} (similar for the other two modes). The
+ restriction we impose on shallow binders is that the {\it labels} must either
+ refer to atom types or to finite sets or
+ lists of atom types. Two examples for the use of shallow binders are the
specification of lambda-terms, where a single name is bound, and
type-schemes, where a finite set of names is bound:
@@ -1111,8 +1111,9 @@
Having dealt with all syntax matters, the problem now is how we can turn
specifications into actual type definitions in Isabelle/HOL and then
- establish a reasoning infrastructure for them. Because of the problem
- Pottier and Cheney pointed out, we cannot in general re-arrange arguments of
+ establish a reasoning infrastructure for them. As
+ Pottier and Cheney pointed out \cite{Pottier06,Cheney5}, we cannot in general
+ re-arrange arguments of
term-constructors so that binders and their bodies are next to each other, and
then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
@{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first