renamings

6 files changed, 49 insertions, 45 deletions

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index ffe3778..5046b6a 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -295,7 +295,7 @@ method_setup this =
 
 subsection \<open>Rewriting\<close>
 
-consts rewrite_hole :: "'a::{}"  ("\<hole>")
+consts compute_hole :: "'a::{}"  ("\<hole>")
 
 lemma eta_expand:
   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
@@ -319,10 +319,10 @@ lemma imp_cong_eq:
   done
 
 ML_file \<open>~~/src/HOL/Library/cconv.ML\<close>
-ML_file \<open>rewrite.ML\<close>
+ML_file \<open>comp.ML\<close>
 
-\<comment> \<open>\<open>reduce\<close> simplifies terms via computational equalities\<close>
-method reduce uses add =
+\<comment> \<open>\<open>compute\<close> simplifies terms via computational equalities\<close>
+method compute uses add =
   changed \<open>repeat_new \<open>(simp add: comp add | subst comp); typechk?\<close>\<close>
 
 
@@ -396,7 +396,7 @@ Lemma refine_codomain:
     "f: \<Prod>x: A. B x"
     "\<And>x. x: A \<Longrightarrow> f `x: C x"
   shows "f: \<Prod>x: A. C x"
-  by (rewrite eta_exp)
+  by (comp eta_exp)
 
 Lemma lift_universe_codomain:
   assumes "A: U i" "f: A \<rightarrow> U j"
@@ -432,7 +432,7 @@ Lemma funcomp_assoc [comp]:
     "h: \<Prod>x: C. D x"
   shows
     "(h \<circ>\<^bsub>B\<^esub> g) \<circ>\<^bsub>A\<^esub> f \<equiv> h \<circ>\<^bsub>A\<^esub> g \<circ>\<^bsub>A\<^esub> f"
-  unfolding funcomp_def by reduce
+  unfolding funcomp_def by compute
 
 Lemma funcomp_lambda_comp [comp]:
   assumes
@@ -441,7 +441,7 @@ Lemma funcomp_lambda_comp [comp]:
     "\<And>x. x: B \<Longrightarrow> c x: C x"
   shows
     "(\<lambda>x: B. c x) \<circ>\<^bsub>A\<^esub> (\<lambda>x: A. b x) \<equiv> \<lambda>x: A. c (b x)"
-  unfolding funcomp_def by reduce
+  unfolding funcomp_def by compute
 
 Lemma funcomp_apply_comp [comp]:
   assumes
@@ -449,7 +449,7 @@ Lemma funcomp_apply_comp [comp]:
     "f: A \<rightarrow> B" "g: \<Prod>x: B. C x"
     "x: A"
   shows "(g \<circ>\<^bsub>A\<^esub> f) x \<equiv> g (f x)"
-  unfolding funcomp_def by reduce
+  unfolding funcomp_def by compute
 
 subsection \<open>Notation\<close>
 
@@ -465,17 +465,17 @@ abbreviation id where "id A \<equiv> \<lambda>x: A. x"
 lemma
   id_type [type]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and
   id_comp [comp]: "x: A \<Longrightarrow> (id A) x \<equiv> x" \<comment> \<open>for the occasional manual rewrite\<close>
-  by reduce+
+  by compute+
 
 Lemma id_left [comp]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "(id B) \<circ>\<^bsub>A\<^esub> f \<equiv> f"
-  by (rewrite eta_exp[of f]) (reduce, rule eta)
+  by (comp eta_exp[of f]) (compute, rule eta)
 
 Lemma id_right [comp]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
   shows "f \<circ>\<^bsub>A\<^esub> (id A) \<equiv> f"
-  by (rewrite eta_exp[of f]) (reduce, rule eta)
+  by (comp eta_exp[of f]) (compute, rule eta)
 
 lemma id_U [type]:
   "id (U i): U i \<rightarrow> U i"
@@ -496,7 +496,7 @@ Lemma fst_comp [comp]:
   assumes
     "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" "a: A" "b: B a"
   shows "fst A B <a, b> \<equiv> a"
-  unfolding fst_def by reduce
+  unfolding fst_def by compute
 
 Lemma snd_type [type]:
   assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
@@ -506,7 +506,7 @@ Lemma snd_type [type]:
 Lemma snd_comp [comp]:
   assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" "a: A" "b: B a"
   shows "snd A B <a, b> \<equiv> b"
-  unfolding snd_def by reduce
+  unfolding snd_def by compute
 
 subsection \<open>Notation\<close>
 
diff --git a/spartan/core/rewrite.ML b/spartan/core/comp.ML
index af70cfc..2e50753 100644
--- a/spartan/core/rewrite.ML
+++ b/spartan/core/comp.ML
@@ -1,10 +1,16 @@
-(*  Title:      rewrite.ML
+(*  Title:      compute.ML
     Author:     Christoph Traut, Lars Noschinski, TU Muenchen
     Modified:   Joshua Chen, University of Innsbruck
 
-This is a rewrite method that supports subterm-selection based on patterns.
+This is a method for rewriting computational equalities that supports subterm
+selection based on patterns.
 
-The patterns accepted by rewrite are of the following form:
+This code has been slightly modified from the original at HOL/Library/compute.ML
+to incorporate automatic discharge of type-theoretic side conditions.
+
+Comment from the original code follows:
+
+The patterns accepted by compute are of the following form:
   <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
   <pattern> ::= (in <atom> | at <atom>) [<pattern>]
   <args>    ::= [<pattern>] ("to" <term>) <thms>
@@ -14,15 +20,12 @@ patterns but has diverged significantly during its development.
 
 We also allow introduction of identifiers for bound variables,
 which can then be used to match arbitrary subterms inside abstractions.
-
-This code has been slightly modified from the original at HOL/Library/rewrite.ML
-to incorporate automatic discharge of type-theoretic side conditions.
 *)
 
 infix 1 then_pconv;
 infix 0 else_pconv;
 
-signature REWRITE =
+signature COMPUTE =
 sig
   type patconv = Proof.context -> Type.tyenv * (string * term) list -> cconv
   val then_pconv: patconv * patconv -> patconv
@@ -41,19 +44,19 @@ sig
   val judgment_pconv: patconv -> patconv
   val in_pconv: patconv -> patconv
   val match_pconv: patconv -> term * (string option * typ) list -> patconv
-  val rewrs_pconv: term option -> thm list -> patconv
+  val comps_pconv: term option -> thm list -> patconv
 
   datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
 
   val mk_hole: int -> typ -> term
 
-  val rewrite_conv: Proof.context
+  val compute_conv: Proof.context
     -> (term * (string * typ) list, string * typ option) pattern list * term option
     -> thm list
     -> conv
 end
 
-structure Rewrite : REWRITE =
+structure Compute : COMPUTE =
 struct
 
 datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
@@ -72,13 +75,13 @@ fun mk_hole i T = Var ((holeN, i), T)
 fun is_hole (Var ((name, _), _)) = (name = holeN)
   | is_hole _ = false
 
-fun is_hole_const (Const (\<^const_name>\<open>rewrite_hole\<close>, _)) = true
+fun is_hole_const (Const (\<^const_name>\<open>compute_hole\<close>, _)) = true
   | is_hole_const _ = false
 
 val hole_syntax =
   let
     (* Modified variant of Term.replace_hole *)
-    fun replace_hole Ts (Const (\<^const_name>\<open>rewrite_hole\<close>, T)) i =
+    fun replace_hole Ts (Const (\<^const_name>\<open>compute_hole\<close>, T)) i =
           (list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1)
       | replace_hole Ts (Abs (x, T, t)) i =
           let val (t', i') = replace_hole (T :: Ts) t i
@@ -265,7 +268,7 @@ fun match_pconv cv (t,fixes) ctxt (tyenv, env_ts) ct =
     | SOME (tyenv', _) => to_hole t ctxt (tyenv', env_ts) ct
   end
 
-fun rewrs_pconv to thms ctxt (tyenv, env_ts) =
+fun comps_pconv to thms ctxt (tyenv, env_ts) =
   let
     fun instantiate_normalize_env ctxt env thm =
       let
@@ -301,7 +304,7 @@ fun rewrs_pconv to thms ctxt (tyenv, env_ts) =
     
   in CConv.rewrs_cconv (map_filter (inst_thm ctxt env_ts (to, tyenv)) thms) end
 
-fun rewrite_conv ctxt (pattern, to) thms ct =
+fun compute_conv ctxt (pattern, to) thms ct =
   let
     fun apply_pat At = judgment_pconv
       | apply_pat In = in_pconv
@@ -317,15 +320,15 @@ fun rewrite_conv ctxt (pattern, to) thms ct =
         NONE => th
       | SOME (th', _) => th'
 
-    val rewrite = rewrs_pconv to (maps (prep_meta_eq ctxt) thms)
-  in cv rewrite ctxt (Vartab.empty, []) ct |> distinct_prems end
+    val compute = comps_pconv to (maps (prep_meta_eq ctxt) thms)
+  in cv compute ctxt (Vartab.empty, []) ct |> distinct_prems end
 
-fun rewrite_export_tac ctxt (pat, pat_ctxt) thms =
+fun compute_export_tac ctxt (pat, pat_ctxt) thms =
   let
     val export = case pat_ctxt of
         NONE => I
       | SOME inner => singleton (Proof_Context.export inner ctxt)
-  in CCONVERSION (export o rewrite_conv ctxt pat thms) end
+  in CCONVERSION (export o compute_conv ctxt pat thms) end
 
 val _ =
   Theory.setup
@@ -449,17 +452,17 @@ val _ =
       let val scan = raw_pattern -- to_parser -- Parse.thms1
       in context_lift scan prep_args end
 
-    fun rewrite_export_ctac inputs inthms =
-      CONTEXT_TACTIC' (fn ctxt => rewrite_export_tac ctxt inputs inthms)
+    fun compute_export_ctac inputs inthms =
+      CONTEXT_TACTIC' (fn ctxt => compute_export_tac ctxt inputs inthms)
   in
-    Method.setup \<^binding>\<open>rewr\<close> (subst_parser >>
+    Method.setup \<^binding>\<open>cmp\<close> (subst_parser >>
       (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => SIMPLE_METHOD'
-        (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)))
+        (compute_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)))
       "single-step rewriting, allowing subterm selection via patterns" #>
-    Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >>
+    Method.setup \<^binding>\<open>comp\<close> (subst_parser >>
       (fn (pattern, inthms, (to, pat_ctxt)) => K (CONTEXT_METHOD (
         CHEADGOAL o SIDE_CONDS 0
-          (rewrite_export_ctac ((pattern, to), SOME pat_ctxt) inthms)))))
+          (compute_export_ctac ((pattern, to), SOME pat_ctxt) inthms)))))
       "single-step rewriting with auto-typechecking"
   end
 end
diff --git a/spartan/core/context_facts.ML b/spartan/core/context_facts.ML
index c372ca7..5aa7c70 100644
--- a/spartan/core/context_facts.ML
+++ b/spartan/core/context_facts.ML
@@ -17,6 +17,7 @@ val eq: Proof.context -> thm list
 val eq_of: Proof.context -> term -> thm list
 val register_eq: thm -> Context.generic -> Context.generic
 val register_eqs: thm list -> Context.generic -> Context.generic
+
 val register_facts: thm list -> Proof.context -> Proof.context
 
 end = struct
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 1501221..4beb9b6 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -114,7 +114,7 @@ Lemma head_type [type]:
 Lemma head_of_cons [comp]:
   assumes "A: U i" "x: A" "xs: List A"
   shows "head (x # xs) \<equiv> some x"
-  unfolding head_def by reduce
+  unfolding head_def by compute
 
 Lemma tail_type [type]:
   assumes "A: U i" "xs: List A"
@@ -124,7 +124,7 @@ Lemma tail_type [type]:
 Lemma tail_of_cons [comp]:
   assumes "A: U i" "x: A" "xs: List A"
   shows "tail (x # xs) \<equiv> xs"
-  unfolding tail_def by reduce
+  unfolding tail_def by compute
 
 subsection \<open>Append\<close>
 
@@ -185,7 +185,7 @@ Lemma rev_type [type]:
 Lemma rev_nil [comp]:
   assumes "A: U i"
   shows "rev (nil A) \<equiv> nil A"
-  unfolding rev_def by reduce
+  unfolding rev_def by compute
 
 
 end
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index e06a07b..452acc2 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -40,7 +40,7 @@ Lemma Maybe_comp_none:
   shows "MaybeInd A C c\<^sub>0 f (none A) \<equiv> c\<^sub>0"
   using assms
   unfolding Maybe_def MaybeInd_def none_def some_def
-  by reduce
+  by compute
 
 Lemma Maybe_comp_some:
   assumes
@@ -52,7 +52,7 @@ Lemma Maybe_comp_some:
   shows "MaybeInd A C c\<^sub>0 f (some A a) \<equiv> f a"
   using assms
   unfolding Maybe_def MaybeInd_def none_def some_def
-  by reduce
+  by compute
 
 lemmas
   [form] = MaybeF and
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy
index 0043c1e..56adbfc 100644
--- a/spartan/lib/Prelude.thy
+++ b/spartan/lib/Prelude.thy
@@ -116,7 +116,7 @@ Lemma if_true:
   shows "ifelse C true a b \<equiv> a"
   unfolding ifelse_def true_def
   using assms unfolding Bool_def true_def false_def
-  by reduce
+  by compute
 
 Lemma if_false:
   assumes
@@ -126,7 +126,7 @@ Lemma if_false:
   shows "ifelse C false a b \<equiv> b"
   unfolding ifelse_def false_def
   using assms unfolding Bool_def true_def false_def
-  by reduce
+  by compute
 
 lemmas
   [form] = BoolF and
@@ -145,7 +145,7 @@ translations "if x then a else b" \<leftharpoondown> "CONST ifelse C x a b"
 
 subsection \<open>Logical connectives\<close>
 
-definition not ("!_") where "not x \<equiv> ifelse (K Bool) x false true"
+definition not ("!_") where "!x \<equiv> ifelse (K Bool) x false true"
 
 
 end