aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--HoTT_Base.thy53
-rw-r--r--HoTT_Methods.thy5
-rw-r--r--HoTT_Typing.thy (renamed from typing.ML)104
-rw-r--r--util.ML72
4 files changed, 125 insertions, 109 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 1eaed12..9dcf6d0 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,64 +1,21 @@
(********
-Isabelle/HoTT: Foundational definitions and notation
+Isabelle/HoTT: Basic logical definitions and notation
Feb 2019
-This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions.
+This file completes the basic logical and functional setup of the HoTT logic.
Among other things, it:
-* Calls the setup of object-level type inference functionality.
* Defines the universe hierarchy and its governing rules.
* Defines named theorems for later use by proof methods.
********)
theory HoTT_Base
-imports Pure
-keywords "assume_type" "assume_types" :: thy_decl
+imports HoTT_Typing
begin
-section \<open>Terms and typing\<close>
-
-typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
-
-judgment has_type :: "[t, t] \<Rightarrow> prop" ("(3_:/ _)")
-
-section \<open>Setup non-core logic functionality\<close>
-
-declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close>
-
-ML \<open>val trace = Attrib.setup_config_bool @{binding "trace"} (K false)\<close>
- \<comment> \<open>Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on.\<close>
-
-text \<open>Set up type assumption and inference functionality:\<close>
-
-ML_file "util.ML"
-ML_file "typing.ML"
-ML \<open>
-val _ =
- let
- fun store_typing ctxt = Typing.put_declared_typing o (Syntax.read_prop ctxt)
- in
- Outer_Syntax.local_theory
- @{command_keyword "assume_type"}
- "Declare typing assumptions"
- (Parse.prop >>
- (fn prop => fn lthy => Local_Theory.background_theory (store_typing lthy prop) lthy))
- end
-
-val _ =
- let
- val parser = Parse.and_list (Parse.prop)
- fun store_typings ctxt = fold (Typing.put_declared_typing o (Syntax.read_prop ctxt))
- in
- Outer_Syntax.local_theory
- @{command_keyword "assume_types"}
- "Declare typing assumptions"
- (parser >>
- (fn props => fn lthy => Local_Theory.background_theory (store_typings lthy props) lthy))
- end
-\<close>
-
+
section \<open>Universes\<close>
typedecl ord \<comment> \<open>Type of meta-numerals\<close>
@@ -92,6 +49,7 @@ Instead use @{method elim}, or instantiate the rules suitably.
@{thm U_cumulative'} is an alternative rule used by the method @{theory_text cumulativity} in @{file HoTT_Methods.thy}.
\<close>
+
section \<open>Type families\<close>
abbreviation (input) constraint :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop" ("(1_:/ _ \<leadsto> _)")
@@ -99,6 +57,7 @@ where "f: A \<leadsto> B \<equiv> (\<And>x. x: A \<Longrightarrow> f x: B)"
text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type families.\<close>
+
section \<open>Named theorems\<close>
named_theorems form
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 99f3446..088c1fa 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -9,6 +9,7 @@ imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
begin
+
section \<open>Substitution and simplification\<close>
ML_file "~~/src/Tools/misc_legacy.ML"
@@ -25,6 +26,7 @@ Premises of the rule(s) applied are added as new subgoals.
method compute declares comp = (subst comp)
+
section \<open>Handling universes\<close>
text \<open>
@@ -46,6 +48,7 @@ method cumulativity declares form = (
((elim U_cumulative | (rule U_cumulative, rule form)), provelt)
)
+
section \<open>Deriving typing judgments\<close>
method routine uses add = (assumption | rule add | rule)+
@@ -54,6 +57,7 @@ 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}.
\<close>
+
section \<open>Derivation search\<close>
text \<open>
@@ -63,6 +67,7 @@ It also handles universes using @{method hierarchy} and @{method cumulativity}.
method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
+
section \<open>Induction\<close>
text \<open>
diff --git a/typing.ML b/HoTT_Typing.thy
index 8c3d42c..6433139 100644
--- a/typing.ML
+++ b/HoTT_Typing.thy
@@ -1,11 +1,40 @@
(********
-Isabelle/HoTT: typing.ML
+Isabelle/HoTT: Core typing judgment form and associated automation
Feb 2019
-Functionality for object-level type inference.
+This file is the starting point of the definition of Isabelle/HoTT.
+It declares the fundamental typing judgment form and sets up various
+ML functionality to automate type inference.
********)
+theory HoTT_Typing
+imports Pure
+keywords "assume_type" "assume_types" :: thy_decl
+
+begin
+
+
+section \<open>Initial settings\<close>
+
+declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close>
+
+ML \<open>val trace = Attrib.setup_config_bool @{binding "trace"} (K false)\<close>
+ \<comment> \<open>Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on.\<close>
+
+
+section \<open>Terms and typing\<close>
+
+typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
+
+judgment has_type :: "[t, t] \<Rightarrow> prop" ("(3_:/ _)")
+
+
+section \<open>Typing functionality\<close>
+
+ML_file "util.ML"
+
+ML \<open>
signature TYPING =
sig
type jmt = term
@@ -18,10 +47,11 @@ sig
val typing_all: Proof.context -> jmt list
val get_typing_in: term -> jmt list -> term option
+
val get_local_typing: Proof.context -> term -> term option
- val get_declared_typing: theory -> term -> term option
- val put_declared_typing: term -> theory -> theory
+ val put_theory_typing: term -> theory -> theory
+ val get_theory_typing: theory -> term -> term option
val get_typing: Proof.context -> term -> term option
end
@@ -32,23 +62,23 @@ struct
type jmt = term
(* Determine if a term is a typing judgment *)
-fun is_typing_jmt (@{const HoTT_Base.has_type} $ _ $ _) = true
+fun is_typing_jmt (@{const has_type} $ _ $ _) = true
| is_typing_jmt _ = false
(* Functions to extract a and A from propositions "a: A" *)
-fun term_of_jmt (@{const HoTT_Base.has_type} $ t $ _) = t
+fun term_of_jmt (@{const has_type} $ t $ _) = t
| term_of_jmt _ = Exn.error "Not a typing judgment"
-fun type_of_jmt (@{const HoTT_Base.has_type} $ _ $ T) = T
+fun type_of_jmt (@{const has_type} $ _ $ T) = T
| type_of_jmt _ = Exn.error "Not a typing judgment"
(* Get typing assumptions in "this" *)
fun typing_this ctxt = Util.get_this ctxt |> map Thm.prop_of |> filter is_typing_jmt
-(* Get the typing assumptions in the current context *)
+(* Get the typing assumptions in the current proof context *)
val typing_assms = Util.get_assms #> map Thm.prop_of #> filter is_typing_jmt
-(* Get all visible typing judgments—Quick hack for now; should record them separately *)
+(* Search the context and return all visible typing judgments *)
fun typing_all ctxt =
Util.get_all_thms ctxt |> map (Thm.prop_of o snd) |> filter is_typing_jmt
@@ -84,36 +114,56 @@ fun get_local_typing ctxt tm =
NONE => get_typing_in tm (typing_assms ctxt)
| res => res
-(* Storage space for declared typings *)
-structure Declared_Typings = Theory_Data
+(* Dedicated theory data for proven typing judgments *)
+structure Theory_Typings = Theory_Data
(
type T = term Symtab.table
val empty = Symtab.empty
val extend = I
- val merge = K Symtab.empty
-)
+ val merge = Symtab.join (fn key => fn (x, y) => y)
+)
(* Accessor for the above data *)
-fun get_declared_typing thy tm =
- case tm of
- (Free (v, _)) => Symtab.lookup (Declared_Typings.get thy) v
- | _ => NONE
-
-(* Store new typing information for free variables only
- (constants should have their types declared at the moment of definition).
- End users should use the "typing" keyword instead.
-*)
-fun put_declared_typing jmt =
+fun get_theory_typing thy tm =
+ Symtab.lookup (Theory_Typings.get thy) (Util.string_of_term tm)
+
+fun put_theory_typing jmt =
case jmt of
Const("HoTT_Base.has_type", _) $ term $ typing =>
- (case term of
- Free (v, _) => Declared_Typings.map (Symtab.update (v, typing))
- | _ => Exn.error "Cannot declare typing assumption (not a free variable)")
+ Theory_Typings.map (Symtab.update (Util.string_of_term term, typing))
| _ => Exn.error "Not a typing judgment"
(* Get the typing of a term *)
fun get_typing ctxt tm =
case get_local_typing ctxt tm of
- NONE => get_declared_typing (Proof_Context.theory_of ctxt) tm
+ NONE => get_theory_typing (Proof_Context.theory_of ctxt) tm
| res => res
end
+\<close>
+
+ML \<open>
+val _ =
+ let
+ fun store_typing ctxt = Typing.put_theory_typing o (Syntax.read_prop ctxt)
+ in
+ Outer_Syntax.local_theory
+ @{command_keyword "assume_type"}
+ "Declare typing assumptions"
+ (Parse.prop >>
+ (fn prop => fn lthy => Local_Theory.background_theory (store_typing lthy prop) lthy))
+ end
+
+val _ =
+ let
+ val parser = Parse.and_list (Parse.prop)
+ fun store_typings ctxt = fold (Typing.put_theory_typing o (Syntax.read_prop ctxt))
+ in
+ Outer_Syntax.local_theory
+ @{command_keyword "assume_types"}
+ "Declare typing assumptions"
+ (parser >>
+ (fn props => fn lthy => Local_Theory.background_theory (store_typings lthy props) lthy))
+ end
+\<close>
+
+end
diff --git a/util.ML b/util.ML
index c2e962b..f7aab9a 100644
--- a/util.ML
+++ b/util.ML
@@ -28,6 +28,7 @@ end
structure Util: UTIL =
struct
+(* Unmark a name string identifier *)
fun unmark s =
Lexicon.unmark_class s
handle Fail "unprefix" =>
@@ -39,40 +40,6 @@ fun unmark s =
handle Fail "unprefix" =>
s
-fun name_and_thm (fact, thm) =
- ((case fact of
- Facts.Named ((name, _), _) => name
- | Facts.Fact name => name),
- thm)
-
-fun get_all_thms ctxt =
- let val (_, ref_thms) = Find_Theorems.find_theorems ctxt NONE NONE true []
- in ref_thms |> (map name_and_thm)
- end
-
-(* Search all visible theorems (including local assumptions) containing a given name *)
-fun find_thm ctxt name =
- let val (_, ref_thms) =
- Find_Theorems.find_theorems ctxt NONE NONE true [(true, Find_Theorems.Name name)]
- in
- ref_thms |> (map name_and_thm)
- end
-
-(* Get the fact corresponding to the Isar term "this" in the current proof scope *)
-fun get_this ctxt =
- Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN)
- |> Proof_Context.lookup_fact ctxt |> the |> #thms
- handle Option.Option => (
- if (Config.get ctxt trace) then warning "\"this\" undefined in the context" else ();
- []
- )
-
-(* Get all visible assumptions in the current proof scope.
- This includes the facts introduced in the statement of the goal using "assumes",
- as well as all facts introduced using "assume" that are visible in the current block.
- *)
-val get_assms = Assumption.all_prems_of
-
(* Prepare a Pure pre-term, converting it to a (unchecked) term *)
fun prep_term ctxt ptm =
let val ptm = Term_Position.strip_positions ptm
@@ -119,4 +86,39 @@ fun string_of_term tm =
| Abs (_, typ, body) => "Abs (_, " ^ string_of_typ typ ^ ", " ^ string_of_term body ^ ")"
| t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")"
-end \ No newline at end of file
+fun name_and_thm (fact, thm) =
+ ((case fact of
+ Facts.Named ((name, _), _) => name
+ | Facts.Fact name => name),
+ thm)
+
+(* Return all visible theorems *)
+fun get_all_thms ctxt =
+ let val (_, ref_thms) = Find_Theorems.find_theorems ctxt NONE NONE true []
+ in ref_thms |> (map name_and_thm)
+ end
+
+(* Search all visible theorems (including local assumptions) containing a given name *)
+fun find_thm ctxt name =
+ let val (_, ref_thms) =
+ Find_Theorems.find_theorems ctxt NONE NONE true [(true, Find_Theorems.Name name)]
+ in
+ ref_thms |> (map name_and_thm)
+ end
+
+(* Get the fact corresponding to the Isar term "this" in the current proof scope *)
+fun get_this ctxt =
+ Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN)
+ |> Proof_Context.lookup_fact ctxt |> the |> #thms
+ handle Option.Option => (
+ if (Config.get ctxt trace) then warning "\"this\" undefined in the context" else ();
+ []
+ )
+
+(* Get all visible assumptions in the current proof scope.
+ This includes the facts introduced in the statement of the goal using "assumes",
+ as well as all facts introduced using "assume" that are visible in the current block.
+ *)
+val get_assms = Assumption.all_prems_of
+
+end