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