[isabelle] Prelim lifting & coercion done: Want a type of non-negatives for a field, to work like nat/int



On 2/10/2014 11:02 AM, Dmitriy Traytel wrote:
Exactly. In principle this could be supported in the incomplete algorithm (2), but it isn't yet (and I will not promise anything ;-) ).

I added "lifting" and "coercion" in the subject to make sure Ondrej and Dmitriy see it, but here I keep my talk general, since it's a mailing list.

From here, I describe the three files I attach, summarize why I think I would and wouldn't want to use the types I defined, and try to make my case for Ondrej and Dmitriy to expand the ability of lifting and coercion to accept type variables where they currently don't.

Well, things are good already. I'm just finishing this off.

The three files I attach are part of my attempt to make a case. The algebra is already there in HOL, and I'm more interested in working with abstract algebraic structures than with the rational and real numbers. Partly, it's because they're at chapters 4, 13, and 14, where the rationals and reals are at chapter 76 and 79 of the HOL document. It'll take me while to get to chapter 14, let alone chapter 79.

It probably wouldn't be good to use a special type of positives just to get rid of a few conditions in the premises, but there could be applications where their use would be structural, such as being used to generalize positive and negative exponents for different algebraic structures. Also, I could use them in a datatype, as with the following, where the types would be closed under addition:

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

Use them for what? Nothing that I can think of right now.

I tried workarounds using option, ordered pairs, and lists, and those were good enough for what's in the file `lF0_lF1.thy`. In that file, I do "Lift nothing much; Coerce everything". It occurred to me that I didn't have to do anything but use `setup_lifting`.

The main thing I wanted from the lifting was the numerals, and I was having problems proving the type class requirements with the clutter of the types I mentioned.

That led me to `Lifting_Option.thy`, and I cut and pasted and modified from there to set up a datatype in `dID_lifting.thy`, which is just an identity datatype:

datatype 'a dID = dIDc 'a

I couldn't have done it without Sledgehammer, and thanks to Brian Huffman and Ondreg for that file.

With that datatype, I was able to instantiate my typedef datatypes to get the requirements, using lifting, for numeral, up to `semiring_1`, and that file is `lF0_numerals.thy`.

Thanks,
GB

(*Gottfried Barrow*)
theory dID_lifting
imports Complex_Main 
begin

(******************************************************************************)
(* dID: Relator and predicator properties, adapted from Lifting_Option.thy    *)
(******************************************************************************)

datatype 'a dID = dIDc 'a

primrec dIDget :: "'a dID => 'a" where
  "dIDget (dIDc x) = x"

definition 
  dID_rel :: "('a => 'b => bool) => 'a dID => 'b dID => bool"
where 
  "dID_rel R x y = (case (x, y) of (dIDc x, dIDc y) => R x y)"
  
lemma dID_rel_simp [simp]:
  "dID_rel R (dIDc x) (dIDc y) = R x y"
by(simp add: dID_rel_def)

lemma dID_rel_eq [relator_eq]:
  "dID_rel (op =) = (op =)"
by (simp add: dID_rel_def fun_eq_iff split: dID.split)

lemma dID_rel_mono [relator_mono]:
  assumes "A \<le> B"
  shows "(dID_rel A) \<le> (dID_rel B)"
using assms by (auto simp: dID_rel_def split: dID.splits)

lemma dID_rel_OO [relator_distr]:
  "(dID_rel A) OO (dID_rel B) = dID_rel (A OO B)"
apply(rule ext)+  
apply(auto simp: dID_rel_def OO_def split: dID.split)
by(metis dID.exhaust)

lemma Domainp_dID [relator_domain]:
  assumes "Domainp A = P"
  shows "Domainp (dID_rel A) = (dID_case P)"
using assms unfolding Domainp_iff[abs_def] dID_rel_def[abs_def]
apply(auto iff: fun_eq_iff split: dID.split)
apply (metis (full_types) dID.cases dID.exhaust)
by(metis dID.cases)

lemma reflp_dID_rel[reflexivity_rule]:
  "reflp R ==> reflp (dID_rel R)"
  unfolding reflp_def dID.split
by(metis dID.exhaust dID_rel_simp)
   
lemma left_total_dID_rel[reflexivity_rule]:
  "left_total R ==> left_total (dID_rel R)"
  unfolding left_total_def dID.split 
by(metis dID.exhaust dID_rel_simp)

lemma left_unique_dID_rel [reflexivity_rule]:
  "left_unique R ==> left_unique (dID_rel R)"
  unfolding left_unique_def dID.split 
by(metis dID.exhaust dID_rel_simp)

lemma right_total_dID_rel [transfer_rule]:
  "right_total R ==> right_total (dID_rel R)"
  unfolding right_total_def dID.split
by(metis dID.exhaust dID_rel_simp)

lemma right_unique_dID_rel [transfer_rule]:
  "right_unique R ==> right_unique (dID_rel R)"
  unfolding right_unique_def dID.split
by(metis dID.exhaust dID_rel_simp)

lemma bi_total_dID_rel [transfer_rule]:
  "bi_total R ==> bi_total (dID_rel R)"
  unfolding bi_total_def dID.split
by(metis dID.exhaust dID_rel_simp)

lemma bi_unique_dID_rel [transfer_rule]:
  "bi_unique R ==> bi_unique (dID_rel R)"
  unfolding bi_unique_def dID.split
by(metis dID.exhaust dID_rel_simp dIDget.simps)

lemma dID_invariant_commute [invariant_commute]:
  "dID_rel (Lifting.invariant P) = Lifting.invariant (dID_case P)"
apply(auto simp add: fun_eq_iff Lifting.invariant_def dID.split) 
apply(metis (lifting, no_types) Domainp.DomainI Domainp.cases Domainp_dID 
  dID.cases dID.exhaust)
apply(metis (lifting, full_types) dID.exhaust dID_rel_simp)
by(metis (lifting, mono_tags) dID.cases dID.exhaust dID_rel_def prod_caseI)
  
(******************************************************************************)
(* dID: Quotient theorem for the Lifting package                              *) 
(******************************************************************************)

(*MY MAP: Based on Option.map in Option.thy.*)

definition dID_map :: "('a => 'b) => 'a dID => 'b dID" where
  "dID_map = (%f x. case x of dIDc x => dIDc (f x))"

lemma Quotient_dID [quot_map]:
  assumes "Quotient R Abs Rep T"
  shows "Quotient (dID_rel R) (dID_map Abs)
    (dID_map Rep) (dID_rel T)"
  using assms unfolding Quotient_alt_def dID_rel_def
apply(simp split: dID.split)
by(smt dID.cases dID.inject dID_map_def)

(******************************************************************************)
(* dID: Transfer rules for the Transfer package                               *) 
(******************************************************************************)

context
begin
interpretation lifting_syntax .

lemma dIDc_transfer [transfer_rule]: "(A ===> dID_rel A) dIDc dIDc"
  unfolding fun_rel_def by simp
  
lemma dID_case_transfer [transfer_rule]:
  "((A ===> B) ===> dID_rel A ===> B) dID_case dID_case"
  unfolding fun_rel_def dID.split 
apply(auto)
by(metis dID.cases dID.exhaust dID_rel_simp)
  
lemma dID_map_transfer [transfer_rule]:
  "((A ===> B) ===> dID_rel A ===> dID_rel B) dID_map dID_map"
  unfolding dID_map_def by transfer_prover

(*MY BIND: Based on Option.bind in Option.thy.*) 

primrec dID_bind :: "'a dID => ('a => 'b dID) => 'b dID" where
  "dID_bind (dIDc x) f = f x"    
    
lemma dID_bind_transfer [transfer_rule]:
  "(dID_rel A ===> (A ===> dID_rel B) ===> dID_rel B)
    dID_bind dID_bind"
  unfolding fun_rel_def dID.split
by(metis dID.exhaust dID_bind.simps dID_rel_simp)

end 
  

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





(*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





(*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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.