1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
(********
Isabelle/HoTT: util.ML
Feb 2019
Libary of various helper functions.
********)
signature UTIL =
sig
(* Lexical functions *)
val unmark: string -> string
(* Functions on terms *)
val prep_term: Proof.context -> term -> term
(* General functions *)
val get_all_thms: Proof.context -> (string * thm) list
val find_thm: Proof.context -> string -> (string * thm) list
(* Get specific theorems *)
val get_this: Proof.context -> thm list
val get_assms: Proof.context -> thm list
end
structure Util: UTIL =
struct
fun unmark s =
Lexicon.unmark_class s
handle Fail "unprefix" =>
Lexicon.unmark_type s
handle Fail "unprefix" =>
Lexicon.unmark_const s
handle Fail "unprefix" =>
Lexicon.unmark_fixed s
handle Fail "unprefix" =>
s
fun name_and_thm (fact, thm) =
((case fact of
Facts.Named ((name, _), _) => name
| Facts.Fact name => name),
thm)
fun get_all_thms ctxt =
let val (_, ref_thms) = Find_Theorems.find_theorems ctxt NONE NONE true []
in ref_thms |> (map name_and_thm)
end
(* Search all visible theorems (including local assumptions) containing a given name *)
fun find_thm ctxt name =
let val (_, ref_thms) =
Find_Theorems.find_theorems ctxt NONE NONE true [(true, Find_Theorems.Name name)]
in
ref_thms |> (map name_and_thm)
end
(* Get the fact corresponding to the Isar term "this" in the current proof scope *)
fun get_this ctxt =
Proof_Context.get_fact ctxt (Facts.named "local.this")
handle ERROR "Undefined fact: \"local.this\"" => (
if (Config.get ctxt trace) then warning "\"this\" undefined in the context" else ();
[]
)
(* Get all visible assumptions in the current proof scope.
This includes the facts introduced in the statement of the goal using "assumes",
as well as all facts introduced using "assume" that are visible in the current block.
*)
val get_assms = Assumption.all_prems_of
(* Prepare a Pure pre-term, converting it to a (unchecked) term *)
fun prep_term ctxt ptm =
let val ptm = Term_Position.strip_positions ptm
in
(case ptm of
Const ("_constrain", _) $ Free (t, _) $
(Const ("\<^type>fun", _) $ Const(typ1, _) $ Const (typ2, _)) =>
let
val typ1 = Lexicon.unmark_type typ1
val typ2 = Lexicon.unmark_type typ2
val typ = typ1 ^ "\<Rightarrow>" ^ typ2 |> Syntax.read_typ ctxt
in Free (t, typ) end
| Const ("_constrain", _) $ t $ Const (typ, _) =>
let
val T = Syntax.read_typ ctxt (Lexicon.unmark_type typ)
in
case t of
Free (s, _) => Free (s, T)
| Const (s, _) => Const (Lexicon.unmark_const s, T)
| _ => Exn.error "Unimplemented term constraint handler"
end
| ptm1 $ ptm2 =>
(prep_term ctxt ptm1) $ (prep_term ctxt ptm2)
| Abs (t, T, ptm') =>
Abs (t, T, prep_term ctxt ptm')
| Const (t, T) => Const (unmark t, T)
| t => t)
end
end
|
