--- 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