src/HOL/Eisbach/Examples.thy
author wenzelm
Sat, 16 May 2015 12:05:52 +0200
changeset 60285 b4f1a0a701ae
parent 60248 f7e4294216d2
child 61909 d5ead6bfa1ff
permissions -rw-r--r--
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60248
f7e4294216d2 updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents: 60209
diff changeset
     1
(*  Title:      HOL/Eisbach/Examples.thy
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     2
    Author:     Daniel Matichuk, NICTA/UNSW
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     3
*)
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     4
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     5
section \<open>Basic Eisbach examples\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     6
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     7
theory Examples
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     8
imports Main Eisbach_Tools
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
     9
begin
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    10
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    11
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    12
subsection \<open>Basic methods\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    13
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    14
method my_intros = (rule conjI | rule impI)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    15
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    16
lemma "P \<and> Q \<longrightarrow> Z \<and> X"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    17
  apply my_intros+
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    18
  oops
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    19
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    20
method my_intros' uses intros = (rule conjI | rule impI | rule intros)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    21
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    22
lemma "P \<and> Q \<longrightarrow> Z \<or> X"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    23
  apply (my_intros' intros: disjI1)+
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    24
  oops
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    25
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    26
method my_spec for x :: 'a = (drule spec[where x="x"])
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    27
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    28
lemma "\<forall>x. P x \<Longrightarrow> P x"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    29
  apply (my_spec x)
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    30
  apply assumption
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    31
  done
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    32
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    33
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    34
subsection \<open>Focusing and matching\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    35
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    36
method match_test =
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    37
  (match premises in U: "P x \<and> Q x" for P Q x \<Rightarrow>
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    38
    \<open>print_term P,
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    39
     print_term Q,
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    40
     print_term x,
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    41
     print_fact U\<close>)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    42
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    43
lemma "\<And>x. P x \<and> Q x \<Longrightarrow> A x \<and> B x \<Longrightarrow> R x y \<Longrightarrow> True"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    44
  apply match_test  -- \<open>Valid match, but not quite what we were expecting..\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    45
  back  -- \<open>Can backtrack over matches, exploring all bindings\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    46
  back
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    47
  back
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    48
  back
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    49
  back
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    50
  back  -- \<open>Found the other conjunction\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    51
  back
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    52
  back
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    53
  back
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    54
  oops
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    55
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    56
text \<open>Use matching to avoid "improper" methods\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    57
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    58
lemma focus_test:
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    59
  shows "\<And>x. \<forall>x. P x \<Longrightarrow> P x"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    60
  apply (my_spec "x :: 'a", assumption)?  -- \<open>Wrong x\<close>
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    61
  apply (match conclusion in "P x" for x \<Rightarrow> \<open>my_spec x, assumption\<close>)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    62
  done
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    63
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    64
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    65
text \<open>Matches are exclusive. Backtracking will not occur past a match\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    66
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    67
method match_test' =
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    68
  (match conclusion in
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    69
    "P \<and> Q" for P Q \<Rightarrow>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    70
      \<open>print_term P, print_term Q, rule conjI[where P="P" and Q="Q"]; assumption\<close>
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
    71
    \<bar> "H" for H \<Rightarrow> \<open>print_term H\<close>)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    72
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    73
text \<open>Solves goal\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    74
lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    75
  apply match_test'
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    76
  done
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    77
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    78
text \<open>Fall-through case never taken\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    79
lemma "P \<and> Q"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    80
  apply match_test'?
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    81
  oops
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    82
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    83
lemma "P"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    84
  apply match_test'
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    85
  oops
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    86
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    87
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    88
method my_spec_guess =
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    89
  (match conclusion in "P (x :: 'a)" for P x \<Rightarrow>
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    90
    \<open>drule spec[where x=x],
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    91
     print_term P,
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    92
     print_term x\<close>)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    93
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    94
lemma "\<forall>x. P (x :: nat) \<Longrightarrow> Q (x :: nat)"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    95
  apply my_spec_guess
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    96
  oops
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    97
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
    98
method my_spec_guess2 =
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
    99
  (match premises in U[thin]:"\<forall>x. P x \<longrightarrow> Q x" and U':"P x" for P Q x \<Rightarrow>
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   100
    \<open>insert spec[where x=x, OF U],
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   101
     print_term P,
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   102
     print_term Q\<close>)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   103
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   104
lemma "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> Q x \<Longrightarrow> Q x"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   105
  apply my_spec_guess2?  -- \<open>Fails. Note that both "P"s must match\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   106
  oops
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   107
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   108
lemma "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> P x \<Longrightarrow> Q x"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   109
  apply my_spec_guess2
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   110
  apply (erule mp)
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   111
  apply assumption
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   112
  done
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   113
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   114
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   115
subsection \<open>Higher-order methods\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   116
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   117
method higher_order_example for x methods meth =
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   118
  (cases x, meth, meth)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   120
lemma
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   121
  assumes A: "x = Some a"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   122
  shows "the x = a"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   123
  by (higher_order_example x \<open>simp add: A\<close>)
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   124
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   125
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   126
subsection \<open>Recursion\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   127
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   128
method recursion_example for x :: bool =
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   129
  (print_term x,
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   130
     match (x) in "A \<and> B" for A B \<Rightarrow>
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   131
    \<open>print_term A,
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   132
     print_term B,
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   133
     recursion_example A,
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   134
     recursion_example B | -\<close>)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   135
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   136
lemma "P"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   137
  apply (recursion_example "(A \<and> D) \<and> (B \<and> C)")
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   138
  oops
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   139
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   140
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   141
subsection \<open>Solves combinator\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   142
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   143
lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   144
  apply (solves \<open>rule conjI\<close>)?  -- \<open>Doesn't solve the goal!\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   145
  apply (solves \<open>rule conjI, assumption, assumption\<close>)
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   146
  done
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   147
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   148
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   149
subsection \<open>Demo\<close>
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   150
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   151
named_theorems intros and elims and subst
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   152
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   153
method prop_solver declares intros elims subst =
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   154
  (assumption |
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   155
    rule intros | erule elims |
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   156
    subst subst | subst (asm) subst |
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   157
    (erule notE; solves \<open>prop_solver\<close>))+
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   158
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   159
lemmas [intros] =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   160
  conjI
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   161
  impI
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   162
  disjCI
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   163
  iffI
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   164
  notI
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   165
lemmas [elims] =
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   166
  impCE
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   167
  conjE
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   168
  disjE
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   169
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   170
lemma "((A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C)) \<longrightarrow> C"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   171
  apply prop_solver
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   172
  done
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   173
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   174
method guess_all =
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   175
  (match premises in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   176
    \<open>match premises in "?H (y :: 'a)" for y \<Rightarrow>
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   177
       \<open>rule allE[where P = P and x = y, OF U]\<close>
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   178
   | match conclusion in "?H (y :: 'a)" for y \<Rightarrow>
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   179
       \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   180
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   181
lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> P y \<Longrightarrow> Q y"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   182
  apply guess_all
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   183
  apply prop_solver
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   184
  done
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   185
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   186
lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow>  P z \<Longrightarrow> P y \<Longrightarrow> Q y"
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   187
  apply (solves \<open>guess_all, prop_solver\<close>)  -- \<open>Try it without solve\<close>
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   188
  done
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   189
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   190
method guess_ex =
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   191
  (match conclusion in
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   192
    "\<exists>x. P (x :: 'a)" for P \<Rightarrow>
60209
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   193
      \<open>match premises in "?H (x :: 'a)" for x \<Rightarrow>
022ca2799c73 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents: 60119
diff changeset
   194
              \<open>rule exI[where x=x]\<close>\<close>)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   195
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   196
lemma "P x \<Longrightarrow> \<exists>x. P x"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   197
  apply guess_ex
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   198
  apply prop_solver
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   199
  done
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   200
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   201
method fol_solver =
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   202
  ((guess_ex | guess_all | prop_solver) ; solves \<open>fol_solver\<close>)
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   203
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   204
declare
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   205
  allI [intros]
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   206
  exE [elims]
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   207
  ex_simps [subst]
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   208
  all_simps [subst]
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   209
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   210
lemma "(\<forall>x. P x) \<and> (\<forall>x. Q x) \<Longrightarrow> (\<forall>x. P x \<and> Q x)"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   211
  and  "\<exists>x. P x \<longrightarrow> (\<forall>x. P x)"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   212
  and "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   213
  by fol_solver+
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   214
60285
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   215
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   216
text \<open>
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   217
  Eisbach_Tools provides the catch method, which catches run-time method
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   218
  errors. In this example the OF attribute throws an error when it can't
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   219
  compose H with A, forcing H to be re-bound to different members of imps
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   220
  until it succeeds.
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   221
\<close>
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   222
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   223
lemma
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   224
  assumes imps:  "A \<Longrightarrow> B" "A \<Longrightarrow> C" "B \<Longrightarrow> D"
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   225
  assumes A: "A"
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   226
  shows "B \<and> C"
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   227
  apply (rule conjI)
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   228
  apply ((match imps in H:"_ \<Longrightarrow> _" \<Rightarrow> \<open>catch \<open>rule H[OF A], print_fact H\<close> \<open>print_fact H, fail\<close>\<close>)+)
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   229
  done
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   230
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   231
text \<open>
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   232
  Eisbach_Tools provides the curry and uncurry attributes. This is useful
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   233
  when the number of premises of a thm isn't known statically. The pattern
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   234
  @{term "P \<Longrightarrow> Q"} matches P against the major premise of a thm, and Q is the
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   235
  rest of the premises with the conclusion. If we first uncurry, then @{term
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   236
  "P \<Longrightarrow> Q"} will match P with the conjunction of all the premises, and Q with
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   237
  the final conclusion of the rule.
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   238
\<close>
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   239
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   240
lemma
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   241
  assumes imps: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C" "E \<Longrightarrow> D \<Longrightarrow> A"
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   242
  shows "(A \<longrightarrow> B \<longrightarrow> C) \<and> (D \<longrightarrow> C)"
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   243
    by (match imps[uncurry] in H[curry]:"_ \<Longrightarrow> C" (cut, multi) \<Rightarrow>
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   244
                    \<open>match H in "E \<Longrightarrow> _" \<Rightarrow> \<open>fail\<close>
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   245
                                      \<bar> _ \<Rightarrow> \<open>simp add: H\<close>\<close>)
b4f1a0a701ae updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents: 60248
diff changeset
   246
60119
54bea620e54f added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff changeset
   247
end