# HG changeset patch
# User kleing
# Date 1363085942 -3600
# Node ID 27bb849330eac7dbb156cf46c014fce7d86b9426
# Parent  635562bc14effad86180057262d653f3d5e4ac41
more snippets

diff -r 635562bc14ef -r 27bb849330ea src/HOL/IMP/Types.thy
--- a/src/HOL/IMP/Types.thy	Tue Mar 12 07:51:10 2013 +0100
+++ b/src/HOL/IMP/Types.thy	Tue Mar 12 11:59:02 2013 +0100
@@ -11,6 +11,7 @@
 
 datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
 
+text_raw{*\snip{tavalDef}{0}{2}{% *}
 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
 "taval (Ic i) s (Iv i)" |
 "taval (Rc r) s (Rv r)" |
@@ -19,6 +20,7 @@
  \<Longrightarrow> taval (Plus a1 a2) s (Iv(i1+i2))" |
 "taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
  \<Longrightarrow> taval (Plus a1 a2) s (Rv(r1+r2))"
+text_raw{*}%endsnip*}
 
 inductive_cases [elim!]:
   "taval (Ic i) s v"  "taval (Rc i) s v"
@@ -29,12 +31,14 @@
 
 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
 
+text_raw{*\snip{tbvalDef}{0}{2}{% *}
 inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
 "tbval (Bc v) s v" |
 "tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
 "tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
 "taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
 "taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
+text_raw{*}%endsnip*}
 
 subsection "Syntax of Commands"
 (* a copy of Com.thy - keep in sync! *)
@@ -49,6 +53,7 @@
 
 subsection "Small-Step Semantics of Commands"
 
+text_raw{*\snip{tsmallstepDef}{0}{2}{% *}
 inductive
   small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
 where
@@ -61,6 +66,7 @@
 IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
 
 While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
+text_raw{*}%endsnip*}
 
 lemmas small_step_induct = small_step.induct[split_format(complete)]
 
@@ -70,6 +76,7 @@
 
 type_synonym tyenv = "vname \<Rightarrow> ty"
 
+text_raw{*\snip{atypingDef}{0}{2}{% *}
 inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
   ("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
 where
@@ -77,25 +84,30 @@
 Rc_ty: "\<Gamma> \<turnstile> Rc r : Rty" |
 V_ty: "\<Gamma> \<turnstile> V x : \<Gamma> x" |
 Plus_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Plus a1 a2 : \<tau>"
+text_raw{*}%endsnip*}
 
 text{* Warning: the ``:'' notation leads to syntactic ambiguities,
 i.e. multiple parse trees, because ``:'' also stands for set membership.
 In most situations Isabelle's type system will reject all but one parse tree,
 but will still inform you of the potential ambiguity. *}
 
+text_raw{*\snip{btypingDef}{0}{2}{% *}
 inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50)
 where
 B_ty: "\<Gamma> \<turnstile> Bc v" |
 Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b" |
 And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2" |
 Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2"
+text_raw{*}%endsnip*}
 
+text_raw{*\snip{ctypingDef}{0}{2}{% *}
 inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
 Skip_ty: "\<Gamma> \<turnstile> SKIP" |
 Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
 Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" |
 If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
 While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c"
+text_raw{*}%endsnip*}
 
 inductive_cases [elim!]:
   "\<Gamma> \<turnstile> x ::= a"  "\<Gamma> \<turnstile> c1;c2"