author | blanchet |
Mon, 06 Jun 2011 20:36:35 +0200 | |
changeset 43188 | 0c36ae874fcc |
parent 42463 | f270e3e18be5 |
child 45970 | b6d0cff57d96 |
permissions | -rw-r--r-- |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
1 |
theory Examples |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39655
diff
changeset
|
2 |
imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
3 |
begin |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
4 |
|
42208
02513eb26eb7
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
krauss
parents:
42187
diff
changeset
|
5 |
declare [[values_timeout = 480.0]] |
42187 | 6 |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
7 |
section {* Formal Languages *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
8 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
9 |
subsection {* General Context Free Grammars *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
10 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
11 |
text {* a contribution by Aditi Barthwal *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
12 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
13 |
datatype ('nts,'ts) symbol = NTS 'nts |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
14 |
| TS 'ts |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
15 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
16 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
17 |
datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
18 |
|
42463 | 19 |
type_synonym ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
20 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
21 |
fun rules :: "('nts,'ts) grammar => ('nts,'ts) rule set" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
22 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
23 |
"rules (r, s) = r" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
24 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
25 |
definition derives |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
26 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
27 |
"derives g = { (lsl,rsl). \<exists>s1 s2 lhs rhs. |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
28 |
(s1 @ [NTS lhs] @ s2 = lsl) \<and> |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
29 |
(s1 @ rhs @ s2) = rsl \<and> |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
30 |
(rule lhs rhs) \<in> fst g }" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
31 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
32 |
abbreviation "example_grammar == |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
33 |
({ rule ''S'' [NTS ''A'', NTS ''B''], |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
34 |
rule ''S'' [TS ''a''], |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
35 |
rule ''A'' [TS ''b'']}, ''S'')" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
36 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
37 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
38 |
code_pred [inductify, skip_proof] derives . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
39 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
40 |
thm derives.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
41 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
42 |
definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
43 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
44 |
code_pred (modes: o \<Rightarrow> bool) [inductify] test . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
45 |
thm test.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
46 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
47 |
values "{rhs. test rhs}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
48 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
49 |
declare rtrancl.intros(1)[code_pred_def] converse_rtrancl_into_rtrancl[code_pred_def] |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
50 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
51 |
code_pred [inductify] rtrancl . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
52 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
53 |
definition "test2 = { rhs. ([NTS ''S''],rhs) \<in> (derives example_grammar)^* }" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
54 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
55 |
code_pred [inductify, skip_proof] test2 . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
56 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
57 |
values "{rhs. test2 rhs}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
58 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
59 |
subsection {* Some concrete Context Free Grammars *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
60 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
61 |
datatype alphabet = a | b |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
62 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
63 |
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
64 |
"[] \<in> S\<^isub>1" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
65 |
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
66 |
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
67 |
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
68 |
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
69 |
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
70 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
71 |
code_pred [inductify] S\<^isub>1p . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
72 |
code_pred [random_dseq inductify] S\<^isub>1p . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
73 |
thm S\<^isub>1p.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
74 |
thm S\<^isub>1p.random_dseq_equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
75 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
76 |
values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
77 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
78 |
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
79 |
"[] \<in> S\<^isub>2" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
80 |
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
81 |
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
82 |
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
83 |
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
84 |
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
85 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
86 |
code_pred [random_dseq inductify] S\<^isub>2p . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
87 |
thm S\<^isub>2p.random_dseq_equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
88 |
thm A\<^isub>2p.random_dseq_equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
89 |
thm B\<^isub>2p.random_dseq_equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
90 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
91 |
values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
92 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
93 |
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
94 |
"[] \<in> S\<^isub>3" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
95 |
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
96 |
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
97 |
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
98 |
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
99 |
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
100 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
101 |
code_pred [inductify, skip_proof] S\<^isub>3p . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
102 |
thm S\<^isub>3p.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
103 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
104 |
values 10 "{x. S\<^isub>3p x}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
105 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
106 |
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
107 |
"[] \<in> S\<^isub>4" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
108 |
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
109 |
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
110 |
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
111 |
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
112 |
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
113 |
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
114 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
115 |
code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
116 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
117 |
hide_const a b |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
118 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
119 |
section {* Semantics of programming languages *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
120 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
121 |
subsection {* IMP *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
122 |
|
42463 | 123 |
type_synonym var = nat |
124 |
type_synonym state = "int list" |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
125 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
126 |
datatype com = |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
127 |
Skip | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
128 |
Ass var "state => int" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
129 |
Seq com com | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
130 |
IF "state => bool" com com | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
131 |
While "state => bool" com |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
132 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
133 |
inductive exec :: "com => state => state => bool" where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
134 |
"exec Skip s s" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
135 |
"exec (Ass x e) s (s[x := e(s)])" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
136 |
"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
137 |
"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
138 |
"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
139 |
"~b s ==> exec (While b c) s s" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
140 |
"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
141 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
142 |
code_pred exec . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
143 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
144 |
values "{t. exec |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
145 |
(While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1)))) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
146 |
[3,5] t}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
147 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
148 |
subsection {* Lambda *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
149 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
150 |
datatype type = |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
151 |
Atom nat |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
152 |
| Fun type type (infixr "\<Rightarrow>" 200) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
153 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
154 |
datatype dB = |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
155 |
Var nat |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
156 |
| App dB dB (infixl "\<degree>" 200) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
157 |
| Abs type dB |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
158 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
159 |
primrec |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
160 |
nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
161 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
162 |
"[]\<langle>i\<rangle> = None" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
163 |
| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
164 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
165 |
inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
166 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
167 |
"nth_el' (x # xs) 0 x" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
168 |
| "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
169 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
170 |
inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
171 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
172 |
Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
173 |
| Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
174 |
| App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
175 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
176 |
primrec |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
177 |
lift :: "[dB, nat] => dB" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
178 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
179 |
"lift (Var i) k = (if i < k then Var i else Var (i + 1))" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
180 |
| "lift (s \<degree> t) k = lift s k \<degree> lift t k" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
181 |
| "lift (Abs T s) k = Abs T (lift s (k + 1))" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
182 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
183 |
primrec |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
184 |
subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
185 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
186 |
subst_Var: "(Var i)[s/k] = |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
187 |
(if k < i then Var (i - 1) else if i = k then s else Var i)" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
188 |
| subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
189 |
| subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
190 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
191 |
inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
192 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
193 |
beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
194 |
| appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
195 |
| appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
196 |
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
197 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
198 |
code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
199 |
thm typing.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
200 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
201 |
code_pred (modes: i => i => bool, i => o => bool as reduce') beta . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
202 |
thm beta.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
203 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
204 |
values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
205 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
206 |
definition "reduce t = Predicate.the (reduce' t)" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
207 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
208 |
value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
209 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
210 |
code_pred [dseq] typing . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
211 |
code_pred [random_dseq] typing . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
212 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
213 |
values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
214 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
215 |
subsection {* A minimal example of yet another semantics *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
216 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
217 |
text {* thanks to Elke Salecker *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
218 |
|
42463 | 219 |
type_synonym vname = nat |
220 |
type_synonym vvalue = int |
|
221 |
type_synonym var_assign = "vname \<Rightarrow> vvalue" --"variable assignment" |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
222 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
223 |
datatype ir_expr = |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
224 |
IrConst vvalue |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
225 |
| ObjAddr vname |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
226 |
| Add ir_expr ir_expr |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
227 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
228 |
datatype val = |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
229 |
IntVal vvalue |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
230 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
231 |
record configuration = |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
232 |
Env :: var_assign |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
233 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
234 |
inductive eval_var :: |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
235 |
"ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
236 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
237 |
irconst: "eval_var (IrConst i) conf (IntVal i)" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
238 |
| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
239 |
| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
240 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
241 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
242 |
code_pred eval_var . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
243 |
thm eval_var.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
244 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
245 |
values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
246 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
247 |
subsection {* Another semantics *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
248 |
|
42463 | 249 |
type_synonym name = nat --"For simplicity in examples" |
250 |
type_synonym state' = "name \<Rightarrow> nat" |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
251 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
252 |
datatype aexp = N nat | V name | Plus aexp aexp |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
253 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
254 |
fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
255 |
"aval (N n) _ = n" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
256 |
"aval (V x) st = st x" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
257 |
"aval (Plus e\<^isub>1 e\<^isub>2) st = aval e\<^isub>1 st + aval e\<^isub>2 st" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
258 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
259 |
datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
260 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
261 |
primrec bval :: "bexp \<Rightarrow> state' \<Rightarrow> bool" where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
262 |
"bval (B b) _ = b" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
263 |
"bval (Not b) st = (\<not> bval b st)" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
264 |
"bval (And b1 b2) st = (bval b1 st \<and> bval b2 st)" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
265 |
"bval (Less a\<^isub>1 a\<^isub>2) st = (aval a\<^isub>1 st < aval a\<^isub>2 st)" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
266 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
267 |
datatype |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
268 |
com' = SKIP |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
269 |
| Assign name aexp ("_ ::= _" [1000, 61] 61) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
270 |
| Semi com' com' ("_; _" [60, 61] 60) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
271 |
| If bexp com' com' ("IF _ THEN _ ELSE _" [0, 0, 61] 61) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
272 |
| While bexp com' ("WHILE _ DO _" [0, 61] 61) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
273 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
274 |
inductive |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
275 |
big_step :: "com' * state' \<Rightarrow> state' \<Rightarrow> bool" (infix "\<Rightarrow>" 55) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
276 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
277 |
Skip: "(SKIP,s) \<Rightarrow> s" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
278 |
| Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
279 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
280 |
| Semi: "(c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2 \<Longrightarrow> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<Longrightarrow> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
281 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
282 |
| IfTrue: "bval b s \<Longrightarrow> (c\<^isub>1,s) \<Rightarrow> t \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
283 |
| IfFalse: "\<not>bval b s \<Longrightarrow> (c\<^isub>2,s) \<Rightarrow> t \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
284 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
285 |
| WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
286 |
| WhileTrue: "bval b s\<^isub>1 \<Longrightarrow> (c,s\<^isub>1) \<Rightarrow> s\<^isub>2 \<Longrightarrow> (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
287 |
\<Longrightarrow> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
288 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
289 |
code_pred big_step . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
290 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
291 |
thm big_step.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
292 |
|
42094
e6867e9c6d10
allowing special set comprehensions in values command; adding an example for special set comprehension in values
bulwahn
parents:
41413
diff
changeset
|
293 |
definition list :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list" where |
e6867e9c6d10
allowing special set comprehensions in values command; adding an example for special set comprehension in values
bulwahn
parents:
41413
diff
changeset
|
294 |
"list s n = map s [0 ..< n]" |
e6867e9c6d10
allowing special set comprehensions in values command; adding an example for special set comprehension in values
bulwahn
parents:
41413
diff
changeset
|
295 |
|
e6867e9c6d10
allowing special set comprehensions in values command; adding an example for special set comprehension in values
bulwahn
parents:
41413
diff
changeset
|
296 |
values [expected "{[42, (43 :: nat)]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}" |
e6867e9c6d10
allowing special set comprehensions in values command; adding an example for special set comprehension in values
bulwahn
parents:
41413
diff
changeset
|
297 |
|
e6867e9c6d10
allowing special set comprehensions in values command; adding an example for special set comprehension in values
bulwahn
parents:
41413
diff
changeset
|
298 |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
299 |
subsection {* CCS *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
300 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
301 |
text{* This example formalizes finite CCS processes without communication or |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
302 |
recursion. For simplicity, labels are natural numbers. *} |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
303 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
304 |
datatype proc = nil | pre nat proc | or proc proc | par proc proc |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
305 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
306 |
inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
307 |
"step (pre n p) n p" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
308 |
"step p1 a q \<Longrightarrow> step (or p1 p2) a q" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
309 |
"step p2 a q \<Longrightarrow> step (or p1 p2) a q" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
310 |
"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
311 |
"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
312 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
313 |
code_pred step . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
314 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
315 |
inductive steps where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
316 |
"steps p [] p" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
317 |
"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
318 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
319 |
code_pred steps . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
320 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
321 |
values 3 |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
322 |
"{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
323 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
324 |
values 5 |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
325 |
"{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
326 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
327 |
values 3 "{(a,q). step (par nil nil) a q}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
328 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
329 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
330 |
end |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
331 |