aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
Diffstat (limited to 'spartan')
-rw-r--r--spartan/lib/congruence.ML16
-rw-r--r--spartan/lib/elimination.ML33
-rw-r--r--spartan/lib/eqsubst.ML434
-rw-r--r--spartan/lib/equality.ML90
-rw-r--r--spartan/lib/focus.ML125
-rw-r--r--spartan/lib/goals.ML214
-rw-r--r--spartan/lib/implicits.ML78
-rw-r--r--spartan/lib/lib.ML143
-rw-r--r--spartan/lib/rewrite.ML465
-rw-r--r--spartan/lib/tactics.ML143
-rw-r--r--spartan/theories/Equivalence.thy431
-rw-r--r--spartan/theories/Identity.thy433
-rw-r--r--spartan/theories/Spartan.thy463
13 files changed, 3068 insertions, 0 deletions
diff --git a/spartan/lib/congruence.ML b/spartan/lib/congruence.ML
new file mode 100644
index 0000000..bb7348c
--- /dev/null
+++ b/spartan/lib/congruence.ML
@@ -0,0 +1,16 @@
+signature Sym_Attr_Data =
+sig
+ val name: string
+ val symmetry_rule: thm
+end
+
+functor Sym_Attr (D: Sym_Attr_Data) =
+struct
+ local
+ val distinct_prems = the_single o Seq.list_of o Tactic.distinct_subgoals_tac
+ in
+ val attr = Thm.rule_attribute []
+ (K (fn th => distinct_prems (th RS D.symmetry_rule) handle THM _ => th))
+ val setup = Attrib.setup (Binding.name D.name) (Scan.succeed attr) ""
+ end
+end
diff --git a/spartan/lib/elimination.ML b/spartan/lib/elimination.ML
new file mode 100644
index 0000000..85ce669
--- /dev/null
+++ b/spartan/lib/elimination.ML
@@ -0,0 +1,33 @@
+(* Title: elimination.ML
+ Author: Joshua Chen
+
+Type elimination automation.
+*)
+
+structure Elim = struct
+
+(* Elimination rule data *)
+structure Rules = Generic_Data (
+ type T = thm Termtab.table
+ val empty = Termtab.empty
+ val extend = I
+ val merge = Termtab.merge Thm.eq_thm_prop
+)
+
+fun register_rule rl =
+ let val hd = Term.head_of (Lib.type_of_typing (Thm.major_prem_of rl))
+ in Rules.map (Termtab.update (hd, rl)) end
+
+fun get_rule ctxt = Termtab.lookup (Rules.get (Context.Proof ctxt))
+
+fun rules ctxt = map (op #2) (Termtab.dest (Rules.get (Context.Proof ctxt)))
+
+(* Set up [elims] attribute *)
+val _ = Theory.setup (
+ Attrib.setup \<^binding>\<open>elims\<close>
+ (Scan.lift (Scan.succeed (Thm.declaration_attribute register_rule))) ""
+ #> Global_Theory.add_thms_dynamic (\<^binding>\<open>elims\<close>,
+ fn context => (rules (Context.proof_of context)))
+)
+
+end
diff --git a/spartan/lib/eqsubst.ML b/spartan/lib/eqsubst.ML
new file mode 100644
index 0000000..ea6f098
--- /dev/null
+++ b/spartan/lib/eqsubst.ML
@@ -0,0 +1,434 @@
+(* Title: eqsubst.ML
+ Author: Lucas Dixon, University of Edinburgh
+ Modified: Joshua Chen, University of Innsbruck
+
+Perform a substitution using an equation.
+
+This code is slightly modified from the original at Tools/eqsubst..ML,
+to incorporate auto-typechecking for type theory.
+*)
+
+signature EQSUBST =
+sig
+ type match =
+ ((indexname * (sort * typ)) list (* type instantiations *)
+ * (indexname * (typ * term)) list) (* term instantiations *)
+ * (string * typ) list (* fake named type abs env *)
+ * (string * typ) list (* type abs env *)
+ * term (* outer term *)
+
+ type searchinfo =
+ Proof.context
+ * int (* maxidx *)
+ * Zipper.T (* focusterm to search under *)
+
+ datatype 'a skipseq = SkipMore of int | SkipSeq of 'a Seq.seq Seq.seq
+
+ val skip_first_asm_occs_search: ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> int -> 'b -> 'c skipseq
+ val skip_first_occs_search: int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
+ val skipto_skipseq: int -> 'a Seq.seq Seq.seq -> 'a skipseq
+
+ (* tactics *)
+ val eqsubst_asm_tac: Proof.context -> int list -> thm list -> int -> tactic
+ val eqsubst_asm_tac': Proof.context ->
+ (searchinfo -> int -> term -> match skipseq) -> int -> thm -> int -> tactic
+ val eqsubst_tac: Proof.context ->
+ int list -> (* list of occurrences to rewrite, use [0] for any *)
+ thm list -> int -> tactic
+ val eqsubst_tac': Proof.context ->
+ (searchinfo -> term -> match Seq.seq) (* search function *)
+ -> thm (* equation theorem to rewrite with *)
+ -> int (* subgoal number in goal theorem *)
+ -> thm (* goal theorem *)
+ -> thm Seq.seq (* rewritten goal theorem *)
+
+ (* search for substitutions *)
+ val valid_match_start: Zipper.T -> bool
+ val search_lr_all: Zipper.T -> Zipper.T Seq.seq
+ val search_lr_valid: (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
+ val searchf_lr_unify_all: searchinfo -> term -> match Seq.seq Seq.seq
+ val searchf_lr_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
+ val searchf_bt_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
+end;
+
+structure EqSubst: EQSUBST =
+struct
+
+(* changes object "=" to meta "==" which prepares a given rewrite rule *)
+fun prep_meta_eq ctxt =
+ Simplifier.mksimps ctxt #> map Drule.zero_var_indexes;
+
+(* make free vars into schematic vars with index zero *)
+fun unfix_frees frees =
+ fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
+
+
+type match =
+ ((indexname * (sort * typ)) list (* type instantiations *)
+ * (indexname * (typ * term)) list) (* term instantiations *)
+ * (string * typ) list (* fake named type abs env *)
+ * (string * typ) list (* type abs env *)
+ * term; (* outer term *)
+
+type searchinfo =
+ Proof.context
+ * int (* maxidx *)
+ * Zipper.T; (* focusterm to search under *)
+
+
+(* skipping non-empty sub-sequences but when we reach the end
+ of the seq, remembering how much we have left to skip. *)
+datatype 'a skipseq =
+ SkipMore of int |
+ SkipSeq of 'a Seq.seq Seq.seq;
+
+(* given a seqseq, skip the first m non-empty seq's, note deficit *)
+fun skipto_skipseq m s =
+ let
+ fun skip_occs n sq =
+ (case Seq.pull sq of
+ NONE => SkipMore n
+ | SOME (h, t) =>
+ (case Seq.pull h of
+ NONE => skip_occs n t
+ | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) else skip_occs (n - 1) t))
+ in skip_occs m s end;
+
+(* note: outerterm is the taget with the match replaced by a bound
+ variable : ie: "P lhs" beocmes "%x. P x"
+ insts is the types of instantiations of vars in lhs
+ and typinsts is the type instantiations of types in the lhs
+ Note: Final rule is the rule lifted into the ontext of the
+ taget thm. *)
+fun mk_foo_match mkuptermfunc Ts t =
+ let
+ val ty = Term.type_of t
+ val bigtype = rev (map snd Ts) ---> ty
+ fun mk_foo 0 t = t
+ | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
+ val num_of_bnds = length Ts
+ (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
+ val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
+ in Abs ("fooabs", bigtype, mkuptermfunc foo_term) end;
+
+(* T is outer bound vars, n is number of locally bound vars *)
+(* THINK: is order of Ts correct...? or reversed? *)
+fun mk_fake_bound_name n = ":b_" ^ n;
+fun fakefree_badbounds Ts t =
+ let val (FakeTs, Ts, newnames) =
+ fold_rev (fn (n, ty) => fn (FakeTs, Ts, usednames) =>
+ let
+ val newname = singleton (Name.variant_list usednames) n
+ in
+ ((mk_fake_bound_name newname, ty) :: FakeTs,
+ (newname, ty) :: Ts,
+ newname :: usednames)
+ end) Ts ([], [], [])
+ in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
+
+(* before matching we need to fake the bound vars that are missing an
+ abstraction. In this function we additionally construct the
+ abstraction environment, and an outer context term (with the focus
+ abstracted out) for use in rewriting with RW_Inst.rw *)
+fun prep_zipper_match z =
+ let
+ val t = Zipper.trm z
+ val c = Zipper.ctxt z
+ val Ts = Zipper.C.nty_ctxt c
+ val (FakeTs', Ts', t') = fakefree_badbounds Ts t
+ val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
+ in
+ (t', (FakeTs', Ts', absterm))
+ end;
+
+(* Unification with exception handled *)
+(* given context, max var index, pat, tgt; returns Seq of instantiations *)
+fun clean_unify ctxt ix (a as (pat, tgt)) =
+ let
+ (* type info will be re-derived, maybe this can be cached
+ for efficiency? *)
+ val pat_ty = Term.type_of pat;
+ val tgt_ty = Term.type_of tgt;
+ (* FIXME is it OK to ignore the type instantiation info?
+ or should I be using it? *)
+ val typs_unify =
+ SOME (Sign.typ_unify (Proof_Context.theory_of ctxt) (pat_ty, tgt_ty) (Vartab.empty, ix))
+ handle Type.TUNIFY => NONE;
+ in
+ (case typs_unify of
+ SOME (typinsttab, ix2) =>
+ let
+ (* FIXME is it right to throw away the flexes?
+ or should I be using them somehow? *)
+ fun mk_insts env =
+ (Vartab.dest (Envir.type_env env),
+ Vartab.dest (Envir.term_env env));
+ val initenv =
+ Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
+ val useq = Unify.smash_unifiers (Context.Proof ctxt) [a] initenv
+ handle ListPair.UnequalLengths => Seq.empty
+ | Term.TERM _ => Seq.empty;
+ fun clean_unify' useq () =
+ (case (Seq.pull useq) of
+ NONE => NONE
+ | SOME (h, t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
+ handle ListPair.UnequalLengths => NONE
+ | Term.TERM _ => NONE;
+ in
+ (Seq.make (clean_unify' useq))
+ end
+ | NONE => Seq.empty)
+ end;
+
+(* Unification for zippers *)
+(* Note: Ts is a modified version of the original names of the outer
+ bound variables. New names have been introduced to make sure they are
+ unique w.r.t all names in the term and each other. usednames' is
+ oldnames + new names. *)
+fun clean_unify_z ctxt maxidx pat z =
+ let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in
+ Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
+ (clean_unify ctxt maxidx (t, pat))
+ end;
+
+
+fun bot_left_leaf_of (l $ _) = bot_left_leaf_of l
+ | bot_left_leaf_of (Abs (_, _, t)) = bot_left_leaf_of t
+ | bot_left_leaf_of x = x;
+
+(* Avoid considering replacing terms which have a var at the head as
+ they always succeed trivially, and uninterestingly. *)
+fun valid_match_start z =
+ (case bot_left_leaf_of (Zipper.trm z) of
+ Var _ => false
+ | _ => true);
+
+(* search from top, left to right, then down *)
+val search_lr_all = ZipperSearch.all_bl_ur;
+
+(* search from top, left to right, then down *)
+fun search_lr_valid validf =
+ let
+ fun sf_valid_td_lr z =
+ let val here = if validf z then [Zipper.Here z] else [] in
+ (case Zipper.trm z of
+ _ $ _ =>
+ [Zipper.LookIn (Zipper.move_down_left z)] @ here @
+ [Zipper.LookIn (Zipper.move_down_right z)]
+ | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
+ | _ => here)
+ end;
+ in Zipper.lzy_search sf_valid_td_lr end;
+
+(* search from bottom to top, left to right *)
+fun search_bt_valid validf =
+ let
+ fun sf_valid_td_lr z =
+ let val here = if validf z then [Zipper.Here z] else [] in
+ (case Zipper.trm z of
+ _ $ _ =>
+ [Zipper.LookIn (Zipper.move_down_left z),
+ Zipper.LookIn (Zipper.move_down_right z)] @ here
+ | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
+ | _ => here)
+ end;
+ in Zipper.lzy_search sf_valid_td_lr end;
+
+fun searchf_unify_gen f (ctxt, maxidx, z) lhs =
+ Seq.map (clean_unify_z ctxt maxidx lhs) (Zipper.limit_apply f z);
+
+(* search all unifications *)
+val searchf_lr_unify_all = searchf_unify_gen search_lr_all;
+
+(* search only for 'valid' unifiers (non abs subterms and non vars) *)
+val searchf_lr_unify_valid = searchf_unify_gen (search_lr_valid valid_match_start);
+
+val searchf_bt_unify_valid = searchf_unify_gen (search_bt_valid valid_match_start);
+
+(* apply a substitution in the conclusion of the theorem *)
+(* cfvs are certified free var placeholders for goal params *)
+(* conclthm is a theorem of for just the conclusion *)
+(* m is instantiation/match information *)
+(* rule is the equation for substitution *)
+fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
+ RW_Inst.rw ctxt m rule conclthm
+ |> unfix_frees cfvs
+ |> Conv.fconv_rule Drule.beta_eta_conversion
+ |> (fn r => resolve_tac ctxt [r] i st);
+
+(* substitute within the conclusion of goal i of gth, using a meta
+equation rule. Note that we assume rule has var indicies zero'd *)
+fun prep_concl_subst ctxt i gth =
+ let
+ val th = Thm.incr_indexes 1 gth;
+ val tgt_term = Thm.prop_of th;
+
+ val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
+ val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
+
+ val conclterm = Logic.strip_imp_concl fixedbody;
+ val conclthm = Thm.trivial (Thm.cterm_of ctxt conclterm);
+ val maxidx = Thm.maxidx_of th;
+ val ft =
+ (Zipper.move_down_right (* ==> *)
+ o Zipper.move_down_left (* Trueprop *)
+ o Zipper.mktop
+ o Thm.prop_of) conclthm
+ in
+ ((cfvs, conclthm), (ctxt, maxidx, ft))
+ end;
+
+(* substitute using an object or meta level equality *)
+fun eqsubst_tac' ctxt searchf instepthm i st =
+ let
+ val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i st;
+ val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
+ fun rewrite_with_thm r =
+ let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) in
+ searchf searchinfo lhs
+ |> Seq.maps (apply_subst_in_concl ctxt i st cvfsconclthm r)
+ end;
+ in stepthms |> Seq.maps rewrite_with_thm end;
+
+
+(* General substitution of multiple occurrences using one of
+ the given theorems *)
+
+fun skip_first_occs_search occ srchf sinfo lhs =
+ (case skipto_skipseq occ (srchf sinfo lhs) of
+ SkipMore _ => Seq.empty
+ | SkipSeq ss => Seq.flat ss);
+
+(* The "occs" argument is a list of integers indicating which occurrence
+w.r.t. the search order, to rewrite. Backtracking will also find later
+occurrences, but all earlier ones are skipped. Thus you can use [0] to
+just find all rewrites. *)
+
+fun eqsubst_tac ctxt occs thms i st =
+ let val nprems = Thm.nprems_of st in
+ if nprems < i then Seq.empty else
+ let
+ val thmseq = Seq.of_list thms;
+ fun apply_occ occ st =
+ thmseq |> Seq.maps (fn r =>
+ eqsubst_tac' ctxt
+ (skip_first_occs_search occ searchf_lr_unify_valid) r
+ (i + (Thm.nprems_of st - nprems)) st);
+ val sorted_occs = Library.sort (rev_order o int_ord) occs;
+ in
+ Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
+ end
+ end;
+
+
+(* apply a substitution inside assumption j, keeps asm in the same place *)
+fun apply_subst_in_asm ctxt i st rule ((cfvs, j, _, pth),m) =
+ let
+ val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
+ val preelimrule =
+ RW_Inst.rw ctxt m rule pth
+ |> (Seq.hd o prune_params_tac ctxt)
+ |> Thm.permute_prems 0 ~1 (* put old asm first *)
+ |> unfix_frees cfvs (* unfix any global params *)
+ |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
+ in
+ (* ~j because new asm starts at back, thus we subtract 1 *)
+ Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))
+ (dresolve_tac ctxt [preelimrule] i st2)
+ end;
+
+
+(* prepare to substitute within the j'th premise of subgoal i of gth,
+using a meta-level equation. Note that we assume rule has var indicies
+zero'd. Note that we also assume that premt is the j'th premice of
+subgoal i of gth. Note the repetition of work done for each
+assumption, i.e. this can be made more efficient for search over
+multiple assumptions. *)
+fun prep_subst_in_asm ctxt i gth j =
+ let
+ val th = Thm.incr_indexes 1 gth;
+ val tgt_term = Thm.prop_of th;
+
+ val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
+ val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
+
+ val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
+ val asm_nprems = length (Logic.strip_imp_prems asmt);
+
+ val pth = Thm.trivial ((Thm.cterm_of ctxt) asmt);
+ val maxidx = Thm.maxidx_of th;
+
+ val ft =
+ (Zipper.move_down_right (* trueprop *)
+ o Zipper.mktop
+ o Thm.prop_of) pth
+ in ((cfvs, j, asm_nprems, pth), (ctxt, maxidx, ft)) end;
+
+(* prepare subst in every possible assumption *)
+fun prep_subst_in_asms ctxt i gth =
+ map (prep_subst_in_asm ctxt i gth)
+ ((fn l => Library.upto (1, length l))
+ (Logic.prems_of_goal (Thm.prop_of gth) i));
+
+
+(* substitute in an assumption using an object or meta level equality *)
+fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i st =
+ let
+ val asmpreps = prep_subst_in_asms ctxt i st;
+ val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
+ fun rewrite_with_thm r =
+ let
+ val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
+ fun occ_search occ [] = Seq.empty
+ | occ_search occ ((asminfo, searchinfo)::moreasms) =
+ (case searchf searchinfo occ lhs of
+ SkipMore i => occ_search i moreasms
+ | SkipSeq ss =>
+ Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
+ (occ_search 1 moreasms)) (* find later substs also *)
+ in
+ occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i st r)
+ end;
+ in stepthms |> Seq.maps rewrite_with_thm end;
+
+
+fun skip_first_asm_occs_search searchf sinfo occ lhs =
+ skipto_skipseq occ (searchf sinfo lhs);
+
+fun eqsubst_asm_tac ctxt occs thms i st =
+ let val nprems = Thm.nprems_of st in
+ if nprems < i then Seq.empty
+ else
+ let
+ val thmseq = Seq.of_list thms;
+ fun apply_occ occ st =
+ thmseq |> Seq.maps (fn r =>
+ eqsubst_asm_tac' ctxt
+ (skip_first_asm_occs_search searchf_lr_unify_valid) occ r
+ (i + (Thm.nprems_of st - nprems)) st);
+ val sorted_occs = Library.sort (rev_order o int_ord) occs;
+ in
+ Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
+ end
+ end;
+
+(* combination method that takes a flag (true indicates that subst
+ should be done to an assumption, false = apply to the conclusion of
+ the goal) as well as the theorems to use *)
+val _ =
+ Theory.setup
+ (Method.setup \<^binding>\<open>sub\<close>
+ (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
+ Attrib.thms >> (fn ((asm, occs), inthms) => fn ctxt =>
+ SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
+ "single-step substitution"
+ #>
+ (Method.setup \<^binding>\<open>subst\<close>
+ (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
+ Attrib.thms >> (fn ((asm, occs), inthms) => fn ctxt =>
+ SIMPLE_METHOD' (SIDE_CONDS
+ ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)
+ ctxt)))
+ "single-step substitution with auto-typechecking"))
+
+end;
diff --git a/spartan/lib/equality.ML b/spartan/lib/equality.ML
new file mode 100644
index 0000000..79b4086
--- /dev/null
+++ b/spartan/lib/equality.ML
@@ -0,0 +1,90 @@
+(* Title: equality.ML
+ Author: Joshua Chen
+
+Equality reasoning with identity types.
+*)
+
+structure Equality:
+sig
+
+val dest_Id: term -> term * term * term
+
+val push_hyp_tac: term * term -> Proof.context -> int -> tactic
+val induction_tac: term -> term -> term -> term -> Proof.context -> tactic
+val equality_context_tac: Facts.ref -> Proof.context -> context_tactic
+
+end = struct
+
+fun dest_Id tm = case tm of
+ Const (\<^const_name>\<open>Id\<close>, _) $ A $ x $ y => (A, x, y)
+ | _ => error "dest_Id"
+
+(*Context assumptions that have already been pushed into the type family*)
+structure Inserts = Proof_Data (
+ type T = term Item_Net.T
+ val init = K (Item_Net.init Term.aconv_untyped single)
+)
+
+fun push_hyp_tac (t, _) =
+ Subgoal.FOCUS_PARAMS (fn {context = ctxt, concl, ...} =>
+ let
+ val (_, C) = Lib.dest_typing (Thm.term_of concl)
+ val B = Thm.cterm_of ctxt (Lib.lambda_var t C)
+ val a = Thm.cterm_of ctxt t
+ (*The resolvent is PiE[where ?B=B and ?a=a]*)
+ val resolvent =
+ Drule.infer_instantiate' ctxt [NONE, NONE, SOME B, SOME a] @{thm PiE}
+ in
+ HEADGOAL (resolve_tac ctxt [resolvent])
+ THEN SOMEGOAL (known_tac ctxt)
+ end)
+
+fun induction_tac p A x y ctxt =
+ let
+ val [p, A, x, y] = map (Thm.cterm_of ctxt) [p, A, x, y]
+ in
+ HEADGOAL (resolve_tac ctxt
+ [Drule.infer_instantiate' ctxt [SOME p, SOME A, SOME x, SOME y] @{thm IdE}])
+ end
+
+val side_conds_tac = TRY oo typechk_tac
+
+fun equality_context_tac fact ctxt =
+ let
+ val eq_th = Proof_Context.get_fact_single ctxt fact
+ val (p, (A, x, y)) = (Lib.dest_typing ##> dest_Id) (Thm.prop_of eq_th)
+
+ val hyps =
+ Facts.props (Proof_Context.facts_of ctxt)
+ |> filter (fn (th, _) => Lib.is_typing (Thm.prop_of th))
+ |> map (Lib.dest_typing o Thm.prop_of o fst)
+ |> filter_out (fn (t, _) =>
+ Term.aconv (t, p) orelse Item_Net.member (Inserts.get ctxt) t)
+ |> map (fn (t, T) => ((t, T), Lib.subterm_count_distinct [p, x, y] T))
+ |> filter (fn (_, i) => i > 0)
+ (*`t1: T1` comes before `t2: T2` if T1 contains t2 as subterm.
+ If they are incomparable, then order by decreasing
+ `subterm_count [p, x, y] T`*)
+ |> sort (fn (((t1, _), i), ((_, T2), j)) =>
+ Lib.cond_order (Lib.subterm_order T2 t1) (int_ord (j, i)))
+ |> map #1
+
+ val record_inserts =
+ Inserts.map (fold (fn (t, _) => fn net => Item_Net.update t net) hyps)
+
+ val tac =
+ fold (fn hyp => fn tac => tac THEN HEADGOAL (push_hyp_tac hyp ctxt))
+ hyps all_tac
+ THEN (
+ induction_tac p A x y ctxt
+ THEN RANGE (replicate 3 (typechk_tac ctxt) @ [side_conds_tac ctxt]) 1
+ )
+ THEN (
+ REPEAT_DETERM_N (length hyps) (SOMEGOAL (resolve_tac ctxt @{thms PiI}))
+ THEN ALLGOALS (side_conds_tac ctxt)
+ )
+ in
+ fn (ctxt, st) => Method.CONTEXT (record_inserts ctxt) (tac st)
+ end
+
+end
diff --git a/spartan/lib/focus.ML b/spartan/lib/focus.ML
new file mode 100644
index 0000000..dd8d3d9
--- /dev/null
+++ b/spartan/lib/focus.ML
@@ -0,0 +1,125 @@
+(* Title: focus.ML
+ Author: Makarius Wenzel, Joshua Chen
+
+A modified version of the Isar `subgoal` command
+that keeps schematic variables in the goal state.
+
+Modified from code originally written by Makarius Wenzel.
+*)
+
+local
+
+fun param_bindings ctxt (param_suffix, raw_param_specs) st =
+ let
+ val _ = if Thm.no_prems st then error "No subgoals!" else ()
+ val subgoal = #1 (Logic.dest_implies (Thm.prop_of st))
+ val subgoal_params =
+ map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
+ |> Term.variant_frees subgoal |> map #1
+
+ val n = length subgoal_params
+ val m = length raw_param_specs
+ val _ =
+ m <= n orelse
+ error ("Excessive subgoal parameter specification" ^
+ Position.here_list (map snd (drop n raw_param_specs)))
+
+ val param_specs =
+ raw_param_specs |> map
+ (fn (NONE, _) => NONE
+ | (SOME x, pos) =>
+ let
+ val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
+ val _ = Variable.check_name b
+ in SOME b end)
+ |> param_suffix ? append (replicate (n - m) NONE)
+
+ fun bindings (SOME x :: xs) (_ :: ys) = x :: bindings xs ys
+ | bindings (NONE :: xs) (y :: ys) = Binding.name y :: bindings xs ys
+ | bindings _ ys = map Binding.name ys
+ in bindings param_specs subgoal_params end
+
+fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
+ let
+ val _ = Proof.assert_backward state
+
+ val state1 = state
+ |> Proof.map_context (Proof_Context.set_mode Proof_Context.mode_schematic)
+ |> Proof.refine_insert []
+
+ val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1
+
+ val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding
+ val (prems_binding, do_prems) =
+ (case raw_prems_binding of
+ SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
+ | NONE => (Binding.empty_atts, false))
+
+ val (subgoal_focus, _) =
+ (if do_prems then Subgoal.focus_prems else Subgoal.focus_params) ctxt
+ 1 (SOME (param_bindings ctxt param_specs st)) st
+
+ fun after_qed (ctxt'', [[result]]) =
+ Proof.end_block #> (fn state' =>
+ let
+ val ctxt' = Proof.context_of state'
+ val results' =
+ Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result)
+ in
+ state'
+ |> Proof.refine_primitive (fn _ => fn _ =>
+ Subgoal.retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1
+ (Goal.protect 0 result) st
+ |> Seq.hd)
+ |> Proof.map_context
+ (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
+ end)
+ #> Proof.reset_facts
+ #> Proof.enter_backward
+ in
+ state1
+ |> Proof.enter_forward
+ |> Proof.using_facts []
+ |> Proof.begin_block
+ |> Proof.map_context (fn _ =>
+ #context subgoal_focus
+ |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
+ |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
+ NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
+ |> Proof.using_facts facts
+ |> pair subgoal_focus
+ end
+
+val opt_fact_binding =
+ Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
+ Binding.empty_atts
+
+val for_params =
+ Scan.optional
+ (\<^keyword>\<open>vars\<close> |--
+ Parse.!!! ((Scan.option Parse.dots >> is_some) --
+ (Scan.repeat1 (Parse.maybe_position Parse.name_position))))
+ (false, [])
+
+val schematic_subgoal_cmd = gen_schematic_subgoal Attrib.attribute_cmd
+
+val parser =
+ opt_fact_binding
+ -- (Scan.option (\<^keyword>\<open>premises\<close> |-- Parse.!!! opt_fact_binding))
+ -- for_params >> (fn ((a, b), c) =>
+ Toplevel.proofs (Seq.make_results o Seq.single o #2 o schematic_subgoal_cmd a b c))
+
+in
+
+(** Outer syntax commands **)
+
+val _ = Outer_Syntax.command \<^command_keyword>\<open>focus\<close>
+ "focus on first subgoal within backward refinement, without instantiating schematic vars"
+ parser
+
+val _ = Outer_Syntax.command \<^command_keyword>\<open>\<guillemotright>\<close> "focus bullet" parser
+val _ = Outer_Syntax.command \<^command_keyword>\<open>\<^item>\<close> "focus bullet" parser
+val _ = Outer_Syntax.command \<^command_keyword>\<open>\<^enum>\<close> "focus bullet" parser
+val _ = Outer_Syntax.command \<^command_keyword>\<open>~\<close> "focus bullet" parser
+
+end
diff --git a/spartan/lib/goals.ML b/spartan/lib/goals.ML
new file mode 100644
index 0000000..ce23751
--- /dev/null
+++ b/spartan/lib/goals.ML
@@ -0,0 +1,214 @@
+(* Title: goals.ML
+ Author: Makarius Wenzel, Joshua Chen
+
+Goal statements and proof term export.
+
+Modified from code originally written by Makarius Wenzel.
+*)
+
+local
+
+val long_keyword =
+ Parse_Spec.includes >> K "" ||
+ Parse_Spec.long_statement_keyword
+
+val long_statement =
+ Scan.optional
+ (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword)
+ Binding.empty_atts --
+ Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
+ >> (fn ((binding, includes), (elems, concl)) =>
+ (true, binding, includes, elems, concl))
+
+val short_statement =
+ Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
+ >> (fn ((shows, assumes), fixes) =>
+ (false, Binding.empty_atts, [],
+ [Element.Fixes 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
+ val prems = Assumption.local_prems_of elems_ctxt ctxt
+ val stmt_ctxt = fold (fold (Variable.auto_fixes o fst) o snd)
+ stmt elems_ctxt
+ in
+ case raw_stmt of
+ Element.Shows _ =>
+ let val stmt' = Attrib.map_specs (map prep_att) stmt
+ in (([], prems, stmt', NONE), stmt_ctxt) end
+ | Element.Obtains raw_obtains =>
+ let
+ val asms_ctxt = stmt_ctxt
+ |> fold (fn ((name, _), asm) =>
+ snd o Proof_Context.add_assms Assumption.assume_export
+ [((name, [Context_Rules.intro_query NONE]), asm)]) stmt
+ val that = Assumption.local_prems_of asms_ctxt stmt_ctxt
+ val ([(_, that')], that_ctxt) = asms_ctxt
+ |> Proof_Context.set_stmt true
+ |> Proof_Context.note_thmss ""
+ [((Binding.name Auto_Bind.thatN, []), [(that, [])])]
+ ||> Proof_Context.restore_stmt asms_ctxt
+
+ val stmt' = [
+ (Binding.empty_atts,
+ [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])
+ ]
+ in
+ ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'),
+ that_ctxt)
+ end
+ 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 concl_vars = Lib.collect_subterms is_Var
+ (Lib.term_of_typing concl)
+
+ val params = inter Term.aconv concl_vars prems_vars
+
+ val prf_tm =
+ fold_rev lambda params (Lib.term_of_typing concl)
+
+ 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
+
+ val def =
+ fold
+ (fn th1 => fn th2 => Thm.combination th2 th1)
+ (map (Thm.reflexive o Thm.cterm_of lthy) params)
+ raw_def
+
+ val ((_, def'), lthy'') = Local_Theory.note
+ ((make_name_binding (SOME "def") local_name, []), [def])
+ lthy'
+ in
+ (def', lthy'')
+ end
+ end
+ | define_proof_term _ _ _ = error
+ ("Unimplemented: handling proof terms of multiple facts in"
+ ^" single result")
+
+fun gen_schematic_theorem
+ bundle_includes prep_att prep_stmt
+ gen_prf long kind before_qed after_qed (name, raw_atts)
+ raw_includes raw_elems raw_concl int lthy =
+ let
+ val _ = Local_Theory.assert lthy;
+
+ val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy))
+ val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
+ |> bundle_includes raw_includes
+ |> prep_statement (prep_att lthy) prep_stmt elems raw_concl
+ val atts = more_atts @ map (prep_att lthy) raw_atts
+ val pos = Position.thread_data ()
+
+ val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN
+
+ fun after_qed' results goal_ctxt' =
+ let
+ val results' = burrow
+ (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy)
+ results
+
+ val ((res, lthy'), substmts) =
+ if forall (Binding.is_empty_atts o fst) stmt
+ then ((map (pair "") results', lthy), false)
+ else
+ (Local_Theory.notes_kind kind
+ (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results')
+ lthy,
+ true)
+
+ val (res', lthy'') =
+ if gen_prf
+ then
+ let
+ val (prf_tm_defs, lthy'') =
+ fold
+ (fn result => fn (defs, lthy) =>
+ apfst (fn new_defs => defs @ new_defs)
+ (define_proof_term (Binding.name_of name) result lthy))
+ res ([], lthy')
+
+ val res_folded =
+ map (apsnd (map (Local_Defs.fold lthy'' prf_tm_defs))) res
+ in
+ Local_Theory.notes_kind kind
+ [((name, @{attributes [typechk]} @ atts),
+ [(maps #2 res_folded, [])])]
+ lthy''
+ end
+ else
+ Local_Theory.notes_kind kind
+ [((name, atts), [(maps #2 res, [])])]
+ lthy'
+
+ val _ = Proof_Display.print_results int pos lthy''
+ ((kind, Binding.name_of name), map (fn (_, ths) => ("", ths)) res')
+
+ val _ =
+ if substmts then map
+ (fn (name, ths) => Proof_Display.print_results int pos lthy''
+ (("and", name), [("", ths)]))
+ res
+ else []
+ in
+ after_qed results' lthy''
+ end
+ in
+ goal_ctxt
+ |> not (null prems) ?
+ (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd)
+ |> Proof.theorem before_qed after_qed' (map snd stmt)
+ |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
+ end
+
+val schematic_theorem_cmd =
+ gen_schematic_theorem
+ Bundle.includes_cmd
+ Attrib.check_src
+ Expression.read_statement
+
+fun theorem spec descr =
+ Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
+ (Scan.option (Args.parens (Args.$$$ "derive"))
+ -- (long_statement || short_statement) >>
+ (fn (opt_derive, (long, binding, includes, elems, concl)) =>
+ schematic_theorem_cmd
+ (case opt_derive of SOME "derive" => true | _ => false)
+ long descr NONE (K I) binding includes elems concl))
+in
+
+val _ = theorem \<^command_keyword>\<open>Theorem\<close> "Theorem"
+val _ = theorem \<^command_keyword>\<open>Lemma\<close> "Lemma"
+val _ = theorem \<^command_keyword>\<open>Corollary\<close> "Corollary"
+val _ = theorem \<^command_keyword>\<open>Proposition\<close> "Proposition"
+
+end
diff --git a/spartan/lib/implicits.ML b/spartan/lib/implicits.ML
new file mode 100644
index 0000000..04fc825
--- /dev/null
+++ b/spartan/lib/implicits.ML
@@ -0,0 +1,78 @@
+structure Implicits :
+sig
+
+val implicit_defs: Proof.context -> (term * term) Symtab.table
+val implicit_defs_attr: attribute
+val make_holes: Proof.context -> term -> term
+
+end = struct
+
+structure Defs = Generic_Data (
+ type T = (term * term) Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ val merge = Symtab.merge (Term.aconv o #1)
+)
+
+val implicit_defs = Defs.get o Context.Proof
+
+val implicit_defs_attr = Thm.declaration_attribute (fn th =>
+ let
+ val (t, def) = Lib.dest_eq (Thm.prop_of th)
+ val (head, args) = Term.strip_comb t
+ val def' = fold_rev lambda args def
+ in
+ Defs.map (Symtab.update (Term.term_name head, (head, def')))
+ end)
+
+fun make_holes ctxt =
+ let
+ fun iarg_to_hole (Const (\<^const_name>\<open>iarg\<close>, T)) =
+ Const (\<^const_name>\<open>hole\<close>, T)
+ | iarg_to_hole t = t
+
+ fun expand head args =
+ let
+ fun betapplys (head', args') =
+ Term.betapplys (map_aterms iarg_to_hole head', args')
+ in
+ case head of
+ Abs (x, T, t) =>
+ list_comb (Abs (x, T, Lib.traverse_term expand t), args)
+ | _ =>
+ case Symtab.lookup (implicit_defs ctxt) (Term.term_name head) of
+ SOME (t, def) => betapplys
+ (Envir.expand_atom
+ (Term.fastype_of head)
+ (Term.fastype_of t, def),
+ args)
+ | NONE => list_comb (head, args)
+ end
+
+ fun holes_to_vars t =
+ let
+ val count = Lib.subterm_count (Const (\<^const_name>\<open>hole\<close>, dummyT))
+
+ fun subst (Const (\<^const_name>\<open>hole\<close>, T)) (Var (idx, _)::_) Ts =
+ let
+ val bounds = map Bound (0 upto (length Ts - 1))
+ val T' = foldr1 (op -->) (Ts @ [T])
+ in
+ foldl1 (op $) (Var (idx, T')::bounds)
+ end
+ | subst (Abs (x, T, t)) vs Ts = Abs (x, T, subst t vs (T::Ts))
+ | subst (t $ u) vs Ts =
+ let val n = count t
+ in subst t (take n vs) Ts $ subst u (drop n vs) Ts end
+ | subst t _ _ = t
+
+ val vars = map (fn n => Var ((n, 0), dummyT))
+ (Name.invent (Variable.names_of ctxt) "*" (count t))
+ in
+ subst t vars []
+ end
+ in
+ Lib.traverse_term expand #> holes_to_vars
+ end
+
+end
diff --git a/spartan/lib/lib.ML b/spartan/lib/lib.ML
new file mode 100644
index 0000000..fd5c597
--- /dev/null
+++ b/spartan/lib/lib.ML
@@ -0,0 +1,143 @@
+structure Lib :
+sig
+
+(*Lists*)
+val max: ('a * 'a -> bool) -> 'a list -> 'a
+val maxint: int list -> int
+
+(*Terms*)
+val is_rigid: term -> bool
+val dest_eq: term -> term * term
+val mk_Var: string -> int -> typ -> term
+val lambda_var: term -> term -> term
+
+val is_typing: term -> bool
+val dest_typing: term -> term * term
+val term_of_typing: term -> term
+val type_of_typing: term -> term
+val mk_Pi: term -> term -> term -> term
+
+val typing_of_term: term -> term
+
+(*Goals*)
+val rigid_typing_concl: term -> bool
+
+(*Subterms*)
+val has_subterm: term list -> term -> bool
+val subterm_count: term -> term -> int
+val subterm_count_distinct: term list -> term -> int
+val traverse_term: (term -> term list -> term) -> term -> term
+val collect_subterms: (term -> bool) -> term -> term list
+
+(*Orderings*)
+val subterm_order: term -> term -> order
+val cond_order: order -> order -> order
+
+end = struct
+
+
+(** Lists **)
+
+fun max gt (x::xs) = fold (fn a => fn b => if gt (a, b) then a else b) xs x
+ | max _ [] = error "max of empty list"
+
+val maxint = max (op >)
+
+
+(** Terms **)
+
+(* Meta *)
+
+val is_rigid = not o is_Var o head_of
+
+fun dest_eq (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ def) = (t, def)
+ | dest_eq _ = error "dest_eq"
+
+fun mk_Var name idx T = Var ((name, idx), T)
+
+fun lambda_var x tm =
+ let
+ fun var_args (Var (idx, T)) = Var (idx, \<^typ>\<open>o\<close> --> T) $ x
+ | var_args t = t
+ in
+ tm |> map_aterms var_args
+ |> lambda x
+ end
+
+(* Object *)
+
+fun is_typing (Const (\<^const_name>\<open>has_type\<close>, _) $ _ $ _) = true
+ | is_typing _ = false
+
+fun dest_typing (Const (\<^const_name>\<open>has_type\<close>, _) $ t $ T) = (t, T)
+ | dest_typing _ = error "dest_typing"
+
+val term_of_typing = #1 o dest_typing
+val type_of_typing = #2 o dest_typing
+
+fun mk_Pi v typ body = Const (\<^const_name>\<open>Pi\<close>, dummyT) $ typ $ lambda v body
+
+fun typing_of_term tm = \<^const>\<open>has_type\<close> $ tm $ Var (("*?", 0), \<^typ>\<open>o\<close>)
+
+
+(** Goals **)
+
+fun rigid_typing_concl goal =
+ let val concl = Logic.strip_assums_concl goal
+ in is_typing concl andalso is_rigid (term_of_typing concl) end
+
+
+(** Subterms **)
+
+fun has_subterm tms =
+ Term.exists_subterm
+ (foldl1 (op orf) (map (fn t => fn s => Term.aconv_untyped (s, t)) tms))
+
+fun subterm_count s t =
+ let
+ fun count (t1 $ t2) i = i + count t1 0 + count t2 0
+ | count (Abs (_, _, t)) i = i + count t 0
+ | count t i = if Term.aconv_untyped (s, t) then i + 1 else i
+ in
+ count t 0
+ end
+
+(*Number of distinct subterms in `tms` that appear in `tm`*)
+fun subterm_count_distinct tms tm =
+ length (filter I (map (fn t => has_subterm [t] tm) tms))
+
+(*
+ "Folds" a function f over the term structure of t by traversing t from child
+ nodes upwards through parents. At each node n in the term syntax tree, f is
+ additionally passed a list of the results of f at all children of n.
+*)
+fun traverse_term f t =
+ let
+ fun map_aux (Abs (x, T, t)) = Abs (x, T, map_aux t)
+ | map_aux t =
+ let
+ val (head, args) = Term.strip_comb t
+ val args' = map map_aux args
+ in
+ f head args'
+ end
+ in
+ map_aux t
+ end
+
+fun collect_subterms f (t $ u) = collect_subterms f t @ collect_subterms f u
+ | collect_subterms f (Abs (_, _, t)) = collect_subterms f t
+ | collect_subterms f t = if f t then [t] else []
+
+
+(** Orderings **)
+
+fun subterm_order t1 t2 =
+ if has_subterm [t1] t2 then LESS
+ else if has_subterm [t2] t1 then GREATER
+ else EQUAL
+
+fun cond_order o1 o2 = case o1 of EQUAL => o2 | _ => o1
+
+
+end
diff --git a/spartan/lib/rewrite.ML b/spartan/lib/rewrite.ML
new file mode 100644
index 0000000..f9c5d8e
--- /dev/null
+++ b/spartan/lib/rewrite.ML
@@ -0,0 +1,465 @@
+(* Title: rewrite.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.
+
+The patterns accepted by rewrite are of the following form:
+ <atom> ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
+ <pattern> ::= (in <atom> | at <atom>) [<pattern>]
+ <args> ::= [<pattern>] ("to" <term>) <thms>
+
+This syntax was clearly inspired by Gonthier's and Tassi's language of
+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 is slightly modified from the original at HOL/Library/rewrite.ML,
+to incorporate auto-typechecking for type theory.
+*)
+
+infix 1 then_pconv;
+infix 0 else_pconv;
+
+signature REWRITE =
+sig
+ type patconv = Proof.context -> Type.tyenv * (string * term) list -> cconv
+ val then_pconv: patconv * patconv -> patconv
+ val else_pconv: patconv * patconv -> patconv
+ val abs_pconv: patconv -> string option * typ -> patconv (*XXX*)
+ val fun_pconv: patconv -> patconv
+ val arg_pconv: patconv -> patconv
+ val imp_pconv: patconv -> patconv
+ val params_pconv: patconv -> patconv
+ val forall_pconv: patconv -> string option * typ option -> patconv
+ val all_pconv: patconv
+ val for_pconv: patconv -> (string option * typ option) list -> patconv
+ val concl_pconv: patconv -> patconv
+ val asm_pconv: patconv -> patconv
+ val asms_pconv: patconv -> patconv
+ 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
+
+ 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
+ -> (term * (string * typ) list, string * typ option) pattern list * term option
+ -> thm list
+ -> conv
+end
+
+structure Rewrite : REWRITE =
+struct
+
+datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
+
+exception NO_TO_MATCH
+
+val holeN = Name.internal "_hole"
+
+fun prep_meta_eq ctxt = Simplifier.mksimps ctxt #> map Drule.zero_var_indexes
+
+
+(* holes *)
+
+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
+ | 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 =
+ (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
+ in (Abs (x, T, t'), i') end
+ | replace_hole Ts (t $ u) i =
+ let
+ val (t', i') = replace_hole Ts t i
+ val (u', i'') = replace_hole Ts u i'
+ in (t' $ u', i'') end
+ | replace_hole _ a i = (a, i)
+ fun prep_holes ts = #1 (fold_map (replace_hole []) ts 1)
+ in
+ Context.proof_map (Syntax_Phases.term_check 101 "hole_expansion" (K prep_holes))
+ #> Proof_Context.set_mode Proof_Context.mode_pattern
+ end
+
+
+(* pattern conversions *)
+
+type patconv = Proof.context -> Type.tyenv * (string * term) list -> cterm -> thm
+
+fun (cv1 then_pconv cv2) ctxt tytenv ct = (cv1 ctxt tytenv then_conv cv2 ctxt tytenv) ct
+
+fun (cv1 else_pconv cv2) ctxt tytenv ct = (cv1 ctxt tytenv else_conv cv2 ctxt tytenv) ct
+
+fun raw_abs_pconv cv ctxt tytenv ct =
+ case Thm.term_of ct of
+ Abs _ => CConv.abs_cconv (fn (x, ctxt') => cv x ctxt' tytenv) ctxt ct
+ | t => raise TERM ("raw_abs_pconv", [t])
+
+fun raw_fun_pconv cv ctxt tytenv ct =
+ case Thm.term_of ct of
+ _ $ _ => CConv.fun_cconv (cv ctxt tytenv) ct
+ | t => raise TERM ("raw_fun_pconv", [t])
+
+fun raw_arg_pconv cv ctxt tytenv ct =
+ case Thm.term_of ct of
+ _ $ _ => CConv.arg_cconv (cv ctxt tytenv) ct
+ | t => raise TERM ("raw_arg_pconv", [t])
+
+fun abs_pconv cv (s,T) ctxt (tyenv, ts) ct =
+ let val u = Thm.term_of ct
+ in
+ case try (fastype_of #> dest_funT) u of
+ NONE => raise TERM ("abs_pconv: no function type", [u])
+ | SOME (U, _) =>
+ let
+ val tyenv' =
+ if T = dummyT then tyenv
+ else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
+ val eta_expand_cconv =
+ case u of
+ Abs _=> Thm.reflexive
+ | _ => CConv.rewr_cconv @{thm eta_expand}
+ fun add_ident NONE _ l = l
+ | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l
+ val abs_cv = CConv.abs_cconv (fn (ct, ctxt) => cv ctxt (tyenv', add_ident s ct ts)) ctxt
+ in (eta_expand_cconv then_conv abs_cv) ct end
+ handle Pattern.MATCH => raise TYPE ("abs_pconv: types don't match", [T,U], [u])
+ end
+
+fun fun_pconv cv ctxt tytenv ct =
+ case Thm.term_of ct of
+ _ $ _ => CConv.fun_cconv (cv ctxt tytenv) ct
+ | Abs (_, T, _ $ Bound 0) => abs_pconv (fun_pconv cv) (NONE, T) ctxt tytenv ct
+ | t => raise TERM ("fun_pconv", [t])
+
+local
+
+fun arg_pconv_gen cv0 cv ctxt tytenv ct =
+ case Thm.term_of ct of
+ _ $ _ => cv0 (cv ctxt tytenv) ct
+ | Abs (_, T, _ $ Bound 0) => abs_pconv (arg_pconv_gen cv0 cv) (NONE, T) ctxt tytenv ct
+ | t => raise TERM ("arg_pconv_gen", [t])
+
+in
+
+fun arg_pconv ctxt = arg_pconv_gen CConv.arg_cconv ctxt
+fun imp_pconv ctxt = arg_pconv_gen (CConv.concl_cconv 1) ctxt
+
+end
+
+(* Move to B in !!x_1 ... x_n. B. Do not eta-expand *)
+fun params_pconv cv ctxt tytenv ct =
+ let val pconv =
+ case Thm.term_of ct of
+ Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs _ => (raw_arg_pconv o raw_abs_pconv) (fn _ => params_pconv cv)
+ | Const (\<^const_name>\<open>Pure.all\<close>, _) => raw_arg_pconv (params_pconv cv)
+ | _ => cv
+ in pconv ctxt tytenv ct end
+
+fun forall_pconv cv ident ctxt tytenv ct =
+ case Thm.term_of ct of
+ Const (\<^const_name>\<open>Pure.all\<close>, T) $ _ =>
+ let
+ val def_U = T |> dest_funT |> fst |> dest_funT |> fst
+ val ident' = apsnd (the_default (def_U)) ident
+ in arg_pconv (abs_pconv cv ident') ctxt tytenv ct end
+ | t => raise TERM ("forall_pconv", [t])
+
+fun all_pconv _ _ = Thm.reflexive
+
+fun for_pconv cv idents ctxt tytenv ct =
+ let
+ fun f rev_idents (Const (\<^const_name>\<open>Pure.all\<close>, _) $ t) =
+ let val (rev_idents', cv') = f rev_idents (case t of Abs (_,_,u) => u | _ => t)
+ in
+ case rev_idents' of
+ [] => ([], forall_pconv cv' (NONE, NONE))
+ | (x :: xs) => (xs, forall_pconv cv' x)
+ end
+ | f rev_idents _ = (rev_idents, cv)
+ in
+ case f (rev idents) (Thm.term_of ct) of
+ ([], cv') => cv' ctxt tytenv ct
+ | _ => raise CTERM ("for_pconv", [ct])
+ end
+
+fun concl_pconv cv ctxt tytenv ct =
+ case Thm.term_of ct of
+ (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _) $ _ => imp_pconv (concl_pconv cv) ctxt tytenv ct
+ | _ => cv ctxt tytenv ct
+
+fun asm_pconv cv ctxt tytenv ct =
+ case Thm.term_of ct of
+ (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _) $ _ => CConv.with_prems_cconv ~1 (cv ctxt tytenv) ct
+ | t => raise TERM ("asm_pconv", [t])
+
+fun asms_pconv cv ctxt tytenv ct =
+ case Thm.term_of ct of
+ (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _) $ _ =>
+ ((CConv.with_prems_cconv ~1 oo cv) else_pconv imp_pconv (asms_pconv cv)) ctxt tytenv ct
+ | t => raise TERM ("asms_pconv", [t])
+
+fun judgment_pconv cv ctxt tytenv ct =
+ if Object_Logic.is_judgment ctxt (Thm.term_of ct)
+ then arg_pconv cv ctxt tytenv ct
+ else cv ctxt tytenv ct
+
+fun in_pconv cv ctxt tytenv ct =
+ (cv else_pconv
+ raw_fun_pconv (in_pconv cv) else_pconv
+ raw_arg_pconv (in_pconv cv) else_pconv
+ raw_abs_pconv (fn _ => in_pconv cv))
+ ctxt tytenv ct
+
+fun replace_idents idents t =
+ let
+ fun subst ((n1, s)::ss) (t as Free (n2, _)) = if n1 = n2 then s else subst ss t
+ | subst _ t = t
+ in Term.map_aterms (subst idents) t end
+
+fun match_pconv cv (t,fixes) ctxt (tyenv, env_ts) ct =
+ let
+ val t' = replace_idents env_ts t
+ val thy = Proof_Context.theory_of ctxt
+ val u = Thm.term_of ct
+
+ fun descend_hole fixes (Abs (_, _, t)) =
+ (case descend_hole fixes t of
+ NONE => NONE
+ | SOME (fix :: fixes', pos) => SOME (fixes', abs_pconv pos fix)
+ | SOME ([], _) => raise Match (* less fixes than abstractions on path to hole *))
+ | descend_hole fixes (t as l $ r) =
+ let val (f, _) = strip_comb t
+ in
+ if is_hole f
+ then SOME (fixes, cv)
+ else
+ (case descend_hole fixes l of
+ SOME (fixes', pos) => SOME (fixes', fun_pconv pos)
+ | NONE =>
+ (case descend_hole fixes r of
+ SOME (fixes', pos) => SOME (fixes', arg_pconv pos)
+ | NONE => NONE))
+ end
+ | descend_hole fixes t =
+ if is_hole t then SOME (fixes, cv) else NONE
+
+ val to_hole = descend_hole (rev fixes) #> the_default ([], cv) #> snd
+ in
+ case try (Pattern.match thy (apply2 Logic.mk_term (t',u))) (tyenv, Vartab.empty) of
+ NONE => raise TERM ("match_pconv: Does not match pattern", [t, t',u])
+ | SOME (tyenv', _) => to_hole t ctxt (tyenv', env_ts) ct
+ end
+
+fun rewrs_pconv to thms ctxt (tyenv, env_ts) =
+ let
+ fun instantiate_normalize_env ctxt env thm =
+ let
+ val prop = Thm.prop_of thm
+ val norm_type = Envir.norm_type o Envir.type_env
+ val insts = Term.add_vars prop []
+ |> map (fn x as (s, T) =>
+ ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x))))
+ val tyinsts = Term.add_tvars prop []
+ |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x))))
+ in Drule.instantiate_normalize (tyinsts, insts) thm end
+
+ fun unify_with_rhs context to env thm =
+ let
+ val (_, rhs) = thm |> Thm.concl_of |> Logic.dest_equals
+ val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env
+ handle Pattern.Unif => raise NO_TO_MATCH
+ in env' end
+
+ fun inst_thm_to _ (NONE, _) thm = thm
+ | inst_thm_to (ctxt : Proof.context) (SOME to, env) thm =
+ instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm
+
+ fun inst_thm ctxt idents (to, tyenv) thm =
+ let
+ (* Replace any identifiers with their corresponding bound variables. *)
+ val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0
+ val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv}
+ val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to)
+ val thm' = Thm.incr_indexes (maxidx + 1) thm
+ in SOME (inst_thm_to ctxt (Option.map (replace_idents idents) to, env) thm') end
+ handle NO_TO_MATCH => NONE
+
+ in CConv.rewrs_cconv (map_filter (inst_thm ctxt env_ts (to, tyenv)) thms) end
+
+fun rewrite_conv ctxt (pattern, to) thms ct =
+ let
+ fun apply_pat At = judgment_pconv
+ | apply_pat In = in_pconv
+ | apply_pat Asm = params_pconv o asms_pconv
+ | apply_pat Concl = params_pconv o concl_pconv
+ | apply_pat (For idents) = (fn cv => for_pconv cv (map (apfst SOME) idents))
+ | apply_pat (Term x) = (fn cv => match_pconv cv (apsnd (map (apfst SOME)) x))
+
+ val cv = fold_rev apply_pat pattern
+
+ fun distinct_prems th =
+ case Seq.pull (distinct_subgoals_tac th) of
+ 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
+
+fun rewrite_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
+
+val _ =
+ Theory.setup
+ let
+ fun mk_fix s = (Binding.name s, NONE, NoSyn)
+
+ val raw_pattern : (string, binding * string option * mixfix) pattern list parser =
+ let
+ val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In)
+ val atom = (Args.$$$ "asm" >> K Asm) ||
+ (Args.$$$ "concl" >> K Concl) ||
+ (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.vars []) >> For) ||
+ (Parse.term >> Term)
+ val sep_atom = sep -- atom >> (fn (s,a) => [s,a])
+
+ fun append_default [] = [Concl, In]
+ | append_default (ps as Term _ :: _) = Concl :: In :: ps
+ | append_default [For x, In] = [For x, Concl, In]
+ | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps
+ | append_default ps = ps
+
+ in Scan.repeats sep_atom >> (rev #> append_default) end
+
+ fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
+ let
+ val (r, toks') = scan toks
+ val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context
+ in (r', (context', toks' : Token.T list)) end
+
+ fun read_fixes fixes ctxt =
+ let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx)
+ in Proof_Context.add_fixes (map read_typ fixes) ctxt end
+
+ fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) =
+ let
+ fun add_constrs ctxt n (Abs (x, T, t)) =
+ let
+ val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt
+ in
+ (case add_constrs ctxt' (n+1) t of
+ NONE => NONE
+ | SOME ((ctxt'', n', xs), t') =>
+ let
+ val U = Type_Infer.mk_param n []
+ val u = Type.constraint (U --> dummyT) (Abs (x, T, t'))
+ in SOME ((ctxt'', n', (x', U) :: xs), u) end)
+ end
+ | add_constrs ctxt n (l $ r) =
+ (case add_constrs ctxt n l of
+ SOME (c, l') => SOME (c, l' $ r)
+ | NONE =>
+ (case add_constrs ctxt n r of
+ SOME (c, r') => SOME (c, l $ r')
+ | NONE => NONE))
+ | add_constrs ctxt n t =
+ if is_hole_const t then SOME ((ctxt, n, []), t) else NONE
+
+ fun prep (Term s) (n, ctxt) =
+ let
+ val t = Syntax.parse_term ctxt s
+ val ((ctxt', n', bs), t') =
+ the_default ((ctxt, n, []), t) (add_constrs ctxt (n+1) t)
+ in (Term (t', bs), (n', ctxt')) end
+ | prep (For ss) (n, ctxt) =
+ let val (ns, ctxt') = read_fixes ss ctxt
+ in (For ns, (n, ctxt')) end
+ | prep At (n,ctxt) = (At, (n, ctxt))
+ | prep In (n,ctxt) = (In, (n, ctxt))
+ | prep Concl (n,ctxt) = (Concl, (n, ctxt))
+ | prep Asm (n,ctxt) = (Asm, (n, ctxt))
+
+ val (xs, (_, ctxt')) = fold_map prep ps (0, ctxt)
+
+ in (xs, ctxt') end
+
+ fun prep_args ctxt (((raw_pats, raw_to), raw_ths)) =
+ let
+
+ fun check_terms ctxt ps to =
+ let
+ fun safe_chop (0: int) xs = ([], xs)
+ | safe_chop n (x :: xs) = chop (n - 1) xs |>> cons x
+ | safe_chop _ _ = raise Match
+
+ fun reinsert_pat _ (Term (_, cs)) (t :: ts) =
+ let val (cs', ts') = safe_chop (length cs) ts
+ in (Term (t, map dest_Free cs'), ts') end
+ | reinsert_pat _ (Term _) [] = raise Match
+ | reinsert_pat ctxt (For ss) ts =
+ let val fixes = map (fn s => (s, Variable.default_type ctxt s)) ss
+ in (For fixes, ts) end
+ | reinsert_pat _ At ts = (At, ts)
+ | reinsert_pat _ In ts = (In, ts)
+ | reinsert_pat _ Concl ts = (Concl, ts)
+ | reinsert_pat _ Asm ts = (Asm, ts)
+
+ fun free_constr (s,T) = Type.constraint T (Free (s, dummyT))
+ fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs
+ | mk_free_constrs _ = []
+
+ val ts = maps mk_free_constrs ps @ the_list to
+ |> Syntax.check_terms (hole_syntax ctxt)
+ val ctxt' = fold Variable.declare_term ts ctxt
+ val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts
+ ||> (fn xs => case to of NONE => (NONE, xs) | SOME _ => (SOME (hd xs), tl xs))
+ val _ = case ts' of (_ :: _) => raise Match | [] => ()
+ in ((ps', to'), ctxt') end
+
+ val (pats, ctxt') = prep_pats ctxt raw_pats
+
+ val ths = Attrib.eval_thms ctxt' raw_ths
+ val to = Option.map (Syntax.parse_term ctxt') raw_to
+
+ val ((pats', to'), ctxt'') = check_terms ctxt' pats to
+
+ in ((pats', ths, (to', ctxt)), ctxt'') end
+
+ val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term)
+
+ val subst_parser =
+ let val scan = raw_pattern -- to_parser -- Parse.thms1
+ in context_lift scan prep_args end
+ in
+ Method.setup \<^binding>\<open>rewr\<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)))
+ "single-step rewriting, allowing subterm selection via patterns"
+ #>
+ (Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >>
+ (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt =>
+ SIMPLE_METHOD' (SIDE_CONDS
+ (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)
+ orig_ctxt)))
+ "single-step rewriting with auto-typechecking")
+ end
+end
diff --git a/spartan/lib/tactics.ML b/spartan/lib/tactics.ML
new file mode 100644
index 0000000..0e09533
--- /dev/null
+++ b/spartan/lib/tactics.ML
@@ -0,0 +1,143 @@
+(* Title: tactics.ML
+ Author: Joshua Chen
+
+General tactics for dependent type theory.
+*)
+
+structure Tactics:
+sig
+
+val assumptions_tac: Proof.context -> int -> tactic
+val known_tac: Proof.context -> int -> tactic
+val typechk_tac: Proof.context -> int -> tactic
+val auto_typechk: bool Config.T
+val SIDE_CONDS: (int -> tactic) -> Proof.context -> int -> tactic
+val rule_tac: thm list -> Proof.context -> int -> tactic
+val dest_tac: int option -> thm list -> Proof.context -> int -> tactic
+val intro_tac: Proof.context -> int -> tactic
+val intros_tac: Proof.context -> int -> tactic
+val elims_tac: term option -> Proof.context -> int -> tactic
+
+end = struct
+
+(*An assumption tactic that only solves typing goals with rigid terms and
+ judgmental equalities without schematic variables*)
+fun assumptions_tac ctxt = SUBGOAL (fn (goal, i) =>
+ let
+ val concl = Logic.strip_assums_concl goal
+ in
+ if
+ Lib.is_typing concl andalso Lib.is_rigid (Lib.term_of_typing concl)
+ orelse not ((exists_subterm is_Var) concl)
+ then assume_tac ctxt i
+ else no_tac
+ end)
+
+(*Solves typing goals with rigid term by resolving with context facts and
+ simplifier premises, or arbitrary goals by *non-unifying* assumption*)
+fun known_tac ctxt = SUBGOAL (fn (goal, i) =>
+ let
+ val concl = Logic.strip_assums_concl goal
+ in
+ ((if Lib.is_typing concl andalso Lib.is_rigid (Lib.term_of_typing concl)
+ then
+ let val ths = map fst (Facts.props (Proof_Context.facts_of ctxt))
+ in resolve_tac ctxt (ths @ Simplifier.prems_of ctxt) end
+ else K no_tac)
+ ORELSE' assumptions_tac ctxt) i
+ end)
+
+(*Typechecking: try to solve goals of the form "a: A" where a is rigid*)
+fun typechk_tac ctxt =
+ let
+ val tac = SUBGOAL (fn (goal, i) =>
+ if Lib.rigid_typing_concl goal
+ then
+ let val net = Tactic.build_net
+ ((Named_Theorems.get ctxt \<^named_theorems>\<open>typechk\<close>)
+ @(Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>)
+ @(Elim.rules ctxt))
+ in (resolve_from_net_tac ctxt net) i end
+ else no_tac)
+ in
+ CHANGED o REPEAT o REPEAT_ALL_NEW (known_tac ctxt ORELSE' tac)
+ end
+
+(*Many methods try to automatically discharge side conditions by typechecking.
+ Switch this flag off to discharge by non-unifying assumption instead.*)
+val auto_typechk = Attrib.setup_config_bool \<^binding>\<open>auto_typechk\<close> (K true)
+
+(*Combinator runs tactic and tries to discharge all new typing side conditions*)
+fun SIDE_CONDS tac ctxt =
+ let
+ val side_cond_tac =
+ if Config.get ctxt auto_typechk then typechk_tac ctxt else known_tac ctxt
+ in
+ tac THEN_ALL_NEW (TRY o side_cond_tac)
+ end
+
+local
+fun mk_rules _ ths [] = ths
+ | mk_rules n ths ths' =
+ let val ths'' = foldr1 (op @)
+ (map (fn th => [rotate_prems n (th RS @{thm PiE})] handle THM _ => []) ths')
+ in
+ mk_rules n (ths @ ths') ths''
+ end
+in
+
+(*Resolves with given rules, discharging as many side conditions as possible*)
+fun rule_tac ths ctxt =
+ SIDE_CONDS (resolve_tac ctxt (mk_rules 0 [] ths)) ctxt
+
+(*Attempts destruct-resolution with the n-th premise of the given rules*)
+fun dest_tac opt_n ths ctxt = SIDE_CONDS (dresolve_tac ctxt
+ (mk_rules (case opt_n of NONE => 0 | SOME 0 => 0 | SOME n => n-1) [] ths))
+ ctxt
+
+end
+
+(*Applies some introduction rule*)
+fun intro_tac ctxt = SUBGOAL (fn (_, i) => SIDE_CONDS
+ (resolve_tac ctxt (Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>)) ctxt i)
+
+fun intros_tac ctxt = SUBGOAL (fn (_, i) =>
+ (CHANGED o REPEAT o CHANGED o intro_tac ctxt) i)
+
+(* Basic elimination tactic *)
+(*Only uses existing type judgments from the context
+ (performs no type synthesis)*)
+fun elims_tac opt_tm ctxt = case opt_tm of
+ NONE => SUBGOAL (fn (_, i) => eresolve_tac ctxt (Elim.rules ctxt) i)
+ | SOME tm => SUBGOAL (fn (goal, i) =>
+ let
+ fun elim_rule typing =
+ let
+ val hd = head_of (Lib.type_of_typing typing)
+ val opt_rl = Elim.get_rule ctxt hd
+ in
+ case opt_rl of
+ NONE => Drule.dummy_thm
+ | SOME rl => Drule.infer_instantiate' ctxt
+ [SOME (Thm.cterm_of ctxt tm)] rl
+ end
+
+ val template = Lib.typing_of_term tm
+
+ val facts = Proof_Context.facts_of ctxt
+ val candidate_typings = Facts.could_unify facts template
+ val candidate_rules =
+ map (elim_rule o Thm.prop_of o #1) candidate_typings
+
+ val prems = Logic.strip_assums_hyp goal
+ val candidate_typings' =
+ filter (fn prem => Term.could_unify (template, prem)) prems
+ val candidate_rules' = map elim_rule candidate_typings'
+ in
+ (resolve_tac ctxt candidate_rules
+ ORELSE' eresolve_tac ctxt candidate_rules') i
+ end)
+
+end
+
+open Tactics
diff --git a/spartan/theories/Equivalence.thy b/spartan/theories/Equivalence.thy
new file mode 100644
index 0000000..44b77dd
--- /dev/null
+++ b/spartan/theories/Equivalence.thy
@@ -0,0 +1,431 @@
+theory Equivalence
+imports Identity
+
+begin
+
+section \<open>Homotopy\<close>
+
+definition "homotopy A B f g \<equiv> \<Prod>x: A. f `x =\<^bsub>B x\<^esub> g `x"
+
+definition homotopy_i (infix "~" 100)
+ where [implicit]: "f ~ g \<equiv> homotopy ? ? f g"
+
+translations "f ~ g" \<leftharpoondown> "CONST homotopy A B f g"
+
+Lemma homotopy_type [typechk]:
+ assumes
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> B x: U i"
+ "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
+ shows "f ~ g: U i"
+ unfolding homotopy_def by typechk
+
+Lemma (derive) homotopy_refl:
+ assumes
+ "A: U i"
+ "f: \<Prod>x: A. B x"
+ shows "f ~ f"
+ unfolding homotopy_def by intros
+
+Lemma (derive) hsym:
+ assumes
+ "f: \<Prod>x: A. B x"
+ "g: \<Prod>x: A. B x"
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> B x: U i"
+ shows "H: f ~ g \<Longrightarrow> g ~ f"
+ unfolding homotopy_def
+ apply intros
+ apply (rule pathinv)
+ \<guillemotright> by (elim H)
+ \<guillemotright> by typechk
+ done
+
+lemmas homotopy_symmetric = hsym[rotated 4]
+
+text \<open>\<open>hsym\<close> attribute for homotopies:\<close>
+
+ML \<open>
+structure HSym_Attr = Sym_Attr (
+ struct
+ val name = "hsym"
+ val symmetry_rule = @{thm homotopy_symmetric}
+ end
+)
+\<close>
+
+setup \<open>HSym_Attr.setup\<close>
+
+Lemma (derive) htrans:
+ assumes
+ "f: \<Prod>x: A. B x"
+ "g: \<Prod>x: A. B x"
+ "h: \<Prod>x: A. B x"
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> B x: U i"
+ shows "\<lbrakk>H1: f ~ g; H2: g ~ h\<rbrakk> \<Longrightarrow> f ~ h"
+ unfolding homotopy_def
+ apply intro
+ \<guillemotright> vars x
+ apply (rule pathcomp[where ?y="g x"])
+ \<^item> by (elim H1)
+ \<^item> by (elim H2)
+ done
+ \<guillemotright> by typechk
+ done
+
+lemmas homotopy_transitive = htrans[rotated 5]
+
+Lemma (derive) commute_homotopy:
+ assumes
+ "A: U i" "B: U i"
+ "x: A" "y: A"
+ "p: x =\<^bsub>A\<^esub> y"
+ "f: A \<rightarrow> B" "g: A \<rightarrow> B"
+ "H: homotopy A (\<lambda>_. B) f g"
+ shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)"
+ \<comment> \<open>Need this assumption unfolded for typechecking:\<close>
+ supply assms(8)[unfolded homotopy_def]
+ apply (equality \<open>p:_\<close>)
+ focus vars x
+ apply reduce
+ \<comment> \<open>Here it would really be nice to have automation for transport and
+ propositional equality.\<close>
+ apply (rule use_transport[where ?y="H x \<bullet> refl (g x)"])
+ \<guillemotright> by (rule pathcomp_right_refl)
+ \<guillemotright> by (rule pathinv) (rule pathcomp_left_refl)
+ \<guillemotright> by typechk
+ done
+ done
+
+Corollary (derive) commute_homotopy':
+ assumes
+ "A: U i"
+ "x: A"
+ "f: A \<rightarrow> A"
+ "H: homotopy A (\<lambda>_. A) f (id A)"
+ shows "H (f x) = f [H x]"
+oops
+
+Lemma homotopy_id_left [typechk]:
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
+ shows "homotopy_refl A f: (id B) \<circ> f ~ f"
+ unfolding homotopy_refl_def homotopy_def by reduce
+
+Lemma homotopy_id_right [typechk]:
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
+ shows "homotopy_refl A f: f \<circ> (id A) ~ f"
+ unfolding homotopy_refl_def homotopy_def by reduce
+
+Lemma homotopy_funcomp_left:
+ assumes
+ "H: homotopy B C g g'"
+ "f: A \<rightarrow> B"
+ "g: \<Prod>x: B. C x"
+ "g': \<Prod>x: B. C x"
+ "A: U i" "B: U i"
+ "\<And>x. x: B \<Longrightarrow> C x: U i"
+ shows "homotopy A {} (g \<circ>\<^bsub>A\<^esub> f) (g' \<circ>\<^bsub>A\<^esub> f)"
+ unfolding homotopy_def
+ apply (intro; reduce)
+ apply (insert \<open>H: _\<close>[unfolded homotopy_def])
+ apply (elim H)
+ done
+
+Lemma homotopy_funcomp_right:
+ assumes
+ "H: homotopy A (\<lambda>_. B) f f'"
+ "f: A \<rightarrow> B"
+ "f': A \<rightarrow> B"
+ "g: B \<rightarrow> C"
+ "A: U i" "B: U i" "C: U i"
+ shows "homotopy A {} (g \<circ>\<^bsub>A\<^esub> f) (g \<circ>\<^bsub>A\<^esub> f')"
+ unfolding homotopy_def
+ apply (intro; reduce)
+ apply (insert \<open>H: _\<close>[unfolded homotopy_def])
+ apply (dest PiE, assumption)
+ apply (rule ap, assumption)
+ done
+
+
+section \<open>Quasi-inverse and bi-invertibility\<close>
+
+subsection \<open>Quasi-inverses\<close>
+
+definition "qinv A B f \<equiv> \<Sum>g: B \<rightarrow> A.
+ homotopy A (\<lambda>_. A) (g \<circ>\<^bsub>A\<^esub> f) (id A) \<times> homotopy B (\<lambda>_. B) (f \<circ>\<^bsub>B\<^esub> g) (id B)"
+
+lemma qinv_type [typechk]:
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
+ shows "qinv A B f: U i"
+ unfolding qinv_def by typechk
+
+definition qinv_i ("qinv")
+ where [implicit]: "qinv f \<equiv> Equivalence.qinv ? ? f"
+
+translations "qinv f" \<leftharpoondown> "CONST Equivalence.qinv A B f"
+
+Lemma (derive) id_qinv:
+ assumes "A: U i"
+ shows "qinv (id A)"
+ unfolding qinv_def
+ apply intro defer
+ apply intro defer
+ apply (rule homotopy_id_right)
+ apply (rule homotopy_id_left)
+ done
+
+Lemma (derive) quasiinv_qinv:
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
+ shows "prf: qinv f \<Longrightarrow> qinv (fst prf)"
+ unfolding qinv_def
+ apply intro
+ \<guillemotright> by (rule \<open>f:_\<close>)
+ \<guillemotright> apply (elim "prf")
+ focus vars g HH
+ apply intro
+ \<^item> by reduce (snd HH)
+ \<^item> by reduce (fst HH)
+ done
+ done
+ done
+
+Lemma (derive) funcomp_qinv:
+ assumes
+ "A: U i" "B: U i" "C: U i"
+ "f: A \<rightarrow> B" "g: B \<rightarrow> C"
+ shows "qinv f \<rightarrow> qinv g \<rightarrow> qinv (g \<circ> f)"
+ apply (intros, unfold qinv_def, elims)
+ focus
+ premises hyps
+ vars _ _ finv _ ginv _ HfA HfB HgB HgC
+
+ apply intro
+ apply (rule funcompI[where ?f=ginv and ?g=finv])
+
+ text \<open>Now a whole bunch of rewrites and we're done.\<close>
+oops
+
+subsection \<open>Bi-invertible maps\<close>
+
+definition "biinv A B f \<equiv>
+ (\<Sum>g: B \<rightarrow> A. homotopy A (\<lambda>_. A) (g \<circ>\<^bsub>A\<^esub> f) (id A))
+ \<times> (\<Sum>g: B \<rightarrow> A. homotopy B (\<lambda>_. B) (f \<circ>\<^bsub>B\<^esub> g) (id B))"
+
+lemma biinv_type [typechk]:
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
+ shows "biinv A B f: U i"
+ unfolding biinv_def by typechk
+
+definition biinv_i ("biinv")
+ where [implicit]: "biinv f \<equiv> Equivalence.biinv ? ? f"
+
+translations "biinv f" \<leftharpoondown> "CONST Equivalence.biinv A B f"
+
+Lemma (derive) qinv_imp_biinv:
+ assumes
+ "A: U i" "B: U i"
+ "f: A \<rightarrow> B"
+ shows "?prf: qinv f \<rightarrow> biinv f"
+ apply intros
+ unfolding qinv_def biinv_def
+ by (rule Sig_dist_exp)
+
+text \<open>
+ Show that bi-invertible maps are quasi-inverses, as a demonstration of how to
+ work in this system.
+\<close>
+
+Lemma (derive) biinv_imp_qinv:
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
+ shows "biinv f \<rightarrow> qinv f"
+
+ text \<open>Split the hypothesis \<^term>\<open>biinv f\<close> into its components:\<close>
+ apply intro
+ unfolding biinv_def
+ apply elims
+
+ text \<open>Name the components:\<close>
+ focus premises vars _ _ _ g H1 h H2
+ thm \<open>g:_\<close> \<open>h:_\<close> \<open>H1:_\<close> \<open>H2:_\<close>
+
+ text \<open>
+ \<^term>\<open>g\<close> is a quasi-inverse to \<^term>\<open>f\<close>, so the proof will be a triple
+ \<^term>\<open><g, <?H1, ?H2>>\<close>.
+ \<close>
+ unfolding qinv_def
+ apply intro
+ \<guillemotright> by (rule \<open>g: _\<close>)
+ \<guillemotright> apply intro
+ text \<open>The first part \<^prop>\<open>?H1: g \<circ> f ~ id A\<close> is given by \<^term>\<open>H1\<close>.\<close>
+ apply (rule \<open>H1: _\<close>)
+
+ text \<open>
+ It remains to prove \<^prop>\<open>?H2: f \<circ> g ~ id B\<close>. First show that \<open>g ~ h\<close>,
+ then the result follows from @{thm \<open>H2: f \<circ> h ~ id B\<close>}. Here a proof
+ block is used to calculate "forward".
+ \<close>
+ proof -
+ have "g \<circ> (id B) ~ g \<circ> f \<circ> h"
+ by (rule homotopy_funcomp_right) (rule \<open>H2:_\<close>[hsym])
+
+ moreover have "g \<circ> f \<circ> h ~ (id A) \<circ> h"
+ by (subst funcomp_assoc[symmetric])
+ (rule homotopy_funcomp_left, rule \<open>H1:_\<close>)
+
+ ultimately have "g ~ h"
+ apply (rewrite to "g \<circ> (id B)" id_right[symmetric])
+ apply (rewrite to "(id A) \<circ> h" id_left[symmetric])
+ by (rule homotopy_transitive) (assumption, typechk)
+
+ then have "f \<circ> g ~ f \<circ> h"
+ by (rule homotopy_funcomp_right)
+
+ with \<open>H2:_\<close>
+ show "f \<circ> g ~ id B"
+ by (rule homotopy_transitive) (assumption+, typechk)
+ qed
+ done
+ done
+
+Lemma (derive) id_biinv:
+ "A: U i \<Longrightarrow> biinv (id A)"
+ by (rule qinv_imp_biinv) (rule id_qinv)
+
+Lemma (derive) funcomp_biinv:
+ assumes
+ "A: U i" "B: U i" "C: U i"
+ "f: A \<rightarrow> B" "g: B \<rightarrow> C"
+ shows "biinv f \<rightarrow> biinv g \<rightarrow> biinv (g \<circ> f)"
+ apply intros
+ focus vars biinv\<^sub>f biinv\<^sub>g
+
+ text \<open>Follows from \<open>funcomp_qinv\<close>.\<close>
+oops
+
+
+section \<open>Equivalence\<close>
+
+text \<open>
+ Following the HoTT book, we first define equivalence in terms of
+ bi-invertibility.
+\<close>
+
+definition equivalence (infix "\<simeq>" 110)
+ where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.biinv A B f"
+
+lemma equivalence_type [typechk]:
+ assumes "A: U i" "B: U i"
+ shows "A \<simeq> B: U i"
+ unfolding equivalence_def by typechk
+
+Lemma (derive) equivalence_refl:
+ assumes "A: U i"
+ shows "A \<simeq> A"
+ unfolding equivalence_def
+ apply intro defer
+ apply (rule qinv_imp_biinv) defer
+ apply (rule id_qinv)
+ done
+
+text \<open>
+ The following could perhaps be easier with transport (but then I think we need
+ univalence?)...
+\<close>
+
+Lemma (derive) equivalence_symmetric:
+ assumes "A: U i" "B: U i"
+ shows "A \<simeq> B \<rightarrow> B \<simeq> A"
+ apply intros
+ unfolding equivalence_def
+ apply elim
+ \<guillemotright> vars _ f "prf"
+ apply (dest (4) biinv_imp_qinv)
+ apply intro
+ \<^item> unfolding qinv_def by (rule fst[of "(biinv_imp_qinv A B f) prf"])
+ \<^item> by (rule qinv_imp_biinv) (rule quasiinv_qinv)
+ done
+ done
+
+Lemma (derive) equivalence_transitive:
+ assumes "A: U i" "B: U i" "C: U i"
+ shows "A \<simeq> B \<rightarrow> B \<simeq> C \<rightarrow> A \<simeq> C"
+ apply intros
+ unfolding equivalence_def
+
+ text \<open>Use \<open>funcomp_biinv\<close>.\<close>
+oops
+
+text \<open>
+ Equal types are equivalent. We give two proofs: the first by induction, and
+ the second by following the HoTT book and showing that transport is an
+ equivalence.
+\<close>
+
+Lemma
+ assumes
+ "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
+ shows "A \<simeq> B"
+ by (equality \<open>p:_\<close>) (rule equivalence_refl)
+
+text \<open>
+ The following proof is wordy because (1) the typechecker doesn't rewrite, and
+ (2) we don't yet have universe automation.
+\<close>
+
+Lemma (derive) id_imp_equiv:
+ assumes
+ "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
+ shows "<trans (id (U i)) p, ?isequiv>: A \<simeq> B"
+ unfolding equivalence_def
+ apply intros defer
+
+ \<comment> \<open>Switch off auto-typechecking, which messes with universe levels\<close>
+ supply [[auto_typechk=false]]
+
+ \<guillemotright> apply (equality \<open>p:_\<close>)
+ \<^item> premises vars A B
+ apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
+ apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
+ apply (rule transport, rule U_in_U)
+ apply (rule lift_universe_codomain, rule U_in_U)
+ apply (typechk, rule U_in_U)
+ done
+ \<^item> premises vars A
+ apply (subst transport_comp)
+ \<^enum> by (rule U_in_U)
+ \<^enum> by reduce (rule lift_universe)
+ \<^enum> by reduce (rule id_biinv)
+ done
+ done
+
+ \<guillemotright> \<comment> \<open>Similar proof as in the first subgoal above\<close>
+ apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
+ apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
+ apply (rule transport, rule U_in_U)
+ apply (rule lift_universe_codomain, rule U_in_U)
+ apply (typechk, rule U_in_U)
+ done
+ done
+
+(*Uncomment this to see all implicits from here on.
+no_translations
+ "f x" \<leftharpoondown> "f `x"
+ "x = y" \<leftharpoondown> "x =\<^bsub>A\<^esub> y"
+ "g \<circ> f" \<leftharpoondown> "g \<circ>\<^bsub>A\<^esub> f"
+ "p\<inverse>" \<leftharpoondown> "CONST pathinv A x y p"
+ "p \<bullet> q" \<leftharpoondown> "CONST pathcomp A x y z p q"
+ "fst" \<leftharpoondown> "CONST Spartan.fst A B"
+ "snd" \<leftharpoondown> "CONST Spartan.snd A B"
+ "f[p]" \<leftharpoondown> "CONST ap A B x y f p"
+ "trans P p" \<leftharpoondown> "CONST transport A P x y p"
+ "trans_const B p" \<leftharpoondown> "CONST transport_const A B x y p"
+ "lift P p u" \<leftharpoondown> "CONST pathlift A P x y p u"
+ "apd f p" \<leftharpoondown> "CONST Identity.apd A P f x y p"
+ "f ~ g" \<leftharpoondown> "CONST homotopy A B f g"
+ "qinv f" \<leftharpoondown> "CONST Equivalence.qinv A B f"
+ "biinv f" \<leftharpoondown> "CONST Equivalence.biinv A B f"
+*)
+
+
+end
diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy
new file mode 100644
index 0000000..0edf20e
--- /dev/null
+++ b/spartan/theories/Identity.thy
@@ -0,0 +1,433 @@
+chapter \<open>The identity type\<close>
+
+text \<open>
+ The identity type, the higher groupoid structure of types,
+ and type families as fibrations.
+\<close>
+
+theory Identity
+imports Spartan
+
+begin
+
+axiomatization
+ Id :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> and
+ refl :: \<open>o \<Rightarrow> o\<close> and
+ IdInd :: \<open>o \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close>
+
+syntax "_Id" :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2_ =\<^bsub>_\<^esub>/ _)" [111, 0, 111] 110)
+
+translations "a =\<^bsub>A\<^esub> b" \<rightleftharpoons> "CONST Id A a b"
+
+axiomatization where
+ IdF: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^bsub>A\<^esub> b: U i" and
+
+ IdI: "a: A \<Longrightarrow> refl a: a =\<^bsub>A\<^esub> a" and
+
+ IdE: "\<lbrakk>
+ p: a =\<^bsub>A\<^esub> b;
+ a: A;
+ b: A;
+ \<And>x y p. \<lbrakk>p: x =\<^bsub>A\<^esub> y; x: A; y: A\<rbrakk> \<Longrightarrow> C x y p: U i;
+ \<And>x. x: A \<Longrightarrow> f x: C x x (refl x)
+ \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a b p: C a b p" and
+
+ Id_comp: "\<lbrakk>
+ a: A;
+ \<And>x y p. \<lbrakk>x: A; y: A; p: x =\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow> C x y p: U i;
+ \<And>x. x: A \<Longrightarrow> f x: C x x (refl x)
+ \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a a (refl a) \<equiv> f a"
+
+lemmas
+ [intros] = IdF IdI and
+ [elims] = IdE and
+ [comps] = Id_comp
+
+
+section \<open>Induction\<close>
+
+ML_file \<open>../lib/equality.ML\<close>
+
+method_setup equality = \<open>Scan.lift Parse.thm >> (fn (fact, _) => fn ctxt =>
+ CONTEXT_METHOD (K (Equality.equality_context_tac fact ctxt)))\<close>
+
+
+section \<open>Symmetry and transitivity\<close>
+
+Lemma (derive) pathinv:
+ assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
+ shows "y =\<^bsub>A\<^esub> x"
+ by (equality \<open>p:_\<close>) intro
+
+lemma pathinv_comp [comps]:
+ assumes "x: A" "A: U i"
+ shows "pathinv A x x (refl x) \<equiv> refl x"
+ unfolding pathinv_def by reduce
+
+Lemma (derive) pathcomp:
+ assumes
+ "A: U i" "x: A" "y: A" "z: A"
+ "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z"
+ shows
+ "x =\<^bsub>A\<^esub> z"
+ apply (equality \<open>p:_\<close>)
+ focus premises vars x p
+ apply (equality \<open>p:_\<close>)
+ apply intro
+ done
+ done
+
+lemma pathcomp_comp [comps]:
+ assumes "a: A" "A: U i"
+ shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a"
+ unfolding pathcomp_def by reduce
+
+text \<open>Set up \<open>sym\<close> attribute for propositional equalities:\<close>
+
+ML \<open>
+structure Id_Sym_Attr = Sym_Attr (
+ struct
+ val name = "sym"
+ val symmetry_rule = @{thm pathinv[rotated 3]}
+ end
+)
+\<close>
+
+setup \<open>Id_Sym_Attr.setup\<close>
+
+
+section \<open>Notation\<close>
+
+definition Id_i (infix "=" 110)
+ where [implicit]: "Id_i x y \<equiv> x =\<^bsub>?\<^esub> y"
+
+definition pathinv_i ("_\<inverse>" [1000])
+ where [implicit]: "pathinv_i p \<equiv> pathinv ? ? ? p"
+
+definition pathcomp_i (infixl "\<bullet>" 121)
+ where [implicit]: "pathcomp_i p q \<equiv> pathcomp ? ? ? ? p q"
+
+translations
+ "x = y" \<leftharpoondown> "x =\<^bsub>A\<^esub> y"
+ "p\<inverse>" \<leftharpoondown> "CONST pathinv A x y p"
+ "p \<bullet> q" \<leftharpoondown> "CONST pathcomp A x y z p q"
+
+
+section \<open>Basic propositional equalities\<close>
+
+(*TODO: Better integration of equality type directly into reasoning...*)
+
+Lemma (derive) pathcomp_left_refl:
+ assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
+ shows "(refl x) \<bullet> p = p"
+ apply (equality \<open>p:_\<close>)
+ apply (reduce; intros)
+ done
+
+Lemma (derive) pathcomp_right_refl:
+ assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
+ shows "p \<bullet> (refl y) = p"
+ apply (equality \<open>p:_\<close>)
+ apply (reduce; intros)
+ done
+
+Lemma (derive) pathcomp_left_inv:
+ assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
+ shows "p\<inverse> \<bullet> p = refl y"
+ apply (equality \<open>p:_\<close>)
+ apply (reduce; intros)
+ done
+
+Lemma (derive) pathcomp_right_inv:
+ assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
+ shows "p \<bullet> p\<inverse> = refl x"
+ apply (equality \<open>p:_\<close>)
+ apply (reduce; intros)
+ done
+
+Lemma (derive) pathinv_pathinv:
+ assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
+ shows "p\<inverse>\<inverse> = p"
+ apply (equality \<open>p:_\<close>)
+ apply (reduce; intros)
+ done
+
+Lemma (derive) pathcomp_assoc:
+ assumes
+ "A: U i" "x: A" "y: A" "z: A" "w: A"
+ "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" "r: z =\<^bsub>A\<^esub> w"
+ shows "p \<bullet> (q \<bullet> r) = p \<bullet> q \<bullet> r"
+ apply (equality \<open>p:_\<close>)
+ focus premises vars x p
+ apply (equality \<open>p:_\<close>)
+ focus premises vars x p
+ apply (equality \<open>p:_\<close>)
+ apply (reduce; intros)
+ done
+ done
+ done
+
+
+section \<open>Functoriality of functions\<close>
+
+Lemma (derive) ap:
+ assumes
+ "A: U i" "B: U i"
+ "x: A" "y: A"
+ "f: A \<rightarrow> B"
+ "p: x =\<^bsub>A\<^esub> y"
+ shows "f x = f y"
+ apply (equality \<open>p:_\<close>)
+ apply intro
+ done
+
+definition ap_i ("_[_]" [1000, 0])
+ where [implicit]: "ap_i f p \<equiv> ap ? ? ? ? f p"
+
+translations "f[p]" \<leftharpoondown> "CONST ap A B x y f p"
+
+Lemma ap_refl [comps]:
+ assumes "f: A \<rightarrow> B" "x: A" "A: U i" "B: U i"
+ shows "f[refl x] \<equiv> refl (f x)"
+ unfolding ap_def by reduce
+
+Lemma (derive) ap_pathcomp:
+ assumes
+ "A: U i" "B: U i"
+ "x: A" "y: A" "z: A"
+ "f: A \<rightarrow> B"
+ "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z"
+ shows
+ "f[p \<bullet> q] = f[p] \<bullet> f[q]"
+ apply (equality \<open>p:_\<close>)
+ focus premises vars x p
+ apply (equality \<open>p:_\<close>)
+ apply (reduce; intro)
+ done
+ done
+
+Lemma (derive) ap_pathinv:
+ assumes
+ "A: U i" "B: U i"
+ "x: A" "y: A"
+ "f: A \<rightarrow> B"
+ "p: x =\<^bsub>A\<^esub> y"
+ shows "f[p\<inverse>] = f[p]\<inverse>"
+ by (equality \<open>p:_\<close>) (reduce; intro)
+
+text \<open>The next two proofs currently use some low-level rewriting.\<close>
+
+Lemma (derive) ap_funcomp:
+ assumes
+ "A: U i" "B: U i" "C: U i"
+ "x: A" "y: A"
+ "f: A \<rightarrow> B" "g: B \<rightarrow> C"
+ "p: x =\<^bsub>A\<^esub> y"
+ shows "(g \<circ> f)[p] = g[f[p]]"
+ apply (equality \<open>p:_\<close>)
+ apply (simp only: funcomp_apply_comp[symmetric])
+ apply (reduce; intro)
+ done
+
+Lemma (derive) ap_id:
+ assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
+ shows "(id A)[p] = p"
+ apply (equality \<open>p:_\<close>)
+ apply (rewrite at "\<hole> = _" id_comp[symmetric])
+ apply (rewrite at "_ = \<hole>" id_comp[symmetric])
+ apply (reduce; intros)
+ done
+
+
+section \<open>Transport\<close>
+
+Lemma (derive) transport:
+ assumes
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ "x: A" "y: A"
+ "p: x =\<^bsub>A\<^esub> y"
+ shows "P x \<rightarrow> P y"
+ by (equality \<open>p:_\<close>) intro
+
+definition transport_i ("trans")
+ where [implicit]: "trans P p \<equiv> transport ? P ? ? p"
+
+translations "trans P p" \<leftharpoondown> "CONST transport A P x y p"
+
+Lemma transport_comp [comps]:
+ assumes
+ "a: A"
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ shows "trans P (refl a) \<equiv> id (P a)"
+ unfolding transport_def id_def by reduce
+
+\<comment> \<open>TODO: Build transport automation!\<close>
+
+Lemma use_transport:
+ assumes
+ "p: y =\<^bsub>A\<^esub> x"
+ "u: P x"
+ "x: A" "y: A"
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ shows "trans P p\<inverse> u: P y"
+ by typechk
+
+Lemma (derive) transport_left_inv:
+ assumes
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ "x: A" "y: A"
+ "p: x =\<^bsub>A\<^esub> y"
+ shows "(trans P p\<inverse>) \<circ> (trans P p) = id (P x)"
+ by (equality \<open>p:_\<close>) (reduce; intro)
+
+Lemma (derive) transport_right_inv:
+ assumes
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ "x: A" "y: A"
+ "p: x =\<^bsub>A\<^esub> y"
+ shows "(trans P p) \<circ> (trans P p\<inverse>) = id (P y)"
+ by (equality \<open>p:_\<close>) (reduce; intros)
+
+Lemma (derive) transport_pathcomp:
+ assumes
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ "x: A" "y: A" "z: A"
+ "u: P x"
+ "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z"
+ shows "trans P q (trans P p u) = trans P (p \<bullet> q) u"
+ apply (equality \<open>p:_\<close>)
+ focus premises vars x p
+ apply (equality \<open>p:_\<close>)
+ apply (reduce; intros)
+ done
+ done
+
+Lemma (derive) transport_compose_typefam:
+ assumes
+ "A: U i" "B: U i"
+ "\<And>x. x: B \<Longrightarrow> P x: U i"
+ "f: A \<rightarrow> B"
+ "x: A" "y: A"
+ "p: x =\<^bsub>A\<^esub> y"
+ "u: P (f x)"
+ shows "trans (\<lambda>x. P (f x)) p u = trans P f[p] u"
+ by (equality \<open>p:_\<close>) (reduce; intros)
+
+Lemma (derive) transport_function_family:
+ assumes
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ "\<And>x. x: A \<Longrightarrow> Q x: U i"
+ "f: \<Prod>x: A. P x \<rightarrow> Q x"
+ "x: A" "y: A"
+ "u: P x"
+ "p: x =\<^bsub>A\<^esub> y"
+ shows "trans Q p ((f x) u) = (f y) (trans P p u)"
+ by (equality \<open>p:_\<close>) (reduce; intros)
+
+Lemma (derive) transport_const:
+ assumes
+ "A: U i" "B: U i"
+ "x: A" "y: A"
+ "p: x =\<^bsub>A\<^esub> y"
+ shows "\<Prod>b: B. trans (\<lambda>_. B) p b = b"
+ by (intro, equality \<open>p:_\<close>) (reduce; intro)
+
+definition transport_const_i ("trans'_const")
+ where [implicit]: "trans_const B p \<equiv> transport_const ? B ? ? p"
+
+translations "trans_const B p" \<leftharpoondown> "CONST transport_const A B x y p"
+
+Lemma transport_const_comp [comps]:
+ assumes
+ "x: A" "b: B"
+ "A: U i" "B: U i"
+ shows "trans_const B (refl x) b\<equiv> refl b"
+ unfolding transport_const_def by reduce
+
+Lemma (derive) pathlift:
+ assumes
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ "x: A" "y: A"
+ "p: x =\<^bsub>A\<^esub> y"
+ "u: P x"
+ shows "<x, u> = <y, trans P p u>"
+ by (equality \<open>p:_\<close>) (reduce; intros)
+
+definition pathlift_i ("lift")
+ where [implicit]: "lift P p u \<equiv> pathlift ? P ? ? p u"
+
+translations "lift P p u" \<leftharpoondown> "CONST pathlift A P x y p u"
+
+Lemma pathlift_comp [comps]:
+ assumes
+ "u: P x"
+ "x: A"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ "A: U i"
+ shows "lift P (refl x) u \<equiv> refl <x, u>"
+ unfolding pathlift_def by reduce
+
+Lemma (derive) pathlift_fst:
+ assumes
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ "x: A" "y: A"
+ "u: P x"
+ "p: x =\<^bsub>A\<^esub> y"
+ shows "fst[lift P p u] = p"
+ apply (equality \<open>p:_\<close>)
+ text \<open>Some rewriting needed here:\<close>
+ \<guillemotright> vars x y
+ (*Here an automatic reordering tactic would be helpful*)
+ apply (rewrite at x in "x = y" fst_comp[symmetric])
+ prefer 4
+ apply (rewrite at y in "_ = y" fst_comp[symmetric])
+ done
+ \<guillemotright> by reduce intro
+ done
+
+
+section \<open>Dependent paths\<close>
+
+Lemma (derive) apd:
+ assumes
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ "f: \<Prod>x: A. P x"
+ "x: A" "y: A"
+ "p: x =\<^bsub>A\<^esub> y"
+ shows "trans P p (f x) = f y"
+ by (equality \<open>p:_\<close>) (reduce; intros; typechk)
+
+definition apd_i ("apd")
+ where [implicit]: "apd f p \<equiv> Identity.apd ? ? f ? ? p"
+
+translations "apd f p" \<leftharpoondown> "CONST Identity.apd A P f x y p"
+
+Lemma dependent_map_comp [comps]:
+ assumes
+ "f: \<Prod>x: A. P x"
+ "x: A"
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> P x: U i"
+ shows "apd f (refl x) \<equiv> refl (f x)"
+ unfolding apd_def by reduce
+
+Lemma (derive) apd_ap:
+ assumes
+ "A: U i" "B: U i"
+ "f: A \<rightarrow> B"
+ "x: A" "y: A"
+ "p: x =\<^bsub>A\<^esub> y"
+ shows "apd f p = trans_const B p (f x) \<bullet> f[p]"
+ by (equality \<open>p:_\<close>) (reduce; intro)
+
+end
diff --git a/spartan/theories/Spartan.thy b/spartan/theories/Spartan.thy
new file mode 100644
index 0000000..fb901d5
--- /dev/null
+++ b/spartan/theories/Spartan.thy
@@ -0,0 +1,463 @@
+text \<open>Spartan type theory\<close>
+
+theory Spartan
+imports
+ Pure
+ "HOL-Eisbach.Eisbach"
+ "HOL-Eisbach.Eisbach_Tools"
+keywords
+ "Theorem" "Lemma" "Corollary" "Proposition" :: thy_goal_stmt and
+ "focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and
+ "derive" "vars":: quasi_command and
+ "print_coercions" :: thy_decl
+
+begin
+
+
+section \<open>Preamble\<close>
+
+declare [[eta_contract=false]]
+
+
+section \<open>Metatype setup\<close>
+
+typedecl o
+
+
+section \<open>Judgments\<close>
+
+judgment has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999)
+
+
+section \<open>Universes\<close>
+
+typedecl lvl \<comment> \<open>Universe levels\<close>
+
+axiomatization
+ O :: \<open>lvl\<close> and
+ S :: \<open>lvl \<Rightarrow> lvl\<close> and
+ lt :: \<open>lvl \<Rightarrow> lvl \<Rightarrow> prop\<close> (infix "<" 900)
+ where
+ O_min: "O < S i" and
+ lt_S: "i < S i" and
+ lt_trans: "i < j \<Longrightarrow> j < k \<Longrightarrow> i < k"
+
+axiomatization U :: \<open>lvl \<Rightarrow> o\<close> where
+ U_hierarchy: "i < j \<Longrightarrow> U i: U j" and
+ U_cumulative: "A: U i \<Longrightarrow> i < j \<Longrightarrow> A: U j"
+
+lemma U_in_U:
+ "U i: U (S i)"
+ by (rule U_hierarchy, rule lt_S)
+
+lemma lift_universe:
+ "A: U i \<Longrightarrow> A: U (S i)"
+ by (erule U_cumulative, rule lt_S)
+
+
+section \<open>\<Prod>-type\<close>
+
+axiomatization
+ Pi :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o\<close> and
+ lam :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o\<close> and
+ app :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("(1_ `_)" [120, 121] 120)
+
+syntax
+ "_Pi" :: \<open>idt \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<Prod>_: _./ _)" 30)
+ "_lam" :: \<open>idt \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<lambda>_: _./ _)" 30)
+translations
+ "\<Prod>x: A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)"
+ "\<lambda>x: A. b" \<rightleftharpoons> "CONST lam A (\<lambda>x. b)"
+
+abbreviation Fn (infixr "\<rightarrow>" 40) where "A \<rightarrow> B \<equiv> \<Prod>_: A. B"
+
+axiomatization where
+ PiF: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; A: U i\<rbrakk> \<Longrightarrow> \<Prod>x: A. B x: U i" and
+
+ PiI: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x: \<Prod>x: A. B x" and
+
+ PiE: "\<lbrakk>f: \<Prod>x: A. B x; a: A\<rbrakk> \<Longrightarrow> f `a: B a" and
+
+ beta: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> (\<lambda>x: A. b x) `a \<equiv> b a" and
+
+ eta: "f: \<Prod>x: A. B x \<Longrightarrow> \<lambda>x: A. f `x \<equiv> f" and
+
+ Pi_cong: "\<lbrakk>
+ A: U i;
+ \<And>x. x: A \<Longrightarrow> B x: U i;
+ \<And>x. x: A \<Longrightarrow> B' x: U i;
+ \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x
+ \<rbrakk> \<Longrightarrow> \<Prod>x: A. B x \<equiv> \<Prod>x: A. B' x" and
+
+ 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"
+
+
+section \<open>\<Sum>-type\<close>
+
+axiomatization
+ Sig :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o\<close> and
+ pair :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("(2<_,/ _>)") and
+ SigInd :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close>
+
+syntax "_Sum" :: \<open>idt \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<Sum>_: _./ _)" 20)
+
+translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (\<lambda>x. B)"
+
+abbreviation Prod (infixl "\<times>" 50)
+ where "A \<times> B \<equiv> \<Sum>_: A. B"
+
+axiomatization where
+ SigF: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; A: U i\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x: U i" and
+
+ SigI: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a, b>: \<Sum>x: A. B x" and
+
+ SigE: "\<lbrakk>
+ p: \<Sum>x: A. B x;
+ A: U i;
+ \<And>x. x : A \<Longrightarrow> B x: U i;
+ \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i;
+ \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>
+ \<rbrakk> \<Longrightarrow> SigInd A (\<lambda>x. B x) (\<lambda>p. C p) f p: C p" and
+
+ Sig_comp: "\<lbrakk>
+ a: A;
+ b: B a;
+ \<And>x. x: A \<Longrightarrow> B x: U i;
+ \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i;
+ \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>
+ \<rbrakk> \<Longrightarrow> SigInd A (\<lambda>x. B x) (\<lambda>p. C p) f <a, b> \<equiv> f a b" and
+
+ Sig_cong: "\<lbrakk>
+ \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x;
+ A: U i;
+ \<And>x. x : A \<Longrightarrow> B x: U i;
+ \<And>x. x : A \<Longrightarrow> B' x: U i
+ \<rbrakk> \<Longrightarrow> \<Sum>x: A. B x \<equiv> \<Sum>x: A. B' x"
+
+
+
+
+
+section \<open>Proof commands\<close>
+
+named_theorems typechk
+
+ML_file \<open>../lib/lib.ML\<close>
+ML_file \<open>../lib/goals.ML\<close>
+ML_file \<open>../lib/focus.ML\<close>
+
+
+section \<open>Congruence automation\<close>
+
+ML_file \<open>../lib/congruence.ML\<close>
+
+
+section \<open>Methods\<close>
+
+ML_file \<open>../lib/elimination.ML\<close> \<comment> \<open>declares the [elims] attribute\<close>
+
+named_theorems intros and comps
+lemmas
+ [intros] = PiF PiI SigF SigI and
+ [elims] = PiE SigE and
+ [comps] = beta Sig_comp and
+ [cong] = Pi_cong lam_cong Sig_cong
+
+ML_file \<open>../lib/tactics.ML\<close>
+
+method_setup assumptions =
+ \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (
+ CHANGED (TRYALL (assumptions_tac ctxt))))\<close>
+
+method_setup known =
+ \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (
+ CHANGED (TRYALL (known_tac ctxt))))\<close>
+
+method_setup intro =
+ \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intro_tac ctxt)))\<close>
+
+method_setup intros =
+ \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\<close>
+
+method_setup elim =
+ \<open>Scan.option Args.term >> (fn tm => fn ctxt =>
+ SIMPLE_METHOD' (SIDE_CONDS (elims_tac tm ctxt) ctxt))\<close>
+
+method elims = elim+
+
+method_setup typechk =
+ \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (
+ CHANGED (ALLGOALS (TRY o typechk_tac ctxt))))\<close>
+
+method_setup rule =
+ \<open>Attrib.thms >> (fn ths => fn ctxt =>
+ SIMPLE_METHOD (HEADGOAL (rule_tac ths ctxt)))\<close>
+
+method_setup dest =
+ \<open>Scan.lift (Scan.option (Args.parens Parse.int)) -- Attrib.thms
+ >> (fn (opt_n, ths) => fn ctxt =>
+ SIMPLE_METHOD (HEADGOAL (dest_tac opt_n ths ctxt)))\<close>
+
+subsection \<open>Rewriting\<close>
+
+\<comment> \<open>\<open>subst\<close> method\<close>
+ML_file "~~/src/Tools/misc_legacy.ML"
+ML_file "~~/src/Tools/IsaPlanner/isand.ML"
+ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
+ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
+ML_file "../lib/eqsubst.ML"
+
+\<comment> \<open>\<open>rewrite\<close> method\<close>
+consts rewrite_HOLE :: "'a::{}" ("\<hole>")
+
+lemma eta_expand:
+ fixes f :: "'a::{} \<Rightarrow> 'b::{}"
+ shows "f \<equiv> \<lambda>x. f x" .
+
+lemma rewr_imp:
+ assumes "PROP A \<equiv> PROP B"
+ shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> PROP C)"
+ apply (rule Pure.equal_intr_rule)
+ apply (drule equal_elim_rule2[OF assms]; assumption)
+ apply (drule equal_elim_rule1[OF assms]; assumption)
+ done
+
+lemma imp_cong_eq:
+ "(PROP A \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv>
+ ((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))"
+ apply (Pure.intro Pure.equal_intr_rule)
+ apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
+ apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
+ done
+
+ML_file \<open>~~/src/HOL/Library/cconv.ML\<close>
+ML_file \<open>../lib/rewrite.ML\<close>
+
+\<comment> \<open>\<open>reduce\<close> method computes terms via judgmental equalities\<close>
+setup \<open>
+ map_theory_simpset (fn ctxt =>
+ ctxt addSolver (mk_solver "" typechk_tac))
+\<close>
+
+method reduce uses add = (simp add: comps add | subst comps, reduce add: add)+
+
+
+section \<open>Implicit notations\<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>../lib/implicits.ML\<close>
+
+attribute_setup implicit = \<open>Scan.succeed Implicits.implicit_defs_attr\<close>
+
+ML \<open>
+val _ = Context.>>
+ (Syntax_Phases.term_check 1 "" (fn ctxt => map (Implicits.make_holes ctxt)))
+\<close>
+
+text \<open>Automatically insert inhabitation judgments where needed:\<close>
+
+consts inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
+translations "CONST inhabited A" \<rightharpoonup> "CONST has_type {} A"
+
+
+section \<open>Lambda coercion\<close>
+
+\<comment> \<open>Coerce object lambdas to meta-lambdas\<close>
+abbreviation (input) lambda :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close>
+ where "lambda f \<equiv> \<lambda>x. f `x"
+
+ML_file \<open>~~/src/Tools/subtyping.ML\<close>
+declare [[coercion_enabled, coercion lambda]]
+
+translations "f x" \<leftharpoondown> "f `x"
+
+
+section \<open>Functions\<close>
+
+lemma eta_exp:
+ assumes "f: \<Prod>x: A. B x"
+ shows "f \<equiv> \<lambda>x: A. f x"
+ by (rule eta[symmetric])
+
+lemma lift_universe_codomain:
+ assumes "A: U i" "f: A \<rightarrow> U j"
+ shows "f: A \<rightarrow> U (S j)"
+ apply (sub eta_exp)
+ apply known
+ apply (Pure.rule intros; rule lift_universe)
+ done
+
+subsection \<open>Function composition\<close>
+
+definition "funcomp A g f \<equiv> \<lambda>x: A. g `(f `x)"
+
+syntax
+ "_funcomp" :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2_ \<circ>\<^bsub>_\<^esub>/ _)" [111, 0, 110] 110)
+translations
+ "g \<circ>\<^bsub>A\<^esub> f" \<rightleftharpoons> "CONST funcomp A g f"
+
+lemma funcompI [typechk]:
+ assumes
+ "A: U i"
+ "B: U i"
+ "\<And>x. x: B \<Longrightarrow> C x: U i"
+ "f: A \<rightarrow> B"
+ "g: \<Prod>x: B. C x"
+ shows
+ "g \<circ>\<^bsub>A\<^esub> f: \<Prod>x: A. C (f x)"
+ unfolding funcomp_def by typechk
+
+lemma funcomp_assoc [comps]:
+ assumes
+ "f: A \<rightarrow> B"
+ "g: B \<rightarrow> C"
+ "h: \<Prod>x: C. D x"
+ "A: U i"
+ 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
+
+lemma funcomp_lambda_comp [comps]:
+ assumes
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> b x: B"
+ "\<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
+
+lemma funcomp_apply_comp [comps]:
+ assumes
+ "f: A \<rightarrow> B" "g: \<Prod>x: B. C x"
+ "x: A"
+ "A: U i" "B: U i"
+ "\<And>x y. x: B \<Longrightarrow> C x: U i"
+ shows "(g \<circ>\<^bsub>A\<^esub> f) x \<equiv> g (f x)"
+ unfolding funcomp_def by reduce
+
+text \<open>Notation:\<close>
+
+definition funcomp_i (infixr "\<circ>" 120)
+ where [implicit]: "funcomp_i g f \<equiv> g \<circ>\<^bsub>?\<^esub> f"
+
+translations "g \<circ> f" \<leftharpoondown> "g \<circ>\<^bsub>A\<^esub> f"
+
+subsection \<open>Identity function\<close>
+
+definition id where "id A \<equiv> \<lambda>x: A. x"
+
+lemma
+ idI [typechk]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and
+ id_comp [comps]: "x: A \<Longrightarrow> (id A) x \<equiv> x"
+ unfolding id_def by reduce
+
+lemma id_left [comps]:
+ assumes "f: A \<rightarrow> B" "A: U i" "B: U i"
+ shows "(id B) \<circ>\<^bsub>A\<^esub> f \<equiv> f"
+ unfolding id_def
+ by (subst eta_exp[of f]) (reduce, rule eta)
+
+lemma id_right [comps]:
+ assumes "f: A \<rightarrow> B" "A: U i" "B: U i"
+ shows "f \<circ>\<^bsub>A\<^esub> (id A) \<equiv> f"
+ unfolding id_def
+ by (subst eta_exp[of f]) (reduce, rule eta)
+
+lemma id_U [typechk]:
+ "id (U i): U i \<rightarrow> U i"
+ by typechk (fact U_in_U)
+
+
+section \<open>Pairs\<close>
+
+definition "fst A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (\<lambda>_. A) (\<lambda>x y. x) p"
+definition "snd A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (\<lambda>p. B (fst A B p)) (\<lambda>x y. y) p"
+
+lemma fst_type [typechk]:
+ assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+ shows "fst A B: (\<Sum>x: A. B x) \<rightarrow> A"
+ unfolding fst_def by typechk
+
+lemma fst_comp [comps]:
+ assumes
+ "a: A"
+ "b: B a"
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> B x: U i"
+ shows "fst A B <a, b> \<equiv> a"
+ unfolding fst_def by reduce
+
+lemma snd_type [typechk]:
+ assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+ shows "snd A B: \<Prod>p: \<Sum>x: A. B x. B (fst A B p)"
+ unfolding snd_def by typechk reduce
+
+lemma snd_comp [comps]:
+ assumes "a: A" "b: B a" "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+ shows "snd A B <a, b> \<equiv> b"
+ unfolding snd_def by reduce
+
+subsection \<open>Notation\<close>
+
+definition fst_i ("fst")
+ where [implicit]: "fst \<equiv> Spartan.fst ? ?"
+
+definition snd_i ("snd")
+ where [implicit]: "snd \<equiv> Spartan.snd ? ?"
+
+translations
+ "fst" \<leftharpoondown> "CONST Spartan.fst A B"
+ "snd" \<leftharpoondown> "CONST Spartan.snd A B"
+
+subsection \<open>Projections\<close>
+
+Lemma fst [typechk]:
+ assumes
+ "p: \<Sum>x: A. B x"
+ "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+ shows "fst p: A"
+ by typechk
+
+Lemma snd [typechk]:
+ assumes
+ "p: \<Sum>x: A. B x"
+ "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
+ shows "snd p: B (fst p)"
+ by typechk
+
+method fst for p::o = rule fst[of p]
+method snd for p::o = rule snd[of p]
+
+subsection \<open>Properties of \<Sigma>\<close>
+
+Lemma (derive) Sig_dist_exp:
+ assumes
+ "p: \<Sum>x: A. B x \<times> C x"
+ "A: U i"
+ "\<And>x. x: A \<Longrightarrow> B x: U i"
+ "\<And>x. x: A \<Longrightarrow> C x: U i"
+ shows "(\<Sum>x: A. B x) \<times> (\<Sum>x: A. C x)"
+ apply (elim p)
+ focus vars x y
+ apply intro
+ \<guillemotright> apply intro
+ apply assumption
+ apply (fst y)
+ done
+ \<guillemotright> apply intro
+ apply assumption
+ apply (snd y)
+ done
+ done
+ done
+
+
+end