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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
structure Lib :
sig
(*Lists*)
val max: ('a * 'a -> bool) -> 'a list -> 'a
val maxint: int list -> int
(*Terms*)
val no_vars: term -> bool
val is_rigid: term -> bool
val is_eq: term -> bool
val dest_prop: term -> term
val dest_eq: term -> term * term
val mk_Var: string -> int -> typ -> term
val lambda_var: term -> term -> term
val is_lvl: term -> bool
val is_typing: term -> bool
val mk_typing: term -> term -> term
val dest_typing: term -> term * term
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 decompose_goal: Proof.context -> term -> term list * term
val rigid_typing_concl: term -> bool
(*Theorems*)
val partition_judgments: thm list -> thm list * thm list * thm list
(*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 lvl_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 no_vars = not o exists_subterm is_Var
val is_rigid = not o is_Var o head_of
fun is_eq (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _) = true
| is_eq _ = false
fun dest_prop (Const (\<^const_name>\<open>Pure.prop\<close>, _) $ P) = P
| dest_prop P = P
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_lvl t = case fastype_of t of Type (\<^type_name>\<open>lvl\<close>, _) => true | _ => false
fun is_typing (Const (\<^const_name>\<open>has_type\<close>, _) $ _ $ _) = true
| is_typing _ = false
fun mk_typing t T = \<^const>\<open>has_type\<close> $ t $ T
fun dest_typing (Const (\<^const_name>\<open>has_type\<close>, _) $ t $ T) = (t, T)
| dest_typing t = raise TERM ("dest_typing", [t])
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>)
(*The above is a bit hacky; basically we need to guarantee that the schematic
var is fresh. This works for now because no other code in the Isabelle system
or the current logic uses this identifier.*)
(** Goals **)
(*Breaks a goal \<And>x ... y. \<lbrakk>P1; ... Pn\<rbrakk> \<Longrightarrow> Q into ([P1, ..., Pn], Q), fixing
\<And>-quantified variables and keeping schematics.*)
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))
in
map Thm.prop_of (#prems focus) @ [Thm.term_of (#concl focus)]
|> map (subst_free schematics)
|> (fn xs => chop (length xs - 1) xs) |> apsnd the_single
end
handle List.Empty => error "Lib.decompose_goal"
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
(** Theorems **)
fun partition_judgments ths =
let
fun part [] facts conds eqs = (facts, conds, eqs)
| part (th::ths) facts conds eqs =
if is_typing (Thm.prop_of th) then
part ths (th::facts) conds eqs
else if is_typing (Thm.concl_of th) then
part ths facts (th::conds) eqs
else part ths facts conds (th::eqs)
in part ths [] [] [] 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 lvl_order t1 t2 =
case fastype_of t1 of
Type (\<^type_name>\<open>lvl\<close>, _) => (case fastype_of t2 of
Type (\<^type_name>\<open>lvl\<close>, _) => EQUAL
| Type (_, _) => LESS
| _ => EQUAL)
| Type (_, _) => (case fastype_of t2 of
Type (\<^type_name>\<open>lvl\<close>, _) => GREATER
| _ => EQUAL)
| _ => EQUAL
fun cond_order o1 o2 = case o1 of EQUAL => o2 | _ => o1
end
|
