# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1236174647 0
# Node ID d7944bdf7b3f93ad46739fac7360b8ab7f472a4b
# Parent  76cdc8f562fc24640620a9c2fe0f0baef39aaeb1
removed infix_conv and moved function no_vars into the FirstSteps chapter

diff -r 76cdc8f562fc -r d7944bdf7b3f CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Wed Mar 04 13:15:29 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Mar 04 13:50:47 2009 +0000
@@ -154,15 +154,26 @@
 
 text {*
   The easiest way to get the string of a theorem is to transform it
-  into a @{ML_type cterm} using the function @{ML crep_thm}.
+  into a @{ML_type cterm} using the function @{ML crep_thm}. Theorems
+  also include schematic variables, such as @{text "?P"}, @{text "?Q"}
+  and so on. In order to improve the readability of theorems we convert
+  these schematic variables into free variables using the 
+  function @{ML Variable.import_thms}.
 *}
 
-ML{*fun str_of_thm ctxt thm =
-  let
-    val {prop, ...} = crep_thm thm
-  in 
-    str_of_cterm ctxt prop
-  end*}
+ML{*fun no_vars ctxt thm =
+let 
+  val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
+in
+  thm'
+end
+
+fun str_of_thm ctxt thm =
+let
+  val {prop, ...} = crep_thm (no_vars ctxt thm)
+in 
+  str_of_cterm ctxt prop
+end*}
 
 text {* 
   Again the function @{ML commas} helps with printing more than one theorem. 
@@ -171,7 +182,6 @@
 ML{*fun str_of_thms ctxt thms =  
   commas (map (str_of_thm ctxt) thms)*}
 
-
 section {* Combinators\label{sec:combinators} *}
 
 text {*
diff -r 76cdc8f562fc -r d7944bdf7b3f CookBook/Solutions.thy
--- a/CookBook/Solutions.thy	Wed Mar 04 13:15:29 2009 +0000
+++ b/CookBook/Solutions.thy	Wed Mar 04 13:50:47 2009 +0000
@@ -1,6 +1,5 @@
 theory Solutions
 imports Base
-uses "infix_conv.ML"
 begin
 
 chapter {* Solutions to Most Exercises\label{ch:solutions} *}
diff -r 76cdc8f562fc -r d7944bdf7b3f CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Wed Mar 04 13:15:29 2009 +0000
+++ b/CookBook/Tactical.thy	Wed Mar 04 13:50:47 2009 +0000
@@ -1,6 +1,5 @@
 theory Tactical
 imports Base FirstSteps
-uses "infix_conv.ML"
 begin
 
 chapter {* Tactical Reasoning\label{chp:tactical} *}
@@ -479,21 +478,10 @@
   takes an additional number as argument that makes explicit which premise 
   should be instantiated. 
 
-  To improve readability of the theorems we produce below, we shall use 
-  the following function
-*}
-
-ML{*fun no_vars ctxt thm =
-let 
-  val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
-in
-  thm'
-end*}
-
-text {*
-  that transform the schematic variables of a theorem into free variables.
-  Using this function for the first @{ML RS}-expression above would produce
-  the more readable result:
+  To improve readability of the theorems we produce below, we shall use the
+  function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
+  schematic variables into free ones.  Using this function for the first @{ML
+  RS}-expression above produces the more readable result:
 
   @{ML_response_fake [display,gray]
   "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
@@ -1018,7 +1006,7 @@
 
 *}
 
-section {* Simplifier Tactics (TBD) *}
+section {* Simplifier Tactics *}
 
 text {*
   A lot of convenience in the reasoning with Isabelle derives from its
@@ -1188,9 +1176,11 @@
   @{ML_response_fake [display,gray]
   "print_parts @{context} ss1"
 "Simplification rules:
-  ??.unknown: ?A1 - ?B1 \<inter> ?C1 \<equiv> ?A1 - ?B1 \<union> (?A1 - ?C1)
+  ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:"}
 
+  (FIXME: Why does it print out ??.unknown)
+
   Adding the congruence rule @{thm [source] UN_cong} 
 *}
 
@@ -1202,10 +1192,9 @@
   @{ML_response_fake [display,gray]
   "print_parts @{context} ss2"
 "Simplification rules:
-  ??.unknown: ?A1 - ?B1 \<inter> ?C1 \<equiv> ?A1 - ?B1 \<union> (?A1 - ?C1)
+  ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
-  UNION: \<lbrakk>?A1 = ?B1; \<And>x. x \<in> ?B1 \<Longrightarrow> ?C1 x = ?D1 x\<rbrakk> \<Longrightarrow> 
-     \<Union>x\<in>?A1. ?C1 x \<equiv> \<Union>x\<in>?B1. ?D1 x"}
+  UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x"}
 
   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 
   expects this form of the simplification and congruence rules. However, even 
@@ -1240,14 +1229,14 @@
   @{ML_response_fake [display,gray]
   "print_parts @{context} HOL_ss"
 "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 y. ?y = y \<equiv> ?y
+  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
   \<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'"}
+    \<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'"}
 
   
   The main point of these simpsets is that they are small enough to
diff -r 76cdc8f562fc -r d7944bdf7b3f CookBook/infix_conv.ML
--- a/CookBook/infix_conv.ML	Wed Mar 04 13:15:29 2009 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-signature INFIX_CONV =
-sig
-  val then_conv : Thm.conv * Thm.conv -> Thm.conv
-  val else_conv : Thm.conv * Thm.conv -> Thm.conv
-end
-
-structure InfixConv : INFIX_CONV = Conv
-
-open InfixConv
diff -r 76cdc8f562fc -r d7944bdf7b3f cookbook.pdf
Binary file cookbook.pdf has changed