65 text FIXME |
65 text FIXME |
66 |
66 |
67 |
67 |
68 section {* Assumptions *} |
68 section {* Assumptions *} |
69 |
69 |
70 text FIXME |
70 text {* |
|
71 An \emph{assumption} is a proposition that it is postulated in the |
|
72 current context. Local conclusions may use assumptions as |
|
73 additional facts, but this imposes implicit hypotheses that weaken |
|
74 the overall statement. |
|
75 |
|
76 Assumptions are restricted to fixed non-schematic statements, all |
|
77 generality needs to be expressed by explicit quantifiers. |
|
78 Nevertheless, the result will be in HHF normal form with outermost |
|
79 quantifiers stripped. For example, by assuming @{text "\<And>x :: \<alpha>. P |
|
80 x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for arbitrary @{text "?x"} |
|
81 of the fixed type @{text "\<alpha>"}. Local derivations accumulate more |
|
82 and more explicit references to hypotheses: @{text "A\<^isub>1, \<dots>, |
|
83 A\<^isub>n \<turnstile> B"} where @{text "A\<^isub>1, \<dots>, A\<^isub>n"} needs to |
|
84 be covered by the assumptions of the current context. |
|
85 |
|
86 \medskip The @{text "add_assm"} operation augments the context by |
|
87 local assumptions, parameterized by an @{text "export"} rule (see |
|
88 below). |
|
89 |
|
90 The @{text "export"} operation moves facts from a (larger) inner |
|
91 context into a (smaller) outer context, by discharging the |
|
92 difference of the assumptions as specified by the associated export |
|
93 rules. Note that the discharged portion is determined by the |
|
94 contexts, not the facts being exported! There is a separate flag to |
|
95 indicate a goal context, where the result is meant to refine an |
|
96 enclosing sub-goal of a structured proof state (cf.\ FIXME). |
|
97 |
|
98 \medskip The most basic export rule discharges assumptions directly |
|
99 by means of the @{text "\<Longrightarrow>"} introduction rule: |
|
100 \[ |
|
101 \infer[(@{text "\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} |
|
102 \] |
|
103 |
|
104 The variant for goal refinements marks the newly introduced |
|
105 premises, which causes the builtin goal refinement scheme of Isar to |
|
106 enforce unification with local premises within the goal: |
|
107 \[ |
|
108 \infer[(@{text "#\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} |
|
109 \] |
|
110 |
|
111 \medskip Alternative versions of assumptions may perform arbitrary |
|
112 transformations as long as a particular portion of hypotheses is |
|
113 removed from the given facts. |
|
114 |
|
115 For example, a local definition works by fixing @{text "x"} and |
|
116 assuming @{text "x \<equiv> t"}, with the following export rule to reverse |
|
117 the effect: |
|
118 \[ |
|
119 \infer{@{text "\<Gamma> \\ x \<equiv> t \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}} |
|
120 \] |
|
121 |
|
122 \medskip The general concept supports block-structured reasoning |
|
123 nicely, with arbitrary mechanisms for introducing local assumptions. |
|
124 The common reasoning pattern is as follows: |
|
125 |
|
126 \medskip |
|
127 \begin{tabular}{l} |
|
128 @{text "add_assm e\<^isub>1 A\<^isub>1"} \\ |
|
129 @{text "\<dots>"} \\ |
|
130 @{text "add_assm e\<^isub>n A\<^isub>n"} \\ |
|
131 @{text "export"} \\ |
|
132 \end{tabular} |
|
133 \medskip |
|
134 |
|
135 \noindent The final @{text "export"} will turn any fact @{text |
|
136 "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} into some @{text "\<turnstile> B'"}, by |
|
137 applying the export rules @{text "e\<^isub>1, \<dots>, e\<^isub>n"} |
|
138 inside-out. |
|
139 *} |
|
140 |
|
141 text %mlref {* |
|
142 \begin{mldecls} |
|
143 @{index_ML_type Assumption.export} \\ |
|
144 @{index_ML Assumption.assume: "cterm -> thm"} \\ |
|
145 @{index_ML Assumption.add_assumes: "cterm list -> Proof.context -> thm list * Proof.context"} \\ |
|
146 @{index_ML Assumption.add_assms: |
|
147 "Assumption.export -> cterm list -> Proof.context -> thm list * Proof.context"} \\ |
|
148 @{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\ |
|
149 \end{mldecls} |
|
150 |
|
151 \begin{description} |
|
152 |
|
153 \item @{ML_type Assumption.export} |
|
154 |
|
155 \item @{ML Assumption.assume}~@{text "A"} produces a raw assumption |
|
156 @{text "A \<turnstile> A'"}, where the conclusion @{text "A'"} is in HHF normal |
|
157 form. |
|
158 |
|
159 \item @{ML Assumption.add_assumes}~@{text "As"} augments the context |
|
160 by plain assumptions that are discharged via @{text "\<Longrightarrow>_intro"} or |
|
161 @{text "#\<Longrightarrow>_intro"}, depending on goal mode. The resulting facts are |
|
162 hypothetical theorems as produced by @{ML Assumption.assume}. |
|
163 |
|
164 \item @{ML Assumption.add_assms}~@{text "e As"} augments the context |
|
165 by generic assumptions that are discharged via rule @{text "e"}. |
|
166 |
|
167 \item @{ML Assumption.export}~@{text "is_goal inner outer th"} |
|
168 exports result @{text "th"} from the the @{text "inner"} context |
|
169 back into the @{text "outer"} one. The @{text "is_goal"} flag is |
|
170 @{text "true"} for goal mode. The result is in HHF normal form. |
|
171 |
|
172 \end{description} |
|
173 *} |
71 |
174 |
72 |
175 |
73 section {* Conclusions *} |
176 section {* Conclusions *} |
74 |
177 |
75 text FIXME |
178 text FIXME |