# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1410579547 -3600
# Node ID 1cde7bf45858038986212fb8704d8e8b9a19d367
# Parent  a5f5b9336007270ab826d6d41228d967d317b8d2
deleted *~ files

diff -r a5f5b9336007 -r 1cde7bf45858 Separation_Algebra/Sep_Tactics.thy~
--- a/Separation_Algebra/Sep_Tactics.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,161 +0,0 @@
-(* Authors: Gerwin Klein and Rafal Kolanski, 2012
-   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
-                Rafal Kolanski <rafal.kolanski at nicta.com.au>
-*)
-
-header "Separation Logic Tactics"
-
-theory Sep_Tactics
-imports Separation_Algebra
-begin
-
-ML_file "sep_tactics.ML"
-
-text {* A number of proof methods to assist with reasoning about separation logic. *}
-
-
-section {* Selection (move-to-front) tactics *}
-
-ML {*
-  fun sep_select_method n ctxt =
-        Method.SIMPLE_METHOD' (sep_select_tac ctxt n);
-  fun sep_select_asm_method n ctxt =
-        Method.SIMPLE_METHOD' (sep_select_asm_tac ctxt n);
-*}
-
-method_setup sep_select = {*
-  Scan.lift Parse.int >> sep_select_method
-*} "Select nth separation conjunct in conclusion"
-
-method_setup sep_select_asm = {*
-  Scan.lift Parse.int >> sep_select_asm_method
-*} "Select nth separation conjunct in assumptions"
-
-
-section {* Substitution *}
-
-ML {*
-  fun sep_subst_method ctxt occs thms =
-        SIMPLE_METHOD' (sep_subst_tac ctxt occs thms);
-  fun sep_subst_asm_method ctxt occs thms =
-        SIMPLE_METHOD' (sep_subst_asm_tac ctxt occs thms);
-
-  val sep_subst_parser =
-        Args.mode "asm"
-        -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0])
-        -- Attrib.thms;
-*}
-
-method_setup "sep_subst" = {*
-  sep_subst_parser >>
-    (fn ((asm, occs), thms) => fn ctxt =>
-      (if asm then sep_subst_asm_method else sep_subst_method) ctxt occs thms)
-*}
-"single-step substitution after solving one separation logic assumption"
-
-
-section {* Forward Reasoning *}
-
-ML {*
-  fun sep_drule_method thms ctxt = SIMPLE_METHOD' (sep_dtac ctxt thms);
-  fun sep_frule_method thms ctxt = SIMPLE_METHOD' (sep_ftac ctxt thms);
-*}
-
-method_setup "sep_drule" = {*
-  Attrib.thms >> sep_drule_method
-*} "drule after separating conjunction reordering"
-
-method_setup "sep_frule" = {*
-  Attrib.thms >> sep_frule_method
-*} "frule after separating conjunction reordering"
-
-
-section {* Backward Reasoning *}
-
-ML {*
-  fun sep_rule_method thms ctxt = SIMPLE_METHOD' (sep_rtac ctxt thms)
-*}
-
-method_setup "sep_rule" = {*
-  Attrib.thms >> sep_rule_method
-*} "applies rule after separating conjunction reordering"
-
-
-section {* Cancellation of Common Conjuncts via Elimination Rules *}
-
-ML {*
-  structure SepCancel_Rules = Named_Thms (
-    val name = @{binding "sep_cancel"};
-    val description = "sep_cancel rules";
-  );
-*}
-setup SepCancel_Rules.setup
-
-text {*
-  The basic @{text sep_cancel_tac} is minimal. It only eliminates
-  erule-derivable conjuncts between an assumption and the conclusion.
-
-  To have a more useful tactic, we augment it with more logic, to proceed as
-  follows:
-  \begin{itemize}
-  \item try discharge the goal first using @{text tac}
-  \item if that fails, invoke @{text sep_cancel_tac}
-  \item if @{text sep_cancel_tac} succeeds
-    \begin{itemize}
-    \item try to finish off with tac (but ok if that fails)
-    \item try to finish off with @{term sep_true} (but ok if that fails)
-    \end{itemize}
-  \end{itemize}
-  *}
-
-ML {*
-  fun sep_cancel_smart_tac ctxt tac =
-    let fun TRY' tac = tac ORELSE' (K all_tac)
-    in
-      tac
-      ORELSE' (sep_cancel_tac ctxt tac
-               THEN' TRY' tac
-               THEN' TRY' (rtac @{thm TrueI}))
-      ORELSE' (etac @{thm sep_conj_sep_emptyE}
-               THEN' sep_cancel_tac ctxt tac
-               THEN' TRY' tac
-               THEN' TRY' (rtac @{thm TrueI}))
-    end;
-
-  fun sep_cancel_smart_tac_rules ctxt etacs =
-      sep_cancel_smart_tac ctxt (FIRST' ([atac] @ etacs));
-
-  fun sep_cancel_method ctxt =
-    let
-      val etacs = map etac (SepCancel_Rules.get ctxt);
-    in
-      SIMPLE_METHOD' (sep_cancel_smart_tac_rules ctxt etacs)
-    end;
-
-  val sep_cancel_syntax = Method.sections [
-    Args.add -- Args.colon >> K (I, SepCancel_Rules.add)];
-*}
-
-method_setup sep_cancel = {*
-  sep_cancel_syntax >> K sep_cancel_method
-*} "Separating conjunction conjunct cancellation"
-
-text {*
-  As above, but use blast with a depth limit to figure out where cancellation
-  can be done. *}
-
-ML {*
-  fun sep_cancel_blast_method ctxt =
-    let
-      val rules = SepCancel_Rules.get ctxt;
-      val tac = Blast.depth_tac (ctxt addIs rules) 10;
-    in
-      SIMPLE_METHOD' (sep_cancel_smart_tac ctxt tac)
-    end;
-*}
-
-method_setup sep_cancel_blast = {*
-  sep_cancel_syntax >> K sep_cancel_blast_method
-*} "Separating conjunction conjunct cancellation using blast"
-
-end
diff -r a5f5b9336007 -r 1cde7bf45858 Separation_Algebra/Separation_Algebra.thy~
--- a/Separation_Algebra/Separation_Algebra.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,815 +0,0 @@
-(* Authors: Gerwin Klein and Rafal Kolanski, 2012
-   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
-                Rafal Kolanski <rafal.kolanski at nicta.com.au>
-*)
-
-header "Abstract Separation Algebra"
-
-theory Separation_Algebra
-imports Main
-begin
-
-
-text {* This theory is the main abstract separation algebra development *}
-
-
-section {* Input syntax for lifting boolean predicates to separation predicates *}
-
-abbreviation (input)
-  pred_and :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "and" 35) where
-  "a and b \<equiv> \<lambda>s. a s \<and> b s"
-
-abbreviation (input)
-  pred_or :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "or" 30) where
-  "a or b \<equiv> \<lambda>s. a s \<or> b s"
-
-abbreviation (input)
-  pred_not :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" ("not _" [40] 40) where
-  "not a \<equiv> \<lambda>s. \<not>a s"
-
-abbreviation (input)
-  pred_imp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "imp" 25) where
-  "a imp b \<equiv> \<lambda>s. a s \<longrightarrow> b s"
-
-abbreviation (input)
-  pred_K :: "'b \<Rightarrow> 'a \<Rightarrow> 'b" ("\<langle>_\<rangle>") where
-  "\<langle>f\<rangle> \<equiv> \<lambda>s. f"
-
-(* abbreviation *)
-  definition pred_ex :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "EXS " 10) where
-  "EXS x. P x \<equiv> \<lambda>s. \<exists>x. P x s"
-
-abbreviation (input)
-  pred_all :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "ALLS " 10) where
-  "ALLS x. P x \<equiv> \<lambda>s. \<forall>x. P x s"
-
-
-section {* Associative/Commutative Monoid Basis of Separation Algebras *}
-
-class pre_sep_algebra = zero + plus +
-  fixes sep_disj :: "'a => 'a => bool" (infix "##" 60)
-
-  assumes sep_disj_zero [simp]: "x ## 0"
-  assumes sep_disj_commuteI: "x ## y \<Longrightarrow> y ## x"
-
-  assumes sep_add_zero [simp]: "x + 0 = x"
-  assumes sep_add_commute: "x ## y \<Longrightarrow> x + y = y + x"
-
-  assumes sep_add_assoc:
-    "\<lbrakk> x ## y; y ## z; x ## z \<rbrakk> \<Longrightarrow> (x + y) + z = x + (y + z)"
-begin
-
-lemma sep_disj_commute: "x ## y = y ## x"
-  by (blast intro: sep_disj_commuteI)
-
-lemma sep_add_left_commute:
-  assumes a: "a ## b" "b ## c" "a ## c"
-  shows "b + (a + c) = a + (b + c)" (is "?lhs = ?rhs")
-proof -
-  have "?lhs = b + a + c" using a
-    by (simp add: sep_add_assoc[symmetric] sep_disj_commute)
-  also have "... = a + b + c" using a
-    by (simp add: sep_add_commute sep_disj_commute)
-  also have "... = ?rhs" using a
-    by (simp add: sep_add_assoc sep_disj_commute)
-  finally show ?thesis .
-qed
-
-lemmas sep_add_ac = sep_add_assoc sep_add_commute sep_add_left_commute
-                    sep_disj_commute (* nearly always necessary *)
-
-end
-
-
-section {* Separation Algebra as Defined by Calcagno et al. *}
-
-class sep_algebra = pre_sep_algebra +
-  assumes sep_disj_addD1: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## y"
-  assumes sep_disj_addI1: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x + y ##  z"
-begin
-
-subsection {* Basic Construct Definitions and Abbreviations *}
-
-definition
-  sep_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "**" 35)
-  where
-  "P ** Q \<equiv> \<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> P x \<and> Q y"
-
-notation
-  sep_conj (infixr "\<and>*" 35)
-
-definition
-  sep_empty :: "'a \<Rightarrow> bool" ("\<box>") where
-  "\<box> \<equiv> \<lambda>h. h = 0"
-
-definition
-  sep_impl :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "\<longrightarrow>*" 25)
-  where
-  "P \<longrightarrow>* Q \<equiv> \<lambda>h. \<forall>h'. h ## h' \<and> P h' \<longrightarrow> Q (h + h')"
-
-definition
-  sep_substate :: "'a => 'a => bool" (infix "\<preceq>" 60) where
-  "x \<preceq> y \<equiv> \<exists>z. x ## z \<and> x + z = y"
-
-(* We want these to be abbreviations not definitions, because basic True and
-   False will occur by simplification in sep_conj terms *)
-abbreviation
-  "sep_true \<equiv> \<langle>True\<rangle>"
-
-abbreviation
-  "sep_false \<equiv> \<langle>False\<rangle>"
-
-definition
-  sep_list_conj :: "('a \<Rightarrow> bool) list \<Rightarrow> ('a \<Rightarrow> bool)"  ("\<And>* _" [60] 90) where
-  "sep_list_conj Ps \<equiv> foldl (op **) \<box> Ps"
-
-
-subsection {* Disjunction/Addition Properties *}
-
-lemma disjoint_zero_sym [simp]: "0 ## x"
-  by (simp add: sep_disj_commute)
-
-lemma sep_add_zero_sym [simp]: "0 + x = x"
-  by (simp add: sep_add_commute)
-
-lemma sep_disj_addD2: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## z"
-  by (metis sep_disj_addD1 sep_add_ac)
-
-lemma sep_disj_addD: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## y \<and> x ## z"
-  by (metis sep_disj_addD1 sep_disj_addD2)
-
-lemma sep_add_disjD: "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## z \<and> y ## z"
-  by (metis sep_disj_addD sep_disj_commuteI)
-
-lemma sep_disj_addI2:
-  "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x + z ## y"
-  by (metis sep_add_ac sep_disj_addI1)
-
-lemma sep_add_disjI1:
-  "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x + z ## y"
-  by (metis sep_add_ac sep_add_disjD sep_disj_addI2)
-
-lemma sep_add_disjI2:
-  "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> z + y ## x"
-  by (metis sep_add_ac sep_add_disjD sep_disj_addI2)
-
-lemma sep_disj_addI3:
-   "x + y ## z \<Longrightarrow> x ## y \<Longrightarrow> x ## y + z"
-   by (metis sep_add_ac sep_add_disjD sep_add_disjI2)
-
-lemma sep_disj_add:
-  "\<lbrakk> y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## y + z = x + y ## z"
-  by (metis sep_disj_addI1 sep_disj_addI3)
-
-
-subsection {* Substate Properties *}
-
-lemma sep_substate_disj_add:
-  "x ## y \<Longrightarrow> x \<preceq> x + y"
-  unfolding sep_substate_def by blast
-
-lemma sep_substate_disj_add':
-  "x ## y \<Longrightarrow> x \<preceq> y + x"
-  by (simp add: sep_add_ac sep_substate_disj_add)
-
-
-subsection {* Separating Conjunction Properties *}
-
-lemma sep_conjD:
-  "(P \<and>* Q) h \<Longrightarrow> \<exists>x y. x ## y \<and> h = x + y \<and> P x \<and> Q y"
-  by (simp add: sep_conj_def)
-
-lemma sep_conjE:
-  "\<lbrakk> (P ** Q) h; \<And>x y. \<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> X \<rbrakk> \<Longrightarrow> X"
-  by (auto simp: sep_conj_def)
-
-lemma sep_conjI:
-  "\<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> (P ** Q) h"
-  by (auto simp: sep_conj_def)
-
-lemma sep_conj_commuteI:
-  "(P ** Q) h \<Longrightarrow> (Q ** P) h"
-  by (auto intro!: sep_conjI elim!: sep_conjE simp: sep_add_ac)
-
-lemma sep_conj_commute:
-  "(P ** Q) = (Q ** P)"
-  by (rule ext) (auto intro: sep_conj_commuteI)
-
-lemma sep_conj_assoc:
-  "((P ** Q) ** R) = (P ** Q ** R)" (is "?lhs = ?rhs")
-proof (rule ext, rule iffI)
-  fix h
-  assume a: "?lhs h"
-  then obtain x y z where "P x" and "Q y" and "R z"
-                      and "x ## y" and "x ## z" and "y ## z" and "x + y ## z"
-                      and "h = x + y + z"
-    by (auto dest!: sep_conjD dest: sep_add_disjD)
-  moreover
-  then have "x ## y + z"
-    by (simp add: sep_disj_add)
-  ultimately
-  show "?rhs h"
-    by (auto simp: sep_add_ac intro!: sep_conjI)
-next
-  fix h
-  assume a: "?rhs h"
-  then obtain x y z where "P x" and "Q y" and "R z"
-                      and "x ## y" and "x ## z" and "y ## z" and "x ## y + z"
-                      and "h = x + y + z"
-    by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD)
-  thus "?lhs h"
-    by (metis sep_conj_def sep_disj_addI1)
-qed
-
-lemma sep_conj_impl:
-  "\<lbrakk> (P ** Q) h; \<And>h. P h \<Longrightarrow> P' h; \<And>h. Q h \<Longrightarrow> Q' h \<rbrakk> \<Longrightarrow> (P' ** Q') h"
-  by (erule sep_conjE, auto intro!: sep_conjI)
-
-lemma sep_conj_impl1:
-  assumes P: "\<And>h. P h \<Longrightarrow> I h"
-  shows "(P ** R) h \<Longrightarrow> (I ** R) h"
-  by (auto intro: sep_conj_impl P)
-
-lemma sep_globalise:
-  "\<lbrakk> (P ** R) h; (\<And>h. P h \<Longrightarrow> Q h) \<rbrakk> \<Longrightarrow> (Q ** R) h"
-  by (fast elim: sep_conj_impl)
-
-lemma sep_conj_trivial_strip2:
-  "Q = R \<Longrightarrow> (Q ** P) = (R ** P)" by simp
-
-lemma disjoint_subheaps_exist:
-  "\<exists>x y. x ## y \<and> h = x + y"
-  by (rule_tac x=0 in exI, auto)
-
-lemma sep_conj_left_commute: (* for permutative rewriting *)
-  "(P ** (Q ** R)) = (Q ** (P ** R))" (is "?x = ?y")
-proof -
-  have "?x = ((Q ** R) ** P)" by (simp add: sep_conj_commute)
-  also have "\<dots> = (Q ** (R ** P))" by (subst sep_conj_assoc, simp)
-  finally show ?thesis by (simp add: sep_conj_commute)
-qed
-
-lemmas sep_conj_ac = sep_conj_commute sep_conj_assoc sep_conj_left_commute
-
-lemma ab_semigroup_mult_sep_conj: "class.ab_semigroup_mult op **"
-  by (unfold_locales)
-     (auto simp: sep_conj_ac)
-
-lemma sep_empty_zero [simp,intro!]: "\<box> 0"
-  by (simp add: sep_empty_def)
-
-
-subsection {* Properties of @{text sep_true} and @{text sep_false} *}
-
-lemma sep_conj_sep_true:
-  "P h \<Longrightarrow> (P ** sep_true) h"
-  by (simp add: sep_conjI[where y=0])
-
-lemma sep_conj_sep_true':
-  "P h \<Longrightarrow> (sep_true ** P) h"
-  by (simp add: sep_conjI[where x=0])
-
-lemma sep_conj_true [simp]:
-  "(sep_true ** sep_true) = sep_true"
-  unfolding sep_conj_def
-  by (auto intro!: ext intro: disjoint_subheaps_exist)
-
-lemma sep_conj_false_right [simp]:
-  "(P ** sep_false) = sep_false"
-  by (force elim: sep_conjE intro!: ext)
-
-lemma sep_conj_false_left [simp]:
-  "(sep_false ** P) = sep_false"
-  by (subst sep_conj_commute) (rule sep_conj_false_right)
-
-
-
-subsection {* Properties of zero (@{const sep_empty}) *}
-
-lemma sep_conj_empty [simp]:
-  "(P ** \<box>) = P"
-  by (simp add: sep_conj_def sep_empty_def)
-
-lemma sep_conj_empty'[simp]:
-  "(\<box> ** P) = P"
-  by (subst sep_conj_commute, rule sep_conj_empty)
-
-lemma sep_conj_sep_emptyI:
-  "P h \<Longrightarrow> (P ** \<box>) h"
-  by simp
-
-lemma sep_conj_sep_emptyE:
-  "\<lbrakk> P s; (P ** \<box>) s \<Longrightarrow> (Q ** R) s \<rbrakk> \<Longrightarrow> (Q ** R) s"
-  by simp
-
-lemma monoid_add: "class.monoid_add (op **) \<box>"
-  by (unfold_locales) (auto simp: sep_conj_ac)
-
-lemma comm_monoid_add: "class.comm_monoid_add op ** \<box>"
-  by (unfold_locales) (auto simp: sep_conj_ac)
-
-
-subsection {* Properties of top (@{text sep_true}) *}
-
-lemma sep_conj_true_P [simp]:
-  "(sep_true ** (sep_true ** P)) = (sep_true ** P)"
-  by (simp add: sep_conj_assoc[symmetric])
-
-lemma sep_conj_disj:
-  "((P or Q) ** R) = ((P ** R) or (Q ** R))"
-  by (auto simp: sep_conj_def intro!: ext)
-
-lemma sep_conj_sep_true_left:
-  "(P ** Q) h \<Longrightarrow> (sep_true ** Q) h"
-  by (erule sep_conj_impl, simp+)
-
-lemma sep_conj_sep_true_right:
-  "(P ** Q) h \<Longrightarrow> (P ** sep_true) h"
-  by (subst (asm) sep_conj_commute, drule sep_conj_sep_true_left,
-      simp add: sep_conj_ac)
-
-
-subsection {* Separating Conjunction with Quantifiers *}
-
-lemma sep_conj_conj:
-  "((P and Q) ** R) h \<Longrightarrow> ((P ** R) and (Q ** R)) h"
-  by (force intro: sep_conjI elim!: sep_conjE)
-
-lemma sep_conj_exists1:
-  "((EXS x. P x) ** Q) = (EXS x. (P x ** Q))"
-  by (unfold pred_ex_def, force intro!: ext intro: sep_conjI elim: sep_conjE)
-
-lemma sep_conj_exists2:
-  "(P ** (EXS x. Q x)) = (EXS x. P ** Q x)"
-  by (unfold pred_ex_def, force intro!: sep_conjI ext elim!: sep_conjE)
-
-lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2
-
-lemma sep_conj_spec:
-  "((ALLS x. P x) ** Q) h \<Longrightarrow> (P x ** Q) h"
-  by (force intro: sep_conjI elim: sep_conjE)
-
-
-subsection {* Properties of Separating Implication *}
-
-lemma sep_implI:
-  assumes a: "\<And>h'. \<lbrakk> h ## h'; P h' \<rbrakk> \<Longrightarrow> Q (h + h')"
-  shows "(P \<longrightarrow>* Q) h"
-  unfolding sep_impl_def by (auto elim: a)
-
-lemma sep_implD:
-  "(x \<longrightarrow>* y) h \<Longrightarrow> \<forall>h'. h ## h' \<and> x h' \<longrightarrow> y (h + h')"
-  by (force simp: sep_impl_def)
-
-lemma sep_implE:
-  "(x \<longrightarrow>* y) h \<Longrightarrow> (\<forall>h'. h ## h' \<and> x h' \<longrightarrow> y (h + h') \<Longrightarrow> Q) \<Longrightarrow> Q"
-  by (auto dest: sep_implD)
-
-lemma sep_impl_sep_true [simp]:
-  "(P \<longrightarrow>* sep_true) = sep_true"
-  by (force intro!: sep_implI ext)
-
-lemma sep_impl_sep_false [simp]:
-  "(sep_false \<longrightarrow>* P) = sep_true"
-  by (force intro!: sep_implI ext)
-
-lemma sep_impl_sep_true_P:
-  "(sep_true \<longrightarrow>* P) h \<Longrightarrow> P h"
-  by (clarsimp dest!: sep_implD elim!: allE[where x=0])
-
-lemma sep_impl_sep_true_false [simp]:
-  "(sep_true \<longrightarrow>* sep_false) = sep_false"
-  by (force intro!: ext dest: sep_impl_sep_true_P)
-
-lemma sep_conj_sep_impl:
-  "\<lbrakk> P h; \<And>h. (P ** Q) h \<Longrightarrow> R h \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>* R) h"
-proof (rule sep_implI)
-  fix h' h
-  assume "P h" and "h ## h'" and "Q h'"
-  hence "(P ** Q) (h + h')" by (force intro: sep_conjI)
-  moreover assume "\<And>h. (P ** Q) h \<Longrightarrow> R h"
-  ultimately show "R (h + h')" by simp
-qed
-
-lemma sep_conj_sep_impl2:
-  "\<lbrakk> (P ** Q) h; \<And>h. P h \<Longrightarrow> (Q \<longrightarrow>* R) h \<rbrakk> \<Longrightarrow> R h"
-  by (force dest: sep_implD elim: sep_conjE)
-
-lemma sep_conj_sep_impl_sep_conj2:
-  "(P ** R) h \<Longrightarrow> (P ** (Q \<longrightarrow>* (Q ** R))) h"
-  by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac)
-
-
-subsection {* Pure assertions *}
-
-definition
-  pure :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "pure P \<equiv> \<forall>h h'. P h = P h'"
-
-lemma pure_sep_true:
-  "pure sep_true"
-  by (simp add: pure_def)
-
-lemma pure_sep_false:
-  "pure sep_true"
-  by (simp add: pure_def)
-
-lemma pure_split:
-  "pure P = (P = sep_true \<or> P = sep_false)"
-  by (force simp: pure_def intro!: ext)
-
-lemma pure_sep_conj:
-  "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<and>* Q)"
-  by (force simp: pure_split)
-
-lemma pure_sep_impl:
-  "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<longrightarrow>* Q)"
-  by (force simp: pure_split)
-
-lemma pure_conj_sep_conj:
-  "\<lbrakk> (P and Q) h; pure P \<or> pure Q \<rbrakk> \<Longrightarrow> (P \<and>* Q) h"
-  by (metis pure_def sep_add_zero sep_conjI sep_conj_commute sep_disj_zero)
-
-lemma pure_sep_conj_conj:
-  "\<lbrakk> (P \<and>* Q) h; pure P; pure Q \<rbrakk> \<Longrightarrow> (P and Q) h"
-  by (force simp: pure_split)
-
-lemma pure_conj_sep_conj_assoc:
-  "pure P \<Longrightarrow> ((P and Q) \<and>* R) = (P and (Q \<and>* R))"
-  by (auto simp: pure_split)
-
-lemma pure_sep_impl_impl:
-  "\<lbrakk> (P \<longrightarrow>* Q) h; pure P \<rbrakk> \<Longrightarrow> P h \<longrightarrow> Q h"
-  by (force simp: pure_split dest: sep_impl_sep_true_P)
-
-lemma pure_impl_sep_impl:
-  "\<lbrakk> P h \<longrightarrow> Q h; pure P; pure Q \<rbrakk> \<Longrightarrow> (P \<longrightarrow>* Q) h"
-  by (force simp: pure_split)
-
-lemma pure_conj_right: "(Q \<and>* (\<langle>P'\<rangle> and Q')) = (\<langle>P'\<rangle> and (Q \<and>* Q'))"
-  by (rule ext, rule, rule, clarsimp elim!: sep_conjE)
-     (erule sep_conj_impl, auto)
-
-lemma pure_conj_right': "(Q \<and>* (P' and \<langle>Q'\<rangle>)) = (\<langle>Q'\<rangle> and (Q \<and>* P'))"
-  by (simp add: conj_comms pure_conj_right)
-
-lemma pure_conj_left: "((\<langle>P'\<rangle> and Q') \<and>* Q) = (\<langle>P'\<rangle> and (Q' \<and>* Q))"
-  by (simp add: pure_conj_right sep_conj_ac)
-
-lemma pure_conj_left': "((P' and \<langle>Q'\<rangle>) \<and>* Q) = (\<langle>Q'\<rangle> and (P' \<and>* Q))"
-  by (subst conj_comms, subst pure_conj_left, simp)
-
-lemmas pure_conj = pure_conj_right pure_conj_right' pure_conj_left
-    pure_conj_left'
-
-declare pure_conj[simp add]
-
-
-subsection {* Intuitionistic assertions *}
-
-definition intuitionistic :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "intuitionistic P \<equiv> \<forall>h h'. P h \<and> h \<preceq> h' \<longrightarrow> P h'"
-
-lemma intuitionisticI:
-  "(\<And>h h'. \<lbrakk> P h; h \<preceq> h' \<rbrakk> \<Longrightarrow> P h') \<Longrightarrow> intuitionistic P"
-  by (unfold intuitionistic_def, fast)
-
-lemma intuitionisticD:
-  "\<lbrakk> intuitionistic P; P h; h \<preceq> h' \<rbrakk> \<Longrightarrow> P h'"
-  by (unfold intuitionistic_def, fast)
-
-lemma pure_intuitionistic:
-  "pure P \<Longrightarrow> intuitionistic P"
-  by (clarsimp simp: intuitionistic_def pure_def, fast)
-
-lemma intuitionistic_conj:
-  "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P and Q)"
-  by (force intro: intuitionisticI dest: intuitionisticD)
-
-lemma intuitionistic_disj:
-  "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P or Q)"
-  by (force intro: intuitionisticI dest: intuitionisticD)
-
-lemma intuitionistic_forall:
-  "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (ALLS x. P x)"
-  by (force intro: intuitionisticI dest: intuitionisticD)
-
-lemma intuitionistic_exists:
-  "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (EXS x. P x)"
-  by (unfold pred_ex_def, force intro: intuitionisticI dest: intuitionisticD)
-
-lemma intuitionistic_sep_conj_sep_true:
-  "intuitionistic (sep_true \<and>* P)"
-proof (rule intuitionisticI)
-  fix h h' r
-  assume a: "(sep_true \<and>* P) h"
-  then obtain x y where P: "P y" and h: "h = x + y" and xyd: "x ## y"
-    by - (drule sep_conjD, clarsimp)
-  moreover assume a2: "h \<preceq> h'"
-  then obtain z where h': "h' = h + z" and hzd: "h ## z"
-    by (clarsimp simp: sep_substate_def)
-
-  moreover have "(P \<and>* sep_true) (y + (x + z))"
-    using P h hzd xyd
-    by (metis sep_add_disjI1 sep_disj_commute sep_conjI)
-  ultimately show "(sep_true \<and>* P) h'" using hzd
-    by (auto simp: sep_conj_commute sep_add_ac dest!: sep_disj_addD)
-qed
-
-lemma intuitionistic_sep_impl_sep_true:
-  "intuitionistic (sep_true \<longrightarrow>* P)"
-proof (rule intuitionisticI)
-  fix h h'
-  assume imp: "(sep_true \<longrightarrow>* P) h" and hh': "h \<preceq> h'"
-
-  from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"
-    by (clarsimp simp: sep_substate_def)
-  show "(sep_true \<longrightarrow>* P) h'" using imp h' hzd
-    apply (clarsimp dest!: sep_implD)
-    apply (metis sep_add_assoc sep_add_disjD sep_disj_addI3 sep_implI)
-    done
-qed
-
-lemma intuitionistic_sep_conj:
-  assumes ip: "intuitionistic (P::('a \<Rightarrow> bool))"
-  shows "intuitionistic (P \<and>* Q)"
-proof (rule intuitionisticI)
-  fix h h'
-  assume sc: "(P \<and>* Q) h" and hh': "h \<preceq> h'"
-
-  from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"
-    by (clarsimp simp: sep_substate_def)
-
-  from sc obtain x y where px: "P x" and qy: "Q y"
-                       and h: "h = x + y" and xyd: "x ## y"
-    by (clarsimp simp: sep_conj_def)
-
-  have "x ## z" using hzd h xyd
-    by (metis sep_add_disjD)
-
-  with ip px have "P (x + z)"
-    by (fastforce elim: intuitionisticD sep_substate_disj_add)
-
-  thus "(P \<and>* Q) h'" using h' h hzd qy xyd
-    by (metis (full_types) sep_add_commute sep_add_disjD sep_add_disjI2
-              sep_add_left_commute sep_conjI)
-qed
-
-lemma intuitionistic_sep_impl:
-  assumes iq: "intuitionistic Q"
-  shows "intuitionistic (P \<longrightarrow>* Q)"
-proof (rule intuitionisticI)
-  fix h h'
-  assume imp: "(P \<longrightarrow>* Q) h" and hh': "h \<preceq> h'"
-
-  from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"
-    by (clarsimp simp: sep_substate_def)
-
-  {
-    fix x
-    assume px: "P x" and hzx: "h + z ## x"
-
-    have "h + x \<preceq> h + x + z" using hzx hzd
-    by (metis sep_add_disjI1 sep_substate_def)
-
-    with imp hzd iq px hzx
-    have "Q (h + z + x)"
-    by (metis intuitionisticD sep_add_assoc sep_add_ac sep_add_disjD sep_implE)
-  }
-
-  with imp h' hzd iq show "(P \<longrightarrow>* Q) h'"
-    by (fastforce intro: sep_implI)
-qed
-
-lemma strongest_intuitionistic:
-  "\<not> (\<exists>Q. (\<forall>h. (Q h \<longrightarrow> (P \<and>* sep_true) h)) \<and> intuitionistic Q \<and>
-      Q \<noteq> (P \<and>* sep_true) \<and> (\<forall>h. P h \<longrightarrow> Q h))"
-  by (fastforce intro!: ext sep_substate_disj_add
-                dest!: sep_conjD intuitionisticD)
-
-lemma weakest_intuitionistic:
-  "\<not> (\<exists>Q. (\<forall>h. ((sep_true \<longrightarrow>* P) h \<longrightarrow> Q h)) \<and> intuitionistic Q \<and>
-      Q \<noteq> (sep_true \<longrightarrow>* P) \<and> (\<forall>h. Q h \<longrightarrow> P h))"
-  apply (clarsimp intro!: ext)
-  apply (rule iffI)
-   apply (rule sep_implI)
-   apply (drule_tac h="x" and h'="x + h'" in intuitionisticD)
-     apply (clarsimp simp: sep_add_ac sep_substate_disj_add)+
-  done
-
-lemma intuitionistic_sep_conj_sep_true_P:
-  "\<lbrakk> (P \<and>* sep_true) s; intuitionistic P \<rbrakk> \<Longrightarrow> P s"
-  by (force dest: intuitionisticD elim: sep_conjE sep_substate_disj_add)
-
-lemma intuitionistic_sep_conj_sep_true_simp:
-  "intuitionistic P \<Longrightarrow> (P \<and>* sep_true) = P"
-  by (fast intro!: sep_conj_sep_true ext
-           elim: intuitionistic_sep_conj_sep_true_P)
-
-lemma intuitionistic_sep_impl_sep_true_P:
-  "\<lbrakk> P h; intuitionistic P \<rbrakk> \<Longrightarrow> (sep_true \<longrightarrow>* P) h"
-  by (force intro!: sep_implI dest: intuitionisticD
-            intro: sep_substate_disj_add)
-
-lemma intuitionistic_sep_impl_sep_true_simp:
-  "intuitionistic P \<Longrightarrow> (sep_true \<longrightarrow>* P) = P"
-  by (fast intro!: ext
-           elim: sep_impl_sep_true_P intuitionistic_sep_impl_sep_true_P)
-
-
-subsection {* Strictly exact assertions *}
-
-definition strictly_exact :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "strictly_exact P \<equiv> \<forall>h h'. P h \<and> P h' \<longrightarrow> h = h'"
-
-lemma strictly_exactD:
-  "\<lbrakk> strictly_exact P; P h; P h' \<rbrakk> \<Longrightarrow> h = h'"
-  by (unfold strictly_exact_def, fast)
-
-lemma strictly_exactI:
-  "(\<And>h h'. \<lbrakk> P h; P h' \<rbrakk> \<Longrightarrow> h = h') \<Longrightarrow> strictly_exact P"
-  by (unfold strictly_exact_def, fast)
-
-lemma strictly_exact_sep_conj:
-  "\<lbrakk> strictly_exact P; strictly_exact Q \<rbrakk> \<Longrightarrow> strictly_exact (P \<and>* Q)"
-  apply (rule strictly_exactI)
-  apply (erule sep_conjE)+
-  apply (drule_tac h="x" and h'="xa" in strictly_exactD, assumption+)
-  apply (drule_tac h="y" and h'="ya" in strictly_exactD, assumption+)
-  apply clarsimp
-  done
-
-lemma strictly_exact_conj_impl:
-  "\<lbrakk> (Q \<and>* sep_true) h; P h; strictly_exact Q \<rbrakk> \<Longrightarrow> (Q \<and>* (Q \<longrightarrow>* P)) h"
-  by (force intro: sep_conjI sep_implI dest: strictly_exactD elim!: sep_conjE
-            simp: sep_add_commute sep_add_assoc)
-
-end
-
-interpretation sep: ab_semigroup_mult "op **"
-  by (rule ab_semigroup_mult_sep_conj)
-
-interpretation sep: comm_monoid_add "op **" \<box>
-  by (rule comm_monoid_add)
-
-
-section {* Separation Algebra with Stronger, but More Intuitive Disjunction Axiom *}
-
-class stronger_sep_algebra = pre_sep_algebra +
-  assumes sep_add_disj_eq [simp]: "y ## z \<Longrightarrow> x ## y + z = (x ## y \<and> x ## z)"
-begin
-
-lemma sep_disj_add_eq [simp]: "x ## y \<Longrightarrow> x + y ## z = (x ## z \<and> y ## z)"
-  by (metis sep_add_disj_eq sep_disj_commute)
-
-subclass sep_algebra by default auto
-
-end
-
-
-section {* Folding separating conjunction over lists of predicates *}
-
-lemma sep_list_conj_Nil [simp]: "\<And>* [] = \<box>"
-  by (simp add: sep_list_conj_def)
-
-(* apparently these two are rarely used and had to be removed from List.thy *)
-lemma (in semigroup_add) foldl_assoc:
-shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
-by (induct zs arbitrary: y) (simp_all add:add_assoc)
-
-lemma (in monoid_add) foldl_absorb0:
-shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
-by (induct zs) (simp_all add:foldl_assoc)
-
-lemma sep_list_conj_Cons [simp]: "\<And>* (x#xs) = (x ** \<And>* xs)"
-  by (simp add: sep_list_conj_def sep.foldl_absorb0)
-
-lemma sep_list_conj_append [simp]: "\<And>* (xs @ ys) = (\<And>* xs ** \<And>* ys)"
-  by (simp add: sep_list_conj_def sep.foldl_absorb0)
-
-lemma (in comm_monoid_add) foldl_map_filter:
-  "foldl op + 0 (map f (filter P xs)) +
-     foldl op + 0 (map f (filter (not P) xs))
-   = foldl op + 0 (map f xs)"
-proof (induct xs)
-  case Nil thus ?case by clarsimp
-next
-  case (Cons x xs)
-  hence IH: "foldl op + 0 (map f xs) =
-               foldl op + 0 (map f (filter P xs)) +
-               foldl op + 0 (map f [x\<leftarrow>xs . \<not> P x])"
-               by (simp only: eq_commute)
-
-  have foldl_Cons':
-    "\<And>x xs. foldl op + 0 (x # xs) = x + (foldl op + 0 xs)"
-    by (simp, subst foldl_absorb0[symmetric], rule refl)
-
-  { assume "P x"
-    hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH add_ac)
-  } moreover {
-    assume "\<not> P x"
-    hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH add_ac)
-  }
-  ultimately show ?case by blast
-qed
-
-
-section {* Separation Algebra with a Cancellative Monoid (for completeness) *}
-
-text {*
-  Separation algebra with a cancellative monoid. The results of being a precise
-  assertion (distributivity over separating conjunction) require this.
-  although we never actually use this property in our developments, we keep
-  it here for completeness.
-  *}
-class cancellative_sep_algebra = sep_algebra +
-  assumes sep_add_cancelD: "\<lbrakk> x + z = y + z ; x ## z ; y ## z \<rbrakk> \<Longrightarrow> x = y"
-begin
-
-definition
-  (* In any heap, there exists at most one subheap for which P holds *)
-  precise :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "precise P = (\<forall>h hp hp'. hp \<preceq> h \<and> P hp \<and> hp' \<preceq> h \<and> P hp' \<longrightarrow> hp = hp')"
-
-lemma "precise (op = s)"
-  by (metis (full_types) precise_def)
-
-lemma sep_add_cancel:
-  "x ## z \<Longrightarrow> y ## z \<Longrightarrow> (x + z = y + z) = (x = y)"
-  by (metis sep_add_cancelD)
-
-lemma precise_distribute:
-  "precise P = (\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P)))"
-proof (rule iffI)
-  assume pp: "precise P"
-  {
-    fix Q R
-    fix h hp hp' s
-
-    { assume a: "((Q and R) \<and>* P) s"
-      hence "((Q \<and>* P) and (R \<and>* P)) s"
-        by (fastforce dest!: sep_conjD elim: sep_conjI)
-    }
-    moreover
-    { assume qs: "(Q \<and>* P) s" and qr: "(R \<and>* P) s"
-
-      from qs obtain x y where sxy: "s = x + y" and xy: "x ## y"
-                           and x: "Q x" and y: "P y"
-        by (fastforce dest!: sep_conjD)
-      from qr obtain x' y' where sxy': "s = x' + y'" and xy': "x' ## y'"
-                           and x': "R x'" and y': "P y'"
-        by (fastforce dest!: sep_conjD)
-
-      from sxy have ys: "y \<preceq> x + y" using xy
-        by (fastforce simp: sep_substate_disj_add' sep_disj_commute)
-      from sxy' have ys': "y' \<preceq> x' + y'" using xy'
-        by (fastforce simp: sep_substate_disj_add' sep_disj_commute)
-
-      from pp have yy: "y = y'" using sxy sxy' xy xy' y y' ys ys'
-        by (fastforce simp: precise_def)
-
-      hence "x = x'" using sxy sxy' xy xy'
-        by (fastforce dest!: sep_add_cancelD)
-
-      hence "((Q and R) \<and>* P) s" using sxy x x' yy y' xy'
-        by (fastforce intro: sep_conjI)
-    }
-    ultimately
-    have "((Q and R) \<and>* P) s = ((Q \<and>* P) and (R \<and>* P)) s" using pp by blast
-  }
-  thus "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))" by (blast intro!: ext)
-
-next
-  assume a: "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))"
-  thus "precise P"
-  proof (clarsimp simp: precise_def)
-    fix h hp hp' Q R
-    assume hp: "hp \<preceq> h" and hp': "hp' \<preceq> h" and php: "P hp" and php': "P hp'"
-
-    obtain z where hhp: "h = hp + z" and hpz: "hp ## z" using hp
-      by (clarsimp simp: sep_substate_def)
-    obtain z' where hhp': "h = hp' + z'" and hpz': "hp' ## z'" using hp'
-      by (clarsimp simp: sep_substate_def)
-
-    have h_eq: "z' + hp' = z + hp" using hhp hhp' hpz hpz'
-      by (fastforce simp: sep_add_ac)
-
-    from hhp hhp' a hpz hpz' h_eq
-    have "\<forall>Q R. ((Q and R) \<and>* P) (z + hp) = ((Q \<and>* P) and (R \<and>* P)) (z' + hp')"
-      by (fastforce simp: h_eq sep_add_ac sep_conj_commute)
-
-    hence "((op = z and op = z') \<and>* P) (z + hp) =
-           ((op = z \<and>* P) and (op = z' \<and>* P)) (z' + hp')" by blast
-
-    thus  "hp = hp'" using php php' hpz hpz' h_eq
-      by (fastforce dest!: iffD2 cong: conj_cong
-                    simp: sep_add_ac sep_add_cancel sep_conj_def)
-  qed
-qed
-
-lemma strictly_precise: "strictly_exact P \<Longrightarrow> precise P"
-  by (metis precise_def strictly_exactD)
-
-end
-
-end
diff -r a5f5b9336007 -r 1cde7bf45858 Separation_Algebra/ex/Sep_Tactics_Test.thy~
--- a/Separation_Algebra/ex/Sep_Tactics_Test.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,122 +0,0 @@
-(* Authors: Gerwin Klein and Rafal Kolanski, 2012
-   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
-                Rafal Kolanski <rafal.kolanski at nicta.com.au>
-*)
-
-theory Sep_Tactics_Test
-imports "../Sep_Tactics"
-begin
-
-text {* Substitution and forward/backward reasoning *}
-
-typedecl p
-typedecl val
-typedecl heap
-
-arities heap :: sep_algebra
-
-axiomatization
-  points_to :: "p \<Rightarrow> val \<Rightarrow> heap \<Rightarrow> bool" and
-  val :: "heap \<Rightarrow> p \<Rightarrow> val"
-where
-  points_to: "(points_to p v ** P) h \<Longrightarrow> val h p = v"
-
-
-lemma
-  "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>
-   \<Longrightarrow> Q (val h p) (val h p)"
-  apply (sep_subst (2) points_to)
-  apply (sep_subst (asm) points_to)
-  apply (sep_subst points_to)
-  oops
-
-lemma
-  "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>
-   \<Longrightarrow> Q (val h p) (val h p)"
-  apply (sep_drule points_to)
-  apply simp
-  oops
-
-lemma
-  "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>
-   \<Longrightarrow> Q (val h p) (val h p)"
-  apply (sep_frule points_to)
-  apply simp
-  oops
-
-consts
-  update :: "p \<Rightarrow> val \<Rightarrow> heap \<Rightarrow> heap"
-
-schematic_lemma
-  assumes a: "\<And>P. (stuff p ** P) H \<Longrightarrow> (other_stuff p v ** P) (update p v H)"
-  shows "(X ** Y ** other_stuff p ?v) (update p v H)"
-  apply (sep_rule a)
-  oops
-
-
-text {* Example of low-level rewrites *}
-
-lemma "\<lbrakk> unrelated s ; (P ** Q ** R) s \<rbrakk> \<Longrightarrow> (A ** B ** Q ** P) s"
-  apply (tactic {* dtac (mk_sep_select_rule @{context} true (3,1)) 1 *})
-  apply (tactic {* rtac (mk_sep_select_rule @{context} false (4,2)) 1 *})
-  (* now sep_conj_impl1 can be used *)
-  apply (erule (1) sep_conj_impl)
-  oops
-
-
-text {* Conjunct selection *}
-
-lemma "(A ** B ** Q ** P) s"
-  apply (sep_select 1)
-  apply (sep_select 3)
-  apply (sep_select 4)
-  oops
-
-lemma "\<lbrakk> also unrelated; (A ** B ** Q ** P) s \<rbrakk> \<Longrightarrow> unrelated"
-  apply (sep_select_asm 2)
-  oops
-
-
-section {* Test cases for @{text sep_cancel}. *}
-
-lemma
-  assumes forward: "\<And>s g p v. A g p v s \<Longrightarrow> AA g p s "
-  shows "\<And>xv yv P s y x s. (A g x yv ** A g y yv ** P) s \<Longrightarrow> (AA g y ** sep_true) s"
-  by (sep_cancel add: forward)
-
-lemma
-  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
-  shows "(A ** generic ** B) s \<Longrightarrow> (instance ** sep_true) s"
-  by (sep_cancel add: forward)
-
-lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (A ** X) s"
-  apply (sep_cancel)
-  oops
-
-lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (\<lambda>s. (A ** X) s) s"
-  apply (sep_cancel)
-  oops
-
-schematic_lemma "\<lbrakk> (B ** A ** C) s \<rbrakk> \<Longrightarrow> (\<lambda>s. (A ** ?X) s) s"
-  by (sep_cancel)
-
-(* test backtracking on premises with same state *)
-lemma
-  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
-  shows "\<lbrakk> (A ** B) s ; (generic ** Y) s \<rbrakk> \<Longrightarrow> (X ** instance) s"
-  apply (sep_cancel add: forward)
-  oops
-
-lemma
-  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
-  shows "generic s \<Longrightarrow> instance s"
-  by (sep_cancel add: forward)
-
-lemma
-  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
-  assumes forward2: "\<And>s. instance s \<Longrightarrow> instance2 s"
-  shows "generic s \<Longrightarrow> (instance2 ** sep_true) s"
-  by (sep_cancel_blast add: forward forward2)
-
-end
-
diff -r a5f5b9336007 -r 1cde7bf45858 Separation_Algebra/ex/Simple_Separation_Example.thy~
--- a/Separation_Algebra/ex/Simple_Separation_Example.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(* Title: Adaptation of example from HOL/Hoare/Separation
-   Author: Gerwin Klein, 2012
-   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
-                Rafal Kolanski <rafal.kolanski at nicta.com.au>
-*)
-
-header "Example from HOL/Hoare/Separation"
-
-theory Simple_Separation_Example
-  imports "~~/src/HOL/Hoare/Hoare_Logic_Abort" "../Sep_Heap_Instance"
-          "../Sep_Tactics"
-begin
-
-declare [[syntax_ambiguity_warning = false]]
-
-type_synonym heap = "(nat \<Rightarrow> nat option)"
-
-(* This syntax isn't ideal, but this is what is used in the original *)
-definition maps_to:: "nat \<Rightarrow> nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> _" [56,51] 56)
-  where "x \<mapsto> y \<equiv> \<lambda>h. h = [x \<mapsto> y]"
-
-(* If you don't mind syntax ambiguity: *)
-notation pred_ex  (binder "\<exists>" 10)
-
-(* could be generated automatically *)
-definition maps_to_ex :: "nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> -" [56] 56)
-  where "x \<mapsto> - \<equiv> \<exists>y. x \<mapsto> y"
-
-
-(* could be generated automatically *)
-lemma maps_to_maps_to_ex [elim!]:
-  "(p \<mapsto> v) s \<Longrightarrow> (p \<mapsto> -) s"
-  by (auto simp: maps_to_ex_def)
-
-(* The basic properties of maps_to: *)
-lemma maps_to_write:
-  "(p \<mapsto> - ** P) H \<Longrightarrow> (p \<mapsto> v ** P) (H (p \<mapsto> v))"
-  apply (clarsimp simp: sep_conj_def maps_to_def maps_to_ex_def split: option.splits)
-  apply (rule_tac x=y in exI)
-  apply (auto simp: sep_disj_fun_def map_convs map_add_def split: option.splits)
-  done
-
-lemma points_to:
-  "(p \<mapsto> v ** P) H \<Longrightarrow> the (H p) = v"
-  by (auto elim!: sep_conjE
-           simp: sep_disj_fun_def maps_to_def map_convs map_add_def
-           split: option.splits)
-
-
-(* This differs from the original and uses separation logic for the definition. *)
-primrec
-  list :: "nat \<Rightarrow> nat list \<Rightarrow> heap \<Rightarrow> bool"
-where
-  "list i [] = (\<langle>i=0\<rangle> and \<box>)"
-| "list i (x#xs) = (\<langle>i=x \<and> i\<noteq>0\<rangle> and (EXS j. i \<mapsto> j ** list j xs))"
-
-lemma list_empty [simp]:
-  shows "list 0 xs = (\<lambda>s. xs = [] \<and> \<box> s)"
-  by (cases xs) auto
-
-(* The examples from Hoare/Separation.thy *)
-lemma "VARS x y z w h
- {(x \<mapsto> y ** z \<mapsto> w) h}
- SKIP
- {x \<noteq> z}"
-  apply vcg
-  apply(auto elim!: sep_conjE simp: maps_to_def sep_disj_fun_def domain_conv)
-done
-
-lemma "VARS H x y z w
- {(P ** Q) H}
- SKIP
- {(Q ** P) H}"
-  apply vcg
-  apply(simp add: sep_conj_commute)
-done
-
-lemma "VARS H
- {p\<noteq>0 \<and> (p \<mapsto> - ** list q qs) H}
- H := H(p \<mapsto> q)
- {list p (p#qs) H}"
-  apply vcg
-  apply (auto intro: maps_to_write)
-done
-
-lemma "VARS H p q r
-  {(list p Ps ** list q Qs) H}
-  WHILE p \<noteq> 0
-  INV {\<exists>ps qs. (list p ps ** list q qs) H \<and> rev ps @ qs = rev Ps @ Qs}
-  DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
-  {list q (rev Ps @ Qs) H}"
-  apply vcg
-    apply fastforce
-   apply clarsimp
-   apply (case_tac ps, simp)
-   apply (rename_tac p ps')
-   apply (clarsimp simp: sep_conj_exists sep_conj_ac)
-   apply (sep_subst points_to)
-   apply (rule_tac x = "ps'" in exI)
-   apply (rule_tac x = "p # qs" in exI)
-   apply (simp add: sep_conj_exists sep_conj_ac)
-   apply (rule exI)
-   apply (sep_rule maps_to_write)
-   apply (sep_cancel)+
-   apply ((sep_cancel add: maps_to_maps_to_ex)+)[1]
-  apply clarsimp
-  done
-
-end
diff -r a5f5b9336007 -r 1cde7bf45858 progtut/Advanced.thy~
--- a/progtut/Advanced.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-theory Advanced
-imports Essential
\ No newline at end of file
diff -r a5f5b9336007 -r 1cde7bf45858 progtut/Essential.thy~
--- a/progtut/Essential.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,213 +0,0 @@
-theory Essential
-imports FirstStep
-begin
-
-ML {*
-fun pretty_helper aux env =
-  env |> Vartab.dest
-      |> map aux
-      |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2])
-      |> Pretty.enum "," "[" "]"
-      |> pwriteln
-
-fun pretty_tyenv ctxt tyenv =
-let
-  fun get_typs (v, (s, T)) = (TVar (v, s), T)
-  val print = pairself (pretty_typ ctxt)
-in
-  pretty_helper (print o get_typs) tyenv
-end
-
-fun pretty_env ctxt env =
-let
-   fun get_trms (v, (T, t)) = (Var (v, T), t)
-   val print = pairself (pretty_term ctxt)
-in
-   pretty_helper (print o get_trms) env
-end
-
-fun prep_trm thy (x, (T, t)) =
-  (cterm_of thy (Var (x, T)), cterm_of thy t)
-
-fun prep_ty thy (x, (S, ty)) =
-  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
-
-fun matcher_inst thy pat trm i =
-  let
-     val univ = Unify.matchers thy [(pat, trm)]
-     val env = nth (Seq.list_of univ) i
-     val tenv = Vartab.dest (Envir.term_env env)
-     val tyenv = Vartab.dest (Envir.type_env env)
-  in
-     (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
-  end
-*}
-
-ML {*
-  let
-     val pat = Logic.strip_imp_concl (prop_of @{thm spec})
-     val trm = @{term "Trueprop (Q True)"}
-     val inst = matcher_inst @{theory} pat trm 1
-  in
-     Drule.instantiate_normalize inst @{thm spec}
-  end
-*}
-
-ML {*
-let
-   val c = Const (@{const_name "plus"}, dummyT)
-   val o = @{term "1::nat"}
-   val v = Free ("x", dummyT)
-in
-   Syntax.check_term @{context} (c $ o $ v)
-end
-*}
-
-ML {*
-   val my_thm =
-   let
-      val assm1 = @{cprop "\<And> (x::nat). P x ==> Q x"}
-      val assm2 = @{cprop "(P::nat => bool) t"}
-
-      val Pt_implies_Qt =
-        Thm.assume assm1
-        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-        |> Thm.forall_elim @{cterm "t::nat"}
-        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-
-      val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2)
-               |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-   in
-      Qt
-      |> Thm.implies_intr assm2
-      |> Thm.implies_intr assm1
-   end
-*}
-
-local_setup {*
-  Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd  
-*}
-
-local_setup {*
-  Local_Theory.note ((@{binding "my_thm_simp"},
-        [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd
-*}
-
-(* pp 62 *)
-
-lemma
-  shows foo_test1: "A \<Longrightarrow> B \<Longrightarrow> C"
-  and   foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry
-
-ML {*
-   Thm.reflexive @{cterm "True"}
-    |> Simplifier.rewrite_rule [@{thm True_def}]
-    |> pretty_thm @{context}
-    |> pwriteln
-*}
-
-ML {*
-Object_Logic.rulify @{thm foo_test2}
-*}
-
-
-ML {*
-  val thm =    @{thm foo_test1};
-  thm 
-  |> cprop_of
-  |> Object_Logic.atomize
-  |> (fn x => Raw_Simplifier.rewrite_rule [x] thm)
-*}
-
-ML {*
-  val thm = @{thm list.induct} |> forall_intr_vars;
-  thm |> forall_intr_vars |> cprop_of |> Object_Logic.atomize
-  |> (fn x => Raw_Simplifier.rewrite_rule [x] thm)
-*}
-
-ML {*
-fun atomize_thm thm =
-let
-  val thm' = forall_intr_vars thm
-  val thm'' = Object_Logic.atomize (cprop_of thm')
-in
-  Raw_Simplifier.rewrite_rule [thm''] thm'
-end
-*}
-
-ML {*
-  @{thm list.induct} |> atomize_thm
-*}
-
-ML {*
-   Skip_Proof.make_thm @{theory} @{prop "True = False"}
-*}
-
-ML {*
-fun pthms_of (PBody {thms, ...}) = map #2 thms
-val get_names = map #1 o pthms_of
-val get_pbodies = map (Future.join o #3) o pthms_of
-*}
-
-lemma my_conjIa:
-shows "A \<and> B \<Longrightarrow> A \<and> B"
-apply(rule conjI)
-apply(drule conjunct1)
-apply(assumption)
-apply(drule conjunct2)
-apply(assumption)
-done
-
-lemma my_conjIb:
-shows "A \<and> B \<Longrightarrow> A \<and> B"
-apply(assumption)
-done
-
-lemma my_conjIc:
-shows "A \<and> B \<Longrightarrow> A \<and> B"
-apply(auto)
-done
-
-
-ML {*
-@{thm my_conjIa}
-  |> Thm.proof_body_of
-  |> get_names
-*}
-
-ML {*
-@{thm my_conjIa}
-  |> Thm.proof_body_of
-  |> get_pbodies
-  |> map get_names
-  |> List.concat
-*}
-
-ML {*
-@{thm my_conjIb}
- |> Thm.proof_body_of
- |> get_pbodies
- |> map get_names
- |> List.concat
-*}
-
-ML {*
-@{thm my_conjIc}
-  |> Thm.proof_body_of
-  |> get_pbodies
-  |> map get_names
-  |> List.concat
-*}
-
-ML {*
-@{thm my_conjIa}
-  |> Thm.proof_body_of
-  |> get_pbodies
-  |> map get_pbodies
-  |> (map o map) get_names
-  |> List.concat
-  |> List.concat
-  |> duplicates (op=)
-*}
-
-end
\ No newline at end of file
diff -r a5f5b9336007 -r 1cde7bf45858 progtut/FirstStep.thy~
--- a/progtut/FirstStep.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,173 +0,0 @@
-theory FistStep
-imports Main
-begin
-
-ML {*
-val pretty_term = Syntax.pretty_term
-val pwriteln = Pretty.writeln
-fun pretty_terms ctxt trms =
-  Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))
-val show_type_ctxt = Config.put show_types true @{context}
-val show_all_types_ctxt = Config.put show_all_types true @{context}
-fun pretty_cterm ctxt ctrm =
-  pretty_term ctxt (term_of ctrm)
-fun pretty_thm ctxt thm =
-  pretty_term ctxt (prop_of thm)
-fun pretty_thm_no_vars ctxt thm =
-let
-  val ctxt' = Config.put show_question_marks false ctxt
-in
-  pretty_term ctxt' (prop_of thm)
-end
-fun pretty_thms ctxt thms =
-  Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms))
-fun pretty_thms_no_vars ctxt thms =
-  Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))
-fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
-fun pretty_typs ctxt tys =
-  Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))
-fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
-fun pretty_ctyps ctxt ctys =
-  Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))
-fun `f = fn x => (f x, x)
-fun (x, y) |>> f = (f x, y)
-fun (x, y) ||> f = (x, f y)
-fun (x, y) |-> f = f x y
-*}
-
-ML {*
-  val _ = pretty_term @{context} @{term "x + y + z"} |> pwriteln
-  val _ = pretty_terms @{context} [@{term "x + y"}, @{term "x + y + z"}] |> pwriteln
-  val show_type_ctxt = Config.put show_types true @{context}
-  *}
-
-ML {*
-   pwriteln (pretty_term show_type_ctxt @{term "(1::nat, x)"})
-*}
-
-ML {*
-pwriteln (Pretty.str (cat_lines ["foo", "bar"]))
-*}
-
-ML {*
-  fun apply_fresh_args f ctxt =
-      f |> fastype_of
-        |> binder_types
-        |> map (pair "z")
-        |> Variable.variant_frees ctxt [f]
-        |> map Free
-        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-        |> curry list_comb f
-*}
-
-ML {*
-let
-   val trm = @{term "P::nat => int => unit => bool"}
-   val ctxt = ML_Context.the_local_context ()
-in
-   apply_fresh_args trm ctxt
-    |> pretty_term ctxt
-    |> pwriteln
-end
-*}
-
-ML {*
-  fun inc_by_three x =
-      x |> (fn x => x + 1)
-        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-        |> (fn x => x + 2)
-*}
-
-ML {*
-  fun `f = fn x => (f x, x)
-*}
-
-ML {*
-  fun inc_as_pair x =
-        x |> `(fn x => x + 1)
-       |> (fn (x, y) => (x, y + 1))
-*}
-
-ML {*
-  3 |> inc_as_pair
-*}
-
-ML {*
-  fun acc_incs x =
-      x |> (fn x => (0, x))
-        ||>> (fn x => (x, x + 1))
-        ||>> (fn x => (x, x + 1))
-        ||>> (fn x => (x, x + 1))
-*}
-
-ML {*
-  2 |> acc_incs
-*}
-
-ML {*
-let
-  val ((names1, names2), _) =
-    @{context}
-    |> Variable.variant_fixes (replicate 4 "x")
-    |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-    ||>> Variable.variant_fixes (replicate 5 "x")
-    |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-in
-  (names1, names2)
-end
-*}
-
-ML {*
-  @{context}
-  |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
-*}
-
-ML {*
-let
-   val ctxt = @{context}
-in
-   Syntax.parse_term ctxt "m + n"
-   |> singleton (Syntax.check_terms ctxt)
-   |> pretty_term ctxt
-   |> pwriteln
-end
-*}
-
-ML {*
-  val term_pat_setup =
-  let
-    val parser = Args.context -- Scan.lift Args.name_source
-      fun term_pat (ctxt, str) =
-         str |> Proof_Context.read_term_pattern ctxt
-             |> ML_Syntax.print_term
-             |> ML_Syntax.atomic
-   in
-      ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat)
-   end
-*}
-
-setup {* term_pat_setup *}
-
-
-ML {*
-val type_pat_setup =
-let
-   val parser = Args.context -- Scan.lift Args.name_source
-   fun typ_pat (ctxt, str) =
-     let
-       val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt
-     in
-       str |> Syntax.read_typ ctxt'
-           |> ML_Syntax.print_typ
-           |> ML_Syntax.atomic
-       end
-in
-   ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)
-end
-*}
-
-setup {* type_pat_setup *}
-
-end
\ No newline at end of file
diff -r a5f5b9336007 -r 1cde7bf45858 progtut/Tactical.thy~
--- a/progtut/Tactical.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-theory Tactical
-imports Advanced
-begin
-
-
-
-
-ML {*
-fun my_print_tac ctxt thm =
-let
-   val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))
-in
-   Seq.single thm
-end
-*}
-
-ML {*
-let
-   val ctxt = @{context}
-   val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
-in
-   Goal.prove ctxt ["x", "y", "u", "v", "P", "Q"] [@{prop "x = y"}, @{prop "u = v"}] goal
-    (fn {prems = pms, context = ctxt} =>  
-              (my_print_tac ctxt)
-              THEN etac @{thm disjE} 1 THEN
-               (my_print_tac ctxt) 
-              THEN rtac @{thm disjI2} 1
-              THEN  (my_print_tac ctxt) 
-              THEN atac 1
-              THEN rtac @{thm disjI1} 1
-              THEN atac 1)
-end
-*}
-
-ML {*
-  Goal.prove
-*}
-
-ML {*
-fun pretty_cterms ctxt ctrms =
-  Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))
-*}
-
-ML {*
-fun foc_tac {prems, params, asms, concl, context, schematics} =
-let
-  fun assgn1 f1 f2 xs =
-    let
-       val out = map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs
-    in
-       Pretty.list "" "" out
-    end
-  fun assgn2 f xs = assgn1 f f xs
-  val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp])
-    [("params: ", assgn1 Pretty.str (pretty_cterm context) params),
-     ("assumptions: ", pretty_cterms context asms),
-     ("conclusion: ", pretty_cterm context concl),
-     ("premises: ", pretty_thms_no_vars context prems),
-     ("schematics: ", assgn2 (pretty_cterm context) (snd schematics))]
-in
-  tracing (Pretty.string_of (Pretty.chunks pps)); all_tac
-end
-*}
-
-
-notation (output) "prop"   ("#_" [1000] 1000)
-
-lemma
-  shows " \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
-apply(tactic {* my_print_tac @{context} *})
-apply(rule conjI)
-apply(tactic {* my_print_tac @{context} *})
-apply(assumption)
-apply(tactic {* my_print_tac @{context} *})
-apply(assumption)
-apply(tactic {* my_print_tac @{context} *})
diff -r a5f5b9336007 -r 1cde7bf45858 progtut/progtut.thy~
diff -r a5f5b9336007 -r 1cde7bf45858 thys2/ROOT~
--- a/thys2/ROOT~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-session "Hoare_gen" = "HOL" +
-  options [document = pdf]
-  theories [document = false]
-     Hoare_gen
-
-session "Hoare_tm_basis" = "Hoare_gen" +
-  options [document = pdf]
-  theories [document = false, document_output = "output_tm", document_variants = "hoare_tm"]
-     Hoare_tm_basis
-  files
-    "document/root_tm.tex"
-
-session "Hoare_tm" = "Hoare_tm_basis" +
-  options [document = pdf]
-  theories [document = false, document_output = "output_tm", document_variants = "hoare_tm"]
-     Hoare_tm
-  files
-    "document/root_tm.tex"
-
-session "Hoare_abc" = "Hoare_tm" +
-  options [document = pdf]
-  theories [document = false, document_output = "./output_abc"]
-     Hoare_abc
-
diff -r a5f5b9336007 -r 1cde7bf45858 thys2/Sort_ops.thy~
--- a/thys2/Sort_ops.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-theory Sort_ops
-imports Main
-begin
-
-ML {*
-local 
-  open Array
-in
-
- fun swap i j a = let val ai = sub(a, i);
-                       val _ = update(a, i, sub(a, j))
-                       val _ = update(a, j, ai)
-                   in
-                        a
-                   end
-
-  fun pre_ops_of a = 
-   getM :|-- (fn (l, r, piv, i, j) => let
-       (* val _ = Output.tracing ("("^string_of_int i^","^string_of_int j^")") *)
-    in
-    if (j < i) then (returnM (swap l j a) |-- returnM [(l, j)])
-    else (if (sub(a, i) <= piv andalso i <= r) then (setM (l, r, piv, i + 1, j)
-                                                        |-- pre_ops_of a)
-          else if (sub(a, j) > piv ) then (setM (l, r, piv, i, j - 1) |-- pre_ops_of a)
-          else (pre_ops_of (swap i j a) :|-- (fn ops => returnM ((i,j)::ops))))
-    end  
-   )
-
-  fun ops_of i j a = 
-     if (j < i) then []
-  else let
-     val piv = sub(a, i)
-     val (ops1, (_, _, _, i', j')) = pre_ops_of a (i, j, piv, i, j) |> normVal
-     val ops2 = ops_of i (j' - 1) a
-     val ops3 = ops_of (j' + 1) j a
-  in
-     ops1 @ ops2 @ ops3 
-  end
-
-  fun rem_sdup [] = []
-    | rem_sdup [c] = [c]
-    | rem_sdup ((i, j)::(i', j')::xs) = if ((i = i' andalso j = j') orelse
-                                            (i = j' andalso j = i')) then rem_sdup (xs)
-                            else (i, j)::rem_sdup ((i', j')::xs)
-  fun sexec [] a = a
-   | sexec ((i, j)::ops) a = sexec ops (swap i j a)
-
-  fun swaps_of (l:int list) = 
-    ops_of 0 (List.length l - 1) (fromList l) |> rem_sdup
-      |> filter (fn (i, j) => i <> j)
-end
-
-*}
-
-text {* Examples *}
-
-ML {*
-  val l = [8, 9, 10, 1, 12, 13, 14] 
-  val ops = (swaps_of l)
-  val a = (sexec ops (Array.fromList l))
-  val l' = Array.vector a
-  val a = sexec (rev ops) a
-*}
-
-end
\ No newline at end of file