equal
deleted
inserted
replaced
11 |
11 |
12 (*********************************************************************************) |
12 (*********************************************************************************) |
13 (**** SHADOW SYNTAX AND SEMANTICS ****) |
13 (**** SHADOW SYNTAX AND SEMANTICS ****) |
14 (*********************************************************************************) |
14 (*********************************************************************************) |
15 |
15 |
16 datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num |
16 datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num |
17 | Mul int num |
17 | Mul int num |
18 |
18 |
19 (* A size for num to make inductive proofs simpler*) |
19 (* A size for num to make inductive proofs simpler*) |
20 primrec num_size :: "num \<Rightarrow> nat" where |
20 primrec num_size :: "num \<Rightarrow> nat" where |
21 "num_size (C c) = 1" |
21 "num_size (C c) = 1" |
34 | "Inum bs (Neg a) = -(Inum bs a)" |
34 | "Inum bs (Neg a) = -(Inum bs a)" |
35 | "Inum bs (Add a b) = Inum bs a + Inum bs b" |
35 | "Inum bs (Add a b) = Inum bs a + Inum bs b" |
36 | "Inum bs (Sub a b) = Inum bs a - Inum bs b" |
36 | "Inum bs (Sub a b) = Inum bs a - Inum bs b" |
37 | "Inum bs (Mul c a) = (real c) * Inum bs a" |
37 | "Inum bs (Mul c a) = (real c) * Inum bs a" |
38 (* FORMULAE *) |
38 (* FORMULAE *) |
39 datatype_new fm = |
39 datatype fm = |
40 T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| |
40 T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| |
41 NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm |
41 NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm |
42 |
42 |
43 |
43 |
44 (* A size for fm *) |
44 (* A size for fm *) |