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