# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1239120279 -3600
# Node ID abc7f90188af7ccd236ad90cff708a555a93c7e2
# Parent  fe45fbb111c55f016e6d3a115e5440cc66506f35
permutation example uses now recent infrastructure

diff -r fe45fbb111c5 -r abc7f90188af ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Fri Apr 03 07:55:07 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Tue Apr 07 17:04:39 2009 +0100
@@ -1554,6 +1554,68 @@
   valid local theory.
 *}
 
+ML{*signature UNIVERSAL_TYPE =
+sig
+  type t
+
+  val embed: unit -> ('a -> t) * (t -> 'a option)
+end*}
+
+ML{*structure U:> UNIVERSAL_TYPE =
+   struct
+      type t = exn
+
+      fun 'a embed () =
+         let
+            exception E of 'a
+            fun project (e: t): 'a option =
+               case e of
+                  E a => SOME a
+                | _ => NONE
+         in
+            (E, project)
+         end
+   end*}
+
+text {*
+  The idea is that type t is the universal type and that each call to embed
+  returns a new pair of functions (inject, project), where inject embeds a
+  value into the universal type and project extracts the value from the
+  universal type. A pair (inject, project) returned by embed works together in
+  that project u will return SOME v if and only if u was created by inject
+  v. If u was created by a different function inject', then project returns
+  NONE.
+
+  in library.ML
+*}
+
+ML_val{*structure Object = struct type T = exn end; *}
+
+ML{*functor Test (U: UNIVERSAL_TYPE): sig end =
+   struct
+      val (intIn: int -> U.t, intOut) = U.embed ()
+      val r: U.t ref = ref (intIn 13)
+      val s1 =
+         case intOut (!r) of
+            NONE => "NONE"
+          | SOME i => Int.toString i
+      val (realIn: real -> U.t, realOut) = U.embed ()
+      val () = r := realIn 13.0
+      val s2 =
+         case intOut (!r) of
+            NONE => "NONE"
+          | SOME i => Int.toString i
+      val s3 =
+         case realOut (!r) of
+            NONE => "NONE"
+          | SOME x => Real.toString x
+      val () = warning (concat [s1, " ", s2, " ", s3, "\n"])
+   end*}
+
+ML_val{*structure t = Test(U) *} 
+
+ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*}
+
 section {* Storing Theorems\label{sec:storing} (TBD) *}
 
 text {* @{ML PureThy.add_thms_dynamic} *}
diff -r fe45fbb111c5 -r abc7f90188af ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Fri Apr 03 07:55:07 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Apr 07 17:04:39 2009 +0100
@@ -748,6 +748,11 @@
   \end{exercise}
 *}
 
+text {*
+  (FIXME: @{ML OuterParse.type_args}, @{ML OuterParse.typ}, @{ML OuterParse.opt_mixfix})
+*}
+
+
 section {* New Commands and Keyword Files\label{sec:newcommand} *}
 
 text {*
diff -r fe45fbb111c5 -r abc7f90188af ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Fri Apr 03 07:55:07 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Tue Apr 07 17:04:39 2009 +0100
@@ -1283,45 +1283,59 @@
 types  prm = "(nat \<times> nat) list"
 consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a"  ("_ \<bullet> _" [80,80] 80)
 
-primrec (perm_nat)
- "[]\<bullet>c = c"
- "(ab#pi)\<bullet>c = (if (pi\<bullet>c)=fst ab then snd ab 
-               else (if (pi\<bullet>c)=snd ab then fst ab else (pi\<bullet>c)))" 
+overloading 
+  perm_nat \<equiv> "perm :: prm \<Rightarrow> nat \<Rightarrow> nat"
+  perm_prod \<equiv> "perm :: prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"
+  perm_list \<equiv> "perm :: prm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+begin
+
+fun swap::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "swap a b c = (if c=a then b else (if c=b then a else c))"
 
-primrec (perm_prod)
- "pi\<bullet>(x, y) = (pi\<bullet>x, pi\<bullet>y)"
+primrec perm_nat
+where
+  "perm_nat [] c = c"
+| "perm_nat (ab#pi) c = swap (fst ab) (snd ab) (perm_nat pi c)"
 
-primrec (perm_list)
- "pi\<bullet>[] = []"
- "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
+fun perm_prod 
+where
+ "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
+
+primrec perm_list
+where
+  "perm_list pi [] = []"
+| "perm_list pi (x#xs) = (pi\<bullet>x)#(perm_list pi xs)"
+
+end
 
 lemma perm_append[simp]:
-  fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-  shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
+fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
 by (induct pi\<^isub>1) (auto) 
 
-lemma perm_eq[simp]:
-  fixes c::"nat" and pi::"prm"
-  shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)" 
+lemma perm_bij[simp]:
+fixes c d::"nat" and pi::"prm"
+shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)" 
 by (induct pi) (auto)
 
 lemma perm_rev[simp]:
-  fixes c::"nat" and pi::"prm"
-  shows "pi\<bullet>((rev pi)\<bullet>c) = c"
+fixes c::"nat" and pi::"prm"
+shows "pi\<bullet>((rev pi)\<bullet>c) = c"
 by (induct pi arbitrary: c) (auto)
 
 lemma perm_compose:
-  fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-  shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)" 
+fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)" 
 by (induct pi\<^isub>2) (auto)
 text_raw {*
 \end{isabelle}
 \end{boxedminipage}
-\caption{A simple theory about permutations over @{typ nat}. The point is that the
+\caption{A simple theory about permutations over @{typ nat}s. The point is that the
   lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
   it would cause the simplifier to loop. It can still be used as a simplification 
-  rule if the permutation is sufficiently protected.\label{fig:perms}
-  (FIXME: Uses old primrec.)}
+  rule if the permutation in the right-hand side is sufficiently protected.
+  \label{fig:perms}}
 \end{figure} *}
 
 
@@ -1341,8 +1355,8 @@
 *}
 
 lemma 
-  fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-  shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
+fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
 apply(simp)
 apply(rule trans)
 apply(rule perm_compose)
@@ -1364,13 +1378,13 @@
 text {* Now the two lemmas *}
 
 lemma perm_aux_expand:
-  fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-  shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)" 
+fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)" 
 unfolding perm_aux_def by (rule refl)
 
 lemma perm_compose_aux:
-  fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-  shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)" 
+fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)" 
 unfolding perm_aux_def by (rule perm_compose)
 
 text {* 
@@ -1391,7 +1405,7 @@
 ML %linenosgray{*val perm_simp_tac =
 let
   val thms1 = [@{thm perm_aux_expand}]
-  val thms2 = [@{thm perm_append}, @{thm perm_eq}, @{thm perm_rev}, 
+  val thms2 = [@{thm perm_append}, @{thm perm_bij}, @{thm perm_rev}, 
                @{thm perm_compose_aux}] @ @{thms perm_prod.simps} @ 
                @{thms perm_list.simps} @ @{thms perm_nat.simps}
   val thms3 = [@{thm perm_aux_def}]
@@ -1408,8 +1422,8 @@
 *}
 
 lemma 
-  fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-  shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
+fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
 apply(tactic {* perm_simp_tac 1 *})
 done
 
diff -r fe45fbb111c5 -r abc7f90188af progtutorial.pdf
Binary file progtutorial.pdf has changed