Theory Generalise

(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer
*)

theory Generalise imports "HOL-Statespace.DistinctTreeProver"
begin

lemma protectRefl: "PROP Pure.prop (PROP C) ⟹ PROP Pure.prop (PROP C)"
  by (simp add: prop_def)

lemma protectImp:
 assumes i: "PROP Pure.prop (PROP P ⟹ PROP Q)"
 shows "PROP Pure.prop (PROP Pure.prop P ⟹ PROP Pure.prop Q)"
proof -
  {
    assume P: "PROP Pure.prop P"
    from i [unfolded prop_def, OF P [unfolded prop_def]]
    have "PROP Pure.prop Q"
      by (simp add: prop_def)
  }
  note i' = this
  show "PROP ?thesis"
    apply (rule protectI)
    apply (rule i')
    apply assumption
    done
qed


lemma generaliseConj:
  assumes i1: "PROP Pure.prop (PROP Pure.prop (Trueprop P) ⟹ PROP Pure.prop (Trueprop Q))"
  assumes i2: "PROP Pure.prop (PROP Pure.prop (Trueprop P') ⟹ PROP Pure.prop (Trueprop Q'))"
  shows "PROP Pure.prop (PROP Pure.prop (Trueprop (P ∧ P')) ⟹ (PROP Pure.prop (Trueprop (Q ∧ Q'))))"
  using i1 i2
  by (auto simp add: prop_def)

lemma generaliseAll:
 assumes i: "PROP Pure.prop (⋀s. PROP Pure.prop (Trueprop (P s)) ⟹ PROP Pure.prop (Trueprop (Q s)))"
 shows "PROP Pure.prop (PROP Pure.prop (Trueprop (∀s. P s)) ⟹ PROP Pure.prop (Trueprop (∀s. Q s)))"
  using i
  by (auto simp add: prop_def)

lemma generalise_all:
 assumes i: "PROP Pure.prop (⋀s. PROP Pure.prop (PROP P s) ⟹ PROP Pure.prop (PROP Q s))"
 shows "PROP Pure.prop ((PROP Pure.prop (⋀s. PROP P s)) ⟹ (PROP Pure.prop (⋀s. PROP Q s)))"
  using i
  proof (unfold prop_def)
    assume i1: "⋀s. (PROP P s) ⟹ (PROP Q s)"
    assume i2: "⋀s. PROP P s"
    show "⋀s. PROP Q s"
      by (rule i1) (rule i2)
  qed

lemma generaliseTrans:
  assumes i1: "PROP Pure.prop (PROP P ⟹ PROP Q)"
  assumes i2: "PROP Pure.prop (PROP Q ⟹ PROP R)"
  shows "PROP Pure.prop (PROP P ⟹ PROP R)"
  using i1 i2
  proof (unfold prop_def)
    assume P_Q: "PROP P ⟹ PROP Q"
    assume Q_R: "PROP Q ⟹ PROP R"
    assume P: "PROP P"
    show "PROP R"
      by (rule Q_R [OF P_Q [OF P]])
  qed

lemma meta_spec:
  assumes "⋀x. PROP P x"
  shows "PROP P x" by fact

lemma meta_spec_protect:
  assumes g: "⋀x. PROP P x"
  shows "PROP Pure.prop (PROP P x)"
using g
by (auto simp add: prop_def)

lemma generaliseImp:
  assumes i: "PROP Pure.prop (PROP Pure.prop (Trueprop P) ⟹ PROP Pure.prop (Trueprop Q))"
  shows "PROP Pure.prop (PROP Pure.prop (Trueprop (X ⟶ P)) ⟹ PROP Pure.prop (Trueprop (X ⟶ Q)))"
  using i
  by (auto simp add: prop_def)

lemma generaliseEx:
 assumes i: "PROP Pure.prop (⋀s. PROP Pure.prop (Trueprop (P s)) ⟹ PROP Pure.prop (Trueprop (Q s)))"
 shows "PROP Pure.prop (PROP Pure.prop (Trueprop (∃s. P s)) ⟹ PROP Pure.prop (Trueprop (∃s. Q s)))"
  using i
  by (auto simp add: prop_def)


lemma generaliseRefl: "PROP Pure.prop (PROP Pure.prop (Trueprop P) ⟹ PROP Pure.prop (Trueprop P))"
  by (auto simp add: prop_def)

lemma generaliseRefl': "PROP Pure.prop (PROP P ⟹ PROP P)"
  by (auto simp add: prop_def)

lemma generaliseAllShift:
  assumes i: "PROP Pure.prop (⋀s. P ⟹ Q s)"
  shows "PROP Pure.prop (PROP Pure.prop (Trueprop P) ⟹ PROP Pure.prop (Trueprop (∀s. Q s)))"
  using i
  by (auto simp add: prop_def)

lemma generalise_allShift:
  assumes i: "PROP Pure.prop (⋀s. PROP P ⟹ PROP Q s)"
  shows "PROP Pure.prop (PROP Pure.prop (PROP P) ⟹ PROP Pure.prop (⋀s. PROP Q s))"
  using i
  proof (unfold prop_def)
    assume P_Q: "⋀s. PROP P ⟹ PROP Q s"
    assume P: "PROP P"
    show "⋀s. PROP Q s"
      by (rule P_Q [OF P])
  qed


lemma generaliseImpl:
  assumes i: "PROP Pure.prop (PROP Pure.prop P ⟹ PROP Pure.prop Q)"
  shows "PROP Pure.prop ((PROP Pure.prop (PROP X ⟹ PROP P)) ⟹ (PROP Pure.prop (PROP X ⟹ PROP Q)))"
  using i
  proof (unfold prop_def)
    assume i1: "PROP P ⟹ PROP Q"
    assume i2: "PROP X ⟹ PROP P"
    assume X: "PROP X"
    show "PROP Q"
      by (rule i1 [OF i2 [OF X]])
  qed


ML_file ‹generalise_state.ML›

end