Commit e34f12e7 authored by makarius's avatar makarius
Browse files

avoid undeclared variables within proofs;

parent 429d40399262
(* Title: An example submission to the Archive of Formal Proof
ID: $Id: Submission.thy,v 1.8 2007-09-02 14:22:19 lsf37 Exp $
ID: $Id: Submission.thy,v 1.9 2008-05-17 19:48:25 makarius Exp $
Author: Gerwin Klein <kleing at>, 2004
Maintainer: Gerwin Klein <kleing at>
......@@ -61,7 +61,7 @@ text {*
lemma very_true: "True"
proof -
-- "a very roundabout way"
have "P \<longrightarrow> True" by blast
fix P have "P \<longrightarrow> True" by blast
-- "to show @{term True}"
thus True by blast
(* Title: A theory of Featherweight Java in Isabelle/HOL
ID: $Id: FJDefs.thy,v 1.7 2007-07-11 10:10:53 stefanberghofer Exp $
ID: $Id: FJDefs.thy,v 1.8 2008-05-17 19:48:25 makarius Exp $
Author: Nate Foster <jnfoster at>,
Dimitrios Vytiniotis <dimitriv at>, 2006
Maintainer: Nate Foster <jnfoster at>,
......@@ -361,6 +361,7 @@ lemma typing_induct:
and "\<And>C CT D \<Gamma> e0. \<lbrakk>CT;\<Gamma> \<turnstile> e0 : D; P CT \<Gamma> e0 D; CT \<turnstile> C \<not><: D; CT \<turnstile> D \<not><: C\<rbrakk> \<Longrightarrow> P CT \<Gamma> (Cast C e0) C"
shows "P CT \<Gamma> e C" (is ?P)
proof -
fix es Cs
let ?IH="CT;\<Gamma> \<turnstile>+ es : Cs \<longrightarrow> (\<forall>i < length es. P CT \<Gamma> (es!i) (Cs!i))"
have "?IH \<and> (?T \<longrightarrow> ?P)"
proof(induct rule:typings_typing.induct)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment