4 Copyright 1994 TUM |
4 Copyright 1994 TUM |
5 *) |
5 *) |
6 |
6 |
7 open Denotation; |
7 open Denotation; |
8 |
8 |
9 (**** Rewrite Rules for A,B,C ****) |
9 (** Rewrite Rules for A,B,C **) |
|
10 Addsimps [A_nat_def,A_loc_def,A_op1_def,A_op2_def]; |
|
11 Addsimps [B_true_def,B_false_def,B_op_def,B_not_def,B_and_def,B_or_def]; |
|
12 Addsimps [C_skip_def,C_assign_def,C_comp_def,C_if_def,C_while_def]; |
10 |
13 |
11 val A_rewrite_rules = |
14 (** Type_intr for A **) |
12 [A_nat_def,A_loc_def,A_op1_def,A_op2_def]; |
|
13 |
|
14 val B_rewrite_rules = |
|
15 [B_true_def,B_false_def,B_op_def,B_not_def,B_and_def,B_or_def] |
|
16 |
|
17 val C_rewrite_rules = |
|
18 [C_skip_def,C_assign_def,C_comp_def,C_if_def,C_while_def]; |
|
19 |
|
20 (**** Type_intr for A ****) |
|
21 |
15 |
22 val A_type = prove_goal Denotation.thy |
16 val A_type = prove_goal Denotation.thy |
23 "!!a.[|a:aexp; sigma:loc->nat|] ==> A(a,sigma):nat" |
17 "!!a.[|a:aexp; sigma:loc->nat|] ==> A(a,sigma):nat" |
24 (fn _ => [(etac aexp.induct 1), |
18 (fn _ => [(etac aexp.induct 1), |
25 (rewrite_goals_tac A_rewrite_rules), |
19 (ALLGOALS Asm_simp_tac), |
26 (ALLGOALS (fast_tac (claset() addSIs [apply_type])))]); |
20 (ALLGOALS (fast_tac (claset() addSIs [apply_type])))]); |
27 |
21 |
28 (**** Type_intr for B ****) |
22 (** Type_intr for B **) |
29 |
23 |
30 val B_type = prove_goal Denotation.thy |
24 val B_type = prove_goal Denotation.thy |
31 "!!b. [|b:bexp; sigma:loc->nat|] ==> B(b,sigma):bool" |
25 "!!b. [|b:bexp; sigma:loc->nat|] ==> B(b,sigma):bool" |
32 (fn _ => [(etac bexp.induct 1), |
26 (fn _ => [(etac bexp.induct 1), |
33 (rewrite_goals_tac B_rewrite_rules), |
27 (ALLGOALS Asm_simp_tac), |
34 (ALLGOALS (fast_tac (claset() |
28 (ALLGOALS (fast_tac (claset() |
35 addSIs [apply_type,A_type]@bool_typechecks)))]); |
29 addSIs [apply_type,A_type]@bool_typechecks)))]); |
36 |
30 |
37 (**** C_subset ****) |
31 (** C_subset **) |
38 |
32 |
39 val C_subset = prove_goal Denotation.thy |
33 val C_subset = prove_goal Denotation.thy |
40 "!!c. c:com ==> C(c) <= (loc->nat)*(loc->nat)" |
34 "!!c. c:com ==> C(c) <= (loc->nat)*(loc->nat)" |
41 (fn _ => [(etac com.induct 1), |
35 (fn _ => [(etac com.induct 1), |
42 (rewrite_tac C_rewrite_rules), |
36 (ALLGOALS Asm_simp_tac), |
43 (ALLGOALS (fast_tac (claset() addDs [lfp_subset RS subsetD])))]); |
37 (ALLGOALS (fast_tac (claset() addDs [lfp_subset RS subsetD])))]); |
44 |
38 |
45 (**** Type_elims for C ****) |
39 (** Type_elims for C **) |
46 |
40 |
47 val C_type = prove_goal Denotation.thy |
41 val C_type = prove_goal Denotation.thy |
48 "[| <x,y>:C(c); c:com; \ |
42 "[| <x,y>:C(c); c:com; \ |
49 \ !!c. [| x:loc->nat; y:loc->nat |] ==> R |] \ |
43 \ !!c. [| x:loc->nat; y:loc->nat |] ==> R |] \ |
50 \ ==> R" |
44 \ ==> R" |