diff -r 95b42288294e -r 438703674711 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Tactical.thy	Tue May 21 14:37:39 2019 +0200
@@ -47,7 +47,7 @@
 text \<open>
   This proof translates to the following ML-code.
   
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>let
   val ctxt = @{context}
   val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
@@ -763,17 +763,19 @@
   constraints is by pre-instantiating theorems with other theorems. 
   The function @{ML_ind RS in Drule}, for example, does this.
   
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>@{thm disjI1} RS @{thm conjI}\<close> \<open>\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q\<close>}
 
   In this example it instantiates the first premise of the \<open>conjI\<close>-theorem 
   with the theorem \<open>disjI1\<close>. If the instantiation is impossible, as in the 
   case of
 
-  @{ML_matchresult_fake_both [display,gray]
+  @{ML_response [display,gray]
   \<open>@{thm conjI} RS @{thm mp}\<close> 
-\<open>*** Exception- THM ("RSN: no unifiers", 1, 
-["\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q", "\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q"]) raised\<close>}
+\<open>exception THM 1 raised\<dots> 
+ RSN: no unifiers 
+ \<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q 
+ \<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\<close>}
 
   then the function raises an exception. The function @{ML_ind  RSN in Drule} 
   is similar to @{ML RS}, but takes an additional number as argument. This 
@@ -782,7 +784,7 @@
   If you want to instantiate more than one premise of a theorem, you can use 
   the function @{ML_ind MRS in Drule}:
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}\<close> 
   \<open>\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)\<close>}
 
@@ -791,17 +793,17 @@
   example in the code below, every theorem in the second list is 
   instantiated with every theorem in the first.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let
   val list1 = [@{thm impI}, @{thm disjI2}]
   val list2 = [@{thm conjI}, @{thm disjI1}]
 in
   list1 RL list2
 end\<close> 
-\<open>[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q, 
- \<lbrakk>?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q,
- (?P1 \<Longrightarrow> ?Q1) \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<or> ?Q, 
- ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]\<close>}
+\<open>["\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q", 
+ "\<lbrakk>?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q",
+ "(?P1 \<Longrightarrow> ?Q1) \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<or> ?Q", 
+ "?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q"]\<close>}
 
   \begin{readmore}
   The combinators for instantiating theorems with other theorems are 
@@ -1458,7 +1460,7 @@
   prints out some parts of a simpset. If you use it to print out the components of the
   empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}
   
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>print_ss @{context} empty_ss\<close>
 \<open>Simplification rules:
 Congruences rules:
@@ -1474,10 +1476,10 @@
 text \<open>
   Printing then out the components of the simpset gives:
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss1)\<close>
 \<open>Simplification rules:
-  ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
+  ??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1)
 Congruences rules:
 Simproc patterns:\<close>}
 
@@ -1491,12 +1493,12 @@
 text \<open>
   gives
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss2)\<close>
 \<open>Simplification rules:
-  ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
+  ??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1)
 Congruences rules:
-  Complete_Lattices.Inf_class.INFIMUM: 
+  Complete_Lattices.Inf_class.Inf: 
     \<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
 Simproc patterns:\<close>}
 
@@ -1508,7 +1510,7 @@
   In the context of HOL, the first really useful simpset is @{ML_ind
   HOL_basic_ss in Simpdata}. While printing out the components of this simpset
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>print_ss @{context} HOL_basic_ss\<close>
 \<open>Simplification rules:
 Congruences rules:
@@ -1534,6 +1536,7 @@
 apply(tactic \<open>ALLGOALS (simp_tac (put_simpset HOL_basic_ss @{context}))\<close>)
 done
 
+declare [[ML_print_depth = 200]]
 text \<open>
   This behaviour is not because of simplification rules, but how the subgoaler, solver 
   and looper are set up in @{ML HOL_basic_ss}.
@@ -1542,17 +1545,17 @@
   already many useful simplification and congruence rules for the logical 
   connectives in HOL. 
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>print_ss @{context} HOL_ss\<close>
 \<open>Simplification rules:
   Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
   HOL.the_eq_trivial: THE x. x = y \<equiv> y
-  HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y
+  HOL.the_sym_eq_trivial: THE y. y = y \<equiv> y
   \<dots>
 Congruences rules:
   HOL.simp_implies: \<dots>
     \<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
-  op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
+  HOL.implies: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
 Simproc patterns:
   \<dots>\<close>}
 
@@ -2064,16 +2067,16 @@
   is the function @{ML_ind  all_conv in Conv}, which maps a @{ML_type cterm} to an
   instance of the (meta)reflexivity theorem. For example:
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>Conv.all_conv @{cterm "Foo \<or> Bar"}\<close>
   \<open>Foo \<or> Bar \<equiv> Foo \<or> Bar\<close>}
 
   Another simple conversion is @{ML_ind  no_conv in Conv} which always raises the 
   exception @{ML CTERM}.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>Conv.no_conv @{cterm True}\<close> 
-  \<open>*** Exception- CTERM ("no conversion", []) raised\<close>}
+  \<open>exception CTERM \<dots>: no conversion\<close>}
 
   A more interesting conversion is the function @{ML_ind  beta_conversion in Thm}: it 
   produces a meta-equation between a term and its beta-normal form. For example
@@ -2111,7 +2114,7 @@
 
 or in the pretty-printed form
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let
    val add = @{cterm "\<lambda>x y. x + (y::nat)"}
    val two = @{cterm "2::nat"}
@@ -2146,7 +2149,7 @@
   It can be used for example to rewrite @{term "True \<and> (Foo \<longrightarrow> Bar)"} 
   to @{term "Foo \<longrightarrow> Bar"}. The code is as follows.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let 
   val ctrm = @{cterm "True \<and> (Foo \<longrightarrow> Bar)"}
 in
@@ -2182,7 +2185,7 @@
   The conversion combinator @{ML_ind else_conv in Conv} tries out the 
   first one, and if it does not apply, tries the second. For example 
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let
   val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
   val ctrm1 = @{cterm "True \<and> Q"}
@@ -2190,7 +2193,7 @@
 in
   (conv ctrm1, conv ctrm2)
 end\<close>
-\<open>(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)\<close>}
+\<open>("True \<and> Q \<equiv> Q", "P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q")\<close>}
 
   Here the conversion @{thm [source] true_conj1} only applies
   in the first case, but fails in the second. The whole conversion
@@ -2199,7 +2202,7 @@
   behaviour can also be achieved with conversion combinator @{ML_ind try_conv in Conv}.
   For example
   
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let
   val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
   val ctrm = @{cterm "True \<or> P"}
@@ -2220,14 +2223,14 @@
   a conversion to the first, respectively second, argument of an application.  
   For example
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let 
   val conv = Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})
   val ctrm = @{cterm "P \<or> (True \<and> Q)"}
 in
   conv ctrm
 end\<close>
-\<open>P \<or> (True \<and> Q) \<equiv> P \<or> Q\<close>}
+\<open>P \<or> True \<and> Q \<equiv> P \<or> Q\<close>}
 
   The reason for this behaviour is that \<open>(op \<or>)\<close> expects two
   arguments.  Therefore the term must be of the form \<open>(Const \<dots> $ t1) $ t2\<close>. The
@@ -2238,14 +2241,14 @@
   The function @{ML_ind  abs_conv in Conv} applies a conversion under an 
   abstraction. For example:
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let 
   val conv = Conv.rewr_conv @{thm true_conj1} 
   val ctrm = @{cterm "\<lambda>P. True \<and> (P \<and> Foo)"}
 in
   Conv.abs_conv (K conv) @{context} ctrm
 end\<close>
-  \<open>\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo\<close>}
+  \<open>"\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"\<close>}
   
   Note that this conversion needs a context as an argument. We also give the
   conversion as \<open>(K conv)\<close>, which is a function that ignores its
@@ -2279,7 +2282,7 @@
   to be able to pattern-match the term. To see this 
   conversion in action, consider the following example:
 
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>let
   val conv = true_conj1_conv @{context}
   val ctrm = @{cterm "distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x"}
@@ -2358,7 +2361,7 @@
   soon as it found one redex. Here is an example for this conversion:
 
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let
   val ctrm = @{cterm "if P (True \<and> 1 \<noteq> (2::nat)) 
                         then True \<and> True else True \<and> False"}
@@ -2382,7 +2385,7 @@
   Using the conversion you can transform this theorem into a 
   new theorem as follows
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let
   val conv = Conv.fconv_rule (true_conj1_conv @{context}) 
   val thm = @{thm foo_test}
@@ -2465,7 +2468,7 @@
   into @{thm [source] id2_def} by abstracting all variables on the 
   left-hand side in the right-hand side.
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>Drule.abs_def @{thm id1_def}\<close>
   \<open>id1 \<equiv> \<lambda>x. x\<close>}
 
@@ -2513,7 +2516,7 @@
   export the context \<open>ctxt'\<close> back to \<open>ctxt\<close> in order to 
   produce meta-variables for the theorem.  An example is as follows.
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>unabs_def @{context} @{thm id2_def}\<close>
   \<open>id2 ?x1 \<equiv> ?x1\<close>}
 \<close>