18 |
18 |
19 notation (xsymbols) |
19 notation (xsymbols) |
20 comb (infixr "\<box>" 55) |
20 comb (infixr "\<box>" 55) |
21 |
21 |
22 lemma comb_nil_left [simp]: "comb_nil \<box> f = f" |
22 lemma comb_nil_left [simp]: "comb_nil \<box> f = f" |
23 by (simp add: comb_def comb_nil_def split_beta) |
23 by (simp add: comb_def comb_nil_def split_beta) |
24 |
24 |
25 lemma comb_nil_right [simp]: "f \<box> comb_nil = f" |
25 lemma comb_nil_right [simp]: "f \<box> comb_nil = f" |
26 by (simp add: comb_def comb_nil_def split_beta) |
26 by (simp add: comb_def comb_nil_def split_beta) |
27 |
27 |
28 lemma comb_assoc [simp]: "(fa \<box> fb) \<box> fc = fa \<box> (fb \<box> fc)" |
28 lemma comb_assoc [simp]: "(fa \<box> fb) \<box> fc = fa \<box> (fb \<box> fc)" |
29 by (simp add: comb_def split_beta) |
29 by (simp add: comb_def split_beta) |
30 |
30 |
31 lemma comb_inv: "(xs', x') = (f1 \<box> f2) x0 \<Longrightarrow> |
31 lemma comb_inv: |
32 \<exists> xs1 x1 xs2 x2. (xs1, x1) = (f1 x0) \<and> (xs2, x2) = f2 x1 \<and> xs'= xs1 @ xs2 \<and> x'=x2" |
32 "(xs', x') = (f1 \<box> f2) x0 \<Longrightarrow> |
33 apply (case_tac "f1 x0") |
33 \<exists>xs1 x1 xs2 x2. (xs1, x1) = (f1 x0) \<and> (xs2, x2) = f2 x1 \<and> xs'= xs1 @ xs2 \<and> x'=x2" |
34 apply (case_tac "f2 x1") |
34 by (case_tac "f1 x0") (simp add: comb_def split_beta) |
35 apply (simp add: comb_def split_beta) |
|
36 done |
|
37 |
35 |
38 (**********************************************************************) |
36 (**********************************************************************) |
39 |
37 |
40 abbreviation (input) |
38 abbreviation (input) |
41 mt_of :: "method_type \<times> state_type \<Rightarrow> method_type" |
39 mt_of :: "method_type \<times> state_type \<Rightarrow> method_type" |