Theory BNF_Nonuniform_Fixpoint

theory BNF_Nonuniform_Fixpoint
imports Main
(*  Title:      HOL/Library/BNF_Nonuniform_Fixpoint.thy
    Author:     Fabian Meier, ETH Zurich
    Author:     Dmitriy Traytel, ETH Zurich

    Copyright   2016

Nonuniform (co)datatypes
*)

chapter {* Nonuniform (Co)datatypes *}

theory BNF_Nonuniform_Fixpoint
imports Main (* "~~/src/HOL/BNF_Greatest_Fixpoint" FIXME *)
keywords
  "nonuniform_datatype" :: thy_decl and
  "nonuniform_codatatype" :: thy_decl and
  "nonuniform_induct" :: thy_goal and
  "nonuniform_coinduct" :: thy_goal and
  "nonuniform_primrec" :: thy_decl and
  "nonuniform_primrecursive" :: thy_goal and
  "nonuniform_primcorec" :: thy_decl and
  "nonuniform_primcorecursive" :: thy_goal
begin

primrec snoc where
  "snoc x [] = [x]"
| "snoc x (y # xs) = y # snoc x xs"

lemma snoc_neq_Nil: "snoc x xs ≠ []"
  by (cases xs; simp)

lemma snoc: "snoc x xs = xs @ [x]"
  by (induct xs) auto

lemma rev_Cons: "rev (x # xs) = snoc x (rev xs)"
  by (auto simp: snoc)

lemma rev_snoc: "rev (snoc x xs) = x # rev xs"
  by (auto simp: snoc)

lemma fun_pred_rel: "pred_fun A B x = rel_fun (eq_onp A) (eq_onp B) x x"
  unfolding pred_fun_def rel_fun_def eq_onp_def by auto

lemma pred_funD: "pred_fun A B f ⟹ A x ⟹ B (f x)"
  unfolding pred_fun_def by auto

lemma bi_unique_Grp: "bi_unique (BNF_Def.Grp A f) = inj_on f A"
  unfolding bi_unique_def Grp_def inj_on_def by auto

lemma left_total_Grp: "left_total (BNF_Def.Grp UNIV f) = True"
  unfolding left_total_def Grp_def by auto

lemma pointfree_idI: "(⋀x. (f (g x)) = x) ⟹ f o g = id"
  unfolding fun_eq_iff by auto
  
lemma reorient_le_o_Abs: "(⋀x. Abs (Rep x) = x) ⟹ (A :: _ :: order) ≤ B o Abs ⟹ A o Rep ≤ B"
  unfolding le_fun_def o_apply by (rule allI, rule order_trans, erule spec) auto

lemma vimage2pD: "BNF_Def.vimage2p f g R x y ⟹ R (f x) (g y)"
  unfolding vimage2p_def .

lemma predicate2I_obj: "(∀x y. P x y ⟶ Q x y) ⟹ P ≤ Q"
  by fast

lemma objectify_coind_prem: "(⋀x y. P x y ⟹ Q x y) ≡ Trueprop (∀x y. P x y ⟶ Q x y)"
  by presburger

abbreviation (input) rimplies (infixr "⟵" 25) where
  "P ⟵ Q ≡ Q ⟶ P"
  
lemma left_total_All_transfer[transfer_rule]:
  "left_total R ⟹ rel_fun (rel_fun R (op ⟵)) (op ⟵) All All"
  unfolding rel_fun_def left_total_def by auto
  
lemma left_total_Ex_transfer[transfer_rule]:
  "left_total R ⟹ rel_fun (rel_fun R (op ⟶)) (op ⟶) Ex Ex"
  unfolding rel_fun_def left_total_def by force

lemma left_total_All_transfer'[transfer_rule]:
  "left_total R ⟹ rel_fun (rel_fun R (op =)) (op ⟵) All All"
  unfolding rel_fun_def left_total_def by auto
  
lemma left_total_Ex_transfer'[transfer_rule]:
  "left_total R ⟹ rel_fun (rel_fun R (op =)) (op ⟶) Ex Ex"
  unfolding rel_fun_def left_total_def by force

ML_file "Tools/bnf_nu_fp_util.ML"
ML_file "Tools/bnf_nu_fp_sugar_tactics.ML"
ML_file "Tools/bnf_nu_fp_def_sugar.ML"
ML_file "Tools/bnf_nu_fp_tactics.ML"
ML_file "Tools/bnf_nu_fp.ML"
ML_file "Tools/bnf_nu_fp_ind.ML"
ML_file "Tools/bnf_nu_fp_ind_sugar.ML"
ML_file "Tools/bnf_nu_fp_rec.ML"
ML_file "Tools/bnf_nu_fp_rec_sugar.ML"

end