equal
deleted
inserted
replaced
76 lemma int_def: "int n = Abs_Integ (n, 0)" |
76 lemma int_def: "int n = Abs_Integ (n, 0)" |
77 by (induct n, simp add: zero_int.abs_eq, |
77 by (induct n, simp add: zero_int.abs_eq, |
78 simp add: one_int.abs_eq plus_int.abs_eq) |
78 simp add: one_int.abs_eq plus_int.abs_eq) |
79 |
79 |
80 lemma int_transfer [transfer_rule]: |
80 lemma int_transfer [transfer_rule]: |
81 "(fun_rel (op =) cr_int) (\<lambda>n. (n, 0)) int" |
81 "(rel_fun (op =) cr_int) (\<lambda>n. (n, 0)) int" |
82 unfolding fun_rel_def cr_int_def int_def by simp |
82 unfolding rel_fun_def cr_int_def int_def by simp |
83 |
83 |
84 lemma int_diff_cases: |
84 lemma int_diff_cases: |
85 obtains (diff) m n where "z = int m - int n" |
85 obtains (diff) m n where "z = int m - int n" |
86 by transfer clarsimp |
86 by transfer clarsimp |
87 |
87 |