aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
Diffstat (limited to 'spartan')
-rw-r--r--spartan/core/Spartan.thy26
-rw-r--r--spartan/core/comp.ML (renamed from spartan/core/rewrite.ML)51
-rw-r--r--spartan/core/context_facts.ML1
-rw-r--r--spartan/lib/List.thy6
-rw-r--r--spartan/lib/Maybe.thy4
-rw-r--r--spartan/lib/Prelude.thy6
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 11:47:57 +0000