src/HOL/Tools/Argo/argo_tactic.ML
changeset 67091 1393c2340eec
parent 66301 8a6a89d6cf2b
child 67149 e61557884799
     1.1 --- a/src/HOL/Tools/Argo/argo_tactic.ML	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Tools/Argo/argo_tactic.ML	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -325,12 +325,12 @@
     1.4  fun taut_or1_term i ts = [mk_nary HOLogic.mk_disj ts, HOLogic.mk_not (nth ts i)]
     1.5  fun taut_or2_term ts = HOLogic.mk_not (mk_nary HOLogic.mk_disj ts) :: ts
     1.6  
     1.7 -val iff_1_taut = @{lemma "P = Q | P | Q" by fast}
     1.8 -val iff_2_taut = @{lemma "P = Q | (~P) | (~Q)" by fast}
     1.9 -val iff_3_taut = @{lemma "~(P = Q) | (~P) | Q" by fast}
    1.10 -val iff_4_taut = @{lemma "~(P = Q) | P | (~Q)" by fast}
    1.11 -val ite_then_taut = @{lemma "~P | (if P then t else u) = t" by auto}
    1.12 -val ite_else_taut = @{lemma "P | (if P then t else u) = u" by auto}
    1.13 +val iff_1_taut = @{lemma "P = Q \<or> P \<or> Q" by fast}
    1.14 +val iff_2_taut = @{lemma "P = Q \<or> (\<not>P) \<or> (\<not>Q)" by fast}
    1.15 +val iff_3_taut = @{lemma "\<not>(P = Q) \<or> (\<not>P) \<or> Q" by fast}
    1.16 +val iff_4_taut = @{lemma "\<not>(P = Q) \<or> P \<or> (\<not>Q)" by fast}
    1.17 +val ite_then_taut = @{lemma "\<not>P \<or> (if P then t else u) = t" by auto}
    1.18 +val ite_else_taut = @{lemma "P \<or> (if P then t else u) = u" by auto}
    1.19  
    1.20  fun taut_rule_of ctxt (Argo_Proof.Taut_And_1 n) = with_frees ctxt n taut_and1_term
    1.21    | taut_rule_of ctxt (Argo_Proof.Taut_And_2 (i, n)) = with_frees ctxt n (taut_and2_term i)
    1.22 @@ -364,8 +364,8 @@
    1.23    if i > 1 then (Conv.rewr_conv rule then_conv Conv.arg_conv (not_nary_conv rule (i - 1))) ct
    1.24    else Conv.all_conv ct
    1.25  
    1.26 -val flatten_and_thm = @{lemma "(P1 & P2) & P3 == P1 & P2 & P3" by simp}
    1.27 -val flatten_or_thm = @{lemma "(P1 | P2) | P3 == P1 | P2 | P3" by simp}
    1.28 +val flatten_and_thm = @{lemma "(P1 \<and> P2) \<and> P3 \<equiv> P1 \<and> P2 \<and> P3" by simp}
    1.29 +val flatten_or_thm = @{lemma "(P1 \<or> P2) \<or> P3 \<equiv> P1 \<or> P2 \<or> P3" by simp}
    1.30  
    1.31  fun flatten_conv cv rule ct = (
    1.32    Conv.try_conv (Conv.arg_conv cv) then_conv
    1.33 @@ -384,14 +384,14 @@
    1.34  fun explode rule1 rule2 thm =
    1.35    explode rule1 rule2 (thm RS rule1) @ explode rule1 rule2 (thm RS rule2) handle THM _ => [thm]
    1.36  val explode_conj = explode @{thm conjunct1} @{thm conjunct2}
    1.37 -val explode_ndis = explode @{lemma "~(P | Q) ==> ~P" by auto} @{lemma "~(P | Q) ==> ~Q" by auto}
    1.38 +val explode_ndis = explode @{lemma "\<not>(P \<or> Q) \<Longrightarrow> \<not>P" by auto} @{lemma "\<not>(P \<or> Q) \<Longrightarrow> \<not>Q" by auto}
    1.39  
    1.40  fun pick_false i thms = nth thms i
    1.41  
    1.42  fun pick_dual rule (i1, i2) thms =
    1.43    rule OF [nth thms i1, nth thms i2] handle THM _ => rule OF [nth thms i2, nth thms i1]
    1.44 -val pick_dual_conj = pick_dual @{lemma "~P ==> P ==> False" by auto}
    1.45 -val pick_dual_ndis = pick_dual @{lemma "~P ==> P ==> ~True" by auto}
    1.46 +val pick_dual_conj = pick_dual @{lemma "\<not>P \<Longrightarrow> P \<Longrightarrow> False" by auto}
    1.47 +val pick_dual_ndis = pick_dual @{lemma "\<not>P \<Longrightarrow> P \<Longrightarrow> \<not>True" by auto}
    1.48  
    1.49  fun join thm0 rule is thms =
    1.50    let
    1.51 @@ -399,13 +399,13 @@
    1.52      val thms' = fold (fn i => cons (if 0 <= i andalso i < l then nth thms i else thm0)) is []
    1.53    in fold (fn thm => fn thm' => discharge2 thm thm' rule) (tl thms') (hd thms') end
    1.54  
    1.55 -val join_conj = join @{lemma "True" by auto} @{lemma "P ==> Q ==> P & Q" by auto}
    1.56 -val join_ndis = join @{lemma "~False" by auto} @{lemma "~P ==> ~Q ==> ~(P | Q)" by auto}
    1.57 +val join_conj = join @{lemma "True" by auto} @{lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" by auto}
    1.58 +val join_ndis = join @{lemma "\<not>False" by auto} @{lemma "\<not>P \<Longrightarrow> \<not>Q \<Longrightarrow> \<not>(P \<or> Q)" by auto}
    1.59  
    1.60 -val false_thm = @{lemma "False ==> P" by auto}
    1.61 -val ntrue_thm = @{lemma "~True ==> P" by auto}
    1.62 -val iff_conj_thm = @{lemma "(P ==> Q) ==> (Q ==> P) ==> P = Q" by auto}
    1.63 -val iff_ndis_thm = @{lemma "(~P ==> ~Q) ==> (~Q ==> ~P) ==> P = Q" by auto}
    1.64 +val false_thm = @{lemma "False \<Longrightarrow> P" by auto}
    1.65 +val ntrue_thm = @{lemma "\<not>True \<Longrightarrow> P" by auto}
    1.66 +val iff_conj_thm = @{lemma "(P \<Longrightarrow> Q) \<Longrightarrow> (Q \<Longrightarrow> P) \<Longrightarrow> P = Q" by auto}
    1.67 +val iff_ndis_thm = @{lemma "(\<not>P \<Longrightarrow> \<not>Q) \<Longrightarrow> (\<not>Q \<Longrightarrow> \<not>P) \<Longrightarrow> P = Q" by auto}
    1.68  
    1.69  fun iff_intro rule lf rf ct =
    1.70    let
    1.71 @@ -421,21 +421,21 @@
    1.72  val sort_conj = sort_nary with_conj join_conj explode_conj
    1.73  val sort_ndis = sort_nary with_ndis join_ndis explode_ndis 
    1.74  
    1.75 -val not_true_thm = mk_rewr @{lemma "(~True) = False" by auto}
    1.76 -val not_false_thm = mk_rewr @{lemma "(~False) = True" by auto}
    1.77 -val not_not_thm = mk_rewr @{lemma "(~~P) = P" by auto}
    1.78 -val not_and_thm = mk_rewr @{lemma "(~(P & Q)) = (~P | ~Q)" by auto}
    1.79 -val not_or_thm = mk_rewr @{lemma "(~(P | Q)) = (~P & ~Q)" by auto}
    1.80 +val not_true_thm = mk_rewr @{lemma "(\<not>True) = False" by auto}
    1.81 +val not_false_thm = mk_rewr @{lemma "(\<not>False) = True" by auto}
    1.82 +val not_not_thm = mk_rewr @{lemma "(\<not>\<not>P) = P" by auto}
    1.83 +val not_and_thm = mk_rewr @{lemma "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" by auto}
    1.84 +val not_or_thm = mk_rewr @{lemma "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" by auto}
    1.85  val not_iff_thms = map mk_rewr
    1.86 -  @{lemma "(~((~P) = Q)) = (P = Q)" "(~(P = (~Q))) = (P = Q)" "(~(P = Q)) = ((~P) = Q)" by auto}
    1.87 +  @{lemma "(\<not>((\<not>P) = Q)) = (P = Q)" "(\<not>(P = (\<not>Q))) = (P = Q)" "(\<not>(P = Q)) = ((\<not>P) = Q)" by auto}
    1.88  val iff_true_thms = map mk_rewr @{lemma "(True = P) = P" "(P = True) = P" by auto}
    1.89 -val iff_false_thms = map mk_rewr @{lemma "(False = P) = (~P)" "(P = False) = (~P)" by auto}
    1.90 -val iff_not_not_thm = mk_rewr @{lemma "((~P) = (~Q)) = (P = Q)" by auto}
    1.91 +val iff_false_thms = map mk_rewr @{lemma "(False = P) = (\<not>P)" "(P = False) = (\<not>P)" by auto}
    1.92 +val iff_not_not_thm = mk_rewr @{lemma "((\<not>P) = (\<not>Q)) = (P = Q)" by auto}
    1.93  val iff_refl_thm = mk_rewr @{lemma "(P = P) = True" by auto}
    1.94  val iff_symm_thm = mk_rewr @{lemma "(P = Q) = (Q = P)" by auto}
    1.95 -val iff_dual_thms = map mk_rewr @{lemma "(P = (~P)) = False" "((~P) = P) = False" by auto}
    1.96 -val imp_thm = mk_rewr @{lemma "(P --> Q) = (~P | Q)" by auto}
    1.97 -val ite_prop_thm = mk_rewr @{lemma "(If P Q R) = ((~P | Q) & (P | R) & (Q | R))" by auto}
    1.98 +val iff_dual_thms = map mk_rewr @{lemma "(P = (\<not>P)) = False" "((\<not>P) = P) = False" by auto}
    1.99 +val imp_thm = mk_rewr @{lemma "(P \<longrightarrow> Q) = (\<not>P \<or> Q)" by auto}
   1.100 +val ite_prop_thm = mk_rewr @{lemma "(If P Q R) = ((\<not>P \<or> Q) \<and> (P \<or> R) \<and> (Q \<or> R))" by auto}
   1.101  val ite_true_thm = mk_rewr @{lemma "(If True t u) = t" by auto}
   1.102  val ite_false_thm = mk_rewr @{lemma "(If False t u) = u" by auto}
   1.103  val ite_eq_thm = mk_rewr @{lemma "(If P t t) = t" by auto}
   1.104 @@ -494,8 +494,8 @@
   1.105  
   1.106  (* proof replay for clauses *)
   1.107  
   1.108 -val prep_clause_rule = @{lemma "P ==> ~P ==> False" by fast}
   1.109 -val extract_lit_rule = @{lemma "(~(P | Q) ==> False) ==> ~P ==> ~Q ==> False" by fast}
   1.110 +val prep_clause_rule = @{lemma "P \<Longrightarrow> \<not>P \<Longrightarrow> False" by fast}
   1.111 +val extract_lit_rule = @{lemma "(\<not>(P \<or> Q) \<Longrightarrow> False) \<Longrightarrow> \<not>P \<Longrightarrow> \<not>Q \<Longrightarrow> False" by fast}
   1.112  
   1.113  fun add_lit i thm lits =
   1.114    let val ct = Thm.cprem_of thm 1
   1.115 @@ -518,7 +518,7 @@
   1.116  
   1.117  (* proof replay for unit resolution *)
   1.118  
   1.119 -val unit_rule = @{lemma "(P ==> False) ==> (~P ==> False) ==> False" by fast}
   1.120 +val unit_rule = @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not>P \<Longrightarrow> False) \<Longrightarrow> False" by fast}
   1.121  val unit_rule_var = Thm.dest_arg (Thm.dest_arg1 (Thm.cprem_of unit_rule 1))
   1.122  val bogus_ct = @{cterm HOL.True}
   1.123  
   1.124 @@ -538,7 +538,7 @@
   1.125  
   1.126  (* proof replay for hypothesis *)
   1.127  
   1.128 -val dneg_rule = @{lemma "~~P ==> P" by auto}
   1.129 +val dneg_rule = @{lemma "\<not>\<not>P \<Longrightarrow> P" by auto}
   1.130  
   1.131  fun replay_hyp i ct =
   1.132    if i < 0 then (Thm.assume ct, [(~i, ct)])
   1.133 @@ -562,7 +562,7 @@
   1.134  
   1.135  (* proof replay for symmetry *)
   1.136  
   1.137 -val symm_rules = @{lemma "a = b ==> b = a" "~(a = b) ==> ~(b = a)" by simp_all}
   1.138 +val symm_rules = @{lemma "a = b ==> b = a" "\<not>(a = b) \<Longrightarrow> \<not>(b = a)" by simp_all}
   1.139  
   1.140  fun replay_symm thm = hd (discharges thm symm_rules)
   1.141  
   1.142 @@ -570,9 +570,9 @@
   1.143  (* proof replay for transitivity *)
   1.144  
   1.145  val trans_rules = @{lemma
   1.146 -  "~(a = b) ==> b = c ==> ~(a = c)"
   1.147 -  "a = b ==> ~(b = c) ==> ~(a = c)"
   1.148 -  "a = b ==> b = c ==> a = c"
   1.149 +  "\<not>(a = b) \<Longrightarrow> b = c \<Longrightarrow> \<not>(a = c)"
   1.150 +  "a = b \<Longrightarrow> \<not>(b = c) \<Longrightarrow> \<not>(a = c)"
   1.151 +  "a = b \<Longrightarrow> b = c ==> a = c"
   1.152    by simp_all}
   1.153  
   1.154  fun replay_trans thm1 thm2 = hd (discharges thm2 (discharges thm1 trans_rules))
   1.155 @@ -585,8 +585,8 @@
   1.156  
   1.157  (* proof replay for substitution *)
   1.158  
   1.159 -val subst_rule1 = @{lemma "~(p a) ==> p = q ==> a = b ==> ~(q b)" by simp}
   1.160 -val subst_rule2 = @{lemma "p a ==> p = q ==> a = b ==> q b" by simp}
   1.161 +val subst_rule1 = @{lemma "\<not>(p a) \<Longrightarrow> p = q \<Longrightarrow> a = b \<Longrightarrow> \<not>(q b)" by simp}
   1.162 +val subst_rule2 = @{lemma "p a \<Longrightarrow> p = q \<Longrightarrow> a = b \<Longrightarrow> q b" by simp}
   1.163  
   1.164  fun replay_subst thm1 thm2 thm3 =
   1.165    subst_rule1 OF [thm1, thm2, thm3] handle THM _ => subst_rule2 OF [thm1, thm2, thm3]
   1.166 @@ -596,8 +596,8 @@
   1.167  
   1.168  structure Thm_Cache = Table(type key = Argo_Proof.proof_id val ord = Argo_Proof.proof_id_ord)
   1.169  
   1.170 -val unclausify_rule1 = @{lemma "(~P ==> False) ==> P" by auto}
   1.171 -val unclausify_rule2 = @{lemma "(P ==> False) ==> ~P" by auto}
   1.172 +val unclausify_rule1 = @{lemma "(\<not>P \<Longrightarrow> False) \<Longrightarrow> P" by auto}
   1.173 +val unclausify_rule2 = @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> \<not>P" by auto}
   1.174  
   1.175  fun unclausify (thm, lits) ls =
   1.176    (case (Thm.prop_of thm, lits) of