aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--spartan/core/Spartan.thy70
-rw-r--r--spartan/core/context_tactical.ML100
-rw-r--r--spartan/core/elaborated_statement.ML (renamed from spartan/core/elaborated_assumption.ML)51
-rw-r--r--spartan/core/elaboration.ML17
-rw-r--r--spartan/core/focus.ML96
-rw-r--r--spartan/core/goals.ML10
-rw-r--r--spartan/core/tactics.ML3
-rw-r--r--spartan/core/typechecking.ML8
-rw-r--r--spartan/lib/List.thy10
-rw-r--r--spartan/lib/Maybe.thy19
-rw-r--r--spartan/lib/Prelude.thy (renamed from spartan/lib/More_Types.thy)6
11 files changed, 268 insertions, 122 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index faa692d..27edd51 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -8,9 +8,9 @@ imports
keywords
"Theorem" "Lemma" "Corollary" "Proposition" "Definition" :: thy_goal_stmt and
"assuming" :: prf_asm % "proof" and
- "focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and
+ "focus" "\<^item>" "\<^enum>" "\<circ>" "\<diamondop>" "~" :: prf_script_goal % "proof" and
"congruence" "print_coercions" :: thy_decl and
- "rhs" "derive" "prems" "vars" :: quasi_command
+ "rhs" "def" "vars" :: quasi_command
begin
@@ -198,8 +198,8 @@ lemmas
[form] = PiF SigF and
[intro] = PiI SigI and
[intros] = PiI[rotated] SigI and
- [elim "?f"] = PiE and
- [elim "?p"] = SigE and
+ [elim ?f] = PiE and
+ [elim ?p] = SigE and
[comp] = beta Sig_comp and
[cong] = Pi_cong lam_cong Sig_cong
@@ -217,7 +217,7 @@ subsection \<open>Statement commands\<close>
ML_file \<open>focus.ML\<close>
ML_file \<open>elaboration.ML\<close>
-ML_file \<open>elaborated_assumption.ML\<close>
+ML_file \<open>elaborated_statement.ML\<close>
ML_file \<open>goals.ML\<close>
subsection \<open>Proof methods\<close>
@@ -229,10 +229,6 @@ method_setup rule =
\<open>Attrib.thms >> (fn ths => K (CONTEXT_METHOD (
CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\<close>
-method_setup rules =
- \<open>Attrib.thms >> (fn ths => K (CONTEXT_METHOD (
- CREPEAT o CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\<close>
-
method_setup dest =
\<open>Scan.lift (Scan.option (Args.parens Parse.int))
-- Attrib.thms >> (fn (n_opt, ths) => K (CONTEXT_METHOD (
@@ -411,10 +407,10 @@ lemma funcompI [typechk]:
lemma funcomp_assoc [comp]:
assumes
+ "A: U i"
"f: A \<rightarrow> B"
"g: B \<rightarrow> C"
"h: \<Prod>x: C. D x"
- "A: U i"
shows
"(h \<circ>\<^bsub>B\<^esub> g) \<circ>\<^bsub>A\<^esub> f \<equiv> h \<circ>\<^bsub>A\<^esub> g \<circ>\<^bsub>A\<^esub> f"
unfolding funcomp_def by reduce
@@ -430,10 +426,9 @@ lemma funcomp_lambda_comp [comp]:
lemma funcomp_apply_comp [comp]:
assumes
+ "A: U i" "B: U i" "\<And>x y. x: B \<Longrightarrow> C x: U i"
"f: A \<rightarrow> B" "g: \<Prod>x: B. C x"
"x: A"
- "A: U i" "B: U i"
- "\<And>x y. x: B \<Longrightarrow> C x: U i"
shows "(g \<circ>\<^bsub>A\<^esub> f) x \<equiv> g (f x)"
unfolding funcomp_def by reduce
@@ -449,17 +444,17 @@ subsection \<open>Identity function\<close>
abbreviation id where "id A \<equiv> \<lambda>x: A. x"
lemma
- id_type[typechk]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and
+ id_type [typechk]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and
id_comp [comp]: "x: A \<Longrightarrow> (id A) x \<equiv> x" \<comment> \<open>for the occasional manual rewrite\<close>
by reduce+
lemma id_left [comp]:
- assumes "f: A \<rightarrow> B" "A: U i" "B: U i"
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
shows "(id B) \<circ>\<^bsub>A\<^esub> f \<equiv> f"
by (subst eta_exp[of f]) (reduce, rule eta)
lemma id_right [comp]:
- assumes "f: A \<rightarrow> B" "A: U i" "B: U i"
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
shows "f \<circ>\<^bsub>A\<^esub> (id A) \<equiv> f"
by (subst eta_exp[of f]) (reduce, rule eta)
@@ -480,10 +475,7 @@ lemma fst_type [typechk]:
lemma fst_comp [comp]:
assumes
- "a: A"
- "b: B a"
- "A: U i"
- "\<And>x. x: A \<Longrightarrow> B x: U i"
+ "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" "a: A" "b: B a"
shows "fst A B <a, b> \<equiv> a"
unfolding fst_def by reduce
@@ -493,7 +485,7 @@ lemma snd_type [typechk]:
unfolding snd_def by typechk reduce
lemma snd_comp [comp]:
- assumes "a: A" "b: B a" "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+ assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" "a: A" "b: B a"
shows "snd A B <a, b> \<equiv> b"
unfolding snd_def by reduce
@@ -513,36 +505,48 @@ subsection \<open>Projections\<close>
Lemma fst [typechk]:
assumes
- "p: \<Sum>x: A. B x"
"A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+ "p: \<Sum>x: A. B x"
shows "fst p: A"
by typechk
Lemma snd [typechk]:
assumes
- "p: \<Sum>x: A. B x"
"A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+ "p: \<Sum>x: A. B x"
shows "snd p: B (fst p)"
by typechk
-method fst for p::o = rule fst[of p]
-method snd for p::o = rule snd[of p]
+method fst for p::o = rule fst[where ?p=p]
+method snd for p::o = rule snd[where ?p=p]
-subsection \<open>Properties of \<Sigma>\<close>
+text \<open>Double projections:\<close>
-Lemma (derive) Sig_dist_exp:
+definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> Spartan.fst ? ? (Spartan.fst ? ? p)"
+definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> Spartan.snd ? ? (Spartan.fst ? ? p)"
+definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> Spartan.fst ? ? (Spartan.snd ? ? p)"
+definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> Spartan.snd ? ? (Spartan.snd ? ? p)"
+
+translations
+ "CONST p\<^sub>1\<^sub>1 p" \<leftharpoondown> "fst (fst p)"
+ "CONST p\<^sub>1\<^sub>2 p" \<leftharpoondown> "snd (fst p)"
+ "CONST p\<^sub>2\<^sub>1 p" \<leftharpoondown> "fst (snd p)"
+ "CONST p\<^sub>2\<^sub>2 p" \<leftharpoondown> "snd (snd p)"
+
+Lemma (def) distribute_Sig:
assumes
- "p: \<Sum>x: A. B x \<times> C x"
"A: U i"
"\<And>x. x: A \<Longrightarrow> B x: U i"
"\<And>x. x: A \<Longrightarrow> C x: U i"
+ "p: \<Sum>x: A. B x \<times> C x"
shows "(\<Sum>x: A. B x) \<times> (\<Sum>x: A. C x)"
-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
+ 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/context_tactical.ML b/spartan/core/context_tactical.ML
index a5159f6..b5a6c00 100644
--- a/spartan/core/context_tactical.ML
+++ b/spartan/core/context_tactical.ML
@@ -2,6 +2,10 @@
Author: Joshua Chen
More context tactics, and context tactic combinators.
+
+Contains code modified from
+ ~~/Pure/search.ML
+ ~~/Pure/tactical.ML
*)
infix 1 CTHEN CTHEN' CTHEN_ALL_NEW CTHEN_ALL_NEW_FWD
@@ -23,6 +27,7 @@ val CORELSE': context_tactic' * context_tactic' -> context_tactic'
val CAPPEND': context_tactic' * context_tactic' -> context_tactic'
val CTRY: context_tactic -> context_tactic
val CREPEAT: context_tactic -> context_tactic
+val CREPEAT1: context_tactic -> context_tactic
val CFILTER: (context_state -> bool) -> context_tactic -> context_tactic
val CCHANGED: context_tactic -> context_tactic
val CTHEN_ALL_NEW: context_tactic' * context_tactic' -> context_tactic'
@@ -34,6 +39,16 @@ val CHEADGOAL: context_tactic' -> context_tactic
val CALLGOALS: context_tactic' -> context_tactic
val CSOMEGOAL: context_tactic' -> context_tactic
val CRANGE: context_tactic' list -> context_tactic'
+val CFIRST: context_tactic list -> context_tactic
+val CFIRST': context_tactic' list -> context_tactic'
+val CTHEN_BEST_FIRST: context_tactic -> (context_state -> bool) ->
+ (context_state -> int) -> context_tactic -> context_tactic
+val CBEST_FIRST: (context_state -> bool) -> (context_state -> int) ->
+ context_tactic -> context_tactic
+val CTHEN_ASTAR: context_tactic -> (context_state -> bool) ->
+ (int -> context_state -> int) -> context_tactic -> context_tactic
+val CASTAR: (context_state -> bool) -> (int -> context_state -> int) ->
+ context_tactic -> context_tactic
end = struct
@@ -74,6 +89,8 @@ fun CREPEAT ctac =
| SOME (cst, q) => rep (q :: qs) cst);
in fn cst => Seq.make_results (Seq.make (fn () => rep [] cst)) end
+fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac
+
fun CFILTER pred ctac cst =
ctac cst
|> Seq.filter_results
@@ -147,6 +164,89 @@ fun CSOMEGOAL ctac (cst as (_, st)) =
fun CRANGE [] _ = all_ctac
| CRANGE (ctac :: ctacs) i = CRANGE ctacs (i + 1) CTHEN ctac i
+fun CFIRST ctacs = fold_rev (curry op CORELSE) ctacs no_ctac
+
+(*FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i*)
+fun CFIRST' ctacs = fold_rev (curry op CORELSE') ctacs (K no_ctac)
+
+
+(** Search tacticals **)
+
+(* Best-first search *)
+
+structure Thm_Heap = Heap (
+ type elem = int * thm;
+ val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 Thm.prop_of)
+)
+
+structure Context_State_Heap = Heap (
+ type elem = int * context_state;
+ val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 (Thm.prop_of o #2))
+)
+
+fun some_of_list [] = NONE
+ | some_of_list (x :: l) = SOME (x, Seq.make (fn () => some_of_list l))
+
+(*Check for and delete duplicate proof states*)
+fun delete_all_min (cst as (_, st)) heap =
+ if Context_State_Heap.is_empty heap then heap
+ else if Thm.eq_thm (st, #2 (#2 (Context_State_Heap.min heap)))
+ then delete_all_min cst (Context_State_Heap.delete_min heap)
+ else heap
+
+(*Best-first search for a state that satisfies satp (incl initial state)
+ Function sizef estimates size of problem remaining (smaller means better).
+ tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
+fun CTHEN_BEST_FIRST ctac0 satp sizef ctac =
+ let
+ fun pairsize cst = (sizef cst, cst);
+ fun bfs (news, nst_heap) =
+ (case List.partition satp news of
+ ([], nonsats) => next (fold_rev Context_State_Heap.insert (map pairsize nonsats) nst_heap)
+ | (sats, _) => some_of_list sats)
+ and next nst_heap =
+ if Context_State_Heap.is_empty nst_heap then NONE
+ else
+ let
+ val (n, cst) = Context_State_Heap.min nst_heap;
+ in
+ bfs (Seq.list_of (Seq.filter_results (ctac cst)), delete_all_min cst (Context_State_Heap.delete_min nst_heap))
+ end;
+ fun btac cst = bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), Context_State_Heap.empty)
+ in fn cst => Seq.make_results (Seq.make (fn () => btac cst)) end
+
+(*Ordinary best-first search, with no initial tactic*)
+val CBEST_FIRST = CTHEN_BEST_FIRST all_ctac
+
+
+(* A*-like search *)
+
+(*Insertion into priority queue of states, marked with level*)
+fun insert_with_level (lnth: int * int * context_state) [] = [lnth]
+ | insert_with_level (l, m, cst) ((l', n, cst') :: csts) =
+ if n < m then (l', n, cst') :: insert_with_level (l, m, cst) csts
+ else if n = m andalso Thm.eq_thm (#2 cst, #2 cst') then (l', n, cst') :: csts
+ else (l, m, cst) :: (l', n, cst') :: csts;
+
+fun CTHEN_ASTAR ctac0 satp costf ctac =
+ let
+ fun bfs (news, nst, level) =
+ let fun cost cst = (level, costf level cst, cst) in
+ (case List.partition satp news of
+ ([], nonsats) => next (fold_rev (insert_with_level o cost) nonsats nst)
+ | (sats, _) => some_of_list sats)
+ end
+ and next [] = NONE
+ | next ((level, n, cst) :: nst) =
+ bfs (Seq.list_of (Seq.filter_results (ctac cst)), nst, level + 1)
+ in fn cst => Seq.make_results
+ (Seq.make (fn () => bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), [], 0)))
+ end
+
+(*Ordinary ASTAR, with no initial tactic*)
+val CASTAR = CTHEN_ASTAR all_ctac;
+
+
end
open Context_Tactical
diff --git a/spartan/core/elaborated_assumption.ML b/spartan/core/elaborated_statement.ML
index af3a384..81f4a7d 100644
--- a/spartan/core/elaborated_assumption.ML
+++ b/spartan/core/elaborated_statement.ML
@@ -1,7 +1,7 @@
-(* Title: elaborated_assumption.ML
+(* Title: elaborated_statement.ML
Author: Joshua Chen
-Term elaboration for goal and proof assumptions.
+Term elaboration for goal statements and proof commands.
Contains code from parts of
~~/Pure/Isar/element.ML and
@@ -9,7 +9,7 @@ Contains code from parts of
in both verbatim and modified forms.
*)
-structure Elaborated_Assumption: sig
+structure Elaborated_Statement: sig
val read_goal_statement:
(string, string, Facts.ref) Element.ctxt list ->
@@ -20,24 +20,7 @@ val read_goal_statement:
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
-
-
-(* 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.*)
+(* Elaborated goal statements *)
local
@@ -371,16 +354,28 @@ 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
+fun filter_assumes ((x as Element.Assumes _) :: xs) = x :: filter_assumes xs
+ | filter_assumes (_ :: xs) = filter_assumes xs
+ | filter_assumes [] = []
+
fun prep_statement prep activate raw_elems raw_stmt ctxt =
let
val ((_, _, _, elems, concl), _) =
prep {strict = true, do_close = false, fixed_frees = true}
- ([], []) I raw_elems raw_stmt ctxt;
- val ctxt' = ctxt
+ ([], []) I raw_elems raw_stmt ctxt
+
+ val (elems', ctxt') = ctxt
|> Proof_Context.set_stmt true
- |> fold_map activate elems |> #2
- |> Proof_Context.restore_stmt ctxt;
- in (concl, ctxt') end
+ |> fold_map activate elems
+ |> apsnd (Proof_Context.restore_stmt ctxt)
+
+ val assumes = filter_assumes elems'
+ val assms = flat (flat (map
+ (fn (Element.Assumes asms) =>
+ map (fn (_, facts) => map (Thm.cterm_of ctxt' o #1) facts) asms)
+ assumes))
+ val concl' = Elab.elaborate ctxt' assms concl handle error => concl
+ in (concl', ctxt') end
fun activate_i elem ctxt =
let
@@ -391,7 +386,7 @@ fun activate_i elem ctxt =
((Thm.def_binding_optional
(Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts),
(t, ps))))
- | Element.Assumes assms => Element.Assumes (elaborate ctxt assms)
+ | Element.Assumes assms => Element.Assumes (Elab.elaborate ctxt [] assms)
| e => e);
val ctxt' = Context.proof_map (Element.init elem') ctxt;
in ((Element.map_ctxt_attrib o map) Token.closure elem', ctxt') end
@@ -437,7 +432,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\<open>assuming\<close> "elabora
val b' = map (map read_terms) b
val c' = c |> map (fn ((b, atts), ss) =>
((b, map (Attrib.attribute_cmd ctxt) atts), map read_terms ss))
- val c'' = elaborate ctxt c'
+ val c'' = Elab.elaborate ctxt [] c'
in Proof.assume a' b' c'' state end)))
end
diff --git a/spartan/core/elaboration.ML b/spartan/core/elaboration.ML
index 27b6bb0..9e5e0bd 100644
--- a/spartan/core/elaboration.ML
+++ b/spartan/core/elaboration.ML
@@ -1,13 +1,14 @@
(* Title: elaboration.ML
Author: Joshua Chen
-Basic elaboration.
+Basic term elaboration.
*)
structure Elab: sig
val elab: Proof.context -> cterm list -> term -> Envir.env
val elab_stmt: Proof.context -> cterm list -> term -> Envir.env * term
+val elaborate: Proof.context -> cterm list -> ('a * (term * term list) list) list -> ('a * (term * term list) list) list
end = struct
@@ -72,5 +73,19 @@ fun elab_stmt ctxt assums stmt =
in (subst', subst_term subst' stmt) end
end
+(*Apply elaboration to the list format that assumptions and goal statements are
+ given in*)
+fun elaborate ctxt known 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_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 known) end
+
end
diff --git a/spartan/core/focus.ML b/spartan/core/focus.ML
index 1d8de78..2ad4c8a 100644
--- a/spartan/core/focus.ML
+++ b/spartan/core/focus.ML
@@ -1,14 +1,51 @@
(* Title: focus.ML
- Author: Makarius Wenzel, Joshua Chen
+ Author: Joshua Chen
-A modified version of the Isar `subgoal` command
-that keeps schematic variables in the goal state.
+Focus on head subgoal, with optional variable renaming.
-Modified from code originally written by Makarius Wenzel.
+Modified from code contained in ~~/Pure/Isar/subgoal.ML.
*)
local
+fun reverse_prems imp =
+ let val (prems, concl) = (Drule.strip_imp_prems imp, Drule.strip_imp_concl imp)
+ in fold (curry mk_implies) prems concl end
+
+fun gen_focus ctxt i bindings raw_st =
+ let
+ val st = raw_st
+ |> Thm.solve_constraints
+ |> Thm.transfer' ctxt
+ |> Raw_Simplifier.norm_hhf_protect ctxt
+
+ val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt
+
+ val ((params, goal), ctxt2) =
+ Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1
+
+ val (asms, concl) =
+ (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
+
+ fun intern_var_assms asm (asms, concl) =
+ if Lib.no_vars (Thm.term_of asm)
+ then (asm :: asms, concl)
+ else (asms, Drule.mk_implies (asm, concl))
+
+ val (asms', concl') = fold intern_var_assms asms ([], concl)
+ |> apfst rev |> apsnd reverse_prems
+
+ val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of (asms')) ctxt2
+ val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst)
+ val schematics = (schematic_types, schematic_terms)
+ val asms' = map (Thm.instantiate_cterm schematics) asms'
+ val concl' = Thm.instantiate_cterm schematics concl'
+ val (prems, context) = Assumption.add_assumes asms' ctxt3
+ in
+ ({context = context, params = params, prems = prems,
+ asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
+ end
+
fun param_bindings ctxt (param_suffix, raw_param_specs) st =
let
val _ = if Thm.no_prems st then error "No subgoals!" else ()
@@ -24,8 +61,8 @@ fun param_bindings ctxt (param_suffix, raw_param_specs) st =
error ("Excessive subgoal parameter specification" ^
Position.here_list (map snd (drop n raw_param_specs)))
- val param_specs =
- raw_param_specs |> map
+ val param_specs = raw_param_specs
+ |> map
(fn (NONE, _) => NONE
| (SOME x, pos) =>
let
@@ -39,7 +76,7 @@ fun param_bindings ctxt (param_suffix, raw_param_specs) st =
| bindings _ ys = map Binding.name ys
in bindings param_specs subgoal_params end
-fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
+fun gen_schematic_subgoal prep_atts raw_result_binding param_specs state =
let
val _ = Proof.assert_backward state
@@ -47,17 +84,13 @@ fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_s
|> Proof.map_context (Proof_Context.set_mode Proof_Context.mode_schematic)
|> Proof.refine_insert []
- val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1
-
+ val {context = ctxt, facts, goal = st} = Proof.raw_goal state1
val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding
- val (prems_binding, do_prems) =
- (case raw_prems_binding of
- SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
- | NONE => (Binding.empty_atts, false))
- val (subgoal_focus, _) =
- (if do_prems then Subgoal.focus_prems else Subgoal.focus_params) ctxt
- 1 (SOME (param_bindings ctxt param_specs st)) st
+ val subgoal_focus = #1
+ (gen_focus ctxt 1 (SOME (param_bindings ctxt param_specs st)) st)
+
+ val prems = #prems subgoal_focus
fun after_qed (ctxt'', [[result]]) =
Proof.end_block #> (fn state' =>
@@ -83,31 +116,29 @@ fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_s
|> Proof.begin_block
|> Proof.map_context (fn _ =>
#context subgoal_focus
- |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
+ |> Proof_Context.note_thmss "" [((Binding.name "prems", []), [(prems, [])])]
+ |> #2)
|> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
- NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
- |> Proof.using_facts facts
+ NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])]
+ |> #2
+ |> Proof.using_facts (facts @ prems)
|> pair subgoal_focus
end
val opt_fact_binding =
- Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
+ Scan.optional ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Args.colon)
Binding.empty_atts
-val for_params =
- Scan.optional
- (\<^keyword>\<open>vars\<close> |--
- Parse.!!! ((Scan.option Parse.dots >> is_some) --
- (Scan.repeat1 (Parse.maybe_position Parse.name_position))))
- (false, [])
+val for_params = Scan.optional
+ (\<^keyword>\<open>vars\<close> |--
+ Parse.!!! ((Scan.option Parse.dots >> is_some) --
+ (Scan.repeat1 (Parse.maybe_position Parse.name_position))))
+ (false, [])
val schematic_subgoal_cmd = gen_schematic_subgoal Attrib.attribute_cmd
-val parser =
- opt_fact_binding
- -- (Scan.option (\<^keyword>\<open>prems\<close> |-- Parse.!!! opt_fact_binding))
- -- for_params >> (fn ((a, b), c) =>
- Toplevel.proofs (Seq.make_results o Seq.single o #2 o schematic_subgoal_cmd a b c))
+val parser = opt_fact_binding -- for_params >> (fn (fact, params) =>
+ Toplevel.proofs (Seq.make_results o Seq.single o #2 o schematic_subgoal_cmd fact params))
in
@@ -117,9 +148,10 @@ val _ = Outer_Syntax.command \<^command_keyword>\<open>focus\<close>
"focus on first subgoal within backward refinement, without instantiating schematic vars"
parser
-val _ = Outer_Syntax.command \<^command_keyword>\<open>\<guillemotright>\<close> "focus bullet" parser
val _ = Outer_Syntax.command \<^command_keyword>\<open>\<^item>\<close> "focus bullet" parser
val _ = Outer_Syntax.command \<^command_keyword>\<open>\<^enum>\<close> "focus bullet" parser
+val _ = Outer_Syntax.command \<^command_keyword>\<open>\<circ>\<close> "focus bullet" parser
+val _ = Outer_Syntax.command \<^command_keyword>\<open>\<diamondop>\<close> "focus bullet" parser
val _ = Outer_Syntax.command \<^command_keyword>\<open>~\<close> "focus bullet" parser
end
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
index 87ec2b8..540f5c7 100644
--- a/spartan/core/goals.ML
+++ b/spartan/core/goals.ML
@@ -1,9 +1,9 @@
(* Title: goals.ML
- Author: Makarius Wenzel, Joshua Chen
+ Author: Joshua Chen
Goal statements and proof term export.
-Modified from code originally written by Makarius Wenzel.
+Modified from code contained in ~~/Pure/Isar/specification.ML.
*)
local
@@ -184,15 +184,15 @@ val schematic_theorem_cmd =
gen_schematic_theorem
Bundle.includes_cmd
Attrib.check_src
- Elaborated_Assumption.read_goal_statement
+ Elaborated_Statement.read_goal_statement
fun theorem spec descr =
Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
- ( Scan.option (Args.parens (Args.$$$ "derive"))
+ ( Scan.option (Args.parens (Args.$$$ "def"))
-- (long_statement || short_statement) >>
(fn (opt_derive, (long, binding, includes, elems, concl)) =>
schematic_theorem_cmd
- (case opt_derive of SOME "derive" => true | _ => false)
+ (case opt_derive of SOME "def" => true | _ => false)
long descr NONE (K I) binding includes elems concl) )
fun definition spec descr =
diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML
index 3922ae0..19d3d71 100644
--- a/spartan/core/tactics.ML
+++ b/spartan/core/tactics.ML
@@ -19,8 +19,7 @@ end = struct
(* Side conditions *)
-val solve_side_conds =
- Attrib.setup_config_int \<^binding>\<open>solve_side_conds\<close> (K 2)
+val solve_side_conds = Attrib.setup_config_int \<^binding>\<open>solve_side_conds\<close> (K 2)
fun SIDE_CONDS ctac facts i (cst as (ctxt, st)) = cst |> (ctac i CTHEN
(case Config.get ctxt solve_side_conds of
diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML
index 57164a1..a6e1726 100644
--- a/spartan/core/typechecking.ML
+++ b/spartan/core/typechecking.ML
@@ -51,10 +51,9 @@ fun known_ctac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
if Lib.no_vars concl orelse
(Lib.is_typing concl andalso Lib.no_vars (Lib.term_of_typing concl))
then
- let val ths = facts
+ let val ths = map (Simplifier.norm_hhf ctxt)
+ (facts @ map fst (Facts.props (Proof_Context.facts_of ctxt)))
(*FIXME: Shouldn't pull nameless facts directly from context*)
- @ map fst (Facts.props (Proof_Context.facts_of ctxt))
- |> map (Simplifier.norm_hhf ctxt)
in
(debug_tac ctxt "resolve" THEN resolve_tac ctxt ths i ORELSE
debug_tac ctxt "assume" THEN assume_tac ctxt i) st
@@ -70,7 +69,8 @@ fun check_infer_step facts i (ctxt, st) =
val tac = SUBGOAL (fn (goal, i) =>
if Lib.rigid_typing_concl goal
then
- let val net = Tactic.build_net (facts
+ let val net = Tactic.build_net (
+ map (Simplifier.norm_hhf ctxt) facts
(*MAYBE FIXME: Remove `typechk` from this list, and instead perform
definitional unfolding to (w?)hnf.*)
@(Named_Theorems.get ctxt \<^named_theorems>\<open>typechk\<close>)
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index be86b63..34873e4 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -132,9 +132,9 @@ Definition app:
assumes "A: U i" "xs: List A" "ys: List A"
shows "List A"
apply (elim xs)
- \<guillemotright> by (fact \<open>ys:_\<close>)
- \<guillemotright> prems vars x _ rec
- proof - show "x # rec: List A" by typechk qed
+ \<^item> by (fact \<open>ys:_\<close>)
+ \<^item> vars x _ rec
+ proof - show "x # rec: List A" by typechk qed
done
definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app ? xs ys"
@@ -169,8 +169,8 @@ Definition rev:
assumes "A: U i" "xs: List A"
shows "List A"
apply (elim xs)
- \<guillemotright> by (rule List_nil)
- \<guillemotright> prems vars x _ rec proof - show "app rec [x]: List A" by typechk qed
+ \<^item> by (rule List_nil)
+ \<^item> vars x _ rec proof - show "app rec [x]: List A" by typechk qed
done
definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev ?"
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index 0ce534c..a2e1638 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -1,7 +1,7 @@
chapter \<open>Maybe type\<close>
theory Maybe
-imports More_Types
+imports Prelude
begin
@@ -25,11 +25,10 @@ Definition MaybeInd:
"\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
"m: Maybe A"
shows "C m"
- supply assms[unfolded Maybe_def none_def some_def]
+ using assms[unfolded Maybe_def none_def some_def]
apply (elim m)
- \<guillemotright> unfolding Maybe_def .
- \<guillemotright> by (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>)
- \<guillemotright> by elim (rule \<open>_: C (inr _ _ _)\<close>)
+ apply (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>)
+ apply (elim, rule \<open>_: C (inr _ _ _)\<close>)
done
Lemma Maybe_comp_none:
@@ -39,8 +38,9 @@ Lemma Maybe_comp_none:
"\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
"\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
shows "MaybeInd A C c\<^sub>0 f (none A) \<equiv> c\<^sub>0"
- supply assms[unfolded Maybe_def some_def none_def]
- unfolding MaybeInd_def none_def by reduce
+ using assms
+ unfolding Maybe_def MaybeInd_def none_def some_def
+ by reduce
Lemma Maybe_comp_some:
assumes
@@ -50,8 +50,9 @@ Lemma Maybe_comp_some:
"\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
"\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
shows "MaybeInd A C c\<^sub>0 f (some A a) \<equiv> f a"
- supply assms[unfolded Maybe_def some_def none_def]
- unfolding MaybeInd_def some_def by (reduce add: Maybe_def)
+ using assms
+ unfolding Maybe_def MaybeInd_def none_def some_def
+ by reduce
lemmas
[form] = MaybeF and
diff --git a/spartan/lib/More_Types.thy b/spartan/lib/Prelude.thy
index 55e6554..36f12d2 100644
--- a/spartan/lib/More_Types.thy
+++ b/spartan/lib/Prelude.thy
@@ -1,4 +1,4 @@
-theory More_Types
+theory Prelude
imports Spartan
begin
@@ -114,7 +114,7 @@ Lemma if_true:
"b: C false"
shows "ifelse C true a b \<equiv> a"
unfolding ifelse_def true_def
- supply assms[unfolded Bool_def true_def false_def]
+ using assms unfolding Bool_def true_def false_def
by reduce
Lemma if_false:
@@ -124,7 +124,7 @@ Lemma if_false:
"b: C false"
shows "ifelse C false a b \<equiv> b"
unfolding ifelse_def false_def
- supply assms[unfolded Bool_def true_def false_def]
+ using assms unfolding Bool_def true_def false_def
by reduce
lemmas
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 15:19:19 +0000