diff options
Diffstat (limited to 'spartan')
-rw-r--r-- | spartan/lib/elimination.ML | 5 | ||||
-rw-r--r-- | spartan/lib/focus.ML | 2 | ||||
-rw-r--r-- | spartan/lib/tactics.ML | 3 | ||||
-rw-r--r-- | spartan/theories/Equivalence.thy | 8 | ||||
-rw-r--r-- | spartan/theories/Identity.thy | 13 | ||||
-rw-r--r-- | spartan/theories/Spartan.thy | 7 |
6 files changed, 21 insertions, 17 deletions
diff --git a/spartan/lib/elimination.ML b/spartan/lib/elimination.ML index 85ce669..bd23c94 100644 --- a/spartan/lib/elimination.ML +++ b/spartan/lib/elimination.ML @@ -6,6 +6,7 @@ Type elimination automation. structure Elim = struct +(** Context data **) (* Elimination rule data *) structure Rules = Generic_Data ( type T = thm Termtab.table @@ -30,4 +31,8 @@ val _ = Theory.setup ( fn context => (rules (Context.proof_of context))) ) +(** General elimination-induction tactic **) + + + end diff --git a/spartan/lib/focus.ML b/spartan/lib/focus.ML index dd8d3d9..1d8de78 100644 --- a/spartan/lib/focus.ML +++ b/spartan/lib/focus.ML @@ -105,7 +105,7 @@ val schematic_subgoal_cmd = gen_schematic_subgoal Attrib.attribute_cmd val parser = opt_fact_binding - -- (Scan.option (\<^keyword>\<open>premises\<close> |-- Parse.!!! 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)) diff --git a/spartan/lib/tactics.ML b/spartan/lib/tactics.ML index 0e09533..c72947a 100644 --- a/spartan/lib/tactics.ML +++ b/spartan/lib/tactics.ML @@ -104,8 +104,7 @@ fun intro_tac ctxt = SUBGOAL (fn (_, i) => SIDE_CONDS fun intros_tac ctxt = SUBGOAL (fn (_, i) => (CHANGED o REPEAT o CHANGED o intro_tac ctxt) i) -(* Basic elimination tactic *) -(*Only uses existing type judgments from the context +(*Basic elimination tactic, only uses existing type judgments from the context (performs no type synthesis)*) fun elims_tac opt_tm ctxt = case opt_tm of NONE => SUBGOAL (fn (_, i) => eresolve_tac ctxt (Elim.rules ctxt) i) diff --git a/spartan/theories/Equivalence.thy b/spartan/theories/Equivalence.thy index 44b77dd..97cd18d 100644 --- a/spartan/theories/Equivalence.thy +++ b/spartan/theories/Equivalence.thy @@ -197,7 +197,7 @@ Lemma (derive) funcomp_qinv: shows "qinv f \<rightarrow> qinv g \<rightarrow> qinv (g \<circ> f)" apply (intros, unfold qinv_def, elims) focus - premises hyps + prems prms vars _ _ finv _ ginv _ HfA HfB HgB HgC apply intro @@ -246,7 +246,7 @@ Lemma (derive) biinv_imp_qinv: apply elims text \<open>Name the components:\<close> - focus premises vars _ _ _ g H1 h H2 + focus prems vars _ _ _ g H1 h H2 thm \<open>g:_\<close> \<open>h:_\<close> \<open>H1:_\<close> \<open>H2:_\<close> text \<open> @@ -384,14 +384,14 @@ Lemma (derive) id_imp_equiv: supply [[auto_typechk=false]] \<guillemotright> apply (equality \<open>p:_\<close>) - \<^item> premises vars A B + \<^item> prems vars A B apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric]) apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric]) apply (rule transport, rule U_in_U) apply (rule lift_universe_codomain, rule U_in_U) apply (typechk, rule U_in_U) done - \<^item> premises vars A + \<^item> prems vars A apply (subst transport_comp) \<^enum> by (rule U_in_U) \<^enum> by reduce (rule lift_universe) diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy index 19b8b7a..4a4cc40 100644 --- a/spartan/theories/Identity.thy +++ b/spartan/theories/Identity.thy @@ -15,7 +15,7 @@ axiomatization refl :: \<open>o \<Rightarrow> o\<close> and IdInd :: \<open>o \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> -syntax "_Id" :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2_ =\<^bsub>_\<^esub>/ _)" [111, 0, 111] 110) +syntax "_Id" :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2_ =\<^bsub>_\<^esub>/ _)" [111, 0, 111] 110) translations "a =\<^bsub>A\<^esub> b" \<rightleftharpoons> "CONST Id A a b" @@ -71,7 +71,7 @@ Lemma (derive) pathcomp: shows "x =\<^bsub>A\<^esub> z" apply (equality \<open>p:_\<close>) - focus premises vars x p + focus prems vars x p apply (equality \<open>p:_\<close>) apply intro done @@ -158,9 +158,9 @@ Lemma (derive) pathcomp_assoc: "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" "r: z =\<^bsub>A\<^esub> w" shows "p \<bullet> (q \<bullet> r) = p \<bullet> q \<bullet> r" apply (equality \<open>p:_\<close>) - focus premises vars x p + focus prems vars x p apply (equality \<open>p:_\<close>) - focus premises vars x p + focus prems vars x p apply (equality \<open>p:_\<close>) apply (reduce; intros) done @@ -200,7 +200,7 @@ Lemma (derive) ap_pathcomp: shows "f[p \<bullet> q] = f[p] \<bullet> f[q]" apply (equality \<open>p:_\<close>) - focus premises vars x p + focus prems vars x p apply (equality \<open>p:_\<close>) apply (reduce; intro) done @@ -302,7 +302,7 @@ Lemma (derive) transport_pathcomp: "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" shows "trans P q (trans P p u) = trans P (p \<bullet> q) u" apply (equality \<open>p:_\<close>) - focus premises vars x p + focus prems vars x p apply (equality \<open>p:_\<close>) apply (reduce; intros) done @@ -430,4 +430,5 @@ Lemma (derive) apd_ap: shows "apd f p = trans_const B p (f x) \<bullet> f[p]" by (equality \<open>p:_\<close>) (reduce; intro) + end diff --git a/spartan/theories/Spartan.thy b/spartan/theories/Spartan.thy index a79f209..5274ea2 100644 --- a/spartan/theories/Spartan.thy +++ b/spartan/theories/Spartan.thy @@ -8,7 +8,7 @@ imports keywords "Theorem" "Lemma" "Corollary" "Proposition" :: thy_goal_stmt and "focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and - "derive" "vars":: quasi_command and + "derive" "prems" "vars":: quasi_command and "print_coercions" :: thy_decl begin @@ -138,9 +138,6 @@ axiomatization where \<rbrakk> \<Longrightarrow> \<Sum>x: A. B x \<equiv> \<Sum>x: A. B' x" - - - section \<open>Proof commands\<close> named_theorems typechk @@ -152,6 +149,7 @@ ML_file \<open>../lib/focus.ML\<close> section \<open>Congruence automation\<close> +(*Work in progress*) ML_file \<open>../lib/congruence.ML\<close> @@ -188,6 +186,7 @@ method_setup elim = method elims = elim+ +(*This could possibly use additional simplification hints via a simp: modifier*) method_setup typechk = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD ( CHANGED (ALLGOALS (TRY o typechk_tac ctxt))))\<close> |