src/HOL/Lifting_Product.thy

plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;

(*  Title:      HOL/Lifting_Product.thy
    Author:     Brian Huffman and Ondrej Kuncar
*)

section {* Setup for Lifting/Transfer for the product type *}

theory Lifting_Product
imports Lifting Basic_BNFs
begin

(* The following lemma can be deleted when product is added to FP sugar *)
lemma prod_pred_inject [simp]:
  "pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)"
  unfolding pred_prod_def fun_eq_iff prod_set_simps by blast

subsection {* Transfer rules for the Transfer package *}

context
begin
interpretation lifting_syntax .

declare Pair_transfer [transfer_rule]
declare fst_transfer [transfer_rule]
declare snd_transfer [transfer_rule]
declare case_prod_transfer [transfer_rule]

lemma curry_transfer [transfer_rule]:
  "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
  unfolding curry_def by transfer_prover

lemma map_prod_transfer [transfer_rule]:
  "((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D)
    map_prod map_prod"
  unfolding map_prod_def [abs_def] by transfer_prover

lemma rel_prod_transfer [transfer_rule]:
  "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
    rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
  unfolding rel_fun_def by auto

end

end