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