1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Oct 26 14:52:41 2000 +0200
     1.3 @@ -0,0 +1,107 @@
     1.4 +theory Compiler = Natural:
     1.5 +
     1.6 +datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
     1.7 +
     1.8 +consts  stepa1 :: "instr list => ((state*nat) * (state*nat))set"
     1.9 +
    1.10 +syntax
    1.11 +        "@stepa1" :: "[instr list,state,nat,state,nat] => bool"
    1.12 +                     ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
    1.13 +        "@stepa" :: "[instr list,state,nat,state,nat] => bool"
    1.14 +                     ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)
    1.15 +
    1.16 +translations  "P |- <s,m> -1-> <t,n>" == "((s,m),t,n) : stepa1 P"
    1.17 +              "P |- <s,m> -*-> <t,n>" == "((s,m),t,n) : ((stepa1 P)^*)"
    1.18 +
    1.19 +
    1.20 +inductive "stepa1 P"
    1.21 +intros
    1.22 +ASIN:  "P!n = ASIN x a ==> P |- <s,n> -1-> <s[x::= a s],Suc n>"
    1.23 +JMPFT: "[| P!n = JMPF b i;  b s |] ==> P |- <s,n> -1-> <s,Suc n>"
    1.24 +JMPFF: "[| P!n = JMPF b i; ~b s; m=n+i |] ==> P |- <s,n> -1-> <s,m>"
    1.25 +JMPB:  "[| P!n = JMB i |] ==> P |- <s,n> -1-> <s,n-i>"
    1.26 +
    1.27 +consts compile :: "com => instr list"
    1.28 +primrec
    1.29 +"compile SKIP = []"
    1.30 +"compile (x:==a) = [ASIN x a]"
    1.31 +"compile (c1;c2) = compile c1 @ compile c2"
    1.32 +"compile (IF b THEN c1 ELSE c2) =
    1.33 + [JMPF b (length(compile c1)+2)] @ compile c1 @
    1.34 + [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
    1.35 +"compile (WHILE b DO c) = [JMPF b (length(compile c)+2)] @ compile c @
    1.36 + [JMPB (length(compile c)+1)]"
    1.37 +
    1.38 +declare nth_append[simp];
    1.39 +
    1.40 +lemma nth_tl[simp]: "tl(xs @ y # ys) ! (length xs + z) = ys!z";
    1.41 +apply(induct_tac xs);
    1.42 +by(auto);
    1.43 +
    1.44 +theorem "<c,s> -c-> t ==> 
    1.45 + !a z. a@compile c@z |- <s,length a> -*-> <t,length a + length(compile c)>";
    1.46 +apply(erule evalc.induct);
    1.47 +      apply simp;
    1.48 +     apply(force intro!: ASIN);
    1.49 +    apply(intro strip);
    1.50 +    apply(erule_tac x = a in allE);
    1.51 +    apply(erule_tac x = "a@compile c0" in allE);
    1.52 +    apply(erule_tac x = "compile c1@z" in allE);
    1.53 +    apply(erule_tac x = z in allE);
    1.54 +    apply(simp add:add_assoc[THEN sym]);
    1.55 +    apply(blast intro:rtrancl_trans);
    1.56 +(* IF b THEN c0 ELSE c1; case b is true *)
    1.57 +   apply(intro strip);
    1.58 +   (* instantiate assumption sufficiently for later: *)
    1.59 +   apply(erule_tac x = "a@[?I]" in allE);
    1.60 +   apply(simp);
    1.61 +   (* execute JMPF: *)
    1.62 +   apply(rule rtrancl_into_rtrancl2);
    1.63 +    apply(rule JMPFT);
    1.64 +     apply(simp);
    1.65 +     apply(blast);
    1.66 +    apply assumption;
    1.67 +   (* execute compile c0: *)
    1.68 +   apply(rule rtrancl_trans);
    1.69 +    apply(erule allE);
    1.70 +    apply assumption;
    1.71 +   (* execute JMPF: *)
    1.72 +   apply(rule r_into_rtrancl);
    1.73 +   apply(rule JMPFF);
    1.74 +     apply(simp);
    1.75 +     apply(blast);
    1.76 +    apply(blast);
    1.77 +   apply(simp);
    1.78 +(* end of case b is true *)
    1.79 +  apply(intro strip);
    1.80 +  apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE);
    1.81 +  apply(simp add:add_assoc);
    1.82 +  apply(rule rtrancl_into_rtrancl2);
    1.83 +   apply(rule JMPFF);
    1.84 +     apply(simp);
    1.85 +     apply(blast);
    1.86 +    apply assumption;
    1.87 +   apply(simp);
    1.88 +  apply(blast);
    1.89 + apply(force intro: JMPFF);
    1.90 +apply(intro strip);
    1.91 +apply(erule_tac x = "a@[?I]" in allE);
    1.92 +apply(erule_tac x = a in allE);
    1.93 +apply(simp);
    1.94 +apply(rule rtrancl_into_rtrancl2);
    1.95 + apply(rule JMPFT);
    1.96 +  apply(simp);
    1.97 +  apply(blast);
    1.98 + apply assumption;
    1.99 +apply(rule rtrancl_trans);
   1.100 + apply(erule allE);
   1.101 + apply assumption;
   1.102 +apply(rule rtrancl_into_rtrancl2);
   1.103 + apply(rule JMPB);
   1.104 + apply(simp);
   1.105 +apply(simp);
   1.106 +done
   1.107 +
   1.108 +(* Missing: the other direction! *)
   1.109 +
   1.110 +end

     2.1 --- a/src/HOL/IMP/ROOT.ML	Thu Oct 26 11:27:48 2000 +0200
     2.2 +++ b/src/HOL/IMP/ROOT.ML	Thu Oct 26 14:52:41 2000 +0200
     2.3 @@ -10,3 +10,4 @@
     2.4  time_use_thy "Transition";
     2.5  time_use_thy "VC";
     2.6  time_use_thy "Examples";
     2.7 +time_use_thy "Compiler";