(*Gottfried Barrow*)
theory lF0_lF1
imports Complex_Main dID_lifting (*"../../../gh/iHelp/i"*)
begin

(*ABSTRACT: Max coercion, Minimal lifting
  (1) Lift nothing. Coerce everything.
  (2) There is `setup_lifting`. Any questions?
*)
 
(******************************************************************************)
(* 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)
  
setup_lifting type_definition_lF0

abbreviation "slF0 == {x::'a::linordered_field. 0 \<le> x}"

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)
  
(******************************************************************************)
(* TYPEDEF lF1: non-negative members of a field                               *) 
(******************************************************************************)  

typedef 'a::linordered_field lF1 = "{x::'a dID. 0 < dIDget x}"
proof- 
have "dIDc 1 \<in> {x::'a dID. 0 < dIDget x}" 
  by(auto) 
thus ?thesis 
  by(blast) 
qed
  
setup_lifting type_definition_lF1

abbreviation "slF1 == {x::'a::linordered_field. 0 < x}"

abbreviation (input) get_Rep_lF1 :: "'a::linordered_field lF1 => 'a" where
  "get_Rep_lF1 x == dIDget(Rep_lF1 x)"
abbreviation (input) get_Rep_lF1_rat :: "rat lF1 => rat" where
  "get_Rep_lF1_rat q == get_Rep_lF1 q"  
abbreviation (input) get_Rep_lF1_real :: "real lF1 => real" where
  "get_Rep_lF1_real r == get_Rep_lF1 r"  
declare 
  [[coercion get_Rep_lF1_rat]]
  [[coercion get_Rep_lF1_real]]
notation 
  get_Rep_lF1 ("_\<^sub>:\<^sub>f\<^sub>1" [1000] 1000) and
  get_Rep_lF1_rat ("_\<^sub>:\<^sub>q\<^sub>1" [1000] 1000) and
  get_Rep_lF1_real ("_\<^sub>:\<^sub>r\<^sub>1" [1000] 1000)
  
(******************************************************************************)
(* SOME THEOREMS                                                              *) 
(******************************************************************************) 

(*ORIGINAL*) 
lemma --"positive_imp_inverse_positive:" (in linordered_field)
  assumes a_gt_0: "0 < a" 
  shows "0 < inverse a"
by(metis positive_imp_inverse_positive assms)

lemma positive_imp_inverse_positive_LF: 
  "0 < inverse a\<^sub>:\<^sub>f\<^sub>1"
apply(transfer, auto)
by(metis positive_imp_inverse_positive)

lemma positive_imp_inverse_positive_RAT: 
  "0 < inverse a\<^sub>:\<^sub>q\<^sub>1"
apply(transfer) 
by(simp) 

lemma positive_imp_inverse_positive_REAL: 
  "0 < inverse a\<^sub>:\<^sub>r\<^sub>1"
apply(transfer) 
by(simp) 

print_statement 
  positive_imp_inverse_positive
  positive_imp_inverse_positive_LF
  positive_imp_inverse_positive_RAT
  positive_imp_inverse_positive_REAL  
  
(*ORIGINAL*) 
lemma --"inverse_le_imp_le:" (in linordered_field)
  assumes invle: "inverse a \<le> inverse b" and apos: "0 < a"
  shows "b \<le> a"
by(metis inverse_le_imp_le assms)

lemma inverse_le_imp_le_LF:
  assumes invle: "inverse a\<^sub>:\<^sub>f\<^sub>1 \<le> inverse b"
  shows "b \<le> a\<^sub>:\<^sub>f\<^sub>1"
using assms
apply(transfer, auto)
by(metis less_imp_inverse_less not_less)
  
lemma inverse_le_imp_le_RAT:
  assumes invle: "inverse a\<^sub>:\<^sub>q\<^sub>1 \<le> inverse b"
  shows "b \<le> a"                                    (* <------ coerced. Nice! *)
using assms  
by(metis inverse_le_imp_le_LF)

lemma inverse_le_imp_le_REAL:
  assumes invle: "inverse a\<^sub>:\<^sub>r\<^sub>1 \<le> inverse b"
  shows "b \<le> a"                                    (* <------ coerced. Nice! *)
using assms  
by(metis inverse_le_imp_le_LF)

print_statement 
  inverse_le_imp_le
  positive_imp_inverse_positive_LF
  positive_imp_inverse_positive_RAT
  positive_imp_inverse_positive_REAL  
  
(******************************************************************************)
(* SIMPLE NUMERAL STUFF                                                       *) 
(******************************************************************************)

theorem stuffer:
  "44 + x\<^sub>:\<^sub>f\<^sub>1 > 44"
apply(simp)
apply(transfer)
using[[simp_trace, simp_trace_depth_limit=100]]
by(simp)

print_statement stuffer

(******************************************************************************)
(* OPS WITH ONLY THE SUBTYPE                                                  *) 
(******************************************************************************)

theorem lF1_closure:
  "x\<^sub>:\<^sub>f\<^sub>1 + y\<^sub>:\<^sub>f\<^sub>1 \<in> slF1"
by(transfer, simp)

(******************************************************************************)
(* A DATATYPE USING NON-NEGATIVES & NON-POSITIVES                             *) 
(******************************************************************************)

typedef 'a::linordered_field lFN0 = "{x::'a dID. dIDget x \<le> 0}"
  by(simp, metis dIDget.simps order_refl)

datatype 'a::linordered_field lofD =
  NNeg "'a lF0"
 |NPos "'a lFN0"
  

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