src/HOL/Eisbach/Examples_FOL.thy
 author wenzelm Fri Oct 27 13:50:08 2017 +0200 (23 months ago) changeset 66924 b4d4027f743b parent 66453 cc19f7ca2ed6 permissions -rw-r--r--
more permissive;
```     1 (*  Title:      HOL/Eisbach/Examples_FOL.thy
```
```     2     Author:     Daniel Matichuk, NICTA/UNSW
```
```     3 *)
```
```     4
```
```     5 section \<open>Basic Eisbach examples (in FOL)\<close>
```
```     6
```
```     7 theory Examples_FOL
```
```     8 imports FOL Eisbach_Old_Appl_Syntax
```
```     9 begin
```
```    10
```
```    11
```
```    12 subsection \<open>Basic methods\<close>
```
```    13
```
```    14 method my_intros = (rule conjI | rule impI)
```
```    15
```
```    16 lemma "P \<and> Q \<longrightarrow> Z \<and> X"
```
```    17   apply my_intros+
```
```    18   oops
```
```    19
```
```    20 method my_intros' uses intros = (rule conjI | rule impI | rule intros)
```
```    21
```
```    22 lemma "P \<and> Q \<longrightarrow> Z \<or> X"
```
```    23   apply (my_intros' intros: disjI1)+
```
```    24   oops
```
```    25
```
```    26 method my_spec for x :: 'a = (drule spec[where x="x"])
```
```    27
```
```    28 lemma "\<forall>x. P(x) \<Longrightarrow> P(x)"
```
```    29   apply (my_spec x)
```
```    30   apply assumption
```
```    31   done
```
```    32
```
```    33
```
```    34 subsection \<open>Demo\<close>
```
```    35
```
```    36 named_theorems intros and elims and subst
```
```    37
```
```    38 method prop_solver declares intros elims subst =
```
```    39   (assumption |
```
```    40     rule intros | erule elims |
```
```    41     subst subst | subst (asm) subst |
```
```    42     (erule notE; solves prop_solver))+
```
```    43
```
```    44 lemmas [intros] =
```
```    45   conjI
```
```    46   impI
```
```    47   disjCI
```
```    48   iffI
```
```    49   notI
```
```    50 lemmas [elims] =
```
```    51   impCE
```
```    52   conjE
```
```    53   disjE
```
```    54
```
```    55 lemma "((A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C)) \<longrightarrow> C"
```
```    56   apply prop_solver
```
```    57   done
```
```    58
```
```    59 method guess_all =
```
```    60   (match premises in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
```
```    61     \<open>match premises in "?H (y :: 'a)" for y \<Rightarrow>
```
```    62        \<open>rule allE[where P = P and x = y, OF U]\<close>
```
```    63    | match conclusion in "?H (y :: 'a)" for y \<Rightarrow>
```
```    64        \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>)
```
```    65
```
```    66 lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> P(y) \<Longrightarrow> Q(y)"
```
```    67   apply guess_all
```
```    68   apply prop_solver
```
```    69   done
```
```    70
```
```    71 lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow>  P(z) \<Longrightarrow> P(y) \<Longrightarrow> Q(y)"
```
```    72   apply (solves \<open>guess_all, prop_solver\<close>)  \<comment> \<open>Try it without solve\<close>
```
```    73   done
```
```    74
```
```    75 method guess_ex =
```
```    76   (match conclusion in
```
```    77     "\<exists>x. P (x :: 'a)" for P \<Rightarrow>
```
```    78       \<open>match premises in "?H (x :: 'a)" for x \<Rightarrow>
```
```    79               \<open>rule exI[where x=x]\<close>\<close>)
```
```    80
```
```    81 lemma "P(x) \<Longrightarrow> \<exists>x. P(x)"
```
```    82   apply guess_ex
```
```    83   apply prop_solver
```
```    84   done
```
```    85
```
```    86 method fol_solver =
```
```    87   ((guess_ex | guess_all | prop_solver); solves fol_solver)
```
```    88
```
```    89 declare
```
```    90   allI [intros]
```
```    91   exE [elims]
```
```    92   ex_simps [subst]
```
```    93   all_simps [subst]
```
```    94
```
```    95 lemma "(\<forall>x. P(x)) \<and> (\<forall>x. Q(x)) \<Longrightarrow> (\<forall>x. P(x) \<and> Q(x))"
```
```    96   and  "\<exists>x. P(x) \<longrightarrow> (\<forall>x. P(x))"
```
```    97   and "(\<exists>x. \<forall>y. R(x, y)) \<longrightarrow> (\<forall>y. \<exists>x. R(x, y))"
```
```    98   by fol_solver+
```
```    99
```
```   100 end
```