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