(*
    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