2015-11-18 23:41:44 +00:00
|
|
|
-- Backward chaining with hypotheses
|
2015-12-07 19:59:21 +00:00
|
|
|
set_option blast.strategy "backward"
|
2015-11-18 23:41:44 +00:00
|
|
|
constants {P Q R S T U : Prop}
|
|
|
|
|
constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T)
|
2015-12-08 05:33:35 +00:00
|
|
|
attribute Huq [intro]
|
|
|
|
|
attribute Hur [intro]
|
|
|
|
|
attribute Hus [intro]
|
|
|
|
|
attribute Hut [intro]
|
2015-11-18 23:41:44 +00:00
|
|
|
|
|
|
|
|
definition lemma1 : (P → Q) → P → Q := by blast
|
|
|
|
|
definition lemma2 : (P → Q) → (Q → R) → P → R := by blast
|
|
|
|
|
definition lemma3 : (P → Q) → (Q → R) → (R → S) → P → S := by blast
|
|
|
|
|
definition lemma4 : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by blast
|
