--- a/IsaMakefile Mon May 24 21:11:33 2010 +0100
+++ b/IsaMakefile Tue May 25 00:24:41 2010 +0100
@@ -60,6 +60,27 @@
$(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated
@cp Quotient-Paper/document.pdf qpaper.pdf
+## Slides
+
+session1: Slides/ROOT.ML \
+ Slides/document/root* \
+ Slides/Slides1.thy
+ @$(USEDIR) -D generated1 -f ROOT.ML HOL-Nominal Slides
+ @perl -i -p -e "s/..isachardoublequoteopen./\\\begin{innerdouble}/g" Sl
+ @perl -i -p -e "s/..isachardoublequoteclose./\\\end{innerdouble}/g" Sli
+ @perl -i -p -e "s/..isacharbackquoteopen./\\\begin{innersingle}/g" Slid
+ @perl -i -p -e "s/..isacharbackquoteclose./\\\end{innersingle}/g" Slide
+
+slides1: session1
+ rm -f Slides/generated1/*.aux # otherwise latex will fall over
+ cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+ cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+ cp Slides/generated1/root.beamer.pdf Slides/slides.pdf
+
+slides: slides1
+
+
+
## clean
--- a/Nominal/Ex/SingleLet.thy Mon May 24 21:11:33 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy Tue May 25 00:24:41 2010 +0100
@@ -5,7 +5,7 @@
atom_decl name
ML {* print_depth 50 *}
-declare [[STEPS = 5]]
+declare [[STEPS = 8]]
nominal_datatype trm =
--- a/Nominal/NewParser.thy Mon May 24 21:11:33 2010 +0100
+++ b/Nominal/NewParser.thy Tue May 25 00:24:41 2010 +0100
@@ -305,6 +305,8 @@
setup STEPS_setup
+ML {* dtyp_no_of_typ *}
+
ML {*
fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
let
@@ -327,6 +329,9 @@
val induct_thm = #induct dtinfo;
val exhaust_thms = map #exhaust dtinfos;
+ val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
+ val bns = raw_bn_funs ~~ bn_nos;
+
(* definitions of raw permutations *)
val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) =
if get_STEPS lthy1 > 2
@@ -354,16 +359,12 @@
then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a
else raise TEST lthy3a
- val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr;
- val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
- val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
-
- val bns = raw_bn_funs ~~ bn_nos;
+ (* HERE *)
+ (* definition of raw_alpha_eq_iff lemmas *)
val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) (rel_distinct ~~ alpha_ts));
val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_bn_ts))
-
- (* definition of raw_alpha_eq_iff lemmas *)
+
val alpha_eq_iff =
if get_STEPS lthy > 5
then build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
@@ -375,7 +376,7 @@
val _ = warning "Proving equivariance";
val (bv_eqvt, lthy5) =
if get_STEPS lthy > 6
- then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4
+ then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) raw_bn_funs lthy4
else raise TEST lthy4
val (fv_eqvt, lthy6) =
--- a/Nominal/nominal_dt_alpha.ML Mon May 24 21:11:33 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML Tue May 25 00:24:41 2010 +0100
@@ -210,8 +210,8 @@
val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss
val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info
- val all_alpha_names = map2 (fn s => fn ty => ((Binding.name s, ty), NoSyn))
- (alpha_names @ alpha_bn_names) (alpha_tys @ alpha_bn_tys)
+ val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
+ (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
val (alphas, lthy') = Inductive.add_inductive_i
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/ROOT.ML Tue May 25 00:24:41 2010 +0100
@@ -0,0 +1,6 @@
+show_question_marks := false;
+quick_and_dirty := true;
+
+no_document use_thy "LaTeXsugar";
+
+use_thy "Slides1"
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides1.thy Tue May 25 00:24:41 2010 +0100
@@ -0,0 +1,61 @@
+(*<*)
+theory Slides1
+imports "LaTeXsugar" "Nominal"
+begin
+
+notation (latex output)
+ set ("_") and
+ Cons ("_::/_" [66,65] 65)
+
+(*>*)
+
+
+text_raw {*
+ \renewcommand{\slidecaption}{TU Munich, 28.~May 2010}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[t]
+ \frametitle{%
+ \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
+ \\
+ \huge Nominal 2\\[-2mm]
+ \large Or, How to Reason Conveniently with\\[-5mm]
+ \large General Bindings\\[15mm]
+ \end{tabular}}
+ \begin{center}
+ joint work with {\bf Cezary} and Brian Huffman\\[0mm]
+ \end{center}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>
+ \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}}
+ \mbox{}\\[-3mm]
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[c]
+ \frametitle{\begin{tabular}{c}Part II: General Bindings\end{tabular}}
+ \mbox{}\\[-3mm]
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/document/root.beamer.tex Tue May 25 00:24:41 2010 +0100
@@ -0,0 +1,12 @@
+\documentclass[14pt,t]{beamer}
+%%%\usepackage{pstricks}
+
+\input{root.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% TeX-command-default: "Slides"
+%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f"))
+%%% End:
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/document/root.notes.tex Tue May 25 00:24:41 2010 +0100
@@ -0,0 +1,18 @@
+\documentclass[11pt]{article}
+%%\usepackage{pstricks}
+\usepackage{dina4}
+\usepackage{beamerarticle}
+\usepackage{times}
+\usepackage{hyperref}
+\usepackage{pgf}
+\usepackage{amssymb}
+\setjobnamebeamerversion{root.beamer}
+\input{root.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% TeX-command-default: "Slides"
+%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f"))
+%%% End:
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/document/root.tex Tue May 25 00:24:41 2010 +0100
@@ -0,0 +1,155 @@
+\usepackage{beamerthemeplaincu}
+\usepackage[T1]{fontenc}
+\usepackage{proof}
+\usepackage{german}
+\usepackage[latin1]{inputenc}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{mathpartir}
+\usepackage[absolute,overlay]{textpos}
+\usepackage{proof}
+\usepackage{ifthen}
+\usepackage{animate}
+\usepackage{tikz}
+\usepackage{pgf}
+\usepackage{calc}
+%%%\usepackage{ulem}
+%%%\newcommand{\uline}[1]{}
+\usetikzlibrary{arrows}
+\usetikzlibrary{automata}
+\usetikzlibrary{shapes}
+\usetikzlibrary{shadows}
+%%%\usetikzlibrary{mindmap}
+
+\usepackage{graphicx}
+\usepackage{xcolor}
+
+
+
+
+% Isabelle configuration
+%%\urlstyle{rm}
+\isabellestyle{rm}
+\renewcommand{\isastyle}{\rm}%
+\renewcommand{\isastyleminor}{\rm}%
+\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
+\renewcommand{\isatagproof}{}
+\renewcommand{\endisatagproof}{}
+\renewcommand{\isamarkupcmt}[1]{#1}
+
+% Isabelle characters
+\renewcommand{\isacharunderscore}{\_}
+\renewcommand{\isacharbar}{\isamath{\mid}}
+\renewcommand{\isasymiota}{}
+\renewcommand{\isacharbraceleft}{\{}
+\renewcommand{\isacharbraceright}{\}}
+\renewcommand{\isacharless}{$\langle$}
+\renewcommand{\isachargreater}{$\rangle$}
+\renewcommand{\isasymsharp}{\isamath{\#}}
+\renewcommand{\isasymdots}{\isamath{...}}
+\renewcommand{\isasymbullet}{\act}
+
+% mathpatir
+\mprset{sep=1em}
+
+% general math stuff
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}}
+\renewcommand{\emptyset}{\varnothing}% nice round empty set
+\renewcommand{\Gamma}{\varGamma}
+\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
+\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
+\newcommand{\smath}[1]{\textcolor{blue}{\ensuremath{#1}}}
+\newcommand{\fresh}{\mathrel{\#}}
+\newcommand{\act}{{\raisebox{-0.5mm}{\Large$\boldsymbol{\cdot}$}}}% swapping action
+\newcommand{\swap}[2]{(#1\,#2)}% swapping operation
+
+% beamer stuff
+\renewcommand{\slidecaption}{Salvador, 26.~August 2008}
+
+
+% colours for Isar Code (in article mode everything is black and white)
+\mode<presentation>{
+\definecolor{isacol:brown}{rgb}{.823,.411,.117}
+\definecolor{isacol:lightblue}{rgb}{.274,.509,.705}
+\definecolor{isacol:green}{rgb}{0,.51,0.14}
+\definecolor{isacol:red}{rgb}{.803,0,0}
+\definecolor{isacol:blue}{rgb}{0,0,.803}
+\definecolor{isacol:darkred}{rgb}{.545,0,0}
+\definecolor{isacol:black}{rgb}{0,0,0}}
+\mode<article>{
+\definecolor{isacol:brown}{rgb}{0,0,0}
+\definecolor{isacol:lightblue}{rgb}{0,0,0}
+\definecolor{isacol:green}{rgb}{0,0,0}
+\definecolor{isacol:red}{rgb}{0,0,0}
+\definecolor{isacol:blue}{rgb}{0,0,0}
+\definecolor{isacol:darkred}{rgb}{0,0,0}
+\definecolor{isacol:black}{rgb}{0,0,0}
+}
+
+
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\bluecmd}[1]{{\color{isacol:lightblue}{\strong{#1}}}}
+\newcommand{\browncmd}[1]{{\color{isacol:brown}{\strong{#1}}}}
+\newcommand{\redcmd}[1]{{\color{isacol:red}{\strong{#1}}}}
+
+\renewcommand{\isakeyword}[1]{%
+\ifthenelse{\equal{#1}{show}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{case}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{assume}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{obtain}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{fix}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{oops}}{\redcmd{#1}}{%
+\ifthenelse{\equal{#1}{thm}}{\redcmd{#1}}{%
+{\bluecmd{#1}}}}}}}}}}%
+
+% inner syntax colour
+\chardef\isachardoublequoteopen=`\"%
+\chardef\isachardoublequoteclose=`\"%
+\chardef\isacharbackquoteopen=`\`%
+\chardef\isacharbackquoteclose=`\`%
+\newenvironment{innersingle}%
+{\isacharbackquoteopen\color{isacol:green}}%
+{\color{isacol:black}\isacharbackquoteclose}
+\newenvironment{innerdouble}%
+{\isachardoublequoteopen\color{isacol:green}}%
+{\color{isacol:black}\isachardoublequoteclose}
+
+%% misc
+\newcommand{\gb}[1]{\textcolor{isacol:green}{#1}}
+\newcommand{\rb}[1]{\textcolor{red}{#1}}
+
+%% animations
+\newcounter{growcnt}
+\newcommand{\grow}[2]
+{\begin{tikzpicture}[baseline=(n.base)]%
+ \node[scale=(0.1 *#1 + 0.001),inner sep=0pt] (n) {#2};
+ \end{tikzpicture}%
+}
+
+%% isatabbing
+%\renewcommand{\isamarkupcmt}[1]%
+%{\ifthenelse{\equal{TABSET}{#1}}{\=}%
+% {\ifthenelse{\equal{TAB}{#1}}{\>}%
+% {\ifthenelse{\equal{NEWLINE}{#1}}{\\}%
+% {\ifthenelse{\equal{DOTS}{#1}}{\ldots}{\isastylecmt--- {#1}}}%
+% }%
+% }%
+%}%
+
+
+\newenvironment{isatabbing}%
+{\renewcommand{\isanewline}{\\}\begin{tabbing}}%
+{\end{tabbing}}
+
+\begin{document}
+\input{session}
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% TeX-command-default: "Slides"
+%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f"))
+%%% End:
+