1829 val (tpairs, Bs, Bi, C) = dest_state (state, i); |
1829 val (tpairs, Bs, Bi, C) = dest_state (state, i); |
1830 fun newth n (env, tpairs) = |
1830 fun newth n (env, tpairs) = |
1831 let |
1831 let |
1832 val normt = Envir.norm_term env; |
1832 val normt = Envir.norm_term env; |
1833 fun assumption_proof prf = |
1833 fun assumption_proof prf = |
1834 Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf |
1834 Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf; |
1835 |> not (Envir.is_empty env) ? Proofterm.norm_proof' env; |
|
1836 in |
1835 in |
1837 Thm (deriv_rule1 assumption_proof der, |
1836 Thm (deriv_rule1 |
|
1837 (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env) der, |
1838 {tags = [], |
1838 {tags = [], |
1839 maxidx = Envir.maxidx_of env, |
1839 maxidx = Envir.maxidx_of env, |
1840 constraints = insert_constraints_env (Context.certificate_theory cert') env constraints, |
1840 constraints = insert_constraints_env (Context.certificate_theory cert') env constraints, |
1841 shyps = Envir.insert_sorts env shyps, |
1841 shyps = Envir.insert_sorts env shyps, |
1842 hyps = hyps, |
1842 hyps = hyps, |
2085 fun bicompose_proof prf1 prf2 = |
2085 fun bicompose_proof prf1 prf2 = |
2086 Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) |
2086 Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) |
2087 prf1 prf2 |
2087 prf1 prf2 |
2088 val th = |
2088 val th = |
2089 Thm (deriv_rule2 |
2089 Thm (deriv_rule2 |
2090 ((if Envir.is_empty env then I |
2090 (if Envir.is_empty env then bicompose_proof |
2091 else if Envir.above env smax then |
2091 else if Envir.above env smax then bicompose_proof o Proofterm.norm_proof' env |
2092 (fn f => fn der => f (Proofterm.norm_proof' env der)) |
2092 else Proofterm.norm_proof' env oo bicompose_proof) rder' sder, |
2093 else |
|
2094 curry op oo (Proofterm.norm_proof' env)) bicompose_proof) rder' sder, |
|
2095 {tags = [], |
2093 {tags = [], |
2096 maxidx = Envir.maxidx_of env, |
2094 maxidx = Envir.maxidx_of env, |
2097 constraints = constraints', |
2095 constraints = constraints', |
2098 shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2), |
2096 shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2), |
2099 hyps = union_hyps hyps1 hyps2, |
2097 hyps = union_hyps hyps1 hyps2, |