diff options
| -rw-r--r-- | spartan/core/Goals.thy | 199 | ||||
| -rw-r--r-- | spartan/core/Spartan.thy | 38 |
2 files changed, 218 insertions, 19 deletions
diff --git a/spartan/core/Goals.thy b/spartan/core/Goals.thy new file mode 100644 index 0000000..f7bcaf5 --- /dev/null +++ b/spartan/core/Goals.thy @@ -0,0 +1,199 @@ +theory Goals +imports Spartan + +begin + +ML \<open> +val long_keyword = + Parse_Spec.includes >> K "" || + Parse_Spec.long_statement_keyword + +val long_statement = + Scan.optional + (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) + Binding.empty_atts + -- Scan.optional Parse_Spec.includes [] + -- Parse_Spec.long_statement + >> (fn ((binding, includes), (elems, concl)) => + (binding, includes, elems, concl)) + +val short_statement = + Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes + >> (fn ((shows, assumes), fixes) => + (false, Binding.empty_atts, [], + [Element.Fixes fixes, Element.Assumes assumes], + Element.Shows shows)) + +fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt = + let + val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt + val prems = Assumption.local_prems_of elems_ctxt ctxt + val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd) + stmt elems_ctxt + in + case raw_stmt of + Element.Shows _ => + let val stmt' = Attrib.map_specs (map prep_att) stmt + in (([], prems, stmt', NONE), stmt_ctxt) end + | Element.Obtains raw_obtains => + let + val asms_ctxt = stmt_ctxt + |> fold (fn ((name, _), asm) => + snd o Proof_Context.add_assms Assumption.assume_export + [((name, [Context_Rules.intro_query NONE]), asm)]) stmt + val that = Assumption.local_prems_of asms_ctxt stmt_ctxt + val ([(_, that')], that_ctxt) = asms_ctxt + |> Proof_Context.set_stmt true + |> Proof_Context.note_thmss "" + [((Binding.name Auto_Bind.thatN, []), [(that, [])])] + ||> Proof_Context.restore_stmt asms_ctxt + + val stmt' = [ + (Binding.empty_atts, + [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])]) + ] + in + ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'), + that_ctxt) + end + end + +fun define_proof_term name (local_name, [th]) lthy = + let + fun make_name_binding suffix local_name = + let val base_local_name = Long_Name.base_name local_name + in + Binding.qualified_name + ((case base_local_name of + "" => name + | _ => base_local_name) + ^(case suffix of + SOME "prf" => "_prf" + | SOME "def" => "_def" + | _ => "")) + end + + val (prems, concl) = + (Logic.strip_assums_hyp (Thm.prop_of th), + Logic.strip_assums_concl (Thm.prop_of th)) + in + if not (Lib.is_typing concl) then + ([], lthy) + else let + val prems_vars = distinct Term.aconv (flat + (map (Lib.collect_subterms is_Var) prems)) + + val concl_vars = Lib.collect_subterms is_Var + (Lib.term_of_typing concl) + + val params = inter Term.aconv concl_vars prems_vars + + val prf_tm = + fold_rev lambda params (Lib.term_of_typing concl) + + val ((_, (_, raw_def)), lthy') = Local_Theory.define + ((make_name_binding NONE local_name, Mixfix.NoSyn), + ((make_name_binding (SOME "prf") local_name, []), prf_tm)) lthy + + val def = + fold + (fn th1 => fn th2 => Thm.combination th2 th1) + (map (Thm.reflexive o Thm.cterm_of lthy) params) + raw_def + + val ((_, def'), lthy'') = Local_Theory.note + ((make_name_binding (SOME "def") local_name, []), [def]) + lthy' + in + (def', lthy'') + end + end + | define_proof_term _ _ _ = error + ("Unimplemented: handling proof terms of multiple facts in" + ^" single result") + +fun gen_schematic_theorem + bundle_includes prep_att prep_stmt + gen_prf long kind before_qed after_qed (name, raw_atts) + raw_includes raw_elems raw_concl int lthy = + let + val _ = Local_Theory.assert lthy; + + val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy)) + val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy + |> bundle_includes raw_includes + |> prep_statement (prep_att lthy) prep_stmt elems raw_concl + val atts = more_atts @ map (prep_att lthy) raw_atts + val pos = Position.thread_data () + + val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN + + fun after_qed' results goal_ctxt' = + let + val results' = burrow + (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy) + results + + val ((res, lthy'), substmts) = + if forall (Binding.is_empty_atts o fst) stmt + then ((map (pair "") results', lthy), false) + else + (Local_Theory.notes_kind kind + (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') + lthy, + true) + + val (res', lthy'') = + if gen_prf + then + let + val (prf_tm_defs, lthy'') = + fold + (fn result => fn (defs, lthy) => + apfst (fn new_defs => defs @ new_defs) + (define_proof_term (Binding.name_of name) result lthy)) + res ([], lthy') + + val res_folded = + map (apsnd (map (Local_Defs.fold lthy'' prf_tm_defs))) res + in + Local_Theory.notes_kind kind + [((name, @{attributes [typechk]} @ atts), + [(maps #2 res_folded, [])])] + lthy'' + end + else + Local_Theory.notes_kind kind + [((name, atts), [(maps #2 res, [])])] + lthy' + + val _ = Proof_Display.print_results int pos lthy'' + ((kind, Binding.name_of name), map (fn (_, ths) => ("", ths)) res') + + val _ = + if substmts then map + (fn (name, ths) => Proof_Display.print_results int pos lthy'' + (("and", name), [("", ths)])) + res + else [] + in + after_qed results' lthy'' + end + in + goal_ctxt + |> not (null prems) ? + (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd) + |> Proof.theorem before_qed after_qed' (map snd stmt) + |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths) + end + +val schematic_theorem_cmd = + gen_schematic_theorem + Bundle.includes_cmd + Attrib.check_src + Expression.read_statement +\<close> + + + +end diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 8c87c2e..2c7216e 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -185,28 +185,13 @@ section \<open>Infrastructure\<close> ML_file \<open>lib.ML\<close> ML_file \<open>context_tactical.ML\<close> -subsection \<open>Proof commands\<close> +subsection \<open>Type-checking/inference\<close> -ML_file \<open>focus.ML\<close> - -named_theorems typechk - -ML_file \<open>goals.ML\<close> - -subsection \<open>Congruence automation\<close> - -consts "rhs" :: \<open>'a\<close> ("..") - -ML_file \<open>congruence.ML\<close> - -subsection \<open>Proof methods and type-checking/inference\<close> - -named_theorems form and intro and intros and comp +named_theorems form and intro and intros and comp and typechk \<comment> \<open>`intros` stores the introduction rule variants used by the `intro` and `intros` methods.\<close> ML_file \<open>elimination.ML\<close> \<comment> \<open>elimination rules\<close> -ML_file \<open>cases.ML\<close> \<comment> \<open>case reasoning rules\<close> lemmas [form] = PiF SigF and @@ -218,7 +203,6 @@ lemmas [cong] = Pi_cong lam_cong Sig_cong ML_file \<open>typechecking.ML\<close> -ML_file \<open>tactics.ML\<close> method_setup typechk = \<open>Scan.succeed (K (CONTEXT_METHOD ( @@ -228,6 +212,16 @@ method_setup known = \<open>Scan.succeed (K (CONTEXT_METHOD ( CHEADGOAL o Types.known_ctac)))\<close> +subsection \<open>Statement commands\<close> + +ML_file \<open>focus.ML\<close> +ML_file \<open>goals.ML\<close> + +subsection \<open>Proof methods\<close> + +ML_file \<open>cases.ML\<close> \<comment> \<open>case reasoning rules\<close> +ML_file \<open>tactics.ML\<close> + method_setup rule = \<open>Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\<close> @@ -319,6 +313,12 @@ setup \<open>map_theory_simpset (fn ctxt => method reduce uses add = changed \<open>repeat_new \<open>(simp add: comp add | sub comp); typechk?\<close>\<close> +subsection \<open>Congruence automation\<close> + +consts "rhs" :: \<open>'a\<close> ("..") + +ML_file \<open>congruence.ML\<close> + subsection \<open>Implicits\<close> text \<open> @@ -513,7 +513,7 @@ Lemma fst [typechk]: "p: \<Sum>x: A. B x" "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" shows "fst p: A" - by typechk + by typechk Lemma snd [typechk]: assumes |