-
Notifications
You must be signed in to change notification settings - Fork 3
/
CompileAuxiliary.thy
47 lines (32 loc) · 1.46 KB
/
CompileAuxiliary.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
chapter {* Generated by Lem from compile.lem. *}
theory "CompileAuxiliary"
imports
Main "~~/src/HOL/Library/Code_Target_Numeral"
"Lem_pervasives"
"Evm"
"Word8"
"Rlp"
"Compile"
begin
(****************************************************)
(* *)
(* Termination Proofs *)
(* *)
(****************************************************)
termination get_expr by lexicographic_order
termination compile_expr by lexicographic_order
(****************************************************)
(* *)
(* Lemmata *)
(* *)
(****************************************************)
theorem program_iter_bigstep :
"( \<forall> x. \<forall> c. \<forall> v. \<forall> n. \<forall> k. \<forall> steps. (Return x = program_iter c (Continue v n k) steps) \<longrightarrow> (program_sem v c n k = x))"
(* Theorem: program_iter_bigstep*)(* try *) by auto
theorem simple_correct :
"( \<forall> expr. \<forall> v. \<forall> addr. eval_expr v addr (compile_simple expr) = get_simple v expr)"
(* Theorem: simple_correct*)(* try *) by auto
theorem expr_correct :
"( \<forall> expr. \<forall> v. \<forall> addr. eval_expr v addr (compile_expr expr) = get_expr v expr)"
(* Theorem: expr_correct*)(* try *) by auto
end