From f46df86db9308dde29e0e5f97f54546ea1dc34bf Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 18 Jan 2021 23:49:13 +0000
Subject: Swapped notation for metas (now ?) and holes (now {}), other notation
 and name changes.

---
 spartan/core/Spartan.thy   | 85 ++++++++++++++++++++------------------------
 spartan/core/calc.ML       | 87 ++++++++++++++++++++++++++++++++++++++++++++++
 spartan/core/congruence.ML | 82 -------------------------------------------
 spartan/core/rewrite.ML    |  4 +--
 spartan/lib/List.thy       | 14 ++++----
 spartan/lib/Maybe.thy      |  4 +--
 spartan/lib/Prelude.thy    |  2 +-
 7 files changed, 137 insertions(+), 141 deletions(-)
 create mode 100644 spartan/core/calc.ML
 delete mode 100644 spartan/core/congruence.ML

(limited to 'spartan')

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 6b2ed58..ffe3778 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -9,23 +9,18 @@ keywords
   "Theorem" "Lemma" "Corollary" "Proposition" "Definition" :: thy_goal_stmt and
   "assuming" :: prf_asm % "proof" and
   "focus" "\<^item>" "\<^enum>" "\<circ>" "\<diamondop>" "~" :: prf_script_goal % "proof" and
-  "congruence" "print_coercions" :: thy_decl and
+  "calc" "print_coercions" :: thy_decl and
   "rhs" "def" "vars" :: quasi_command
 
 begin
 
-
-section \<open>Prelude\<close>
-
-paragraph \<open>Set up the meta-logic just so.\<close>
-
-paragraph \<open>Notation.\<close>
+section \<open>Notation\<close>
 
 declare [[eta_contract=false]]
 
 text \<open>
-  Rebind notation for meta-lambdas since we want to use `\<lambda>` for the object
-  lambdas. Meta-functions now use the binder `fn`.
+Rebind notation for meta-lambdas since we want to use \<open>\<lambda>\<close> for the object
+lambdas. Metafunctions now use the binder \<open>fn\<close>.
 \<close>
 setup \<open>
 let
@@ -41,34 +36,31 @@ in
 end
 \<close>
 
-syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3)
+syntax "_app" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3)
 translations "a $ b" \<rightharpoonup> "a (b)"
 
 abbreviation (input) K where "K x \<equiv> fn _. x"
 
-paragraph \<open>
-  Deeply embed dependent type theory: meta-type of expressions, and typing
-  judgment.
+
+section \<open>Metalogic\<close>
+
+text \<open>
+HOAS embedding of dependent type theory: metatype of expressions, and typing
+judgment.
 \<close>
 
 typedecl o
 
 consts has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999)
 
-text \<open>Type annotations for type-checking and inference.\<close>
-
-definition anno :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("'(_ : _')")
-  where "(a : A) \<equiv> a" if "a: A"
-
-lemma anno: "a: A \<Longrightarrow> (a : A): A"
-  by (unfold anno_def)
-
 
 section \<open>Axioms\<close>
 
 subsection \<open>Universes\<close>
 
-typedecl lvl \<comment> \<open>Universe levels\<close>
+text \<open>\<omega>-many cumulative Russell universes.\<close>
+
+typedecl lvl
 
 axiomatization
   O  :: \<open>lvl\<close> and
@@ -81,16 +73,15 @@ axiomatization
 
 axiomatization U :: \<open>lvl \<Rightarrow> o\<close> where
   Ui_in_Uj: "i < j \<Longrightarrow> U i: U j" and
-  in_Uj_if_in_Ui: "A: U i \<Longrightarrow> i < j \<Longrightarrow> A: U j"
+  U_cumul: "A: U i \<Longrightarrow> i < j \<Longrightarrow> A: U j"
 
 lemma Ui_in_USi:
   "U i: U (S i)"
   by (rule Ui_in_Uj, rule lt_S)
 
-lemma in_USi_if_in_Ui:
+lemma U_lift:
   "A: U i \<Longrightarrow> A: U (S i)"
-  by (erule in_Uj_if_in_Ui, rule lt_S)
-
+  by (erule U_cumul, rule lt_S)
 
 subsection \<open>\<Prod>-type\<close>
 
@@ -134,7 +125,6 @@ axiomatization where
 
   lam_cong: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x \<equiv> \<lambda>x: A. c x"
 
-
 subsection \<open>\<Sum>-type\<close>
 
 axiomatization
@@ -207,7 +197,7 @@ lemma sub:
   shows "a: A'"
   using assms by simp
 
-\<comment> \<open>Basic substitution of definitional equalities\<close>
+\<comment> \<open>Basic rewriting of computational equality\<close>
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
@@ -305,7 +295,7 @@ method_setup this =
 
 subsection \<open>Rewriting\<close>
 
-consts rewrite_HOLE :: "'a::{}"  ("\<hole>")
+consts rewrite_hole :: "'a::{}"  ("\<hole>")
 
 lemma eta_expand:
   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
@@ -331,28 +321,28 @@ lemma imp_cong_eq:
 ML_file \<open>~~/src/HOL/Library/cconv.ML\<close>
 ML_file \<open>rewrite.ML\<close>
 
-\<comment> \<open>\<open>reduce\<close> computes terms via judgmental equalities\<close>
+\<comment> \<open>\<open>reduce\<close> simplifies terms via computational equalities\<close>
 method reduce uses add =
   changed \<open>repeat_new \<open>(simp add: comp add | subst comp); typechk?\<close>\<close>
 
 
-subsection \<open>Congruence relations\<close>
+subsection \<open>Calculational reasoning\<close>
 
 consts "rhs" :: \<open>'a\<close> ("..")
 
-ML_file \<open>congruence.ML\<close>
+ML_file \<open>calc.ML\<close>
 
 
 section \<open>Implicits\<close>
 
 text \<open>
-  \<open>?\<close> is used to mark implicit arguments in definitions, while \<open>{}\<close> is expanded
+  \<open>{}\<close> is used to mark implicit arguments in definitions, while \<open>?\<close> is expanded
   immediately for elaboration in statements.
 \<close>
 
 consts
-  iarg :: \<open>'a\<close> ("?")
-  hole :: \<open>'b\<close> ("{}")
+  iarg :: \<open>'a\<close> ("{}")
+  hole :: \<open>'b\<close> ("?")
 
 ML_file \<open>implicits.ML\<close>
 
@@ -363,11 +353,12 @@ ML \<open>val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes
 text \<open>Automatically insert inhabitation judgments where needed:\<close>
 
 syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
-translations "inhabited A" \<rightharpoonup> "CONST has_type {} A"
+translations "inhabited A" \<rightharpoonup> "CONST has_type ? A"
+
 
-text \<open>Implicit lambdas\<close>
+subsection \<open>Implicit lambdas\<close>
 
-definition lam_i where [implicit]: "lam_i f \<equiv> lam ? f"
+definition lam_i where [implicit]: "lam_i f \<equiv> lam {} f"
 
 syntax
   "_lam_i"  :: \<open>idts \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<lambda>_./ _)" 30)
@@ -410,7 +401,7 @@ Lemma refine_codomain:
 Lemma lift_universe_codomain:
   assumes "A: U i" "f: A \<rightarrow> U j"
   shows "f: A \<rightarrow> U (S j)"
-  using in_USi_if_in_Ui[of "f {}"]
+  using U_lift
   by (rule refine_codomain)
 
 subsection \<open>Function composition\<close>
@@ -460,10 +451,10 @@ Lemma funcomp_apply_comp [comp]:
   shows "(g \<circ>\<^bsub>A\<^esub> f) x \<equiv> g (f x)"
   unfolding funcomp_def by reduce
 
-text \<open>Notation:\<close>
+subsection \<open>Notation\<close>
 
 definition funcomp_i (infixr "\<circ>" 120)
-  where [implicit]: "funcomp_i g f \<equiv> g \<circ>\<^bsub>?\<^esub> f"
+  where [implicit]: "funcomp_i g f \<equiv> g \<circ>\<^bsub>{}\<^esub> f"
 
 translations "g \<circ> f" \<leftharpoondown> "g \<circ>\<^bsub>A\<^esub> f"
 
@@ -520,10 +511,10 @@ Lemma snd_comp [comp]:
 subsection \<open>Notation\<close>
 
 definition fst_i ("fst")
-  where [implicit]: "fst \<equiv> Spartan.fst ? ?"
+  where [implicit]: "fst \<equiv> Spartan.fst {} {}"
 
 definition snd_i ("snd")
-  where [implicit]: "snd \<equiv> Spartan.snd ? ?"
+  where [implicit]: "snd \<equiv> Spartan.snd {} {}"
 
 translations
   "fst" \<leftharpoondown> "CONST Spartan.fst A B"
@@ -550,10 +541,10 @@ method snd for p::o = rule snd[where ?p=p]
 
 text \<open>Double projections:\<close>
 
-definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> Spartan.fst ? ? (Spartan.fst ? ? p)"
-definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> Spartan.snd ? ? (Spartan.fst ? ? p)"
-definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> Spartan.fst ? ? (Spartan.snd ? ? p)"
-definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> Spartan.snd ? ? (Spartan.snd ? ? p)"
+definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.fst {} {} p)"
+definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.fst {} {} p)"
+definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.snd {} {} p)"
+definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.snd {} {} p)"
 
 translations
   "CONST p\<^sub>1\<^sub>1 p" \<leftharpoondown> "fst (fst p)"
diff --git a/spartan/core/calc.ML b/spartan/core/calc.ML
new file mode 100644
index 0000000..67dc7fc
--- /dev/null
+++ b/spartan/core/calc.ML
@@ -0,0 +1,87 @@
+structure Calc = struct
+
+(* Calculational type context data
+
+A "calculational" type is a type expressing some congruence relation. In
+particular, it has a notion of composition of terms that is often used to derive
+proofs equationally.
+*)
+
+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
+    RHS.map (Termtab.update (key, (t, idxname)))
+  end
+
+fun lookup_calc ctxt t =
+  Termtab.lookup (RHS.get (Context.Proof ctxt)) (Term.head_of t)
+
+
+(* Declaration *)
+
+local val Frees_to_Vars =
+  map_aterms (fn tm =>
+    case tm of
+      Free (name, T) => Var (("*!"^name, 0), T) (*FIXME: Hacky naming!*)
+    | _ => tm)
+in
+
+(*Declare the "right-hand side" of calculational types. Does not handle bound
+  variables, so no dependent RHS in declarations!*)
+val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>calc\<close>
+  "declare right hand side of calculational type"
+  (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
+
+
+(* Ditto "''" 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_calc 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 calculational type"))
+          | _ => 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/congruence.ML b/spartan/core/congruence.ML
deleted file mode 100644
index d9f4ffa..0000000
--- a/spartan/core/congruence.ML
+++ /dev/null
@@ -1,82 +0,0 @@
-structure Congruence = struct
-
-(* Congruence context data *)
-
-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
-    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/rewrite.ML b/spartan/core/rewrite.ML
index 99c21b5..af70cfc 100644
--- a/spartan/core/rewrite.ML
+++ b/spartan/core/rewrite.ML
@@ -72,13 +72,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>rewrite_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>rewrite_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
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 83e5149..1501221 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -64,10 +64,10 @@ Lemma list_cases [cases]:
 section \<open>Notation\<close>
 
 definition nil_i ("[]")
-  where [implicit]: "[] \<equiv> nil ?"
+  where [implicit]: "[] \<equiv> nil {}"
 
 definition cons_i (infixr "#" 120)
-  where [implicit]: "x # xs \<equiv> cons ? x xs"
+  where [implicit]: "x # xs \<equiv> cons {} x xs"
 
 translations
   "[]" \<leftharpoondown> "CONST List.nil A"
@@ -99,8 +99,8 @@ proof (cases xs)
   show "\<And>xs. xs: List A \<Longrightarrow> xs: List A" .
 qed
 
-definition head_i ("head") where [implicit]: "head xs \<equiv> List.head ? xs"
-definition tail_i ("tail") where [implicit]: "tail xs \<equiv> List.tail ? xs"
+definition head_i ("head") where [implicit]: "head xs \<equiv> List.head {} xs"
+definition tail_i ("tail") where [implicit]: "tail xs \<equiv> List.tail {} xs"
 
 translations
   "head" \<leftharpoondown> "CONST List.head A"
@@ -137,7 +137,7 @@ Definition app:
       proof - show "x # rec: List A" by typechk qed
   done
 
-definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app ? xs ys"
+definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app {} xs ys"
 
 translations "app" \<leftharpoondown> "CONST List.app A"
 
@@ -153,7 +153,7 @@ proof (elim xs)
   show "f x # ys: List B" by typechk
 qed
 
-definition map_i ("map") where [implicit]: "map \<equiv> List.map ? ?"
+definition map_i ("map") where [implicit]: "map \<equiv> List.map {} {}"
 
 translations "map" \<leftharpoondown> "CONST List.map A B"
 
@@ -173,7 +173,7 @@ Definition rev:
     \<^item> vars x _ rec proof - show "app rec [x]: List A" by typechk qed
   done
 
-definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev ?"
+definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev {}"
 
 translations "rev" \<leftharpoondown> "CONST List.rev A"
 
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index da22a4e..e06a07b 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -64,8 +64,8 @@ lemmas
 
 abbreviation "MaybeRec A C \<equiv> MaybeInd A (K C)"
 
-definition none_i ("none") where [implicit]: "none \<equiv> Maybe.none ?"
-definition some_i ("some") where [implicit]: "some a \<equiv> Maybe.some ? a"
+definition none_i ("none") where [implicit]: "none \<equiv> Maybe.none {}"
+definition some_i ("some") where [implicit]: "some a \<equiv> Maybe.some {} a"
 
 translations
   "none" \<leftharpoondown> "CONST Maybe.none A"
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy
index c0abf31..0043c1e 100644
--- a/spartan/lib/Prelude.thy
+++ b/spartan/lib/Prelude.thy
@@ -139,7 +139,7 @@ lemmas
 subsection \<open>Notation\<close>
 
 definition ifelse_i ("if _ then _ else _")
-  where [implicit]: "if x then a else b \<equiv> ifelse ? x a b"
+  where [implicit]: "if x then a else b \<equiv> ifelse {} x a b"
 
 translations "if x then a else b" \<leftharpoondown> "CONST ifelse C x a b"
 
-- 
cgit v1.2.3