--- a/src/Pure/proofterm.ML Fri Sep 28 11:07:40 2001 +0200
+++ b/src/Pure/proofterm.ML Fri Sep 28 11:08:53 2001 +0200
@@ -6,7 +6,7 @@
LF style proof terms.
*)
-infix 8 % %% %%%;
+infix 8 % %% %>;
signature BASIC_PROOFTERM =
sig
@@ -16,15 +16,15 @@
PBound of int
| Abst of string * typ option * proof
| AbsP of string * term option * proof
- | op %% of proof * term option
- | op % of proof * proof
+ | op % of proof * term option
+ | op %% of proof * proof
| Hyp of term
| PThm of (string * (string * string list) list) * proof * term * typ list option
| PAxm of string * term * typ list option
| Oracle of string * term * typ list option
| MinProof of proof list;
- val %%% : proof * term -> proof
+ val %> : proof * term -> proof
end;
signature PROOFTERM =
@@ -101,6 +101,8 @@
(string * (Term.typ list -> proof -> proof option)) list -> unit
val rewrite_proof : Type.type_sig -> (proof * proof) list *
(string * (typ list -> proof -> proof option)) list -> proof -> proof
+ val rewrite_proof_notypes : (proof * proof) list *
+ (string * (typ list -> proof -> proof option)) list -> proof -> proof
val init : theory -> theory
end
@@ -112,8 +114,8 @@
PBound of int
| Abst of string * typ option * proof
| AbsP of string * term option * proof
- | op %% of proof * term option
- | op % of proof * proof
+ | op % of proof * term option
+ | op %% of proof * proof
| Hyp of term
| PThm of (string * (string * string list) list) * proof * term * typ list option
| PAxm of string * term * typ list option
@@ -124,8 +126,8 @@
let
fun oras_of (tabs, Abst (_, _, prf)) = oras_of (tabs, prf)
| oras_of (tabs, AbsP (_, _, prf)) = oras_of (tabs, prf)
- | oras_of (tabs, prf %% _) = oras_of (tabs, prf)
- | oras_of (tabs, prf1 % prf2) = oras_of (oras_of (tabs, prf1), prf2)
+ | oras_of (tabs, prf % _) = oras_of (tabs, prf)
+ | oras_of (tabs, prf1 %% prf2) = oras_of (oras_of (tabs, prf1), prf2)
| oras_of (tabs as (thms, oras), PThm ((name, _), prf, prop, _)) =
(case Symtab.lookup (thms, name) of
None => oras_of ((Symtab.update ((name, [prop]), thms), oras), prf)
@@ -140,8 +142,8 @@
fun thms_of_proof tab (Abst (_, _, prf)) = thms_of_proof tab prf
| thms_of_proof tab (AbsP (_, _, prf)) = thms_of_proof tab prf
- | thms_of_proof tab (prf1 % prf2) = thms_of_proof (thms_of_proof tab prf1) prf2
- | thms_of_proof tab (prf %% _) = thms_of_proof tab prf
+ | thms_of_proof tab (prf1 %% prf2) = thms_of_proof (thms_of_proof tab prf1) prf2
+ | thms_of_proof tab (prf % _) = thms_of_proof tab prf
| thms_of_proof tab (prf' as PThm ((s, _), prf, prop, _)) =
(case Symtab.lookup (tab, s) of
None => thms_of_proof (Symtab.update ((s, [(prop, prf')]), tab)) prf
@@ -151,8 +153,8 @@
fun axms_of_proof tab (Abst (_, _, prf)) = axms_of_proof tab prf
| axms_of_proof tab (AbsP (_, _, prf)) = axms_of_proof tab prf
- | axms_of_proof tab (prf1 % prf2) = axms_of_proof (axms_of_proof tab prf1) prf2
- | axms_of_proof tab (prf %% _) = axms_of_proof tab prf
+ | axms_of_proof tab (prf1 %% prf2) = axms_of_proof (axms_of_proof tab prf1) prf2
+ | axms_of_proof tab (prf % _) = axms_of_proof tab prf
| axms_of_proof tab (prf as PAxm (s, _, _)) = Symtab.update ((s, prf), tab)
| axms_of_proof tab _ = tab;
@@ -160,8 +162,8 @@
fun mk_min_proof (prfs, Abst (_, _, prf)) = mk_min_proof (prfs, prf)
| mk_min_proof (prfs, AbsP (_, _, prf)) = mk_min_proof (prfs, prf)
- | mk_min_proof (prfs, prf %% _) = mk_min_proof (prfs, prf)
- | mk_min_proof (prfs, prf1 % prf2) = mk_min_proof (mk_min_proof (prfs, prf1), prf2)
+ | mk_min_proof (prfs, prf % _) = mk_min_proof (prfs, prf)
+ | mk_min_proof (prfs, prf1 %% prf2) = mk_min_proof (mk_min_proof (prfs, prf1), prf2)
| mk_min_proof (prfs, prf as PThm _) = prf ins prfs
| mk_min_proof (prfs, prf as PAxm _) = prf ins prfs
| mk_min_proof (prfs, prf as Oracle _) = prf ins prfs
@@ -193,19 +195,19 @@
| 0 => MinProof (if_ora ora [] prf)
| i => err_illegal_level i);
-fun (prf %%% t) = prf %% Some t;
+fun (prf %> t) = prf % Some t;
-val proof_combt = foldl (op %%%);
-val proof_combt' = foldl (op %%);
-val proof_combP = foldl (op %);
+val proof_combt = foldl (op %>);
+val proof_combt' = foldl (op %);
+val proof_combP = foldl (op %%);
fun strip_combt prf =
- let fun stripc (prf %% t, ts) = stripc (prf, t::ts)
+ let fun stripc (prf % t, ts) = stripc (prf, t::ts)
| stripc x = x
in stripc (prf, []) end;
fun strip_combP prf =
- let fun stripc (prf % prf', prfs) = stripc (prf, prf'::prfs)
+ let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs)
| stripc x = x
in stripc (prf, []) end;
@@ -218,8 +220,8 @@
fun map_proof_terms f g (Abst (s, T, prf)) = Abst (s, apsome g T, map_proof_terms f g prf)
| map_proof_terms f g (AbsP (s, t, prf)) = AbsP (s, apsome f t, map_proof_terms f g prf)
- | map_proof_terms f g (prf %% t) = map_proof_terms f g prf %% apsome f t
- | map_proof_terms f g (prf1 % prf2) = map_proof_terms f g prf1 % map_proof_terms f g prf2
+ | map_proof_terms f g (prf % t) = map_proof_terms f g prf % apsome f t
+ | map_proof_terms f g (prf1 %% prf2) = map_proof_terms f g prf1 %% map_proof_terms f g prf2
| map_proof_terms _ g (PThm (a, prf, prop, Some Ts)) = PThm (a, prf, prop, Some (map g Ts))
| map_proof_terms _ g (PAxm (a, prop, Some Ts)) = PAxm (a, prop, Some (map g Ts))
| map_proof_terms _ _ prf = prf;
@@ -228,9 +230,9 @@
| fold_proof_terms f g (a, Abst (_, None, prf)) = fold_proof_terms f g (a, prf)
| fold_proof_terms f g (a, AbsP (_, Some t, prf)) = fold_proof_terms f g (f (t, a), prf)
| fold_proof_terms f g (a, AbsP (_, None, prf)) = fold_proof_terms f g (a, prf)
- | fold_proof_terms f g (a, prf %% Some t) = f (t, fold_proof_terms f g (a, prf))
- | fold_proof_terms f g (a, prf %% None) = fold_proof_terms f g (a, prf)
- | fold_proof_terms f g (a, prf1 % prf2) = fold_proof_terms f g
+ | fold_proof_terms f g (a, prf % Some t) = f (t, fold_proof_terms f g (a, prf))
+ | fold_proof_terms f g (a, prf % None) = fold_proof_terms f g (a, prf)
+ | fold_proof_terms f g (a, prf1 %% prf2) = fold_proof_terms f g
(fold_proof_terms f g (a, prf1), prf2)
| fold_proof_terms _ g (a, PThm (_, _, _, Some Ts)) = foldr g (Ts, a)
| fold_proof_terms _ g (a, PAxm (_, prop, Some Ts)) = foldr g (Ts, a)
@@ -259,8 +261,8 @@
fun abst Ts (AbsP (a, t, prf)) = AbsP (a, apsome (abst' Ts) t, abst Ts prf)
| abst Ts (Abst (a, T, prf)) = Abst (a, T, abst (dummyT::Ts) prf)
- | abst Ts (prf1 % prf2) = abst Ts prf1 % abst Ts prf2
- | abst Ts (prf %% t) = abst Ts prf %% apsome (abst' Ts) t
+ | abst Ts (prf1 %% prf2) = abst Ts prf1 %% abst Ts prf2
+ | abst Ts (prf % t) = abst Ts prf % apsome (abst' Ts) t
| abst _ prf = prf
in abst [] end;
@@ -278,27 +280,27 @@
AbsP (a, apsome (incr_bv' inct tlev) t, prf_incr_bv incP inct (Plev+1) tlev body)
| prf_incr_bv incP inct Plev tlev (Abst (a, T, body)) =
Abst (a, T, prf_incr_bv incP inct Plev (tlev+1) body)
- | prf_incr_bv incP inct Plev tlev (prf % prf') =
- prf_incr_bv incP inct Plev tlev prf % prf_incr_bv incP inct Plev tlev prf'
- | prf_incr_bv incP inct Plev tlev (prf %% t) =
- prf_incr_bv incP inct Plev tlev prf %% apsome (incr_bv' inct tlev) t
+ | prf_incr_bv incP inct Plev tlev (prf %% prf') =
+ prf_incr_bv incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf'
+ | prf_incr_bv incP inct Plev tlev (prf % t) =
+ prf_incr_bv incP inct Plev tlev prf % apsome (incr_bv' inct tlev) t
| prf_incr_bv _ _ _ _ prf = prf;
fun incr_pboundvars 0 0 prf = prf
| incr_pboundvars incP inct prf = prf_incr_bv incP inct 0 0 prf;
-fun prf_loose_bvar1 (prf1 % prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k
- | prf_loose_bvar1 (prf %% Some t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k)
- | prf_loose_bvar1 (_ %% None) _ = true
+fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k
+ | prf_loose_bvar1 (prf % Some t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k)
+ | prf_loose_bvar1 (_ % None) _ = true
| prf_loose_bvar1 (AbsP (_, Some t, prf)) k = loose_bvar1 (t, k) orelse prf_loose_bvar1 prf k
| prf_loose_bvar1 (AbsP (_, None, _)) k = true
| prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1)
| prf_loose_bvar1 _ _ = false;
fun prf_loose_Pbvar1 (PBound i) k = i = k
- | prf_loose_Pbvar1 (prf1 % prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k
- | prf_loose_Pbvar1 (prf %% _) k = prf_loose_Pbvar1 prf k
+ | prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k
+ | prf_loose_Pbvar1 (prf % _) k = prf_loose_Pbvar1 prf k
| prf_loose_Pbvar1 (AbsP (_, _, prf)) k = prf_loose_Pbvar1 prf (k+1)
| prf_loose_Pbvar1 (Abst (_, _, prf)) k = prf_loose_Pbvar1 prf k
| prf_loose_Pbvar1 _ _ = false;
@@ -317,10 +319,10 @@
handle SAME => Abst (s, T, norm prf))
| norm (AbsP (s, t, prf)) = (AbsP (s, apsome' (norm_term_same env) t, normh prf)
handle SAME => AbsP (s, t, norm prf))
- | norm (prf %% t) = (norm prf %% apsome (norm_term env) t
- handle SAME => prf %% apsome' (norm_term_same env) t)
- | norm (prf1 % prf2) = (norm prf1 % normh prf2
- handle SAME => prf1 % norm prf2)
+ | norm (prf % t) = (norm prf % apsome (norm_term env) t
+ handle SAME => prf % apsome' (norm_term_same env) t)
+ | norm (prf1 %% prf2) = (norm prf1 %% normh prf2
+ handle SAME => prf1 %% norm prf2)
| norm (PThm (s, prf, t, Ts)) = PThm (s, prf, t, apsome' (norm_types_same env) Ts)
| norm (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome' (norm_types_same env) Ts)
| norm _ = raise SAME
@@ -357,10 +359,10 @@
fun subst lev (AbsP (a, t, body)) = (AbsP (a, apsome' (subst' lev) t, substh lev body)
handle SAME => AbsP (a, t, subst lev body))
| subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body)
- | subst lev (prf % prf') = (subst lev prf % substh lev prf'
- handle SAME => prf % subst lev prf')
- | subst lev (prf %% t) = (subst lev prf %% apsome (substh' lev) t
- handle SAME => prf %% apsome' (subst' lev) t)
+ | subst lev (prf %% prf') = (subst lev prf %% substh lev prf'
+ handle SAME => prf %% subst lev prf')
+ | subst lev (prf % t) = (subst lev prf % apsome (substh' lev) t
+ handle SAME => prf % apsome' (subst' lev) t)
| subst _ _ = raise SAME
and substh lev prf = (subst lev prf handle SAME => prf)
in case args of [] => prf | _ => substh 0 prf end;
@@ -374,9 +376,9 @@
handle Subscript => PBound (i-n) (*loose: change it*))
| subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev)
| subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1))
- | subst (prf % prf') Plev tlev = (subst prf Plev tlev % substh prf' Plev tlev
- handle SAME => prf % subst prf' Plev tlev)
- | subst (prf %% t) Plev tlev = subst prf Plev tlev %% t
+ | subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev
+ handle SAME => prf %% subst prf' Plev tlev)
+ | subst (prf % t) Plev tlev = subst prf Plev tlev % t
| subst prf _ _ = raise SAME
and substh prf Plev tlev = (subst prf Plev tlev handle SAME => prf)
in case args of [] => prf | _ => substh prf 0 0 end;
@@ -447,8 +449,8 @@
fun abshyp i (Hyp t) = if h aconv t then PBound i else Hyp t
| abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf)
| abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i+1) prf)
- | abshyp i (prf %% t) = abshyp i prf %% t
- | abshyp i (prf1 % prf2) = abshyp i prf1 % abshyp i prf2
+ | abshyp i (prf % t) = abshyp i prf % t
+ | abshyp i (prf1 %% prf2) = abshyp i prf1 %% abshyp i prf2
| abshyp _ prf = prf;
in
AbsP ("H", None (*h*), abshyp 0 prf)
@@ -545,8 +547,8 @@
fun lift' Us Ts (Abst (s, T, prf)) = Abst (s, apsome (incr_tvar inc) T, lift' Us (dummyT::Ts) prf)
| lift' Us Ts (AbsP (s, t, prf)) = AbsP (s, apsome (lift'' Us Ts) t, lift' Us Ts prf)
- | lift' Us Ts (prf %% t) = lift' Us Ts prf %% apsome (lift'' Us Ts) t
- | lift' Us Ts (prf1 % prf2) = lift' Us Ts prf1 % lift' Us Ts prf2
+ | lift' Us Ts (prf % t) = lift' Us Ts prf % apsome (lift'' Us Ts) t
+ | lift' Us Ts (prf1 %% prf2) = lift' Us Ts prf1 %% lift' Us Ts prf2
| lift' _ _ (PThm (s, prf, prop, Ts)) = PThm (s, prf, prop, apsome (map (incr_tvar inc)) Ts)
| lift' _ _ (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome (map (incr_tvar inc)) Ts)
| lift' _ _ prf = prf;
@@ -555,7 +557,7 @@
val k = length ps;
fun mk_app (b, (i, j, prf)) =
- if b then (i-1, j, prf % PBound i) else (i, j-1, prf %%% Bound j);
+ if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
fun lift Us bs i j (Const ("==>", _) $ A $ B) =
AbsP ("H", None (*A*), lift Us (true::bs) (i+1) j B)
@@ -595,7 +597,7 @@
val lb = length Bs;
in
mk_AbsP (lb+la, proof_combP (sprf,
- map PBound (lb + la - 1 downto la)) %
+ map PBound (lb + la - 1 downto la)) %%
proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) (~n)] else []) @
map (flatten_params_proof 0 0 n) (oldAs ~~ (la - 1 downto 0))))
end;
@@ -635,26 +637,26 @@
end;
-val reflexive = reflexive_axm %% None;
+val reflexive = reflexive_axm % None;
-fun symmetric (prf as PAxm ("ProtoPure.reflexive", _, _) %% _) = prf
- | symmetric prf = symmetric_axm %% None %% None % prf;
+fun symmetric (prf as PAxm ("ProtoPure.reflexive", _, _) % _) = prf
+ | symmetric prf = symmetric_axm % None % None %% prf;
-fun transitive _ _ (PAxm ("ProtoPure.reflexive", _, _) %% _) prf2 = prf2
- | transitive _ _ prf1 (PAxm ("ProtoPure.reflexive", _, _) %% _) = prf1
+fun transitive _ _ (PAxm ("ProtoPure.reflexive", _, _) % _) prf2 = prf2
+ | transitive _ _ prf1 (PAxm ("ProtoPure.reflexive", _, _) % _) = prf1
| transitive u (Type ("prop", [])) prf1 prf2 =
- transitive_axm %% None %% Some (remove_types u) %% None % prf1 % prf2
+ transitive_axm % None % Some (remove_types u) % None %% prf1 %% prf2
| transitive u T prf1 prf2 =
- transitive_axm %% None %% None %% None % prf1 % prf2;
+ transitive_axm % None % None % None %% prf1 %% prf2;
fun abstract_rule x a prf =
- abstract_rule_axm %% None %% None % forall_intr_proof x a prf;
+ abstract_rule_axm % None % None %% forall_intr_proof x a prf;
-fun check_comb (PAxm ("ProtoPure.combination", _, _) %% f %% g %% _ %% _ % prf % _) =
+fun check_comb (PAxm ("ProtoPure.combination", _, _) % f % g % _ % _ %% prf %% _) =
is_some f orelse check_comb prf
- | check_comb (PAxm ("ProtoPure.transitive", _, _) %% _ %% _ %% _ % prf1 % prf2) =
+ | check_comb (PAxm ("ProtoPure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) =
check_comb prf1 andalso check_comb prf2
- | check_comb (PAxm ("ProtoPure.symmetric", _, _) %% _ %% _ % prf) = check_comb prf
+ | check_comb (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
| check_comb _ = false;
fun combination f g t u (Type (_, [T, U])) prf1 prf2 =
@@ -662,30 +664,30 @@
val f = Envir.beta_norm f;
val g = Envir.beta_norm g;
val prf = if check_comb prf1 then
- combination_axm %% None %% None
+ combination_axm % None % None
else (case prf1 of
- PAxm ("ProtoPure.reflexive", _, _) %% _ =>
- combination_axm %%% remove_types f %% None
- | _ => combination_axm %%% remove_types f %%% remove_types g)
+ PAxm ("ProtoPure.reflexive", _, _) % _ =>
+ combination_axm %> remove_types f % None
+ | _ => combination_axm %> remove_types f %> remove_types g)
in
(case T of
- Type ("fun", _) => prf %%
+ Type ("fun", _) => prf %
(case head_of f of
Abs _ => Some (remove_types t)
| Var _ => Some (remove_types t)
- | _ => None) %%
+ | _ => None) %
(case head_of g of
Abs _ => Some (remove_types u)
| Var _ => Some (remove_types u)
- | _ => None) % prf1 % prf2
- | _ => prf %% None %% None % prf1 % prf2)
+ | _ => None) %% prf1 %% prf2
+ | _ => prf % None % None %% prf1 %% prf2)
end;
fun equal_intr A B prf1 prf2 =
- equal_intr_axm %%% remove_types A %%% remove_types B % prf1 % prf2;
+ equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
fun equal_elim A B prf1 prf2 =
- equal_elim_axm %%% remove_types A %%% remove_types B % prf1 % prf2;
+ equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
(***** axioms and theorems *****)
@@ -764,20 +766,22 @@
| shrink ls lev prf =
let val (is, ch, _, prf') = shrink' ls lev [] [] prf
in (false, is, ch, prf') end
-and shrink' ls lev ts prfs (prf as prf1 % prf2) =
+and shrink' ls lev ts prfs (prf as prf1 %% prf2) =
let
val p as (_, is', ch', prf') = shrink ls lev prf2;
val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1
in (is union is', ch orelse ch', ts',
- if ch orelse ch' then prf'' % prf' else prf)
+ if ch orelse ch' then prf'' %% prf' else prf)
end
- | shrink' ls lev ts prfs (prf as prf1 %% t) =
+ | shrink' ls lev ts prfs (prf as prf1 % t) =
let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1
- in (is, ch orelse ch', ts', if ch orelse ch' then prf' %% t' else prf) end
+ in (is, ch orelse ch', ts', if ch orelse ch' then prf' % t' else prf) end
| shrink' ls lev ts prfs (prf as PBound i) =
(if exists (fn Some (Bound j) => lev-j <= nth_elem (i, ls) | _ => true) ts
orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
| shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf)
+ | shrink' ls lev ts prfs (prf as MinProof _) =
+ ([], false, map (pair false) ts, prf)
| shrink' ls lev ts prfs prf =
let
val prop = (case prf of PThm (_, _, prop, _) => prop | PAxm (_, prop, _) => prop
@@ -824,14 +828,14 @@
let
fun mtch (inst as (pinst, tinst as (tyinsts, insts))) = fn
(Hyp (Var (ixn, _)), prf) => ((ixn, prf)::pinst, tinst)
- | (prf1 %% opt1, prf2 %% opt2) =>
+ | (prf1 % opt1, prf2 % opt2) =>
let val inst' as (pinst, tinst) = mtch inst (prf1, prf2)
in (case (opt1, opt2) of
(None, _) => inst'
| (Some _, None) => raise PMatch
| (Some t, Some u) => (pinst, fomatch Ts tmatch tinst (t, Envir.beta_norm u)))
end
- | (prf1 % prf2, prf1' % prf2') =>
+ | (prf1 %% prf2, prf1' %% prf2') =>
mtch (mtch inst (prf1, prf1')) (prf2, prf2')
| (PThm ((name1, _), _, prop1, None), PThm ((name2, _), _, prop2, _)) =>
if name1=name2 andalso prop1=prop2 then inst else raise PMatch
@@ -865,8 +869,8 @@
AbsP (a, apsome (subst' tlev) t, subst (plev+1) tlev body)
| subst plev tlev (Abst (a, T, body)) =
Abst (a, apsome substT T, subst plev (tlev+1) body)
- | subst plev tlev (prf % prf') = subst plev tlev prf % subst plev tlev prf'
- | subst plev tlev (prf %% t) = subst plev tlev prf %% apsome (subst' tlev) t
+ | subst plev tlev (prf %% prf') = subst plev tlev prf %% subst plev tlev prf'
+ | subst plev tlev (prf % t) = subst plev tlev prf % apsome (subst' tlev) t
| subst plev tlev (prf as Hyp (Var (ixn, _))) = (case assoc (pinst, ixn) of
None => prf
| Some prf' => incr_pboundvars plev tlev prf')
@@ -881,20 +885,20 @@
fun rewrite_prf tmatch (rules, procs) prf =
let
- fun rew _ (Abst (_, _, body) %% Some t) = Some (prf_subst_bounds [t] body)
- | rew _ (AbsP (_, _, body) % prf) = Some (prf_subst_pbounds [prf] body)
+ fun rew _ (Abst (_, _, body) % Some t) = Some (prf_subst_bounds [t] body)
+ | rew _ (AbsP (_, _, body) %% prf) = Some (prf_subst_pbounds [prf] body)
| rew Ts prf = (case get_first (fn (_, r) => r Ts prf) procs of
Some prf' => Some prf'
| None => get_first (fn (prf1, prf2) => Some (prf_subst
(match_proof Ts tmatch ([], (Vartab.empty, [])) (prf1, prf)) prf2)
handle PMatch => None) rules);
- fun rew0 Ts (prf as AbsP (_, _, prf' % PBound 0)) =
+ fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) =
if prf_loose_Pbvar1 prf' 0 then rew Ts prf
else
let val prf'' = incr_pboundvars (~1) 0 prf'
in Some (if_none (rew Ts prf'') prf'') end
- | rew0 Ts (prf as Abst (_, _, prf' %% Some (Bound 0))) =
+ | rew0 Ts (prf as Abst (_, _, prf' % Some (Bound 0))) =
if prf_loose_bvar1 prf' 0 then rew Ts prf
else
let val prf'' = incr_pboundvars 0 (~1) prf'
@@ -909,24 +913,24 @@
Some prf1 => Some (if_none (rew1 Ts prf1) prf1)
| None => None))
- and rew2 Ts (prf %% Some t) = (case prf of
+ and rew2 Ts (prf % Some t) = (case prf of
Abst (_, _, body) =>
let val prf' = prf_subst_bounds [t] body
in Some (if_none (rew2 Ts prf') prf') end
| _ => (case rew1 Ts prf of
- Some prf' => Some (prf' %% Some t)
+ Some prf' => Some (prf' % Some t)
| None => None))
- | rew2 Ts (prf %% None) = apsome (fn prf' => prf' %% None) (rew1 Ts prf)
- | rew2 Ts (prf1 % prf2) = (case prf1 of
+ | rew2 Ts (prf % None) = apsome (fn prf' => prf' % None) (rew1 Ts prf)
+ | rew2 Ts (prf1 %% prf2) = (case prf1 of
AbsP (_, _, body) =>
let val prf' = prf_subst_pbounds [prf2] body
in Some (if_none (rew2 Ts prf') prf') end
| _ => (case rew1 Ts prf1 of
Some prf1' => (case rew1 Ts prf2 of
- Some prf2' => Some (prf1' % prf2')
- | None => Some (prf1' % prf2))
+ Some prf2' => Some (prf1' %% prf2')
+ | None => Some (prf1' %% prf2))
| None => (case rew1 Ts prf2 of
- Some prf2' => Some (prf1 % prf2')
+ Some prf2' => Some (prf1 %% prf2')
| None => None)))
| rew2 Ts (Abst (s, T, prf)) = (case rew1 (if_none T dummyT :: Ts) prf of
Some prf' => Some (Abst (s, T, prf'))
@@ -941,6 +945,8 @@
fun rewrite_proof tsig = rewrite_prf (fn (tab, f) =>
Type.typ_match tsig (tab, f ()) handle Type.TYPE_MATCH => raise PMatch);
+val rewrite_proof_notypes = rewrite_prf fst;
+
(**** theory data ****)
(* data kind 'Pure/proof' *)