wneuper/isa: src/HOL/IMP/Compiler.thy@b124d59f7b61

     1 theory Compiler = Natural:

     3 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat

     5 consts  stepa1 :: "instr list => ((state*nat) * (state*nat))set"

     7 syntax

     8         "@stepa1" :: "[instr list,state,nat,state,nat] => bool"

     9                      ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)

    10         "@stepa" :: "[instr list,state,nat,state,nat] => bool"

    11                      ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)

    13 translations  "P |- <s,m> -1-> <t,n>" == "((s,m),t,n) : stepa1 P"

    14               "P |- <s,m> -*-> <t,n>" == "((s,m),t,n) : ((stepa1 P)^*)"

    17 inductive "stepa1 P"

    18 intros

    19 ASIN:  "P!n = ASIN x a ==> P |- <s,n> -1-> <s[x::= a s],Suc n>"

    20 JMPFT: "[| P!n = JMPF b i;  b s |] ==> P |- <s,n> -1-> <s,Suc n>"

    21 JMPFF: "[| P!n = JMPF b i; ~b s; m=n+i |] ==> P |- <s,n> -1-> <s,m>"

    22 JMPB:  "[| P!n = JMB i |] ==> P |- <s,n> -1-> <s,n-i>"

    24 consts compile :: "com => instr list"

    25 primrec

    26 "compile SKIP = []"

    27 "compile (x:==a) = [ASIN x a]"

    28 "compile (c1;c2) = compile c1 @ compile c2"

    29 "compile (IF b THEN c1 ELSE c2) =

    30  [JMPF b (length(compile c1)+2)] @ compile c1 @

    31  [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"

    32 "compile (WHILE b DO c) = [JMPF b (length(compile c)+2)] @ compile c @

    33  [JMPB (length(compile c)+1)]"

    35 declare nth_append[simp];

    37 lemma nth_tl[simp]: "tl(xs @ y # ys) ! (length xs + z) = ys!z";

    38 apply(induct_tac xs);

    39 by(auto);

    41 theorem "<c,s> -c-> t ==>

    42  !a z. a@compile c@z |- <s,length a> -*-> <t,length a + length(compile c)>";

    43 apply(erule evalc.induct);

    44       apply simp;

    45      apply(force intro!: ASIN);

    46     apply(intro strip);

    47     apply(erule_tac x = a in allE);

    48     apply(erule_tac x = "a@compile c0" in allE);

    49     apply(erule_tac x = "compile c1@z" in allE);

    50     apply(erule_tac x = z in allE);

    51     apply(simp add:add_assoc[THEN sym]);

    52     apply(blast intro:rtrancl_trans);

    53 (* IF b THEN c0 ELSE c1; case b is true *)

    54    apply(intro strip);

    55    (* instantiate assumption sufficiently for later: *)

    56    apply(erule_tac x = "a@[?I]" in allE);

    57    apply(simp);

    58    (* execute JMPF: *)

    59    apply(rule rtrancl_into_rtrancl2);

    60     apply(rule JMPFT);

    61      apply(simp);

    62      apply(blast);

    63     apply assumption;

    64    (* execute compile c0: *)

    65    apply(rule rtrancl_trans);

    66     apply(erule allE);

    67     apply assumption;

    68    (* execute JMPF: *)

    69    apply(rule r_into_rtrancl);

    70    apply(rule JMPFF);

    71      apply(simp);

    72      apply(blast);

    73     apply(blast);

    74    apply(simp);

    75 (* end of case b is true *)

    76   apply(intro strip);

    77   apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE);

    78   apply(simp add:add_assoc);

    79   apply(rule rtrancl_into_rtrancl2);

    80    apply(rule JMPFF);

    81      apply(simp);

    82      apply(blast);

    83     apply assumption;

    84    apply(simp);

    85   apply(blast);

    86  apply(force intro: JMPFF);

    87 apply(intro strip);

    88 apply(erule_tac x = "a@[?I]" in allE);

    89 apply(erule_tac x = a in allE);

    90 apply(simp);

    91 apply(rule rtrancl_into_rtrancl2);

    92  apply(rule JMPFT);

    93   apply(simp);

    94   apply(blast);

    95  apply assumption;

    96 apply(rule rtrancl_trans);

    97  apply(erule allE);

    98  apply assumption;

    99 apply(rule rtrancl_into_rtrancl2);

   100  apply(rule JMPB);

   101  apply(simp);

   102 apply(simp);

   103 done

   105 (* Missing: the other direction! *)

   107 end

author	nipkow
	Thu, 26 Oct 2000 14:52:41 +0200
changeset 10342	b124d59f7b61
child 10343	24c87e1366d8
permissions	-rw-r--r--