equal
deleted
inserted
replaced
93 val thm1 = if to_right then prove_contradiction_imp clhs else prove_any_imp clhs |
93 val thm1 = if to_right then prove_contradiction_imp clhs else prove_any_imp clhs |
94 val thm2 = if to_right then prove_any_imp crhs else prove_contradiction_imp crhs |
94 val thm2 = if to_right then prove_any_imp crhs else prove_contradiction_imp crhs |
95 in eq_from_impls thm1 thm2 end |
95 in eq_from_impls thm1 thm2 end |
96 |
96 |
97 val contrapos_rule = @{lemma "(\<not>P) = (\<not>Q) \<Longrightarrow> P = Q" by auto} |
97 val contrapos_rule = @{lemma "(\<not>P) = (\<not>Q) \<Longrightarrow> P = Q" by auto} |
98 fun contrapos prove cp = contrapos_rule OF [prove (apply2 (Thm.apply @{cterm HOL.Not}) cp)] |
98 fun contrapos prove cp = contrapos_rule OF [prove (apply2 (Thm.apply \<^cterm>\<open>HOL.Not\<close>) cp)] |
99 |
99 |
100 datatype kind = True | False | Conj | Disj | Other |
100 datatype kind = True | False | Conj | Disj | Other |
101 |
101 |
102 fun choose t _ _ _ \<^const>\<open>HOL.True\<close> = t |
102 fun choose t _ _ _ \<^const>\<open>HOL.True\<close> = t |
103 | choose _ f _ _ \<^const>\<open>HOL.False\<close> = f |
103 | choose _ f _ _ \<^const>\<open>HOL.False\<close> = f |