diff options
| -rw-r--r-- | mltt/core/MLTT.thy | 15 | ||||
| -rw-r--r-- | mltt/core/comp.ML | 2 | ||||
| -rw-r--r-- | mltt/core/elaborated_statement.ML | 8 | ||||
| -rw-r--r-- | mltt/core/focus.ML | 2 | ||||
| -rw-r--r-- | mltt/core/lib.ML | 5 |
5 files changed, 20 insertions, 12 deletions
diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy index 96cbe96..ec923e2 100644 --- a/mltt/core/MLTT.thy +++ b/mltt/core/MLTT.thy @@ -25,11 +25,11 @@ let val typ = Simple_Syntax.read_typ fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range) in - Sign.del_syntax (Print_Mode.ASCII, true) + Sign.syntax false (Print_Mode.ASCII, true) [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3%_./ _)", [0, 3], 3))] - #> Sign.del_syntax Syntax.mode_default + #> Sign.syntax false Syntax.mode_default [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3\<lambda>_./ _)", [0, 3], 3))] - #> Sign.add_syntax Syntax.mode_default + #> Sign.syntax true Syntax.mode_default [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3fn _./ _)", [0, 3], 3))] end \<close> @@ -309,10 +309,16 @@ subsection \<open>Trivial proofs (modulo automatic discharge of side conditions) method_setup this = \<open>Scan.succeed (K (CONTEXT_METHOD (fn facts => CHEADGOAL (SIDE_CONDS 0 - (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts)) + (CONTEXT_TACTIC' (fn ctxt => simp_tac (ctxt addsimps facts))) facts))))\<close> +method_setup infer = + \<open>Scan.succeed (K (CONTEXT_METHOD (fn facts => + CHEADGOAL (SIDE_CONDS 0 + (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts)) + facts))))\<close> + subsection \<open>Rewriting\<close> consts compute_hole :: "'a::{}" ("\<hole>") @@ -564,5 +570,4 @@ Lemma (def) distribute_Sig: by typechk+ qed - end diff --git a/mltt/core/comp.ML b/mltt/core/comp.ML index 2e50753..8725ba3 100644 --- a/mltt/core/comp.ML +++ b/mltt/core/comp.ML @@ -279,7 +279,7 @@ fun comps_pconv to thms ctxt (tyenv, env_ts) = ((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 + in Drule.instantiate_normalize (TVars.make tyinsts, Vars.make insts) thm end fun unify_with_rhs context to env thm = let diff --git a/mltt/core/elaborated_statement.ML b/mltt/core/elaborated_statement.ML index 33f88cf..2e129c8 100644 --- a/mltt/core/elaborated_statement.ML +++ b/mltt/core/elaborated_statement.ML @@ -95,12 +95,14 @@ fun inst_morphism params ((prfx, mandatory), insts') ctxt = (*instantiation*) val instT = (type_parms ~~ map Logic.dest_type type_parms'') - |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T)); + |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T)) + |> TFrees.make; val cert_inst = ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'') - |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t)); + |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t)) + |> Frees.make; in - (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $> + (Element.instantiate_normalize_morphism (TFrees.map (K certT) instT, cert_inst) $> Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt') end; diff --git a/mltt/core/focus.ML b/mltt/core/focus.ML index b963cfe..ac4de08 100644 --- a/mltt/core/focus.ML +++ b/mltt/core/focus.ML @@ -36,7 +36,7 @@ fun gen_focus ctxt i bindings raw_st = |> apfst rev |> apsnd reverse_prems val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of (asms')) ctxt2 - val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst) + val schematic_terms = Vars.map (fn _ => fn b => Thm.cterm_of ctxt3 b) (#2 inst) val schematics = (schematic_types, schematic_terms) val asms' = map (Thm.instantiate_cterm schematics) asms' val concl' = Thm.instantiate_cterm schematics concl' diff --git a/mltt/core/lib.ML b/mltt/core/lib.ML index 98d83cc..6949de6 100644 --- a/mltt/core/lib.ML +++ b/mltt/core/lib.ML @@ -113,9 +113,10 @@ fun decompose_goal ctxt goal = let val focus = #1 (Subgoal.focus_prems ctxt 1 NONE (Thm.trivial (Thm.cterm_of ctxt goal))) - val schematics = #2 (#schematics focus) - |> map (fn (v, ctm) => (Thm.term_of ctm, Var v)) + |> Vars.map (fn v => fn ctm => (Thm.term_of ctm, Var v)) + |> Vars.dest + |> map snd in map Thm.prop_of (#prems focus) @ [Thm.term_of (#concl focus)] |> map (subst_free schematics) |