# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1274978272 -7200
# Node ID c6db12ddb60c3afde65c46d7ce5a8b59c7f3df67
# Parent  8732ff59068b2c24a89303c45565f8ed0837c18a
intermediate state

diff -r 8732ff59068b -r c6db12ddb60c Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Nominal/Abs.thy	Thu May 27 18:37:52 2010 +0200
@@ -847,7 +847,8 @@
   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
 lemma [mono]: 
-  shows "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D"
+  shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
+  unfolding prod_alpha_def
   by auto
 
 lemma [eqvt]: 
@@ -861,5 +862,6 @@
   unfolding prod_fv.simps
   by (perm_simp) (rule refl)
 
+
 end
 
diff -r 8732ff59068b -r c6db12ddb60c Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Thu May 27 18:37:52 2010 +0200
@@ -23,9 +23,40 @@
   "bn (As x t) = {atom x}"
 
 
+thm permute_trm_raw_permute_assg_raw.simps[no_vars]
 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars]
 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
 
+ML {* val {inducts, ... } = Function.get_info @{context} @{term "fv_trm_raw"}*}
+ML {* Rule_Cases.strict_mutual_rule @{context} (the inducts) *}
+
+(*
+lemma empty_eqvt[eqvt]:
+  shows "p \<bullet> {} = {}"
+  unfolding empty_def
+  by (perm_simp) (rule refl)
+*)
+lemma 
+  "(p \<bullet> {}) = {}"
+thm eqvts_raw
+thm eqvts
+apply(perm_strict_simp)
+
+
+lemma
+ shows "p1 \<bullet> fv_trm_raw trm_raw = fv_trm_raw (p1 \<bullet> trm_raw)"
+ and "p1 \<bullet> fv_assg_raw assg_raw = fv_assg_raw (p1 \<bullet> assg_raw)"
+ and "p1 \<bullet> fv_bn_raw assg_raw = fv_bn_raw (p1 \<bullet> assg_raw)"
+apply(induct trm_raw and assg_raw and assg_raw rule: fv_trm_raw_fv_assg_raw_fv_bn_raw.induct)
+apply(simp_all)
+apply(perm_simp)
+apply(rule refl)
+apply(perm_simp)
+apply(rule refl)
+apply(perm_simp)
+apply(rule refl)
+apply(simp add: fv_trm_raw.simps)
+
 
 
 ML {* Inductive.the_inductive *}
diff -r 8732ff59068b -r c6db12ddb60c Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Nominal/NewParser.thy	Thu May 27 18:37:52 2010 +0200
@@ -358,6 +358,7 @@
   val ths_loc = prove_by_induct tys (build_eqvt_gl p) ind tac funs ctxt'
   val ths = Variable.export ctxt' ctxt ths_loc
   val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
+  val _ = tracing ("eqvt thms\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) ths))
 in
   (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
 end
diff -r 8732ff59068b -r c6db12ddb60c Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Thu May 27 18:37:52 2010 +0200
@@ -1,8 +1,14 @@
 theory Nominal2_FSet
 imports "../Nominal-General/Nominal2_Supp"
+        "../Nominal-General/Nominal2_Atoms" 
+        "../Nominal-General/Nominal2_Eqvt" 
         FSet 
 begin
 
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
 lemma permute_rsp_fset[quot_respect]:
   "(op = ===> list_eq ===> list_eq) permute permute"
   apply (simp add: eqvts[symmetric])
@@ -34,12 +40,29 @@
 
 end
 
-lemma permute_fset[simp, eqvt]:
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
+lemma permute_fset[simp]:
   fixes S::"('a::pt) fset"
   shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
   and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
+ML {* @{term "{}"} ; @{term "{||}"} *}
+
+declare permute_fset[eqvt]
+
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
+
 lemma fmap_eqvt[eqvt]: 
   shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
@@ -119,4 +142,8 @@
   apply auto
   done
 
+lemma "p \<bullet> {} = {}"
+apply(perm_simp)
+by simp
+
 end
diff -r 8732ff59068b -r c6db12ddb60c Nominal/Perm.thy
--- a/Nominal/Perm.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Nominal/Perm.thy	Thu May 27 18:37:52 2010 +0200
@@ -2,10 +2,12 @@
 imports 
   "../Nominal-General/Nominal2_Base"
   "../Nominal-General/Nominal2_Atoms" 
-  "Nominal2_FSet" "Abs"
-uses ("nominal_dt_rawperm.ML")
+  "../Nominal-General/Nominal2_Eqvt" 
+  "Nominal2_FSet"
+  "Abs"
+(*uses ("nominal_dt_rawperm.ML")
      ("nominal_dt_rawfuns.ML")
-     ("nominal_dt_alpha.ML")
+     ("nominal_dt_alpha.ML")*)
 begin
 
 use "nominal_dt_rawperm.ML"
diff -r 8732ff59068b -r c6db12ddb60c Nominal/Tacs.thy
--- a/Nominal/Tacs.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Nominal/Tacs.thy	Thu May 27 18:37:52 2010 +0200
@@ -17,6 +17,17 @@
 end
 *}
 
+ML {*
+fun mk_conjl props =
+  fold (fn a => fn b =>
+    if a = @{term True} then b else
+    if b = @{term True} then a else
+    HOLogic.mk_conj (a, b)) (rev props) @{term True};
+*}
+
+ML {*
+val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+*}
 
 
 ML {*
diff -r 8732ff59068b -r c6db12ddb60c Slides/Slides1.thy
--- a/Slides/Slides1.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Slides/Slides1.thy	Thu May 27 18:37:52 2010 +0200
@@ -41,16 +41,16 @@
   \item sorted atoms and sort-respecting permutations\medskip
 
   \onslide<2->{
-  \item[] in old Nominal: atoms have dif\!ferent type
+  \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{7mm}}c}
-  $[] \act c \dn c$ &
-  @{text "(a b)::\<pi> \<bullet> c \<equiv>"} 
+  $[]\;\act\;c \dn c$ &
+  $(a\;b)\!::\!\pi\;\act\;c \dn$ 
   $\begin{cases}
-  \mbox{@{text "b"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = a"}}\\
-  \mbox{@{text "a"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = b"}}\\
-  \mbox{@{text "\<pi> \<bullet> c"}} & \text{otherwise}
+  b & \text{if}\; \pi \act c = a\\
+  a & \text{if}\; \pi \act c = b\\
+  \pi \act c & \text{otherwise}
   \end{cases}$
   \end{tabular}
   \end{center}}
@@ -68,29 +68,165 @@
   \mbox{}\\[-3mm]
 
   \begin{itemize}
-  \item $\_ \act \_ :: \alpha perm \Rightarrow \beta \Rightarrow \beta$
+  \item @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}\bigskip
 
-  \item $supp \_ :: \beta \Rightarrow \alpha set$
+  \item @{text "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
 
   \begin{center}
-  $finite (supp x)_{\alpha_1} \ldots finite (supp x)_{\alpha_n}$
-  \end{center}
+  $\text{finite} (\text{supp}\;x)_{\,\alpha_1\,\text{set}}$ \ldots 
+  $\text{finite} (\text{supp}\;x)_{\,\alpha_n\,\text{set}}$
+  \end{center}\bigskip
   
-  \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$
+  \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$\bigskip
+
+  \item type-classes
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-4>
+  \frametitle{\begin{tabular}{c}Our New Solution\end{tabular}}
+  \mbox{}\\[-3mm]
+*}
+datatype atom = Atom string nat
+
+text_raw {*
+  \mbox{}\bigskip
+  \begin{itemize}
+  \item<2-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"}
+
+     \begin{itemize}
+     \item sort-respecting \hspace{5mm}($\forall a.\;\text{sort}(f a) = \text{sort}(a)$)
+     \item finite domain \hspace{5mm}($\text{finite} \{a.\;f a \not= a\}$)
+     \end{itemize}\medskip
+
+  \item<3-> swappings:
+     \small
+     \[
+     \begin{array}{l@ {\hspace{1mm}}l}
+     (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\
+        & \text{then}\;\lambda  c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\;
+          \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\
+        & \text{else}\;\only<3>{\mbox{\textcolor{red}{\bf ?}}}\only<4->{\text{id}}
+     \end{array}
+     \]
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-4>
+  \frametitle{\begin{tabular}{c}\LARGE{}A Smoother Nominal Theory\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item<1-> $(a\;b) = (b\;a)$\bigskip  
+
+  \item<2-> permutations are an instance of group\_add\\ $0$, $\pi_1 + \pi_2$, $- \pi$\bigskip
+
+  \item<3-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip
+  
+   \begin{itemize}
+   \item $0\;\act\;x = x$\\
+   \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$
+   \end{itemize}
+
+   \small
+   \onslide<4->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}
   \end{itemize}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>
+  \frametitle{\begin{tabular}{c}Very Few Snatches\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item \underline{concrete} atoms:
+  \end{itemize}
+*}
+(*<*)
+consts sort :: "atom \<Rightarrow> string"
+(*>*)
+
+typedef name = "{a :: atom. sort a = ''name''}"
+(*<*)sorry(*>*)
+
+text_raw {*
+  \mbox{}\bigskip\bigskip
+  \begin{itemize}
+  \item<2-> there is a function \underline{atom}, which injects concrete atoms into generic atoms\medskip 
+  \begin{center}
+  \begin{tabular}{l}
+  $\text{atom}(a) \fresh x$\\
+  $(a \leftrightarrow b) \dn (\text{atom}(a)\;\;\text{atom}(b))$
+  \end{tabular}
+  \end{center}\bigskip\medskip
+
+  \onslide<3->
+  {I would like to have $a \fresh x$, $(a\; b)$, \ldots}
+
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
 
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1>[c]
-  \frametitle{\begin{tabular}{c}Part II: General Bindings\end{tabular}}
+  \begin{frame}<1-2>[c]
+  \frametitle{\begin{tabular}{c}\LARGE{}End of Part I\end{tabular}}
   \mbox{}\\[-3mm]
 
+  \begin{itemize}
+  \item the formalised version of the nominal theory is much nicer to 
+  work with (no assumptions, just two type classes; sorts are occasionally 
+  explicit)\bigskip
+
+  \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\bigskip
+
+  \item allow sort-disrespecting swappings\onslide<2->{: just define them as the identity}
+  \end{itemize}
+
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-2>
+  \frametitle{\begin{tabular}{c}\LARGE{}Part II: General Bindings\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item old Nominal provided single binders
+  \begin{center}
+  Lam [a].(Var a)
+  \end{center}\bigskip
+
+  \item<2-> representing 
+  \begin{center}
+  $\forall\{a_1,\ldots,a_n\}.\; T$ 
+  \end{center}
+  is a major pain, take my word for it
+  \end{itemize}
   
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
diff -r 8732ff59068b -r c6db12ddb60c Slides/document/root.tex
--- a/Slides/document/root.tex	Wed May 26 15:37:56 2010 +0200
+++ b/Slides/document/root.tex	Thu May 27 18:37:52 2010 +0200
@@ -40,10 +40,10 @@
 
 % Isabelle configuration
 %%\urlstyle{rm}
-\isabellestyle{it}
-\renewcommand{\isastyle}{\it}%
-\renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isastylescript}{\footnotesize\it\slshape}%
+\isabellestyle{rm}
+\renewcommand{\isastyle}{\rm}%
+\renewcommand{\isastyleminor}{\rm}%
+\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
 \renewcommand{\isatagproof}{}
 \renewcommand{\endisatagproof}{}
 \renewcommand{\isamarkupcmt}[1]{#1}