doc-src/Tutorial/CodeGen/CodeGenIf.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/CodeGenIf.ML	Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,39 @@
+Addsimps exec.rules;
+Addsimps [Let_def,drop_all];
+Addsplits [split_instr_case];
+
+Goal "!xs. wf xs --> wf(drop n xs)";
+by(induct_tac "n" 1);
+by(Simp_tac 1);
+by(Clarify_tac 1);
+by(exhaust_tac "xs" 1);
+by(Asm_simp_tac 1);
+by(Asm_full_simp_tac 1);
+qed_spec_mp "wf_drop";
+Addsimps [wf_drop];
+
+Goal "wf xs --> wf ys --> wf(xs@ys)";
+by(induct_tac "xs" 1);
+by(Simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [trans_le_add1]) 1);
+qed_spec_mp "wf_append";
+Addsimps [wf_append];
+
+Goal "!vs ys. wf xs --> exec(s,vs,xs@ys) = exec(s,exec(s,vs,xs),ys)"; 
+by(res_inst_tac [("xs","xs")] length_induct 1);
+by(exhaust_tac "xs" 1);
+by(Asm_full_simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [less_imp_diff_is_0,diff_less_Suc,le_imp_less_Suc]) 1);
+qed_spec_mp "exec_append";
+Addsimps [exec_append];
+
+Goal "wf(comp e)";
+by(induct_tac "e" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "wf_comp";
+Addsimps [wf_comp];
+
+Goal "!vs. exec(s, vs, comp e) = (value s e) # vs";
+by(induct_tac "e" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "exec_comp";