(*Gottfried Barrow*)
theory lF0_numerals
imports Complex_Main i140208sa__dID_lifting "../../../gh/iHelp/i" 
begin

(*ABSTRACT: Lift everything I can for the non-negatives of a given algebraic 
  structure.
(1) Here, I instantiated up to `semiring_1`.
(2) I don't know how to do `semiring_char_0`.
*)

(******************************************************************************)
(* TYPEDEF lF0: non-negative members of a field                               *) 
(******************************************************************************)

typedef 'a::linordered_field lF0 = "{x::'a dID. 0 \<le> dIDget x}"
  by(simp, metis dIDget.simps order_refl)
declare Abs_lF0_inverse [simp add]
declare Abs_lF0_inject [simp add]
declare Rep_lF0_inject [simp add]
declare Rep_lF0_inverse [simp add]
  
setup_lifting type_definition_lF0

abbreviation (input) get_Rep_lF0 :: "'a::linordered_field lF0 => 'a" where
  "get_Rep_lF0 x == dIDget(Rep_lF0 x)"
abbreviation (input) get_Rep_lF0_rat :: "rat lF0 => rat" where
  "get_Rep_lF0_rat q == get_Rep_lF0 q"  
abbreviation (input) get_Rep_lF0_real :: "real lF0 => real" where
  "get_Rep_lF0_real r == get_Rep_lF0 r"  
declare 
  [[coercion get_Rep_lF0_rat]]
  [[coercion get_Rep_lF0_real]]
notation 
  get_Rep_lF0 ("_\<^sub>:\<^sub>f\<^sub>0" [1000] 1000) and
  get_Rep_lF0_rat ("_\<^sub>:\<^sub>q\<^sub>0" [1000] 1000) and
  get_Rep_lF0_real ("_\<^sub>:\<^sub>r\<^sub>0" [1000] 1000)
  
abbreviation "slF0 == {x::'a::linordered_field. 0 \<le> x}"

(********************)
(* ord              *)
(********************)
instantiation lF0 :: (linordered_field) "{ord}"
begin

lift_definition less_eq_lF0 :: "'a lF0 => 'a lF0 => bool" 
  is "\<lambda>x y. x\<^sub>:\<^sub>f\<^sub>0 \<le> y\<^sub>:\<^sub>f\<^sub>0" .
declare less_eq_lF0_def [simp add]

lift_definition less_lF0 :: "'a lF0 => 'a lF0 => bool" 
  is "\<lambda>x y. x\<^sub>:\<^sub>f\<^sub>0 < y\<^sub>:\<^sub>f\<^sub>0" .
declare less_lF0_def [simp add]
instance proof
qed
end

(********************)
(* equal, zero, one *)
(********************)
instantiation lF0 :: (linordered_field) "{equal,zero,one}"
begin
lift_definition zero_lF0 :: "'a lF0" is "dIDc 0"
  by(auto) 
declare zero_lF0_def [simp add]

lift_definition one_lF0 :: "'a lF0" is "dIDc 1"
  by(simp) 
declare one_lF0_def [simp add]

lift_definition equal_lF0 :: "'a lF0 => 'a lF0 => bool" 
  is "\<lambda>x y. x\<^sub>:\<^sub>f\<^sub>0 = y\<^sub>:\<^sub>f\<^sub>0" .
declare equal_lF0_def [simp add]

instance proof
  fix x y :: "'a lF0"
show "equal_class.equal x y = (x = y)"
  by(simp, metis Rep_lF0_inverse dID.exhaust dIDget.simps)
qed 
end

(**********************************************************)
(* plus, times, semiring_numeral = semiring + monoid_mult *)
(**********************************************************)

theorem nnmult_in_lF0_set:
  assumes "0 \<le> (a::'a::linordered_field)"
  assumes "0 \<le> b"
  shows "dIDc(a * b) \<in> {x::'a dID. 0 \<le> dIDget x}"
by(simp, metis assms(1) assms(2) split_mult_pos_le)

theorem nnmult_Abs_lF0_inver [simp]:
  assumes a1: "0 \<le> (a::'a::linordered_field)"
  assumes a2: "0 \<le> b"
  shows "Rep_lF0(Abs_lF0(dIDc(a * b))) = dIDc(a * b)"
by(metis (lifting, no_types) assms(1) a1 a2 Abs_lF0_inverse nnmult_in_lF0_set)

(**********************************************************)

instantiation lF0 :: (linordered_field) semiring_numeral
begin

lift_definition plus_lF0 :: "'a lF0 => 'a lF0 => 'a lF0" 
  is "\<lambda>x y. Abs_lF0(dIDc(x\<^sub>:\<^sub>f\<^sub>0 + y\<^sub>:\<^sub>f\<^sub>0))" . 
declare plus_lF0_def [simp add]

lift_definition times_lF0 :: "'a lF0 => 'a lF0 => 'a lF0" 
  is "\<lambda>x y. Abs_lF0(dIDc(x\<^sub>:\<^sub>f\<^sub>0 * y\<^sub>:\<^sub>f\<^sub>0))" . 
declare times_lF0_def [simp add]

instance proof
  fix a b c :: "'a lF0"
show "(a * b) * c = a * (b * c)"
  apply(simp,transfer,auto)
  by(metis comm_semiring_1_class.normalizing_semiring_rules(17))
next
  fix a :: "'a lF0"
show "1 * a = a"
  by(simp, metis Rep_lF0_inverse dID.exhaust dIDget.simps)
next
  fix a :: "'a lF0"
show "a * 1 = a"
  by(simp, metis Rep_lF0_inverse dID.exhaust dIDget.simps)
next
  fix a b c :: "'a lF0"
show "(a + b) + c = a + (b + c)"
  by(simp,transfer,auto)
next
  fix a b :: "'a lF0"
show "a + b = b + a"
  by(simp,transfer,auto)
next
  fix a b c :: "'a lF0"
show "(a + b) * c = (a * c) + (b * c)"
  by(simp,transfer,auto,metis comm_semiring_class.distrib)
next
  fix a b c :: "'a lF0"
show "a * (b + c) = (a * b) + (a * c)"
  apply(simp,transfer,auto)
  by(metis comm_semiring_1_class.normalizing_semiring_rules(34))
qed 
end

(***************************************************************************)
(* NUMERAL: ring_char_0 = ring_1 + semiring_char_0                         *)
(*   semiring_char_0 = semiring_1 + assumes inj_of_nat:"inj of_nat"        *)
(***************************************************************************)
print_locale ring_char_0
  print_locale ring_1
  print_locale semiring_char_0
    print_locale semiring_1

instantiation lF0 :: (linordered_field) semiring_1
begin
instance proof
  fix a :: "'a lF0"
show "0 + a = a"
  by(simp,metis Rep_lF0_inverse dID.exhaust dIDget.simps)
next
  fix a :: "'a lF0"
show "a * 0 = 0"
  by(simp)
next
  fix a :: "'a lF0"
show "0 * a = 0"
  by(simp)
next
  fix a :: "'a lF0"
show "0 \<noteq> (1::'a lF0)"
  by(simp)
qed
end

instance lF0 :: (linordered_field) semiring_char_0
proof
show "inj (of_nat :: nat => 'a::linordered_field lF0)"
oops

(******************************************************************************)
end