# HG changeset patch
# User kleing
# Date 1371011052 25200
# Node ID ec46a485bf60c001114d7a65959ee02c9200f324
# Parent  0b395800fdf0d0dfeda1b738c9c3a4b538a8e3ba
some comments on syntax and automation setup

diff -r 0b395800fdf0 -r ec46a485bf60 src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Tue Jun 11 19:58:09 2013 -0400
+++ b/src/HOL/IMP/Big_Step.thy	Tue Jun 11 21:24:12 2013 -0700
@@ -4,6 +4,12 @@
 
 subsection "Big-Step Semantics of Commands"
 
+text {*
+The big-step semantics is a straight-forward inductive definition
+with concrete syntax. Note that the first paramenter is a tuple,
+so the syntax becomes @{text "(c,s) \<Rightarrow> s'"}.
+*}
+
 text_raw{*\snip{BigStepdef}{0}{1}{% *}
 inductive
   big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
@@ -57,6 +63,10 @@
 
 text{* Proof automation: *}
 
+text {* The introduction rules are good for automatically
+construction small program executions. The recursive cases
+may require backtracking, so we declare the set as unsafe
+intro rules. *}
 declare big_step.intros [intro]
 
 text{* The standard induction rule 
@@ -64,8 +74,13 @@
 
 thm big_step.induct
 
-text{* A customized induction rule for (c,s) pairs: *}
-
+text{*
+This induction schema is almost perfect for our purposes, but
+our trick for reusing the tuple syntax means that the induction
+schema has two parameters instead of the @{text c}, @{text s},
+and @{text s'} that we are likely to encounter. Splitting
+the tuple parameter fixes this:
+*}
 lemmas big_step_induct = big_step.induct[split_format(complete)]
 thm big_step_induct
 text {*