equal
deleted
inserted
replaced
74 |
74 |
75 fun cache_conv cv = |
75 fun cache_conv cv = |
76 let |
76 let |
77 val cache = ref Termtab.empty; |
77 val cache = ref Termtab.empty; |
78 fun conv ct = |
78 fun conv ct = |
79 (case Termtab.lookup (! cache) (term_of ct) of |
79 (case Termtab.lookup (! cache) (Thm.term_of ct) of |
80 SOME th => th |
80 SOME th => th |
81 | NONE => |
81 | NONE => |
82 let val th = cv ct |
82 let val th = cv ct |
83 in change cache (Termtab.update (term_of ct, th)); th end); |
83 in change cache (Termtab.update (Thm.term_of ct, th)); th end); |
84 in conv end; |
84 in conv end; |
85 |
85 |
86 |
86 |
87 |
87 |
88 (** Pure conversions **) |
88 (** Pure conversions **) |
89 |
89 |
90 (* lambda terms *) |
90 (* lambda terms *) |
91 |
91 |
92 fun abs_conv cv ct = |
92 fun abs_conv cv ct = |
93 (case term_of ct of |
93 (case Thm.term_of ct of |
94 Abs (x, _, _) => |
94 Abs (x, _, _) => |
95 let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct |
95 let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct |
96 in Thm.abstract_rule x v (cv ct') end |
96 in Thm.abstract_rule x v (cv ct') end |
97 | _ => raise CTERM ("abs_conv", [ct])); |
97 | _ => raise CTERM ("abs_conv", [ct])); |
98 |
98 |
116 fun forall_conv 0 cv ct = cv ct |
116 fun forall_conv 0 cv ct = cv ct |
117 | forall_conv n cv ct = |
117 | forall_conv n cv ct = |
118 (case try Thm.dest_comb ct of |
118 (case try Thm.dest_comb ct of |
119 NONE => cv ct |
119 NONE => cv ct |
120 | SOME (A, B) => |
120 | SOME (A, B) => |
121 (case (term_of A, term_of B) of |
121 (case (Thm.term_of A, Thm.term_of B) of |
122 (Const ("all", _), Abs (x, _, _)) => |
122 (Const ("all", _), Abs (x, _, _)) => |
123 let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in |
123 let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in |
124 Thm.combination (all_conv A) |
124 Thm.combination (all_conv A) |
125 (Thm.abstract_rule x v (forall_conv (n - 1) cv B')) |
125 (Thm.abstract_rule x v (forall_conv (n - 1) cv B')) |
126 end |
126 end |