src/Doc/Tutorial/CodeGen/CodeGen.thy
changeset 58860 fee7cfa69c50
parent 58305 57752a91eec4
child 67406 23307fd33906
     1.1 --- a/src/Doc/Tutorial/CodeGen/CodeGen.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Tutorial/CodeGen/CodeGen.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -15,10 +15,10 @@
     1.4  appropriate function itself.
     1.5  *}
     1.6  
     1.7 -type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v";
     1.8 +type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"
     1.9  datatype (dead 'a, 'v) expr = Cex 'v
    1.10                        | Vex 'a
    1.11 -                      | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr";
    1.12 +                      | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr"
    1.13  
    1.14  text{*\noindent
    1.15  The three constructors represent constants, variables and the application of
    1.16 @@ -42,7 +42,7 @@
    1.17  
    1.18  datatype (dead 'a, 'v) instr = Const 'v
    1.19                         | Load 'a
    1.20 -                       | Apply "'v binop";
    1.21 +                       | Apply "'v binop"
    1.22  
    1.23  text{*
    1.24  The execution of the stack machine is modelled by a function
    1.25 @@ -83,22 +83,22 @@
    1.26  Now we have to prove the correctness of the compiler, i.e.\ that the
    1.27  execution of a compiled expression results in the value of the expression:
    1.28  *}
    1.29 -theorem "exec (compile e) s [] = [value e s]";
    1.30 -(*<*)oops;(*>*)
    1.31 +theorem "exec (compile e) s [] = [value e s]"
    1.32 +(*<*)oops(*>*)
    1.33  text{*\noindent
    1.34  This theorem needs to be generalized:
    1.35  *}
    1.36  
    1.37 -theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs";
    1.38 +theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs"
    1.39  
    1.40  txt{*\noindent
    1.41  It will be proved by induction on @{term"e"} followed by simplification.  
    1.42  First, we must prove a lemma about executing the concatenation of two
    1.43  instruction sequences:
    1.44  *}
    1.45 -(*<*)oops;(*>*)
    1.46 +(*<*)oops(*>*)
    1.47  lemma exec_app[simp]:
    1.48 -  "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    1.49 +  "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)" 
    1.50  
    1.51  txt{*\noindent
    1.52  This requires induction on @{term"xs"} and ordinary simplification for the
    1.53 @@ -106,7 +106,7 @@
    1.54  that contains two @{text"case"}-expressions over instructions. Thus we add
    1.55  automatic case splitting, which finishes the proof:
    1.56  *}
    1.57 -apply(induct_tac xs, simp, simp split: instr.split);
    1.58 +apply(induct_tac xs, simp, simp split: instr.split)
    1.59  (*<*)done(*>*)
    1.60  text{*\noindent
    1.61  Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can
    1.62 @@ -114,10 +114,10 @@
    1.63  rewritten as
    1.64  *}
    1.65  (*<*)
    1.66 -declare exec_app[simp del];
    1.67 -lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    1.68 +declare exec_app[simp del]
    1.69 +lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)" 
    1.70  (*>*)
    1.71 -apply(induct_tac xs, simp_all split: instr.split);
    1.72 +apply(induct_tac xs, simp_all split: instr.split)
    1.73  (*<*)done(*>*)
    1.74  text{*\noindent
    1.75  Although this is more compact, it is less clear for the reader of the proof.
    1.76 @@ -129,7 +129,7 @@
    1.77  \index{compiling expressions example|)}
    1.78  *}
    1.79  (*<*)
    1.80 -theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs";
    1.81 -by(induct_tac e, auto);
    1.82 +theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs"
    1.83 +by(induct_tac e, auto)
    1.84  end
    1.85  (*>*)