135 Prove (_, _, t, byline) => (t, byline, false) |
135 Prove (_, _, t, byline) => (t, byline, false) |
136 | Obtain (_, xs, _, t, byline) => |
136 | Obtain (_, xs, _, t, byline) => |
137 (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
137 (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
138 (see ~~/src/Pure/Isar/obtain.ML) *) |
138 (see ~~/src/Pure/Isar/obtain.ML) *) |
139 let |
139 let |
140 (*val thesis = Term.Free ("thesis", HOLogic.boolT) |
140 val thesis = Term.Free ("thesis", HOLogic.boolT) |
141 |> HOLogic.mk_Trueprop |
141 val thesis_prop = thesis |> HOLogic.mk_Trueprop |
142 val frees = map Term.Free xs |
142 val frees = map Term.Free xs |
143 |
143 |
144 (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
144 (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
145 val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis)) |
145 val inner_prop = |
|
146 fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) |
146 |
147 |
147 (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
148 (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
148 val prop = Logic.all thesis (Logic.mk_implies (inner_prop, thesis))*) |
|
149 |
|
150 val thesis = Term.Free ("thesis", HOLogic.boolT) |
|
151 val prop = |
149 val prop = |
152 HOLogic.mk_imp (HOLogic.dest_Trueprop t, thesis) |
150 Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) |
153 |> fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) xs |
|
154 |> rpair thesis |
|
155 |> HOLogic.mk_imp |
|
156 |> (fn t => HOLogic.mk_all ("thesis", HOLogic.boolT, t)) |
|
157 |> HOLogic.mk_Trueprop |
|
158 in |
151 in |
159 (prop, byline, true) |
152 (prop, byline, true) |
160 end |
153 end |
161 | _ => raise ZEROTIME) |
154 | _ => raise ZEROTIME) |
162 val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
155 val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |