Theory ProdContrib (Isabelle2005: October 2005)

(*************************************************************************)
(*   Author             : Thomas Santen, GMD First                       *)
(*   $Id: ProdContrib.thy,v 1.1 2001/01/08 15:51:24 wolff Exp $  *)
(*   This theory        : more proof support for product types           *)
(*   Copyright          : GMD First, Berlin                              *)
(*                        Germany                                        *)
(*************************************************************************)

theory    ProdContrib 
imports   Main (* Product_Type: *)
begin

(* unfortunately, this rule loops! *)
lemma split_paired_Lam: "P = (λ  (a,b). P (a,b))"
apply (rule ext)
apply (simp (no_asm_simp) only: split_tupled_all)
apply (simp (no_asm))
done

lemma split_paired_split: "(% x. split f x) = (% (a,b). split f (a,b))"
apply (rule ext)
apply (simp (no_asm_simp) only: split_tupled_all)
apply (simp (no_asm))
done

lemma split_paired_CollectL: "{(a,b). P a b} = {((a,c),b). P (a,c) b}"
apply auto
apply (tactic {* TRYALL split_all_tac *} )
done

lemma split_pattern: assumes a: "z=(x,y)" shows "(% (x,y). F x y) z = F x y"
apply (simp (no_asm) add: a)
done

lemma split_paired_Ex: "(EX x. P x) = (EX a b. P (a,b))"
apply auto
done

ML
{*
val split_pattern = thm "split_pattern"
*}

declare split_paired_Ex [simp]

(* das evtl. mit addbefore als Vorverarbeitung zum claset() setzen! *)
ML {* 
val norm_split_apply_tac = 
    (SELECT_GOAL (CHANGED 
     (EVERY1 [(match_tac [split_pattern RS ssubst]),
              (rtac refl)])
     THEN flexflex_tac))

*}

(*-----------------------------------------------------------------------*)
(* Meta-Simplification for unit                                          *)
(*-----------------------------------------------------------------------*)

lemma  "METACOND x ==> ((x::unit),y) = ((),y)"
apply (subst unit_eq)
apply (rule refl)
done

lemma METACOND_pair_snd_unit: "METACOND y ==> (x,(y::unit)) = (x,())"
apply (subst unit_eq)
apply (rule refl)
done

lemma unit_eq_true: "((x::unit) = y) = True"
apply ((subst unit_eq))
apply (simp (no_asm))
done

declare unit_eq_true [simp]
(*
fun is_not_unit_const (Const ("()",Type ("unit",[]))) = false
  | is_not_unit_const _ = true
*)

end

lemma split_paired_Lam:

  P = (%(a, b). P (a, b))

lemma split_paired_split:

  (%(x, y). f x y) = (%(a, b). split f (a, b))

lemma split_paired_CollectL:

  {(a, b). P a b} = {((a, c), b). P (a, c) b}

lemma split_pattern:

  z = (x, y) ==> split F z = F x y

lemma split_paired_Ex:

  (∃x. P x) = (∃a b. P (a, b))

lemma

  METACOND x ==> (x, y) = ((), y)

lemma METACOND_pair_snd_unit:

  METACOND y ==> (x, y) = (x, ())

lemma unit_eq_true:

  (x = y) = True