1. New congruence declarations for calculational reasoning. 2. Remove old elimination tactic.

3 files changed, 87 insertions, 56 deletions

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 50002a6..1d93885 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -8,8 +8,9 @@ imports
 keywords
   "Theorem" "Lemma" "Corollary" "Proposition" :: thy_goal_stmt and
   "focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and
-  "derive" "prems" "vars":: quasi_command and
-  "print_coercions" :: thy_decl
+  "congruence" "print_coercions" :: thy_decl and
+  "rhs" "derive" "prems" "vars" :: quasi_command
+  
 
 begin
 
@@ -154,7 +155,8 @@ ML_file \<open>focus.ML\<close>
 
 section \<open>Congruence automation\<close>
 
-(*Potential to be retired*)
+consts "rhs" :: \<open>'a\<close> ("..")
+
 ML_file \<open>congruence.ML\<close>
 
 
@@ -186,10 +188,6 @@ method_setup intro =
 method_setup intros =
   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\<close>
 
-method_setup old_elim =
-  \<open>Scan.option Args.term >> (fn tm => fn ctxt =>
-    SIMPLE_METHOD' (SIDE_CONDS (old_elims_tac tm ctxt) ctxt))\<close>
-
 method_setup elim =
   \<open>Scan.repeat Args.term >> (fn tms => fn ctxt =>
     CONTEXT_METHOD (K (elim_context_tac tms ctxt 1)))\<close>
diff --git a/spartan/core/congruence.ML b/spartan/core/congruence.ML
index bb7348c..d9f4ffa 100644
--- a/spartan/core/congruence.ML
+++ b/spartan/core/congruence.ML
@@ -1,16 +1,82 @@
-signature Sym_Attr_Data =
-sig
-  val name: string
-  val symmetry_rule: thm
-end
+structure Congruence = struct
+
+(* Congruence context data *)
 
-functor Sym_Attr (D: Sym_Attr_Data) =
-struct
-  local
-    val distinct_prems = the_single o Seq.list_of o Tactic.distinct_subgoals_tac
+structure RHS = Generic_Data (
+  type T = (term * indexname) Termtab.table
+  val empty = Termtab.empty
+  val extend = I
+  val merge = Termtab.merge (Term.aconv o apply2 #1)
+)
+
+fun register_rhs t var =
+  let
+    val key = Term.head_of t
+    val idxname = #1 (dest_Var var)
   in
-    val attr = Thm.rule_attribute []
-      (K (fn th => distinct_prems (th RS D.symmetry_rule) handle THM _ => th))
-    val setup = Attrib.setup (Binding.name D.name) (Scan.succeed attr) ""
+    RHS.map (Termtab.update (key, (t, idxname)))
   end
+
+fun lookup_congruence ctxt t =
+  Termtab.lookup (RHS.get (Context.Proof ctxt)) (Term.head_of t)
+
+
+(* Congruence declarations *)
+
+local val Frees_to_Vars =
+  map_aterms (fn tm =>
+    case tm of
+      Free (name, T) => Var (("*!"^name, 0), T) (*Hacky naming!*)
+    | _ => tm)
+in
+
+(*Declare the "right-hand side" of types that are congruences.
+  Does not handle bound variables, so no dependent RHS in declarations!*)
+val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>congruence\<close>
+  "declare right hand side of congruence"
+  (Parse.term -- (\<^keyword>\<open>rhs\<close> |-- Parse.term) >>
+    (fn (t_str, rhs_str) => fn lthy =>
+    let
+      val (t, rhs) = apply2 (Frees_to_Vars o Syntax.read_term lthy)
+        (t_str, rhs_str)
+    in lthy |>
+      Local_Theory.background_theory (
+        Context.theory_map (register_rhs t rhs))
+    end))
+
+end
+
+
+(* Calculational reasoning: ".." setup *)
+
+fun last_rhs ctxt = map_aterms (fn t =>
+  case t of
+    Const (\<^const_name>\<open>rhs\<close>, _) =>
+      let
+        val this_name = Name_Space.full_name (Proof_Context.naming_of ctxt)
+          (Binding.name Auto_Bind.thisN)
+        val this = #thms (the (Proof_Context.lookup_fact ctxt this_name))
+          handle Option => []
+        val rhs =
+          (case map Thm.prop_of this of
+            [prop] =>
+              (let
+                val typ = Lib.type_of_typing (Logic.strip_assums_concl prop)
+                val (cong_pttrn, varname) = the (lookup_congruence ctxt typ)
+                val unif_res = Pattern.unify (Context.Proof ctxt)
+                  (cong_pttrn, typ) Envir.init
+                val rhs = #2 (the
+                  (Vartab.lookup (Envir.term_env unif_res) varname))
+              in
+                rhs
+              end handle Option =>
+                error (".. can't match right-hand side of congruence"))
+          | _ => Term.dummy)
+      in rhs end
+  | _ => t)
+
+val _ = Context.>>
+  (Syntax_Phases.term_check 5 "" (fn ctxt => map (last_rhs ctxt)))
+
+
 end
diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML
index f23bfee..0e7db43 100644
--- a/spartan/core/tactics.ML
+++ b/spartan/core/tactics.ML
@@ -4,7 +4,7 @@
 General tactics for dependent type theory.
 *)
 
-structure Tactics(* :
+structure Tactics:
 sig
 
 val assumptions_tac: Proof.context -> int -> tactic
@@ -16,9 +16,9 @@ val rule_tac: thm list -> Proof.context -> int -> tactic
 val dest_tac: int option -> thm list -> Proof.context -> int -> tactic
 val intro_tac: Proof.context -> int -> tactic
 val intros_tac: Proof.context -> int -> tactic
-val old_elims_tac: term option -> Proof.context -> int -> tactic
+val elim_context_tac: term list -> Proof.context -> int -> context_tactic
 
-end *) = struct
+end = struct
 
 (*An assumption tactic that only solves typing goals with rigid terms and
   judgmental equalities without schematic variables*)
@@ -99,40 +99,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
-  (performs no type synthesis)*)
-fun old_elims_tac opt_tm ctxt = case opt_tm of
-    NONE => SUBGOAL (fn (_, i) => eresolve_tac ctxt (map #1 (Elim.rules ctxt)) i)
-  | SOME tm => SUBGOAL (fn (goal, i) =>
-      let
-        fun elim_rule typing =
-          let
-            val hd = head_of (Lib.type_of_typing typing)
-            val opt_rl = Elim.lookup_rule ctxt hd
-          in
-            case opt_rl of
-              NONE => Drule.dummy_thm
-            | SOME (rl, _) => Drule.infer_instantiate' ctxt
-                [SOME (Thm.cterm_of ctxt tm)] rl
-          end
-
-        val template = Lib.typing_of_term tm
-
-        val facts = Proof_Context.facts_of ctxt
-        val candidate_typings = Facts.could_unify facts template
-        val candidate_rules =
-          map (elim_rule o Thm.prop_of o #1) candidate_typings
-
-        val prems = Logic.strip_assums_hyp goal
-        val candidate_typings' =
-          filter (fn prem => Term.could_unify (template, prem)) prems
-        val candidate_rules' = map elim_rule candidate_typings'
-      in
-        (resolve_tac ctxt candidate_rules
-        ORELSE' eresolve_tac ctxt candidate_rules') i
-      end)
-
-(* Revamped general induction/elimination *)
+(* Induction/elimination *)
 
 (*Pushes a context/goal premise typing t:T into a \<Prod>-type*)
 fun internalize_fact_tac t =