25 instance i :: prog .. |
25 instance i :: prog .. |
26 |
26 |
27 |
27 |
28 consts |
28 consts |
29 (*** Evaluation Judgement ***) |
29 (*** Evaluation Judgement ***) |
30 Eval :: "[i,i]\<Rightarrow>prop" (infixl "\<longlongrightarrow>" 20) |
30 Eval :: "[i,i]\<Rightarrow>prop" (infixl \<open>\<longlongrightarrow>\<close> 20) |
31 |
31 |
32 (*** Bisimulations for pre-order and equality ***) |
32 (*** Bisimulations for pre-order and equality ***) |
33 po :: "['a,'a]\<Rightarrow>o" (infixl "[=" 50) |
33 po :: "['a,'a]\<Rightarrow>o" (infixl \<open>[=\<close> 50) |
34 |
34 |
35 (*** Term Formers ***) |
35 (*** Term Formers ***) |
36 true :: "i" |
36 true :: "i" |
37 false :: "i" |
37 false :: "i" |
38 pair :: "[i,i]\<Rightarrow>i" ("(1<_,/_>)") |
38 pair :: "[i,i]\<Rightarrow>i" (\<open>(1<_,/_>)\<close>) |
39 lambda :: "(i\<Rightarrow>i)\<Rightarrow>i" (binder "lam " 55) |
39 lambda :: "(i\<Rightarrow>i)\<Rightarrow>i" (binder \<open>lam \<close> 55) |
40 "case" :: "[i,i,i,[i,i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i" |
40 "case" :: "[i,i,i,[i,i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i" |
41 "apply" :: "[i,i]\<Rightarrow>i" (infixl "`" 56) |
41 "apply" :: "[i,i]\<Rightarrow>i" (infixl \<open>`\<close> 56) |
42 bot :: "i" |
42 bot :: "i" |
43 |
43 |
44 (******* EVALUATION SEMANTICS *******) |
44 (******* EVALUATION SEMANTICS *******) |
45 |
45 |
46 (** This is the evaluation semantics from which the axioms below were derived. **) |
46 (** This is the evaluation semantics from which the axioms below were derived. **) |