doc-src/Tutorial/CodeGen/CodeGenIf.ML
author wenzelm
Sat, 01 Jul 2000 19:49:20 +0200
changeset 9226 cbe6144f0f15
parent 5377 efb799c5ed3c
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5377
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
     1
Addsimps exec.rules;
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
     2
Addsimps [Let_def,drop_all];
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
     3
Addsplits [split_instr_case];
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
     4
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
     5
Goal "!xs. wf xs --> wf(drop n xs)";
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
     6
by(induct_tac "n" 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
     7
by(Simp_tac 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
     8
by(Clarify_tac 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
     9
by(exhaust_tac "xs" 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    10
by(Asm_simp_tac 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    11
by(Asm_full_simp_tac 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    12
qed_spec_mp "wf_drop";
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    13
Addsimps [wf_drop];
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    14
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    15
Goal "wf xs --> wf ys --> wf(xs@ys)";
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    16
by(induct_tac "xs" 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    17
by(Simp_tac 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    18
by(asm_full_simp_tac (simpset() addsimps [trans_le_add1]) 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    19
qed_spec_mp "wf_append";
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    20
Addsimps [wf_append];
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    21
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    22
Goal "!vs ys. wf xs --> exec(s,vs,xs@ys) = exec(s,exec(s,vs,xs),ys)"; 
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    23
by(res_inst_tac [("xs","xs")] length_induct 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    24
by(exhaust_tac "xs" 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    25
by(Asm_full_simp_tac 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    26
by(asm_full_simp_tac (simpset() addsimps [less_imp_diff_is_0,diff_less_Suc,le_imp_less_Suc]) 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    27
qed_spec_mp "exec_append";
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    28
Addsimps [exec_append];
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    29
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    30
Goal "wf(comp e)";
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    31
by(induct_tac "e" 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    32
by(ALLGOALS Asm_simp_tac);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    33
qed "wf_comp";
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    34
Addsimps [wf_comp];
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    35
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    36
Goal "!vs. exec(s, vs, comp e) = (value s e) # vs";
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    37
by(induct_tac "e" 1);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    38
by(ALLGOALS Asm_simp_tac);
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
    39
qed "exec_comp";