From 232856fbef15105f619a5c1056da2602984804df Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 23 Feb 2019 18:57:15 +0100
Subject: compute method solves subgoals arising from subst

---
 HoTT_Methods.thy | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'HoTT_Methods.thy')

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index c9744e9..ad7384d 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -2,7 +2,7 @@
 Isabelle/HoTT: Proof methods
 Jan 2019
 
-Setup various proof methods and auxiliary functionality.
+Set up various proof methods and auxiliary functionality.
 
 ********)
 
@@ -23,10 +23,12 @@ ML_file "~~/src/Tools/eqsubst.ML"
 
 text \<open>
 Method @{theory_text compute} performs single-step simplifications, using any rules declared @{attribute comp} in the context.
-Premises of the rule(s) applied are added as new subgoals.
+Subgoals arising from a substitution are solved by assumption and standard rules, as well as rules passed using @{theory_text add}.
+
+Note that the solving is sometimes a little eager; for more manual control one should use @{method subst} directly.
 \<close>
 
-method compute declares comp = (subst comp)
+method compute uses add declares comp = (subst comp; (rule add | assumption | rule)?)
 
 
 section \<open>Handling universes\<close>
@@ -51,7 +53,7 @@ method cumulativity declares form = (
 
 section \<open>Deriving typing judgments\<close>
 
-method routine uses add = (assumption | rule add | rule)+
+method routine uses add = (rule add | assumption | rule)+
 
 text \<open>
 The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}.
@@ -65,8 +67,8 @@ The method @{theory_text derive} combines @{method routine} and @{method compute
 It also handles universes using @{method hierarchy} and @{method cumulativity}.
 \<close>
 
-method derive uses lems =
-  (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
+method derive uses lems declares comp =
+  (routine add: lems | compute add: lems comp: comp | cumulativity form: lems | hierarchy)+
 
 
 section \<open>Additional method combinators\<close>
-- 
cgit v1.2.3