diff options
| author | Josh Chen | 2020-07-28 14:10:34 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-28 14:10:34 +0200 |
| commit | 6b27aa578257a6f4db9242b413a8008962b7f2e1 (patch) | |
| tree | f49e1decc18bddb4a2ccbc4b181d470eac77ed03 /spartan/core/Spartan.thy | |
| parent | 223a253732ced7d89dcea506ab56d92d1cfe8281 (diff) | |
New `assuming` proof command for elaborated assumptions
Diffstat (limited to 'spartan/core/Spartan.thy')
| -rw-r--r-- | spartan/core/Spartan.thy | 22 |
1 files changed, 8 insertions, 14 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 11bdc2b..faa692d 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -7,6 +7,7 @@ imports "HOL-Eisbach.Eisbach_Tools" keywords "Theorem" "Lemma" "Corollary" "Proposition" "Definition" :: thy_goal_stmt and + "assuming" :: prf_asm % "proof" and "focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and "congruence" "print_coercions" :: thy_decl and "rhs" "derive" "prems" "vars" :: quasi_command @@ -216,7 +217,7 @@ subsection \<open>Statement commands\<close> ML_file \<open>focus.ML\<close> ML_file \<open>elaboration.ML\<close> -ML_file \<open>elaborated_expression.ML\<close> +ML_file \<open>elaborated_assumption.ML\<close> ML_file \<open>goals.ML\<close> subsection \<open>Proof methods\<close> @@ -536,19 +537,12 @@ Lemma (derive) Sig_dist_exp: "\<And>x. x: A \<Longrightarrow> B x: U i" "\<And>x. x: A \<Longrightarrow> C x: U i" shows "(\<Sum>x: A. B x) \<times> (\<Sum>x: A. C x)" - apply (elim p) - focus vars x y - apply intro - \<guillemotright> apply intro - apply assumption - apply (fst y) - done - \<guillemotright> apply intro - apply assumption - apply (snd y) - done - done - done +proof intro + have "fst p: A" and "snd p: B (fst p) \<times> C (fst p)" by typechk+ + thus "<fst p, fst (snd p)>: \<Sum>x: A. B x" + and "<fst p, snd (snd p)>: \<Sum>x: A. C x" + by typechk+ +qed end |