diff options
author | Josh Chen | 2020-07-21 16:28:05 +0200 |
---|---|---|
committer | Josh Chen | 2020-07-21 16:28:05 +0200 |
commit | 306721649f0963ab225deb8d5670cfe196bb360d (patch) | |
tree | d44a93c55215bd24d9b9938418d6058d0343cf4e /spartan/core/Spartan.thy | |
parent | dfd241b2d85fc5a4ad4d7ddd64adf0138b05f083 (diff) |
1. Bugfix: implicits now properly name schematic variables. Fixes problems caused by variable name clashes. 2. reduce method now more principled: restricts to repeating on first subgoal. 3. An example declarative proof in Equivalence.thy.
Diffstat (limited to '')
-rw-r--r-- | spartan/core/Spartan.thy | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index a4ad300..fa6148f 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -52,7 +52,7 @@ paragraph \<open> typedecl o -judgment has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999) +consts has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999) text \<open>Type annotations for type-checking and inference.\<close> @@ -232,6 +232,10 @@ 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 ( @@ -255,6 +259,8 @@ method_setup cases = \<open>Args.term >> (fn tm => K (CONTEXT_METHOD ( CHEADGOAL o SIDE_CONDS (cases_ctac tm))))\<close> +method facts = fact+ + subsection \<open>Reflexivity\<close> @@ -310,7 +316,8 @@ setup \<open>map_theory_simpset (fn ctxt => ctxt addSolver (mk_solver "" (fn ctxt' => NO_CONTEXT_TACTIC ctxt' o Types.check_infer (Simplifier.prems_of ctxt'))))\<close> -method reduce uses add = changed \<open>((simp add: comp add | sub comp); typechk?)+\<close> +method reduce uses add = + changed \<open>repeat_new \<open>(simp add: comp add | sub comp); typechk?\<close>\<close> subsection \<open>Implicits\<close> @@ -327,10 +334,7 @@ ML_file \<open>implicits.ML\<close> attribute_setup implicit = \<open>Scan.succeed Implicits.implicit_defs_attr\<close> -ML \<open> -val _ = Context.>> - (Syntax_Phases.term_check 1 "" (fn ctxt => map (Implicits.make_holes ctxt))) -\<close> +ML \<open>val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes)\<close> text \<open>Automatically insert inhabitation judgments where needed:\<close> @@ -488,7 +492,7 @@ lemma snd_type [typechk]: lemma snd_comp [comp]: assumes "a: A" "b: B a" "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" shows "snd A B <a, b> \<equiv> b" - unfolding snd_def by reduce+ + unfolding snd_def by reduce subsection \<open>Notation\<close> |