aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--spartan/core/Spartan.thy22
-rw-r--r--spartan/core/elaborated_assumption.ML (renamed from spartan/core/elaborated_expression.ML)173
-rw-r--r--spartan/core/goals.ML2
3 files changed, 118 insertions, 79 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
diff --git a/spartan/core/elaborated_expression.ML b/spartan/core/elaborated_assumption.ML
index 49b7758..e10a882 100644
--- a/spartan/core/elaborated_expression.ML
+++ b/spartan/core/elaborated_assumption.ML
@@ -1,18 +1,45 @@
-(* Title: elaborated_expression.ML
+(* Title: elaborated_assumption.ML
Author: Joshua Chen
-A modification of parts of ~~/Pure/Isar/expression.ML to incorporate elaboration
-into the assumptions mechanism.
+Term elaboration for goal and proof assumptions.
-Most of this file is copied verbatim from the original; the only changes are the
-addition of `elaborate` and a modification to `activate_i`.
+Contains code from parts of
+ ~~/Pure/Isar/element.ML and
+ ~~/Pure/Isar/expression.ML
+in both verbatim and modified forms.
*)
-structure Elaborated_Expression = struct
+structure Elaborated_Assumption: sig
+
+val read_goal_statement:
+ (string, string, Facts.ref) Element.ctxt list ->
+ (string, string) Element.stmt ->
+ Proof.context ->
+ (Attrib.binding * (term * term list) list) list * Proof.context
+
+end = struct
+
+
+(*Apply elaboration to the list format assumptions are given in*)
+fun elaborate ctxt assms =
+ let
+ fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env)
+ fun elab_fact (fact, xs) assums =
+ let val (subst, fact') = Elab.elab_stmt ctxt assums fact in
+ ((fact', map (subst_term subst) xs), Thm.cterm_of ctxt fact' :: assums)
+ end
+ fun elab (b, facts) assums =
+ let val (facts', assums') = fold_map elab_fact facts assums
+ in ((b, facts'), assums') end
+ in #1 (fold_map elab assms []) end
-local
-open Element
+(* Goal assumptions *)
+
+(*Most of the code in this section is copied verbatim from the originals; the
+ only change is a modification to`activate_i` incorporating elaboration.*)
+
+local
fun mk_type T = (Logic.mk_type T, [])
fun mk_term t = (t, [])
@@ -28,25 +55,25 @@ fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs))
fun extract_eqns es = map (mk_term o snd) es
fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs
-fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes
- | extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts
- | extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms
- | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs
- | extract_elem (Notes _) = []
- | extract_elem (Lazy_Notes _) = []
+fun extract_elem (Element.Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes
+ | extract_elem (Element.Constrains csts) = map (#2 #> single #> map mk_type) csts
+ | extract_elem (Element.Assumes asms) = map (#2 #> map mk_propp) asms
+ | extract_elem (Element.Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs
+ | extract_elem (Element.Notes _) = []
+ | extract_elem (Element.Lazy_Notes _) = []
-fun restore_elem (Fixes fixes, css) =
+fun restore_elem (Element.Fixes fixes, css) =
(fixes ~~ css) |> map (fn ((x, _, mx), cs) =>
- (x, cs |> map dest_type |> try hd, mx)) |> Fixes
- | restore_elem (Constrains csts, css) =
+ (x, cs |> map dest_type |> try hd, mx)) |> Element.Fixes
+ | restore_elem (Element.Constrains csts, css) =
(csts ~~ css) |> map (fn ((x, _), cs) =>
- (x, cs |> map dest_type |> hd)) |> Constrains
- | restore_elem (Assumes asms, css) =
- (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Assumes
- | restore_elem (Defines defs, css) =
- (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines
- | restore_elem (elem as Notes _, _) = elem
- | restore_elem (elem as Lazy_Notes _, _) = elem
+ (x, cs |> map dest_type |> hd)) |> Element.Constrains
+ | restore_elem (Element.Assumes asms, css) =
+ (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Element.Assumes
+ | restore_elem (Element.Defines defs, css) =
+ (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Element.Defines
+ | restore_elem (elem as Element.Notes _, _) = elem
+ | restore_elem (elem as Element.Lazy_Notes _, _) = elem
fun prep (_, pats) (ctxt, t :: ts) =
let val ctxt' = Proof_Context.augment t ctxt
@@ -65,11 +92,11 @@ fun check cs ctxt =
fun inst_morphism params ((prfx, mandatory), insts') ctxt =
let
- (* parameters *)
+ (*parameters*)
val parm_types = map #2 params;
val type_parms = fold Term.add_tfreesT parm_types [];
- (* type inference *)
+ (*type inference*)
val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
val type_parms' = fold Term.add_tvarsT parm_types' [];
val checked =
@@ -77,12 +104,12 @@ fun inst_morphism params ((prfx, mandatory), insts') ctxt =
|> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt)
val (type_parms'', insts'') = chop (length type_parms') checked;
- (* context *)
+ (*context*)
val ctxt' = fold Proof_Context.augment checked ctxt;
val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt';
val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt';
- (* instantiation *)
+ (*instantiation*)
val instT =
(type_parms ~~ map Logic.dest_type type_parms'')
|> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
@@ -203,7 +230,7 @@ fun finish_inst ctxt (loc, (prfx, inst)) =
fun closeup _ _ false elem = elem
| closeup (outer_ctxt, ctxt) parms true elem =
let
- (* FIXME consider closing in syntactic phase -- before type checking *)
+ (*FIXME consider closing in syntactic phase -- before type checking*)
fun close_frees t =
let
val rev_frees =
@@ -216,20 +243,20 @@ fun closeup _ _ false elem = elem
| no_binds _ = error "Illegal term bindings in context element";
in
(case elem of
- Assumes asms => Assumes (asms |> map (fn (a, propps) =>
+ Element.Assumes asms => Element.Assumes (asms |> map (fn (a, propps) =>
(a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
- | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
+ | Element.Defines defs => Element.Defines (defs |> map (fn ((name, atts), (t, ps)) =>
let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t)
in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
| e => e)
end
-fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes)
- | finish_elem _ _ _ (Constrains _) = Constrains []
- | finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms)
- | finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs)
- | finish_elem _ _ _ (elem as Notes _) = elem
- | finish_elem _ _ _ (elem as Lazy_Notes _) = elem
+fun finish_elem _ parms _ (Element.Fixes fixes) = Element.Fixes (finish_fixes parms fixes)
+ | finish_elem _ _ _ (Element.Constrains _) = Element.Constrains []
+ | finish_elem ctxts parms do_close (Element.Assumes asms) = closeup ctxts parms do_close (Element.Assumes asms)
+ | finish_elem ctxts parms do_close (Element.Defines defs) = closeup ctxts parms do_close (Element.Defines defs)
+ | finish_elem _ _ _ (elem as Element.Notes _) = elem
+ | finish_elem _ _ _ (elem as Element.Lazy_Notes _) = elem
fun check_autofix insts eqnss elems concl ctxt =
let
@@ -237,7 +264,7 @@ fun check_autofix insts eqnss elems concl ctxt =
val eqns_cs = map extract_eqns eqnss;
val elem_css = map extract_elem elems;
val concl_cs = (map o map) mk_propp (map snd concl);
- (* Type inference *)
+ (*Type inference*)
val (inst_cs' :: eqns_cs' :: css', ctxt') =
(fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt;
val (elem_css', [concl_cs']) = chop (length elem_css) css';
@@ -317,7 +344,7 @@ fun prep_full_context_statement
|> fold_map prep_elem raw_elems
|-> prep_stmt
- (* parameters from expression and elements *)
+ (*parameters from expression and elements*)
val xs = maps (fn Element.Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
(Element.Fixes fors :: elems')
val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4
@@ -344,8 +371,6 @@ val read_full_context_statement = prep_full_context_statement
Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src
Proof_Context.read_var check_expr
-in
-
fun prep_statement prep activate raw_elems raw_stmt ctxt =
let
val ((_, _, _, elems, concl), _) =
@@ -357,46 +382,66 @@ fun prep_statement prep activate raw_elems raw_stmt ctxt =
|> Proof_Context.restore_stmt ctxt;
in (concl, ctxt') end
-fun elaborate ctxt assms =
- let
- fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env)
- fun elab_fact (fact, xs) assums =
- let val (subst, fact') = Elab.elab_stmt ctxt assums fact in
- ((fact', map (subst_term subst) xs), Thm.cterm_of ctxt fact' :: assums)
- end
- fun elab (b, facts) assums =
- let val (facts', assums') = fold_map elab_fact facts assums
- in ((b, facts'), assums') end
- in
- #1 (fold_map elab assms [])
- end
-
fun activate_i elem ctxt =
let
val elem' =
- (case (map_ctxt_attrib o map) Token.init_assignable elem of
- Defines defs =>
- Defines (defs |> map (fn ((a, atts), (t, ps)) =>
+ (case (Element.map_ctxt_attrib o map) Token.init_assignable elem of
+ Element.Defines defs =>
+ Element.Defines (defs |> map (fn ((a, atts), (t, ps)) =>
((Thm.def_binding_optional
(Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts),
(t, ps))))
- | Assumes assms => Assumes (elaborate ctxt assms)
+ | Element.Assumes assms => Element.Assumes (elaborate ctxt assms)
| e => e);
- val ctxt' = Context.proof_map (init elem') ctxt;
- in ((map_ctxt_attrib o map) Token.closure elem', ctxt') end
+ val ctxt' = Context.proof_map (Element.init elem') ctxt;
+ in ((Element.map_ctxt_attrib o map) Token.closure elem', ctxt') end
fun activate raw_elem ctxt =
- let val elem = raw_elem |> map_ctxt
+ let val elem = raw_elem |> Element.map_ctxt
{binding = I,
typ = I,
term = I,
pattern = I,
fact = Proof_Context.get_fact ctxt,
attrib = Attrib.check_src ctxt}
- in activate_i elem ctxt end;
+ in activate_i elem ctxt end
+
+in
+
+val read_goal_statement = prep_statement read_full_context_statement activate
-fun read_statement x = prep_statement read_full_context_statement activate x
+end
+
+
+(* Proof assumption command *)
+
+local
+
+val structured_statement =
+ Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
+ >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows))
+
+in
+
+val _ = Outer_Syntax.command \<^command_keyword>\<open>assuming\<close> "elaborated assumption"
+ (structured_statement >> (fn (a, b, c) => Toplevel.proof (fn state =>
+ let
+ val ctxt = Proof.context_of state
+
+ fun read_option_typ NONE = NONE
+ | read_option_typ (SOME s) = SOME (Syntax.read_typ ctxt s)
+ fun read_terms (s, ss) =
+ let val f = Syntax.read_term ctxt in (f s, map f ss) end
+
+ val a' = map (fn (b, s, m) => (b, read_option_typ s, m)) a
+ val b' = map (map read_terms) b
+ val c' = c |> map (fn ((b, atts), ss) =>
+ ((b, map (Attrib.attribute ctxt o Attrib.check_src ctxt) atts),
+ map read_terms ss))
+ val c'' = elaborate ctxt c'
+ in Proof.assume a' b' c'' state end)))
end
+
end \ No newline at end of file
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
index 3e2bd09..87ec2b8 100644
--- a/spartan/core/goals.ML
+++ b/spartan/core/goals.ML
@@ -184,7 +184,7 @@ val schematic_theorem_cmd =
gen_schematic_theorem
Bundle.includes_cmd
Attrib.check_src
- Elaborated_Expression.read_statement
+ Elaborated_Assumption.read_goal_statement
fun theorem spec descr =
Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)