diff options
| -rw-r--r-- | spartan/core/Spartan.thy | 12 | ||||
| -rw-r--r-- | spartan/core/congruence.ML | 90 | ||||
| -rw-r--r-- | spartan/core/tactics.ML | 41 |
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 = |