chapter {* Nonuniform (Co)datatypes *}
theory BNF_Nonuniform_Fixpoint
imports Main
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