-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathGeneralise.thy
154 lines (126 loc) · 5.34 KB
/
Generalise.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Generalise.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2005-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
theory Generalise imports "HOL-Statespace.DistinctTreeProver"
begin
lemma protectRefl: "PROP Pure.prop (PROP C) \<Longrightarrow> PROP Pure.prop (PROP C)"
by (simp add: prop_def)
lemma protectImp:
assumes i: "PROP Pure.prop (PROP P \<Longrightarrow> PROP Q)"
shows "PROP Pure.prop (PROP Pure.prop P \<Longrightarrow> 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) \<Longrightarrow> PROP Pure.prop (Trueprop Q))"
assumes i2: "PROP Pure.prop (PROP Pure.prop (Trueprop P') \<Longrightarrow> PROP Pure.prop (Trueprop Q'))"
shows "PROP Pure.prop (PROP Pure.prop (Trueprop (P \<and> P')) \<Longrightarrow> (PROP Pure.prop (Trueprop (Q \<and> Q'))))"
using i1 i2
by (auto simp add: prop_def)
lemma generaliseAll:
assumes i: "PROP Pure.prop (\<And>s. PROP Pure.prop (Trueprop (P s)) \<Longrightarrow> PROP Pure.prop (Trueprop (Q s)))"
shows "PROP Pure.prop (PROP Pure.prop (Trueprop (\<forall>s. P s)) \<Longrightarrow> PROP Pure.prop (Trueprop (\<forall>s. Q s)))"
using i
by (auto simp add: prop_def)
lemma generalise_all:
assumes i: "PROP Pure.prop (\<And>s. PROP Pure.prop (PROP P s) \<Longrightarrow> PROP Pure.prop (PROP Q s))"
shows "PROP Pure.prop ((PROP Pure.prop (\<And>s. PROP P s)) \<Longrightarrow> (PROP Pure.prop (\<And>s. PROP Q s)))"
using i
proof (unfold prop_def)
assume i1: "\<And>s. (PROP P s) \<Longrightarrow> (PROP Q s)"
assume i2: "\<And>s. PROP P s"
show "\<And>s. PROP Q s"
by (rule i1) (rule i2)
qed
lemma generaliseTrans:
assumes i1: "PROP Pure.prop (PROP P \<Longrightarrow> PROP Q)"
assumes i2: "PROP Pure.prop (PROP Q \<Longrightarrow> PROP R)"
shows "PROP Pure.prop (PROP P \<Longrightarrow> PROP R)"
using i1 i2
proof (unfold prop_def)
assume P_Q: "PROP P \<Longrightarrow> PROP Q"
assume Q_R: "PROP Q \<Longrightarrow> PROP R"
assume P: "PROP P"
show "PROP R"
by (rule Q_R [OF P_Q [OF P]])
qed
lemma meta_spec:
assumes "\<And>x. PROP P x"
shows "PROP P x" by fact
lemma meta_spec_protect:
assumes g: "\<And>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) \<Longrightarrow> PROP Pure.prop (Trueprop Q))"
shows "PROP Pure.prop (PROP Pure.prop (Trueprop (X \<longrightarrow> P)) \<Longrightarrow> PROP Pure.prop (Trueprop (X \<longrightarrow> Q)))"
using i
by (auto simp add: prop_def)
lemma generaliseEx:
assumes i: "PROP Pure.prop (\<And>s. PROP Pure.prop (Trueprop (P s)) \<Longrightarrow> PROP Pure.prop (Trueprop (Q s)))"
shows "PROP Pure.prop (PROP Pure.prop (Trueprop (\<exists>s. P s)) \<Longrightarrow> PROP Pure.prop (Trueprop (\<exists>s. Q s)))"
using i
by (auto simp add: prop_def)
lemma generaliseRefl: "PROP Pure.prop (PROP Pure.prop (Trueprop P) \<Longrightarrow> PROP Pure.prop (Trueprop P))"
by (auto simp add: prop_def)
lemma generaliseRefl': "PROP Pure.prop (PROP P \<Longrightarrow> PROP P)"
by (auto simp add: prop_def)
lemma generaliseAllShift:
assumes i: "PROP Pure.prop (\<And>s. P \<Longrightarrow> Q s)"
shows "PROP Pure.prop (PROP Pure.prop (Trueprop P) \<Longrightarrow> PROP Pure.prop (Trueprop (\<forall>s. Q s)))"
using i
by (auto simp add: prop_def)
lemma generalise_allShift:
assumes i: "PROP Pure.prop (\<And>s. PROP P \<Longrightarrow> PROP Q s)"
shows "PROP Pure.prop (PROP Pure.prop (PROP P) \<Longrightarrow> PROP Pure.prop (\<And>s. PROP Q s))"
using i
proof (unfold prop_def)
assume P_Q: "\<And>s. PROP P \<Longrightarrow> PROP Q s"
assume P: "PROP P"
show "\<And>s. PROP Q s"
by (rule P_Q [OF P])
qed
lemma generaliseImpl:
assumes i: "PROP Pure.prop (PROP Pure.prop P \<Longrightarrow> PROP Pure.prop Q)"
shows "PROP Pure.prop ((PROP Pure.prop (PROP X \<Longrightarrow> PROP P)) \<Longrightarrow> (PROP Pure.prop (PROP X \<Longrightarrow> PROP Q)))"
using i
proof (unfold prop_def)
assume i1: "PROP P \<Longrightarrow> PROP Q"
assume i2: "PROP X \<Longrightarrow> PROP P"
assume X: "PROP X"
show "PROP Q"
by (rule i1 [OF i2 [OF X]])
qed
ML_file \<open>generalise_state.ML\<close>
end