# HG changeset patch # User Cezary Kaliszyk # Date 1271869911 -7200 # Node ID 77eccce38a175923f2a9666dd31d021e56ce60af # Parent 6c5e3ac737d9cab993e0f2ae58de33ddf06beea9# Parent e42bd9d95f093a88fcb31ec03abb377012d41de2 merge diff -r 6c5e3ac737d9 -r 77eccce38a17 Nominal-General/Nominal2_Supp.thy --- 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: "\p a b. \P p; a \ b; sort_of a = sort_of b\ \ P ((a \ 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 \ S" assumes zero: "P 0" diff -r 6c5e3ac737d9 -r 77eccce38a17 Nominal/Abs.thy --- 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) \ (Abs as t1 = Abs as s1 \ 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) \ (Abs as t1 = Abs bs s1 \ 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 \* p" - shows "\a \ as. p \ a = a" -using a by (simp add: fresh_star_def fresh_def supp_perm) - -lemma fresh_star_set_eq: - assumes a: "as \* p" - shows "p \ 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 \ Abs (as \ cs) t1 = Abs (bs \ 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 \ Abs as t2 = Abs bs s2) \ 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 \ 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 "\q. supp q \ S \ p \ S \ (\a \ S. q \ a = p \ 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 \ x) \ 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 \ x = x") -apply(simp) -apply(simp add: supp_perm) -apply(case_tac "x \ p \ F") -sorry - lemma supp_atom_image: fixes as::"'a::at_base set" diff -r 6c5e3ac737d9 -r 77eccce38a17 PAPER-TODO --- 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 diff -r 6c5e3ac737d9 -r 77eccce38a17 Paper/Paper.thy --- 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 "\"}-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