equal
deleted
inserted
replaced
6 imports Main |
6 imports Main |
7 begin |
7 begin |
8 |
8 |
9 datatype cmp_val = LT | EQ | GT |
9 datatype cmp_val = LT | EQ | GT |
10 |
10 |
11 function cmp :: "'a:: linorder \<Rightarrow> 'a \<Rightarrow> cmp_val" where |
11 definition cmp :: "'a:: linorder \<Rightarrow> 'a \<Rightarrow> cmp_val" where |
12 "x < y \<Longrightarrow> cmp x y = LT" | |
12 "cmp x y = (if x < y then LT else if x=y then EQ else GT)" |
13 "x = y \<Longrightarrow> cmp x y = EQ" | |
|
14 "x > y \<Longrightarrow> cmp x y = GT" |
|
15 by (auto, force) |
|
16 termination by lexicographic_order |
|
17 |
13 |
18 lemma |
14 lemma |
19 LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y" |
15 LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y" |
20 and EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y" |
16 and EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y" |
21 and GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y" |
17 and GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y" |
22 by (cases x y rule: linorder_cases, auto)+ |
18 by (auto simp: cmp_def) |
23 |
19 |
24 lemma case_cmp_if[simp]: "(case c of EQ \<Rightarrow> e | LT \<Rightarrow> l | GT \<Rightarrow> g) = |
20 lemma case_cmp_if[simp]: "(case c of EQ \<Rightarrow> e | LT \<Rightarrow> l | GT \<Rightarrow> g) = |
25 (if c = LT then l else if c = GT then g else e)" |
21 (if c = LT then l else if c = GT then g else e)" |
26 by(simp split: cmp_val.split) |
22 by(simp split: cmp_val.split) |
27 |
23 |