# HG changeset patch # User Christian Urban # Date 1274743481 -3600 # Node ID 09bbed4f21d68550156c3177a8ee3f7f70f94ab8 # Parent aead2aad845c45003a2364eb0b712ce17b9af6c9 added slides diff -r aead2aad845c -r 09bbed4f21d6 IsaMakefile --- 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 diff -r aead2aad845c -r 09bbed4f21d6 Nominal/Ex/SingleLet.thy --- 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 = diff -r aead2aad845c -r 09bbed4f21d6 Nominal/NewParser.thy --- 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) = diff -r aead2aad845c -r 09bbed4f21d6 Nominal/nominal_dt_alpha.ML --- 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 diff -r aead2aad845c -r 09bbed4f21d6 Slides/ROOT.ML --- /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 diff -r aead2aad845c -r 09bbed4f21d6 Slides/Slides1.thy --- /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{ + \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{ + \begin{frame}<1> + \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}} + \mbox{}\\[-3mm] + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \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 diff -r aead2aad845c -r 09bbed4f21d6 Slides/document/root.beamer.tex --- /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: + diff -r aead2aad845c -r 09bbed4f21d6 Slides/document/root.notes.tex --- /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: + diff -r aead2aad845c -r 09bbed4f21d6 Slides/document/root.tex --- /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{ +\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
{ +\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: +