author | traytel |
Fri, 28 Feb 2020 21:23:11 +0100 | |
changeset 71494 | cbe0b6b0bed8 |
parent 67443 | 3abf6a722518 |
child 80914 | d97fdabd9e2b |
permissions | -rw-r--r-- |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
1 |
theory Examples |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66283
diff
changeset
|
2 |
imports Main "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 |
|
63167 | 7 |
section \<open>Formal Languages\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
8 |
|
63167 | 9 |
subsection \<open>General Context Free Grammars\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
10 |
|
63167 | 11 |
text \<open>a contribution by Aditi Barthwal\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
12 |
|
58310 | 13 |
datatype ('nts,'ts) symbol = NTS 'nts |
39655
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 |
|
58310 | 17 |
datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list" |
39655
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 |
|
52666 | 32 |
definition derivesp :: |
33 |
"(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool" |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
34 |
where |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
35 |
"derivesp g = (\<lambda> lhs rhs. (lhs, rhs) \<in> derives (Collect (fst g), snd g))" |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
36 |
|
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
37 |
lemma [code_pred_def]: |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
38 |
"derivesp g = (\<lambda> lsl rsl. \<exists>s1 s2 lhs rhs. |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
39 |
(s1 @ [NTS lhs] @ s2 = lsl) \<and> |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
40 |
(s1 @ rhs @ s2) = rsl \<and> |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
41 |
(fst g) (rule lhs rhs))" |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
42 |
unfolding derivesp_def derives_def by auto |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
43 |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
44 |
abbreviation "example_grammar == |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
45 |
({ rule ''S'' [NTS ''A'', NTS ''B''], |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
46 |
rule ''S'' [TS ''a''], |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
47 |
rule ''A'' [TS ''b'']}, ''S'')" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
48 |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
49 |
definition "example_rules == |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
50 |
(%x. x = rule ''S'' [NTS ''A'', NTS ''B''] \<or> |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
51 |
x = rule ''S'' [TS ''a''] \<or> |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
52 |
x = rule ''A'' [TS ''b''])" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
53 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
54 |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
55 |
code_pred [inductify, skip_proof] derivesp . |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
56 |
|
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
57 |
thm derivesp.equation |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
58 |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
59 |
definition "testp = (% rhs. derivesp (example_rules, ''S'') [NTS ''S''] rhs)" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
60 |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
61 |
code_pred (modes: o \<Rightarrow> bool) [inductify] testp . |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
62 |
thm testp.equation |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
63 |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
64 |
values "{rhs. testp rhs}" |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
65 |
|
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
66 |
declare rtranclp.intros(1)[code_pred_def] converse_rtranclp_into_rtranclp[code_pred_def] |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
67 |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
68 |
code_pred [inductify] rtranclp . |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
69 |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
42463
diff
changeset
|
70 |
definition "test2 = (\<lambda> rhs. rtranclp (derivesp (example_rules, ''S'')) [NTS ''S''] rhs)" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
71 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
72 |
code_pred [inductify, skip_proof] test2 . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
73 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
74 |
values "{rhs. test2 rhs}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
75 |
|
63167 | 76 |
subsection \<open>Some concrete Context Free Grammars\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
77 |
|
58310 | 78 |
datatype alphabet = a | b |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
79 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
80 |
inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
81 |
"[] \<in> S\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
82 |
| "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
83 |
| "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
84 |
| "w \<in> S\<^sub>1 \<Longrightarrow> a # w \<in> A\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
85 |
| "w \<in> S\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
86 |
| "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
87 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
88 |
code_pred [inductify] S\<^sub>1p . |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
89 |
code_pred [random_dseq inductify] S\<^sub>1p . |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
90 |
thm S\<^sub>1p.equation |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
91 |
thm S\<^sub>1p.random_dseq_equation |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
92 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
93 |
values [random_dseq 5, 5, 5] 5 "{x. S\<^sub>1p x}" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
94 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
95 |
inductive_set S\<^sub>2 and A\<^sub>2 and B\<^sub>2 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
96 |
"[] \<in> S\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
97 |
| "w \<in> A\<^sub>2 \<Longrightarrow> b # w \<in> S\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
98 |
| "w \<in> B\<^sub>2 \<Longrightarrow> a # w \<in> S\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
99 |
| "w \<in> S\<^sub>2 \<Longrightarrow> a # w \<in> A\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
100 |
| "w \<in> S\<^sub>2 \<Longrightarrow> b # w \<in> B\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
101 |
| "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
102 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
103 |
code_pred [random_dseq inductify] S\<^sub>2p . |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
104 |
thm S\<^sub>2p.random_dseq_equation |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
105 |
thm A\<^sub>2p.random_dseq_equation |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
106 |
thm B\<^sub>2p.random_dseq_equation |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
107 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
108 |
values [random_dseq 5, 5, 5] 10 "{x. S\<^sub>2p x}" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
109 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
110 |
inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
111 |
"[] \<in> S\<^sub>3" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
112 |
| "w \<in> A\<^sub>3 \<Longrightarrow> b # w \<in> S\<^sub>3" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
113 |
| "w \<in> B\<^sub>3 \<Longrightarrow> a # w \<in> S\<^sub>3" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
114 |
| "w \<in> S\<^sub>3 \<Longrightarrow> a # w \<in> A\<^sub>3" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
115 |
| "w \<in> S\<^sub>3 \<Longrightarrow> b # w \<in> B\<^sub>3" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
116 |
| "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
117 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
118 |
code_pred [inductify, skip_proof] S\<^sub>3p . |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
119 |
thm S\<^sub>3p.equation |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
120 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
121 |
values 10 "{x. S\<^sub>3p x}" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
122 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
123 |
inductive_set S\<^sub>4 and A\<^sub>4 and B\<^sub>4 where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
124 |
"[] \<in> S\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
125 |
| "w \<in> A\<^sub>4 \<Longrightarrow> b # w \<in> S\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
126 |
| "w \<in> B\<^sub>4 \<Longrightarrow> a # w \<in> S\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
127 |
| "w \<in> S\<^sub>4 \<Longrightarrow> a # w \<in> A\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
128 |
| "\<lbrakk>v \<in> A\<^sub>4; w \<in> A\<^sub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
129 |
| "w \<in> S\<^sub>4 \<Longrightarrow> b # w \<in> B\<^sub>4" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
130 |
| "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
131 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
132 |
code_pred (expected_modes: o => bool, i => bool) S\<^sub>4p . |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
133 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
134 |
hide_const a b |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
135 |
|
63167 | 136 |
section \<open>Semantics of programming languages\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
137 |
|
63167 | 138 |
subsection \<open>IMP\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
139 |
|
42463 | 140 |
type_synonym var = nat |
141 |
type_synonym state = "int list" |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
142 |
|
58310 | 143 |
datatype com = |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
144 |
Skip | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
145 |
Ass var "state => int" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
146 |
Seq com com | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
147 |
IF "state => bool" com com | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
148 |
While "state => bool" com |
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 |
inductive exec :: "com => state => state => bool" where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
151 |
"exec Skip s s" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
152 |
"exec (Ass x e) s (s[x := e(s)])" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
153 |
"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
|
154 |
"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
|
155 |
"~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
|
156 |
"~b s ==> exec (While b c) s s" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
157 |
"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
|
158 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
159 |
code_pred exec . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
160 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
161 |
values "{t. exec |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
162 |
(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
|
163 |
[3,5] t}" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
164 |
|
63167 | 165 |
subsection \<open>Lambda\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
166 |
|
58310 | 167 |
datatype type = |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
168 |
Atom nat |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
169 |
| Fun type type (infixr "\<Rightarrow>" 200) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
170 |
|
58310 | 171 |
datatype dB = |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
172 |
Var nat |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
173 |
| App dB dB (infixl "\<degree>" 200) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
174 |
| Abs type dB |
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 |
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
|
178 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
179 |
"[]\<langle>i\<rangle> = None" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
180 |
| "(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
|
181 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
182 |
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
|
183 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
184 |
"nth_el' (x # xs) 0 x" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
185 |
| "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
|
186 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
187 |
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
|
188 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
189 |
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
|
190 |
| 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
|
191 |
| 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
|
192 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
193 |
primrec |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
194 |
lift :: "[dB, nat] => dB" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
195 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
196 |
"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
|
197 |
| "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
|
198 |
| "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
|
199 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
200 |
primrec |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
201 |
subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
202 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
203 |
subst_Var: "(Var i)[s/k] = |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
204 |
(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
|
205 |
| 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
|
206 |
| 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
|
207 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
208 |
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
|
209 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
210 |
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
|
211 |
| 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
|
212 |
| 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
|
213 |
| 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
|
214 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
215 |
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
|
216 |
thm typing.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
217 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
218 |
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
|
219 |
thm beta.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
220 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
221 |
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
|
222 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
223 |
definition "reduce t = Predicate.the (reduce' t)" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
224 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
225 |
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
|
226 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
227 |
code_pred [dseq] typing . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
228 |
code_pred [random_dseq] typing . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
229 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
230 |
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
|
231 |
|
63167 | 232 |
subsection \<open>A minimal example of yet another semantics\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
233 |
|
63167 | 234 |
text \<open>thanks to Elke Salecker\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
235 |
|
42463 | 236 |
type_synonym vname = nat |
237 |
type_synonym vvalue = int |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
66453
diff
changeset
|
238 |
type_synonym var_assign = "vname \<Rightarrow> vvalue" \<comment> \<open>variable assignment\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
239 |
|
58310 | 240 |
datatype ir_expr = |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
241 |
IrConst vvalue |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
242 |
| ObjAddr vname |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
243 |
| Add ir_expr ir_expr |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
244 |
|
58310 | 245 |
datatype val = |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
246 |
IntVal vvalue |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
247 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
248 |
record configuration = |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
249 |
Env :: var_assign |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
250 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
251 |
inductive eval_var :: |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
252 |
"ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
253 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
254 |
irconst: "eval_var (IrConst i) conf (IntVal i)" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
255 |
| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)" |
52666 | 256 |
| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> |
257 |
eval_var (Add l r) conf (IntVal (vl+vr))" |
|
39655
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 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
260 |
code_pred eval_var . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
261 |
thm eval_var.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
262 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
263 |
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
|
264 |
|
63167 | 265 |
subsection \<open>Another semantics\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
266 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
66453
diff
changeset
|
267 |
type_synonym name = nat \<comment> \<open>For simplicity in examples\<close> |
42463 | 268 |
type_synonym state' = "name \<Rightarrow> nat" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
269 |
|
58310 | 270 |
datatype aexp = N nat | V name | Plus aexp aexp |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
271 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
272 |
fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
273 |
"aval (N n) _ = n" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
274 |
"aval (V x) st = st x" | |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
275 |
"aval (Plus e\<^sub>1 e\<^sub>2) st = aval e\<^sub>1 st + aval e\<^sub>2 st" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
276 |
|
58310 | 277 |
datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
278 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
279 |
primrec bval :: "bexp \<Rightarrow> state' \<Rightarrow> bool" where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
280 |
"bval (B b) _ = b" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
281 |
"bval (Not b) st = (\<not> bval b st)" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
282 |
"bval (And b1 b2) st = (bval b1 st \<and> bval b2 st)" | |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
283 |
"bval (Less a\<^sub>1 a\<^sub>2) st = (aval a\<^sub>1 st < aval a\<^sub>2 st)" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
284 |
|
58310 | 285 |
datatype |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
286 |
com' = SKIP |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
287 |
| Assign name aexp ("_ ::= _" [1000, 61] 61) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
288 |
| Semi com' com' ("_; _" [60, 61] 60) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
289 |
| 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
|
290 |
| While bexp com' ("WHILE _ DO _" [0, 61] 61) |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
291 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
292 |
inductive |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
293 |
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
|
294 |
where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
295 |
Skip: "(SKIP,s) \<Rightarrow> s" |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
296 |
| 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
|
297 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
298 |
| Semi: "(c\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2 \<Longrightarrow> (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3 \<Longrightarrow> (c\<^sub>1;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
299 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
300 |
| IfTrue: "bval b s \<Longrightarrow> (c\<^sub>1,s) \<Rightarrow> t \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
301 |
| IfFalse: "\<not>bval b s \<Longrightarrow> (c\<^sub>2,s) \<Rightarrow> t \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
302 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
303 |
| WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
304 |
| WhileTrue: "bval b s\<^sub>1 \<Longrightarrow> (c,s\<^sub>1) \<Rightarrow> s\<^sub>2 \<Longrightarrow> (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52666
diff
changeset
|
305 |
\<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
306 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
307 |
code_pred big_step . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
308 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
309 |
thm big_step.equation |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
310 |
|
42094
e6867e9c6d10
allowing special set comprehensions in values command; adding an example for special set comprehension in values
bulwahn
parents:
41413
diff
changeset
|
311 |
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
|
312 |
"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
|
313 |
|
66283
adf3155c57e2
Printing natural numbers as numerals in evaluation
eberlm <eberlm@in.tum.de>
parents:
63167
diff
changeset
|
314 |
values [expected "{[42::nat, 43]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}" |
42094
e6867e9c6d10
allowing special set comprehensions in values command; adding an example for special set comprehension in values
bulwahn
parents:
41413
diff
changeset
|
315 |
|
e6867e9c6d10
allowing special set comprehensions in values command; adding an example for special set comprehension in values
bulwahn
parents:
41413
diff
changeset
|
316 |
|
63167 | 317 |
subsection \<open>CCS\<close> |
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
318 |
|
63167 | 319 |
text\<open>This example formalizes finite CCS processes without communication or |
320 |
recursion. For simplicity, labels are natural numbers.\<close> |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
321 |
|
58310 | 322 |
datatype proc = nil | pre nat proc | or proc proc | par proc proc |
39655
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 |
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
|
325 |
"step (pre n p) n p" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
326 |
"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
|
327 |
"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
|
328 |
"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
|
329 |
"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
|
330 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
331 |
code_pred step . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
332 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
333 |
inductive steps where |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
334 |
"steps p [] p" | |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
335 |
"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
|
336 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
337 |
code_pred steps . |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
338 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
339 |
values 3 |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
340 |
"{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
|
341 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
342 |
values 5 |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
343 |
"{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
|
344 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
345 |
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
|
346 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
347 |
|
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
348 |
end |
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset
|
349 |