equal
deleted
inserted
replaced
1436 let |
1436 let |
1437 val assm1 = @{cprop "\<And>(x::nat). P x \<Longrightarrow> Q x"} |
1437 val assm1 = @{cprop "\<And>(x::nat). P x \<Longrightarrow> Q x"} |
1438 val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"} |
1438 val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"} |
1439 |
1439 |
1440 val Pt_implies_Qt = |
1440 val Pt_implies_Qt = |
1441 assume assm1 |
1441 Thm.assume assm1 |
1442 |> forall_elim @{cterm "t::nat"} |
1442 |> Thm.forall_elim @{cterm "t::nat"} |
1443 |
1443 |
1444 val Qt = implies_elim Pt_implies_Qt (assume assm2) |
1444 val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2) |
1445 in |
1445 in |
1446 Qt |
1446 Qt |
1447 |> implies_intr assm2 |
1447 |> Thm.implies_intr assm2 |
1448 |> implies_intr assm1 |
1448 |> Thm.implies_intr assm1 |
1449 end*} |
1449 end*} |
1450 |
1450 |
1451 text {* |
1451 text {* |
1452 Note that in Line 3 and 4 we use the antiquotation @{text "@{cprop \<dots>}"}, which |
1452 Note that in Line 3 and 4 we use the antiquotation @{text "@{cprop \<dots>}"}, which |
1453 inserts necessary @{text "Trueprop"}s. |
1453 inserts necessary @{text "Trueprop"}s. |