7 |
7 |
8 theory SemilatAlg |
8 theory SemilatAlg |
9 imports Typing_Framework Product |
9 imports Typing_Framework Product |
10 begin |
10 begin |
11 |
11 |
12 constdefs |
12 definition lesubstep_type :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool" |
13 lesubstep_type :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool" |
13 ("(_ /<=|_| _)" [50, 0, 51] 50) where |
14 ("(_ /<=|_| _)" [50, 0, 51] 50) |
|
15 "x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'" |
14 "x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'" |
16 |
15 |
17 consts |
16 primrec plusplussub :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65) where |
18 plusplussub :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65) |
|
19 primrec |
|
20 "[] ++_f y = y" |
17 "[] ++_f y = y" |
21 "(x#xs) ++_f y = xs ++_f (x +_f y)" |
18 | "(x#xs) ++_f y = xs ++_f (x +_f y)" |
22 |
19 |
23 constdefs |
20 definition bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool" where |
24 bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool" |
|
25 "bounded step n == !p<n. !s. !(q,t):set(step p s). q<n" |
21 "bounded step n == !p<n. !s. !(q,t):set(step p s). q<n" |
26 |
22 |
27 pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool" |
23 definition pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool" where |
28 "pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A" |
24 "pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A" |
29 |
25 |
30 mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool" |
26 definition mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool" where |
31 "mono r step n A == |
27 "mono r step n A == |
32 \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t" |
28 \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t" |
33 |
|
34 |
29 |
35 lemma pres_typeD: |
30 lemma pres_typeD: |
36 "\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A" |
31 "\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A" |
37 by (unfold pres_type_def, blast) |
32 by (unfold pres_type_def, blast) |
38 |
33 |