src/HOL/Meson.thy
 author blanchet Tue Oct 05 10:28:11 2010 +0200 (2010-10-05) changeset 39948 317010af8972 parent 39947 f95834c8bb4d child 39950 f3c4849868b8 permissions -rw-r--r--
factor out "Meson_Tactic" from "Meson_Clausify"
```     1 (*  Title:      HOL/Meson.thy
```
```     2     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
```
```     3     Author:     Tobias Nipkow, TU Muenchen
```
```     4     Author:     Jasmin Blanchette, TU Muenchen
```
```     5     Copyright   2001  University of Cambridge
```
```     6 *)
```
```     7
```
```     8 header {* MESON Proof Method *}
```
```     9
```
```    10 theory Meson
```
```    11 imports Datatype
```
```    12 uses ("Tools/Meson/meson.ML")
```
```    13      ("Tools/Meson/meson_clausify.ML")
```
```    14      ("Tools/Meson/meson_tactic.ML")
```
```    15 begin
```
```    16
```
```    17 section {* Negation Normal Form *}
```
```    18
```
```    19 text {* de Morgan laws *}
```
```    20
```
```    21 lemma meson_not_conjD: "~(P&Q) ==> ~P | ~Q"
```
```    22   and meson_not_disjD: "~(P|Q) ==> ~P & ~Q"
```
```    23   and meson_not_notD: "~~P ==> P"
```
```    24   and meson_not_allD: "!!P. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)"
```
```    25   and meson_not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)"
```
```    26   by fast+
```
```    27
```
```    28 text {* Removal of @{text "-->"} and @{text "<->"} (positive and
```
```    29 negative occurrences) *}
```
```    30
```
```    31 lemma meson_imp_to_disjD: "P-->Q ==> ~P | Q"
```
```    32   and meson_not_impD: "~(P-->Q) ==> P & ~Q"
```
```    33   and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
```
```    34   and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
```
```    35     -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *}
```
```    36   and meson_not_refl_disj_D: "x ~= x | P ==> P"
```
```    37   by fast+
```
```    38
```
```    39
```
```    40 section {* Pulling out the existential quantifiers *}
```
```    41
```
```    42 text {* Conjunction *}
```
```    43
```
```    44 lemma meson_conj_exD1: "!!P Q. (\<exists>x. P(x)) & Q ==> \<exists>x. P(x) & Q"
```
```    45   and meson_conj_exD2: "!!P Q. P & (\<exists>x. Q(x)) ==> \<exists>x. P & Q(x)"
```
```    46   by fast+
```
```    47
```
```    48
```
```    49 text {* Disjunction *}
```
```    50
```
```    51 lemma meson_disj_exD: "!!P Q. (\<exists>x. P(x)) | (\<exists>x. Q(x)) ==> \<exists>x. P(x) | Q(x)"
```
```    52   -- {* DO NOT USE with forall-Skolemization: makes fewer schematic variables!! *}
```
```    53   -- {* With ex-Skolemization, makes fewer Skolem constants *}
```
```    54   and meson_disj_exD1: "!!P Q. (\<exists>x. P(x)) | Q ==> \<exists>x. P(x) | Q"
```
```    55   and meson_disj_exD2: "!!P Q. P | (\<exists>x. Q(x)) ==> \<exists>x. P | Q(x)"
```
```    56   by fast+
```
```    57
```
```    58 lemma meson_disj_assoc: "(P|Q)|R ==> P|(Q|R)"
```
```    59   and meson_disj_comm: "P|Q ==> Q|P"
```
```    60   and meson_disj_FalseD1: "False|P ==> P"
```
```    61   and meson_disj_FalseD2: "P|False ==> P"
```
```    62   by fast+
```
```    63
```
```    64
```
```    65 text{* Generation of contrapositives *}
```
```    66
```
```    67 text{*Inserts negated disjunct after removing the negation; P is a literal.
```
```    68   Model elimination requires assuming the negation of every attempted subgoal,
```
```    69   hence the negated disjuncts.*}
```
```    70 lemma make_neg_rule: "~P|Q ==> ((~P==>P) ==> Q)"
```
```    71 by blast
```
```    72
```
```    73 text{*Version for Plaisted's "Postive refinement" of the Meson procedure*}
```
```    74 lemma make_refined_neg_rule: "~P|Q ==> (P ==> Q)"
```
```    75 by blast
```
```    76
```
```    77 text{*@{term P} should be a literal*}
```
```    78 lemma make_pos_rule: "P|Q ==> ((P==>~P) ==> Q)"
```
```    79 by blast
```
```    80
```
```    81 text{*Versions of @{text make_neg_rule} and @{text make_pos_rule} that don't
```
```    82 insert new assumptions, for ordinary resolution.*}
```
```    83
```
```    84 lemmas make_neg_rule' = make_refined_neg_rule
```
```    85
```
```    86 lemma make_pos_rule': "[|P|Q; ~P|] ==> Q"
```
```    87 by blast
```
```    88
```
```    89 text{* Generation of a goal clause -- put away the final literal *}
```
```    90
```
```    91 lemma make_neg_goal: "~P ==> ((~P==>P) ==> False)"
```
```    92 by blast
```
```    93
```
```    94 lemma make_pos_goal: "P ==> ((P==>~P) ==> False)"
```
```    95 by blast
```
```    96
```
```    97
```
```    98 section {* Lemmas for Forward Proof *}
```
```    99
```
```   100 text{*There is a similarity to congruence rules*}
```
```   101
```
```   102 (*NOTE: could handle conjunctions (faster?) by
```
```   103     nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)
```
```   104 lemma conj_forward: "[| P'&Q';  P' ==> P;  Q' ==> Q |] ==> P&Q"
```
```   105 by blast
```
```   106
```
```   107 lemma disj_forward: "[| P'|Q';  P' ==> P;  Q' ==> Q |] ==> P|Q"
```
```   108 by blast
```
```   109
```
```   110 (*Version of @{text disj_forward} for removal of duplicate literals*)
```
```   111 lemma disj_forward2:
```
```   112     "[| P'|Q';  P' ==> P;  [| Q'; P==>False |] ==> Q |] ==> P|Q"
```
```   113 apply blast
```
```   114 done
```
```   115
```
```   116 lemma all_forward: "[| \<forall>x. P'(x);  !!x. P'(x) ==> P(x) |] ==> \<forall>x. P(x)"
```
```   117 by blast
```
```   118
```
```   119 lemma ex_forward: "[| \<exists>x. P'(x);  !!x. P'(x) ==> P(x) |] ==> \<exists>x. P(x)"
```
```   120 by blast
```
```   121
```
```   122
```
```   123 section {* Clausification helper *}
```
```   124
```
```   125 lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
```
```   126 by simp
```
```   127
```
```   128
```
```   129 text{* Combinator translation helpers *}
```
```   130
```
```   131 definition COMBI :: "'a \<Rightarrow> 'a" where
```
```   132 [no_atp]: "COMBI P = P"
```
```   133
```
```   134 definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
```
```   135 [no_atp]: "COMBK P Q = P"
```
```   136
```
```   137 definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
```
```   138 "COMBB P Q R = P (Q R)"
```
```   139
```
```   140 definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
```
```   141 [no_atp]: "COMBC P Q R = P R Q"
```
```   142
```
```   143 definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
```
```   144 [no_atp]: "COMBS P Q R = P R (Q R)"
```
```   145
```
```   146 lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
```
```   147 apply (rule eq_reflection)
```
```   148 apply (rule ext)
```
```   149 apply (simp add: COMBS_def)
```
```   150 done
```
```   151
```
```   152 lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
```
```   153 apply (rule eq_reflection)
```
```   154 apply (rule ext)
```
```   155 apply (simp add: COMBI_def)
```
```   156 done
```
```   157
```
```   158 lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
```
```   159 apply (rule eq_reflection)
```
```   160 apply (rule ext)
```
```   161 apply (simp add: COMBK_def)
```
```   162 done
```
```   163
```
```   164 lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
```
```   165 apply (rule eq_reflection)
```
```   166 apply (rule ext)
```
```   167 apply (simp add: COMBB_def)
```
```   168 done
```
```   169
```
```   170 lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
```
```   171 apply (rule eq_reflection)
```
```   172 apply (rule ext)
```
```   173 apply (simp add: COMBC_def)
```
```   174 done
```
```   175
```
```   176
```
```   177 section {* Skolemization helpers *}
```
```   178
```
```   179 definition skolem :: "'a \<Rightarrow> 'a" where
```
```   180 [no_atp]: "skolem = (\<lambda>x. x)"
```
```   181
```
```   182 lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))"
```
```   183 unfolding skolem_def COMBK_def by (rule refl)
```
```   184
```
```   185 lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
```
```   186 lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
```
```   187
```
```   188
```
```   189 section {* Meson package *}
```
```   190
```
```   191 ML {*
```
```   192 structure Meson_Choices = Named_Thms
```
```   193 (
```
```   194   val name = "meson_choice"
```
```   195   val description = "choice axioms for MESON's (and Metis's) skolemizer"
```
```   196 )
```
```   197 *}
```
```   198
```
```   199 use "Tools/Meson/meson.ML"
```
```   200 use "Tools/Meson/meson_clausify.ML"
```
```   201 use "Tools/Meson/meson_tactic.ML"
```
```   202
```
```   203 setup {*
```
```   204   Meson_Choices.setup
```
```   205   #> Meson.setup
```
```   206   #> Meson_Tactic.setup
```
```   207 *}
```
```   208
```
```   209 end
```