Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
authorwenzelm
Wed Jan 13 16:41:32 2016 +0100 (2016-01-13)
changeset 62168e97452d79102
parent 62167 cb806a024bba
child 62169 a6047f511de7
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
NEWS
src/HOL/Eisbach/Eisbach_Old_Appl_Syntax.thy
src/HOL/Eisbach/Examples_FOL.thy
src/HOL/ROOT
     1.1 --- a/NEWS	Wed Jan 13 16:01:03 2016 +0100
     1.2 +++ b/NEWS	Wed Jan 13 16:41:32 2016 +0100
     1.3 @@ -9,6 +9,12 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Eisbach is now based on Pure instead of HOL. Objects-logics may import
     1.8 +either the theory ~~/src/HOL/Eisbach/Eisbach (for HOL etc.) or
     1.9 +~~/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax (for FOL, ZF etc.). Note that
    1.10 +the HOL-Eisbach session located in ~~/src/HOL/Eisbach/ contains further
    1.11 +examples that do require HOL.
    1.12 +
    1.13  * Better resource usage on all platforms (Linux, Windows, Mac OS X) for
    1.14  both Isabelle/ML and Isabelle/Scala.  Slightly reduced heap space usage.
    1.15  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax.thy	Wed Jan 13 16:41:32 2016 +0100
     2.3 @@ -0,0 +1,13 @@
     2.4 +(*  Title:      HOL/Eisbach/Eisbach_Old_Appl_Syntax.thy
     2.5 +    Author:     Makarius
     2.6 +*)
     2.7 +
     2.8 +section \<open>Alternative Eisbach entry point for FOL, ZF etc.\<close>
     2.9 +
    2.10 +theory Eisbach_Old_Appl_Syntax
    2.11 +imports Eisbach
    2.12 +begin
    2.13 +
    2.14 +setup Pure_Thy.old_appl_syntax_setup
    2.15 +
    2.16 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Eisbach/Examples_FOL.thy	Wed Jan 13 16:41:32 2016 +0100
     3.3 @@ -0,0 +1,100 @@
     3.4 +(*  Title:      HOL/Eisbach/Examples.thy
     3.5 +    Author:     Daniel Matichuk, NICTA/UNSW
     3.6 +*)
     3.7 +
     3.8 +section \<open>Basic Eisbach examples (in FOL)\<close>
     3.9 +
    3.10 +theory Examples_FOL
    3.11 +imports "~~/src/FOL/FOL" Eisbach_Old_Appl_Syntax
    3.12 +begin
    3.13 +
    3.14 +
    3.15 +subsection \<open>Basic methods\<close>
    3.16 +
    3.17 +method my_intros = (rule conjI | rule impI)
    3.18 +
    3.19 +lemma "P \<and> Q \<longrightarrow> Z \<and> X"
    3.20 +  apply my_intros+
    3.21 +  oops
    3.22 +
    3.23 +method my_intros' uses intros = (rule conjI | rule impI | rule intros)
    3.24 +
    3.25 +lemma "P \<and> Q \<longrightarrow> Z \<or> X"
    3.26 +  apply (my_intros' intros: disjI1)+
    3.27 +  oops
    3.28 +
    3.29 +method my_spec for x :: 'a = (drule spec[where x="x"])
    3.30 +
    3.31 +lemma "\<forall>x. P(x) \<Longrightarrow> P(x)"
    3.32 +  apply (my_spec x)
    3.33 +  apply assumption
    3.34 +  done
    3.35 +
    3.36 +
    3.37 +subsection \<open>Demo\<close>
    3.38 +
    3.39 +named_theorems intros and elims and subst
    3.40 +
    3.41 +method prop_solver declares intros elims subst =
    3.42 +  (assumption |
    3.43 +    rule intros | erule elims |
    3.44 +    subst subst | subst (asm) subst |
    3.45 +    (erule notE; solves prop_solver))+
    3.46 +
    3.47 +lemmas [intros] =
    3.48 +  conjI
    3.49 +  impI
    3.50 +  disjCI
    3.51 +  iffI
    3.52 +  notI
    3.53 +lemmas [elims] =
    3.54 +  impCE
    3.55 +  conjE
    3.56 +  disjE
    3.57 +
    3.58 +lemma "((A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C)) \<longrightarrow> C"
    3.59 +  apply prop_solver
    3.60 +  done
    3.61 +
    3.62 +method guess_all =
    3.63 +  (match premises in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
    3.64 +    \<open>match premises in "?H (y :: 'a)" for y \<Rightarrow>
    3.65 +       \<open>rule allE[where P = P and x = y, OF U]\<close>
    3.66 +   | match conclusion in "?H (y :: 'a)" for y \<Rightarrow>
    3.67 +       \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>)
    3.68 +
    3.69 +lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> P(y) \<Longrightarrow> Q(y)"
    3.70 +  apply guess_all
    3.71 +  apply prop_solver
    3.72 +  done
    3.73 +
    3.74 +lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow>  P(z) \<Longrightarrow> P(y) \<Longrightarrow> Q(y)"
    3.75 +  apply (solves \<open>guess_all, prop_solver\<close>)  \<comment> \<open>Try it without solve\<close>
    3.76 +  done
    3.77 +
    3.78 +method guess_ex =
    3.79 +  (match conclusion in
    3.80 +    "\<exists>x. P (x :: 'a)" for P \<Rightarrow>
    3.81 +      \<open>match premises in "?H (x :: 'a)" for x \<Rightarrow>
    3.82 +              \<open>rule exI[where x=x]\<close>\<close>)
    3.83 +
    3.84 +lemma "P(x) \<Longrightarrow> \<exists>x. P(x)"
    3.85 +  apply guess_ex
    3.86 +  apply prop_solver
    3.87 +  done
    3.88 +
    3.89 +method fol_solver =
    3.90 +  ((guess_ex | guess_all | prop_solver); solves fol_solver)
    3.91 +
    3.92 +declare
    3.93 +  allI [intros]
    3.94 +  exE [elims]
    3.95 +  ex_simps [subst]
    3.96 +  all_simps [subst]
    3.97 +
    3.98 +lemma "(\<forall>x. P(x)) \<and> (\<forall>x. Q(x)) \<Longrightarrow> (\<forall>x. P(x) \<and> Q(x))"
    3.99 +  and  "\<exists>x. P(x) \<longrightarrow> (\<forall>x. P(x))"
   3.100 +  and "(\<exists>x. \<forall>y. R(x, y)) \<longrightarrow> (\<forall>y. \<exists>x. R(x, y))"
   3.101 +  by fol_solver+
   3.102 +
   3.103 +end
     4.1 --- a/src/HOL/ROOT	Wed Jan 13 16:01:03 2016 +0100
     4.2 +++ b/src/HOL/ROOT	Wed Jan 13 16:41:32 2016 +0100
     4.3 @@ -658,6 +658,7 @@
     4.4      Eisbach
     4.5      Tests
     4.6      Examples
     4.7 +    Examples_FOL
     4.8  
     4.9  session "HOL-SET_Protocol" in SET_Protocol = HOL +
    4.10    description {*