Bad practice huge commit:

1. Rudimentary prototype definitional package
2. Started univalence
3. Various compatibility fixes and new theory stubs
4. Updated ROOT file

6 files changed, 101 insertions, 67 deletions

diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy
index 5888a90..29c7248 100644
--- a/mltt/core/MLTT.thy
+++ b/mltt/core/MLTT.thy
@@ -220,6 +220,27 @@ in
 end
 \<close>
 
+section \<open>Implicits\<close>
+
+text \<open>
+  \<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> ("?")
+
+ML_file \<open>implicits.ML\<close>
+
+attribute_setup implicit = \<open>Scan.succeed Implicits.implicit_defs_attr\<close>
+
+ML \<open>val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes)\<close>
+
+text \<open>Automatically insert inhabitation judgments where needed:\<close>
+syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
+translations "inhabited A" \<rightharpoonup> "CONST has_type ? A"
+
 
 section \<open>Statements and goals\<close>
 
@@ -228,6 +249,10 @@ ML_file \<open>elaboration.ML\<close>
 ML_file \<open>elaborated_statement.ML\<close>
 ML_file \<open>goals.ML\<close>
 
+text \<open>Syntax for definition bodies.\<close>
+syntax defn :: \<open>o \<Rightarrow> prop\<close> ("(:=_)")
+translations "defn t" \<rightharpoonup> "CONST has_type t ?"
+
 
 section \<open>Proof methods\<close>
 
@@ -328,29 +353,6 @@ consts "rhs" :: \<open>'a\<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
-  immediately for elaboration in statements.
-\<close>
-
-consts
-  iarg :: \<open>'a\<close> ("{}")
-  hole :: \<open>'b\<close> ("?")
-
-ML_file \<open>implicits.ML\<close>
-
-attribute_setup implicit = \<open>Scan.succeed Implicits.implicit_defs_attr\<close>
-
-ML \<open>val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes)\<close>
-
-text \<open>Automatically insert inhabitation judgments where needed:\<close>
-
-syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
-translations "inhabited A" \<rightharpoonup> "CONST has_type ? A"
-
-
 subsection \<open>Implicit lambdas\<close>
 
 definition lam_i where [implicit]: "lam_i f \<equiv> lam {} f"
diff --git a/mltt/core/goals.ML b/mltt/core/goals.ML
index d69c800..4d03133 100644
--- a/mltt/core/goals.ML
+++ b/mltt/core/goals.ML
@@ -28,6 +28,15 @@ val short_statement =
       [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)
     )
 
+val where_statement = Scan.optional (Parse.$$$ "where" |-- Parse.!!! Parse_Spec.statement) []
+
+val def_statement =
+  Parse_Spec.statement -- where_statement >>
+    (fn (shows, assumes) =>
+      (false, Binding.empty_atts, [],
+      [Element.Fixes [], Element.Assumes assumes], Element.Shows shows)
+    )
+
 fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
   let
     val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt
@@ -58,56 +67,60 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
         end
   end
 
+fun make_name_binding name suffix local_name =
+  let val base_local_name = Long_Name.base_name local_name
+  in Binding.qualified_name
+    ((case base_local_name of "" => name | _ => base_local_name) ^
+     (case suffix
+      of SOME s => "_" ^ s
+      | NONE => ""))
+  end
+
 fun define_proof_term name (local_name, [th]) lthy =
       let
-        fun make_name_binding suffix local_name =
-          let val base_local_name = Long_Name.base_name local_name
-          in Binding.qualified_name
-            ((case base_local_name of "" => name | _ => base_local_name) ^
-             (case suffix
-              of SOME "prf" => "_prf"
-              | SOME "def" => "_def"
-              | _ => ""))
-          end
-
         val (prems, concl) =
           (Logic.strip_assums_hyp (Thm.prop_of th),
            Logic.strip_assums_concl (Thm.prop_of th))
       in
         if not (Lib.is_typing concl) then ([], lthy)
         else let
-          val prems_vars = distinct Term.aconv (flat
-            (map (Lib.collect_subterms is_Var) prems))
+          val prems_vars = distinct Term.aconv (
+            flat (map (Lib.collect_subterms is_Var) prems))
 
-          val concl_vars = Lib.collect_subterms is_Var
-            (Lib.term_of_typing concl)
+          val concl_vars = distinct Term.aconv (
+            Lib.collect_subterms is_Var (Lib.term_of_typing concl))
 
           val params = sort (uncurry Lib.lvl_order) (inter Term.aconv concl_vars prems_vars)
 
           val prf_tm = fold_rev lambda params (Lib.term_of_typing concl)
 
+          val levels = filter Lib.is_lvl (distinct Term.aconv (
+            Lib.collect_subterms is_Var prf_tm))
+
+          val prf_tm' = fold_rev lambda levels prf_tm
+
           val ((_, (_, raw_def)), lthy') = Local_Theory.define
-            ((make_name_binding NONE local_name, Mixfix.NoSyn),
-            ((make_name_binding (SOME "prf") local_name, []), prf_tm)) lthy
+            ((make_name_binding name NONE local_name, Mixfix.NoSyn),
+            ((make_name_binding name (SOME "prf") local_name, []), prf_tm')) lthy
 
           val def = fold
             (fn th1 => fn th2 => Thm.combination th2 th1)
-            (map (Thm.reflexive o Thm.cterm_of lthy) params)
+            (map (Thm.reflexive o Thm.cterm_of lthy) (params @ levels))
             raw_def
 
           val ((_, def'), lthy'') = Local_Theory.note
-            ((make_name_binding (SOME "def") local_name, []), [def])
+            ((make_name_binding name (SOME "def") local_name, []), [def])
             lthy'
         in
           (def', lthy'')
         end
       end
   | define_proof_term _ _ _ = error
-      ("Unimplemented: proof terms for multiple facts in one statement")
+      ("Can't generate proof terms for multiple facts in one statement")
 
 fun gen_schematic_theorem
   bundle_includes prep_att prep_stmt
-  gen_prf_tm long kind
+  gen_prf_tm long kind defn
   before_qed after_qed
   (name, raw_atts) raw_includes raw_elems raw_concl
   do_print lthy
@@ -137,7 +150,7 @@ fun gen_schematic_theorem
               lthy,
             true)
 
-        val (res', lthy'') =
+        val ((name_def, defs), (res', lthy'')) =
           if gen_prf_tm
           then
             let
@@ -147,28 +160,46 @@ fun gen_schematic_theorem
                     (define_proof_term (Binding.name_of name) result lthy))
                 res
                 ([], lthy')
+
               val res_folded =
                 map (apsnd (map (Local_Defs.fold new_lthy prf_tm_defs))) res
+
+              val name_def =
+                make_name_binding (Binding.name_of name) (SOME "def") (#1 (hd res_folded))
+
+              val name_type =
+                if defn then
+                  make_name_binding (Binding.name_of name) (SOME "type") (#1 (hd res_folded))
+                else name
             in
+              ((name_def, prf_tm_defs),
               Local_Theory.notes_kind kind
-                [((name, @{attributes [type]} @ atts),
+                [((name_type, @{attributes [type]} @ atts),
                   [(maps #2 res_folded, [])])]
-                new_lthy
+                new_lthy)
             end
           else
+            ((Binding.empty, []),
             Local_Theory.notes_kind kind
               [((name, atts), [(maps #2 res, [])])]
-              lthy'
-
-        val _ = Proof_Display.print_results do_print pos lthy''
-            ((kind, Binding.name_of name), map (fn (_, ths) => ("", ths)) res')
+              lthy')
 
+        (*Display theorems*)
         val _ =
-          if substmts then map
-            (fn (name, ths) => Proof_Display.print_results do_print pos lthy''
-              (("and", name), [("", ths)]))
-            res
-          else []
+          if defn then
+            single (Proof_Display.print_results do_print pos lthy''
+              ((kind, Binding.name_of name_def), [("", defs)]))
+          else
+            (if long then
+              Proof_Display.print_results do_print pos lthy''
+                ((kind, Binding.name_of name), map (fn (_, ths) => ("", ths)) res')
+            else ();
+            if substmts then
+              map (fn (name, ths) =>
+                    Proof_Display.print_results do_print pos lthy''
+                      ((kind, name), [("", ths)]))
+                  res
+            else [])
       in
         after_qed results' lthy''
       end
@@ -194,14 +225,14 @@ fun theorem spec descr =
         (fn (opt_derive, (long, binding, includes, elems, concl)) =>
           schematic_theorem_cmd
             (case opt_derive of SOME "def" => true | _ => false)
-            long descr NONE (K I) binding includes elems concl))
+            long descr false NONE (K I) binding includes elems concl))
 
 fun definition spec descr =
   Outer_Syntax.local_theory_to_proof' spec "definition with explicit type checking obligation"
-    ((long_statement || short_statement) >>
+    (def_statement >>
       (fn (long, binding, includes, elems, concl) =>
         schematic_theorem_cmd
-          true long descr NONE (K I) binding includes elems concl))
+          true long descr true NONE (K I) binding includes elems concl))
 
 in
 
diff --git a/mltt/core/lib.ML b/mltt/core/lib.ML
index f15daf6..98d83cc 100644
--- a/mltt/core/lib.ML
+++ b/mltt/core/lib.ML
@@ -14,6 +14,7 @@ val dest_eq: term -> term * term
 val mk_Var: string -> int -> typ -> term
 val lambda_var: term -> term -> term
 
+val is_lvl: term -> bool
 val is_typing: term -> bool
 val mk_typing: term -> term -> term
 val dest_typing: term -> term * term
@@ -83,6 +84,8 @@ fun lambda_var x tm =
 
 (* Object *)
 
+fun is_lvl t = case fastype_of t of Type (\<^type_name>\<open>lvl\<close>, _) => true | _ => false
+
 fun is_typing (Const (\<^const_name>\<open>has_type\<close>, _) $ _ $ _) = true
   | is_typing _ = false
 
@@ -189,7 +192,6 @@ fun subterm_order t1 t2 =
   else EQUAL
 
 fun lvl_order t1 t2 =
-  let val _ = @{print} (fastype_of t1) in
   case fastype_of t1 of
     Type (\<^type_name>\<open>lvl\<close>, _) => (case fastype_of t2 of
                           Type (\<^type_name>\<open>lvl\<close>, _) => EQUAL
@@ -199,7 +201,6 @@ fun lvl_order t1 t2 =
                           Type (\<^type_name>\<open>lvl\<close>, _) => GREATER
                         | _ => EQUAL)
   | _ => EQUAL
-  end
 
 fun cond_order o1 o2 = case o1 of EQUAL => o2 | _ => o1
 
diff --git a/mltt/lib/List.thy b/mltt/lib/List.thy
index 4beb9b6..0cd43c8 100644
--- a/mltt/lib/List.thy
+++ b/mltt/lib/List.thy
@@ -83,7 +83,7 @@ section \<open>Standard functions\<close>
 
 subsection \<open>Head and tail\<close>
 
-Definition head:
+Lemma (def) head:
   assumes "A: U i" "xs: List A"
   shows "Maybe A"
 proof (cases xs)
@@ -91,7 +91,7 @@ proof (cases xs)
   show "\<And>x. x: A \<Longrightarrow> some x: Maybe A" by intro
 qed
 
-Definition tail:
+Lemma (def) tail:
   assumes "A: U i" "xs: List A"
   shows "List A"
 proof (cases xs)
@@ -128,7 +128,7 @@ Lemma tail_of_cons [comp]:
 
 subsection \<open>Append\<close>
 
-Definition app:
+Lemma (def) app:
   assumes "A: U i" "xs: List A" "ys: List A"
   shows "List A"
   apply (elim xs)
@@ -143,7 +143,7 @@ translations "app" \<leftharpoondown> "CONST List.app A"
 
 subsection \<open>Map\<close>
 
-Definition map:
+Lemma (def) map:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
   shows "List B"
 proof (elim xs)
@@ -165,7 +165,7 @@ Lemma map_type [type]:
 
 subsection \<open>Reverse\<close>
 
-Definition rev:
+Lemma (def) rev:
   assumes "A: U i" "xs: List A"
   shows "List A"
   apply (elim xs)
diff --git a/mltt/lib/Maybe.thy b/mltt/lib/Maybe.thy
index 452acc2..257bc8f 100644
--- a/mltt/lib/Maybe.thy
+++ b/mltt/lib/Maybe.thy
@@ -17,7 +17,7 @@ lemma
   Maybe_some: "a: A \<Longrightarrow> some A a: Maybe A"
   unfolding Maybe_def none_def some_def by typechk+
 
-Definition MaybeInd:
+Lemma (def) MaybeInd:
   assumes
     "A: U i"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
diff --git a/mltt/lib/Prelude.thy b/mltt/lib/Prelude.thy
index 0393968..86165cd 100644
--- a/mltt/lib/Prelude.thy
+++ b/mltt/lib/Prelude.thy
@@ -100,7 +100,7 @@ Lemma
   unfolding Bool_def true_def false_def by typechk+
 
 \<comment> \<open>Definitions like these should be handled by a future function package\<close>
-Definition ifelse [rotated 1]:
+Lemma (def) ifelse [rotated 1]:
   assumes *[unfolded Bool_def true_def false_def]:
     "\<And>x. x: Bool \<Longrightarrow> C x: U i"
     "x: Bool"