src/HOL/ex/Refute_Examples.thy
author wenzelm
Fri, 12 Oct 2012 18:58:20 +0200
changeset 49834 b27bbb021df1
parent 46099 40ac5ae6d16f
child 49988 ef811090e106
permissions -rw-r--r--
discontinued obsolete typedef (open) syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     1
(*  Title:      HOL/ex/Refute_Examples.thy
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     2
    Author:     Tjark Weber
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
     3
    Copyright   2003-2007
32968
wenzelm
parents: 28524
diff changeset
     4
wenzelm
parents: 28524
diff changeset
     5
See HOL/Refute.thy for help.
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     6
*)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     7
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     8
header {* Examples for the 'refute' command *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     9
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    10
theory Refute_Examples
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    11
imports Main
15297
0aff5d912422 imports (new syntax for theory headers)
webertj
parents: 15161
diff changeset
    12
begin
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    13
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    14
refute_params [satsolver = "dpll"]
18774
7cf74a743c32 works with DPLL solver now
webertj
parents: 16910
diff changeset
    15
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    16
lemma "P \<and> Q"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    17
apply (rule conjI)
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    18
refute [expect = genuine] 1  -- {* refutes @{term "P"} *}
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    19
refute [expect = genuine] 2  -- {* refutes @{term "Q"} *}
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    20
refute [expect = genuine]    -- {* equivalent to 'refute 1' *}
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    21
  -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    22
refute [maxsize = 5, expect = genuine]   -- {* we can override parameters ... *}
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    23
refute [satsolver = "dpll", expect = genuine] 2
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    24
  -- {* ... and specify a subgoal at the same time *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    25
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    26
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
    27
(*****************************************************************************)
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
    28
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
    29
subsection {* Examples and Test Cases *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    30
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
    31
subsubsection {* Propositional logic *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    32
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    33
lemma "True"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    34
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    35
by auto
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    36
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    37
lemma "False"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    38
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    39
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    40
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    41
lemma "P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    42
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    43
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    44
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    45
lemma "~ P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    46
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    47
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    48
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    49
lemma "P & Q"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    50
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    51
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    52
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    53
lemma "P | Q"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    54
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    55
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    56
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    57
lemma "P \<longrightarrow> Q"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    58
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    59
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    60
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    61
lemma "(P::bool) = Q"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    62
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    63
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    64
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    65
lemma "(P | Q) \<longrightarrow> (P & Q)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    66
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    67
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    68
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
    69
(*****************************************************************************)
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
    70
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
    71
subsubsection {* Predicate logic *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    72
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
    73
lemma "P x y z"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    74
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    75
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    76
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    77
lemma "P x y \<longrightarrow> P y x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    78
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    79
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    80
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
    81
lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    82
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
    83
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
    84
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
    85
(*****************************************************************************)
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
    86
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
    87
subsubsection {* Equality *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    88
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    89
lemma "P = True"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    90
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    91
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    92
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    93
lemma "P = False"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    94
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    95
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    96
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    97
lemma "x = y"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
    98
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    99
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   100
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   101
lemma "f x = g x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   102
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   103
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   104
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   105
lemma "(f::'a\<Rightarrow>'b) = g"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   106
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   107
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   108
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   109
lemma "(f::('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   110
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   111
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   112
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   113
lemma "distinct [a, b]"
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   114
(* refute *)
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   115
apply simp
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   116
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   117
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   118
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   119
(*****************************************************************************)
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   120
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   121
subsubsection {* First-Order Logic *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   122
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   123
lemma "\<exists>x. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   124
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   125
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   126
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   127
lemma "\<forall>x. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   128
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   129
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   130
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   131
lemma "EX! x. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   132
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   133
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   134
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   135
lemma "Ex P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   136
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   137
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   138
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   139
lemma "All P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   140
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   141
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   142
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   143
lemma "Ex1 P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   144
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   145
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   146
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   147
lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   148
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   149
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   150
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   151
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   152
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   153
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   154
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   155
lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   156
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   157
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   158
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   159
text {* A true statement (also testing names of free and bound variables being identical) *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   160
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   161
lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   162
refute [maxsize = 4, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   163
by fast
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   164
18789
8a5c6fc3ad27 smaller example to prevent timeout
webertj
parents: 18774
diff changeset
   165
text {* "A type has at most 4 elements." *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   166
18789
8a5c6fc3ad27 smaller example to prevent timeout
webertj
parents: 18774
diff changeset
   167
lemma "a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   168
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   169
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   170
18789
8a5c6fc3ad27 smaller example to prevent timeout
webertj
parents: 18774
diff changeset
   171
lemma "\<forall>a b c d e. a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   172
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   173
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   174
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   175
text {* "Every reflexive and symmetric relation is transitive." *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   176
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   177
lemma "\<lbrakk> \<forall>x. P x x; \<forall>x y. P x y \<longrightarrow> P y x \<rbrakk> \<Longrightarrow> P x y \<longrightarrow> P y z \<longrightarrow> P x z"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   178
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   179
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   180
14465
8cc21ed7ef41 \<dots> replaced by ...
webertj
parents: 14462
diff changeset
   181
text {* The "Drinker's theorem" ... *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   182
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   183
lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   184
refute [maxsize = 4, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   185
by (auto simp add: ext)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   186
14465
8cc21ed7ef41 \<dots> replaced by ...
webertj
parents: 14462
diff changeset
   187
text {* ... and an incorrect version of it *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   188
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   189
lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   190
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   191
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   192
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   193
text {* "Every function has a fixed point." *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   194
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   195
lemma "\<exists>x. f x = x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   196
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   197
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   198
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   199
text {* "Function composition is commutative." *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   200
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   201
lemma "f (g x) = g (f x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   202
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   203
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   204
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   205
text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   206
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   207
lemma "((P::('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   208
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   209
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   210
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   211
(*****************************************************************************)
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   212
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   213
subsubsection {* Higher-Order Logic *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   214
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   215
lemma "\<exists>P. P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   216
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   217
by auto
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   218
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   219
lemma "\<forall>P. P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   220
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   221
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   222
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   223
lemma "EX! P. P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   224
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   225
by auto
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   226
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   227
lemma "EX! P. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   228
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   229
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   230
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   231
lemma "P Q | Q x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   232
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   233
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   234
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   235
lemma "x \<noteq> All"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   236
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   237
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   238
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   239
lemma "x \<noteq> Ex"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   240
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   241
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   242
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   243
lemma "x \<noteq> Ex1"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   244
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   245
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   246
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   247
text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   248
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   249
definition "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   250
  "trans P == (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   251
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   252
definition "subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   253
  "subset P Q == (ALL x y. P x y \<longrightarrow> Q x y)"
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   254
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   255
definition "trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   256
  "trans_closure P Q == (subset Q P) & (trans P) & (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   257
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   258
lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   259
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   260
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   261
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   262
text {* "The union of transitive closures is equal to the transitive closure of unions." *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   263
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   264
lemma "(\<forall>x y. (P x y | R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y | R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   265
        \<longrightarrow> trans_closure TP P
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   266
        \<longrightarrow> trans_closure TR R
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   267
        \<longrightarrow> (T x y = (TP x y | TR x y))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   268
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   269
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   270
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   271
text {* "Every surjective function is invertible." *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   272
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   273
lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   274
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   275
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   276
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   277
text {* "Every invertible function is surjective." *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   278
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   279
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   280
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   281
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   282
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   283
text {* Every point is a fixed point of some function. *}
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   284
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   285
lemma "\<exists>f. f x = x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   286
refute [maxsize = 4, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   287
apply (rule_tac x="\<lambda>x. x" in exI)
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   288
by simp
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   289
14465
8cc21ed7ef41 \<dots> replaced by ...
webertj
parents: 14462
diff changeset
   290
text {* Axiom of Choice: first an incorrect version ... *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   291
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   292
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   293
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   294
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   295
14465
8cc21ed7ef41 \<dots> replaced by ...
webertj
parents: 14462
diff changeset
   296
text {* ... and now two correct ones *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   297
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   298
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   299
refute [maxsize = 4, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   300
by (simp add: choice)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   301
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   302
lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   303
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   304
apply auto
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   305
  apply (simp add: ex1_implies_ex choice)
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   306
by (fast intro: ext)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   307
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   308
(*****************************************************************************)
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   309
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   310
subsubsection {* Meta-logic *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   311
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   312
lemma "!!x. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   313
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   314
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   315
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   316
lemma "f x == g x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   317
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   318
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   319
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   320
lemma "P \<Longrightarrow> Q"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   321
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   322
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   323
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   324
lemma "\<lbrakk> P; Q; R \<rbrakk> \<Longrightarrow> S"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   325
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   326
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   327
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   328
lemma "(x == all) \<Longrightarrow> False"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   329
refute [expect = genuine]
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   330
oops
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   331
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   332
lemma "(x == (op ==)) \<Longrightarrow> False"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   333
refute [expect = genuine]
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   334
oops
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   335
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   336
lemma "(x == (op \<Longrightarrow>)) \<Longrightarrow> False"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   337
refute [expect = genuine]
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   338
oops
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   339
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   340
(*****************************************************************************)
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   341
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   342
subsubsection {* Schematic variables *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   343
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 36131
diff changeset
   344
schematic_lemma "?P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   345
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   346
by auto
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   347
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 36131
diff changeset
   348
schematic_lemma "x = ?y"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   349
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   350
by auto
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   351
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   352
(******************************************************************************)
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   353
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   354
subsubsection {* Abstractions *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   355
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   356
lemma "(\<lambda>x. x) = (\<lambda>x. y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   357
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   358
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   359
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   360
lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   361
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   362
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   363
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   364
lemma "(\<lambda>x. x) = (\<lambda>y. y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   365
refute
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   366
by simp
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   367
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   368
(*****************************************************************************)
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   369
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   370
subsubsection {* Sets *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   371
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   372
lemma "P (A::'a set)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   373
refute
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   374
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   375
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   376
lemma "P (A::'a set set)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   377
refute
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   378
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   379
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   380
lemma "{x. P x} = {y. P y}"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   381
refute
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   382
by simp
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   383
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   384
lemma "x : {x. P x}"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   385
refute
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   386
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   387
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   388
lemma "P op:"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   389
refute
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   390
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   391
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   392
lemma "P (op: x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   393
refute
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   394
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   395
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   396
lemma "P Collect"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   397
refute
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   398
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   399
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   400
lemma "A Un B = A Int B"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   401
refute
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   402
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   403
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   404
lemma "(A Int B) Un C = (A Un C) Int B"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   405
refute
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   406
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   407
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   408
lemma "Ball A P \<longrightarrow> Bex A P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   409
refute
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   410
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   411
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   412
(*****************************************************************************)
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   413
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 25032
diff changeset
   414
subsubsection {* undefined *}
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   415
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 25032
diff changeset
   416
lemma "undefined"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   417
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   418
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   419
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 25032
diff changeset
   420
lemma "P undefined"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   421
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   422
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   423
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 25032
diff changeset
   424
lemma "undefined x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   425
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   426
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   427
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 25032
diff changeset
   428
lemma "undefined undefined"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   429
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   430
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   431
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   432
(*****************************************************************************)
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   433
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   434
subsubsection {* The *}
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   435
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   436
lemma "The P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   437
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   438
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   439
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   440
lemma "P The"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   441
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   442
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   443
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   444
lemma "P (The P)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   445
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   446
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   447
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   448
lemma "(THE x. x=y) = z"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   449
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   450
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   451
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   452
lemma "Ex P \<longrightarrow> P (The P)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   453
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   454
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   455
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   456
(*****************************************************************************)
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
   457
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   458
subsubsection {* Eps *}
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   459
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   460
lemma "Eps P"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   461
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   462
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   463
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   464
lemma "P Eps"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   465
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   466
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   467
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   468
lemma "P (Eps P)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   469
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   470
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   471
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   472
lemma "(SOME x. x=y) = z"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   473
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   474
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   475
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   476
lemma "Ex P \<longrightarrow> P (Eps P)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   477
refute [maxsize = 3, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   478
by (auto simp add: someI)
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   479
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   480
(*****************************************************************************)
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
   481
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   482
subsubsection {* Subtypes (typedef), typedecl *}
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   483
15161
065ce5385a06 comment modified
webertj
parents: 14809
diff changeset
   484
text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
065ce5385a06 comment modified
webertj
parents: 14809
diff changeset
   485
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 37388
diff changeset
   486
definition "myTdef = insert (undefined::'a) (undefined::'a set)"
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 37388
diff changeset
   487
49834
b27bbb021df1 discontinued obsolete typedef (open) syntax;
wenzelm
parents: 46099
diff changeset
   488
typedef 'a myTdef = "myTdef :: 'a set"
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 37388
diff changeset
   489
  unfolding myTdef_def by auto
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   490
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   491
lemma "(x::'a myTdef) = y"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   492
refute
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   493
oops
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   494
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   495
typedecl myTdecl
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   496
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 37388
diff changeset
   497
definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 37388
diff changeset
   498
49834
b27bbb021df1 discontinued obsolete typedef (open) syntax;
wenzelm
parents: 46099
diff changeset
   499
typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 37388
diff changeset
   500
  unfolding T_bij_def by auto
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   501
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   502
lemma "P (f::(myTdecl myTdef) T_bij)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   503
refute
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   504
oops
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   505
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   506
(*****************************************************************************)
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
   507
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   508
subsubsection {* Inductive datatypes *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   509
21502
7f3ea2b3bab6 prefer antiquotations over LaTeX macros;
wenzelm
parents: 18789
diff changeset
   510
text {* With @{text quick_and_dirty} set, the datatype package does
7f3ea2b3bab6 prefer antiquotations over LaTeX macros;
wenzelm
parents: 18789
diff changeset
   511
  not generate certain axioms for recursion operators.  Without these
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   512
  axioms, Refute may find spurious countermodels. *}
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   513
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   514
text {* unit *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   515
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   516
lemma "P (x::unit)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   517
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   518
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   519
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   520
lemma "\<forall>x::unit. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   521
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   522
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   523
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   524
lemma "P ()"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   525
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   526
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   527
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   528
lemma "unit_rec u x = u"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   529
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   530
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   531
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   532
lemma "P (unit_rec u x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   533
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   534
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   535
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   536
lemma "P (case x of () \<Rightarrow> u)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   537
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   538
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   539
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   540
text {* option *}
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   541
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   542
lemma "P (x::'a option)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   543
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   544
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   545
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   546
lemma "\<forall>x::'a option. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   547
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   548
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   549
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   550
lemma "P None"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   551
refute [expect = genuine]
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   552
oops
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   553
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   554
lemma "P (Some x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   555
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   556
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   557
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   558
lemma "option_rec n s None = n"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   559
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   560
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   561
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   562
lemma "option_rec n s (Some x) = s x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   563
refute [maxsize = 4, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   564
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   565
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   566
lemma "P (option_rec n s x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   567
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   568
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   569
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   570
lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   571
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   572
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   573
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   574
text {* * *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   575
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   576
lemma "P (x::'a*'b)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   577
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   578
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   579
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   580
lemma "\<forall>x::'a*'b. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   581
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   582
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   583
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   584
lemma "P (x, y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   585
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   586
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   587
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   588
lemma "P (fst x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   589
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   590
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   591
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   592
lemma "P (snd x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   593
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   594
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   595
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   596
lemma "P Pair"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   597
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   598
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   599
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   600
lemma "prod_rec p (a, b) = p a b"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   601
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   602
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   603
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   604
lemma "P (prod_rec p x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   605
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   606
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   607
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   608
lemma "P (case x of Pair a b \<Rightarrow> p a b)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   609
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   610
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   611
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   612
text {* + *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   613
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   614
lemma "P (x::'a+'b)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   615
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   616
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   617
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   618
lemma "\<forall>x::'a+'b. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   619
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   620
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   621
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   622
lemma "P (Inl x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   623
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   624
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   625
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   626
lemma "P (Inr x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   627
refute [expect = genuine]
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   628
oops
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   629
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   630
lemma "P Inl"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   631
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   632
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   633
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   634
lemma "sum_rec l r (Inl x) = l x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   635
refute [maxsize = 3, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   636
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   637
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   638
lemma "sum_rec l r (Inr x) = r x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   639
refute [maxsize = 3, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   640
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   641
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   642
lemma "P (sum_rec l r x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   643
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   644
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   645
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   646
lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   647
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   648
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   649
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   650
text {* Non-recursive datatypes *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   651
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   652
datatype T1 = A | B
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   653
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   654
lemma "P (x::T1)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   655
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   656
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   657
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   658
lemma "\<forall>x::T1. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   659
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   660
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   661
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   662
lemma "P A"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   663
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   664
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   665
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   666
lemma "P B"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   667
refute [expect = genuine]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   668
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   669
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   670
lemma "T1_rec a b A = a"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   671
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   672
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   673
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   674
lemma "T1_rec a b B = b"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   675
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   676
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   677
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   678
lemma "P (T1_rec a b x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   679
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   680
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   681
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   682
lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   683
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   684
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   685
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   686
datatype 'a T2 = C T1 | D 'a
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   687
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   688
lemma "P (x::'a T2)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   689
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   690
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   691
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   692
lemma "\<forall>x::'a T2. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   693
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   694
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   695
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   696
lemma "P D"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   697
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   698
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   699
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   700
lemma "T2_rec c d (C x) = c x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   701
refute [maxsize = 4, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   702
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   703
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   704
lemma "T2_rec c d (D x) = d x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   705
refute [maxsize = 4, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   706
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   707
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   708
lemma "P (T2_rec c d x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   709
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   710
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   711
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   712
lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   713
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   714
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   715
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   716
datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   717
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   718
lemma "P (x::('a,'b) T3)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   719
refute [expect = genuine]
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   720
oops
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   721
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   722
lemma "\<forall>x::('a,'b) T3. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   723
refute [expect = genuine]
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   724
oops
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   725
14455
5c4a1e96efd6 Updated examples
webertj
parents: 14350
diff changeset
   726
lemma "P E"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   727
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   728
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   729
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   730
lemma "T3_rec e (E x) = e x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   731
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   732
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   733
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   734
lemma "P (T3_rec e x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   735
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   736
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   737
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   738
lemma "P (case x of E f \<Rightarrow> e f)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   739
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   740
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   741
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   742
text {* Recursive datatypes *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   743
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   744
text {* nat *}
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   745
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   746
lemma "P (x::nat)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   747
refute [expect = potential]
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   748
oops
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   749
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   750
lemma "\<forall>x::nat. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   751
refute [expect = potential]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   752
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   753
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   754
lemma "P (Suc 0)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   755
refute [expect = potential]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   756
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   757
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   758
lemma "P Suc"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   759
refute [maxsize = 3, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   760
-- {* @{term Suc} is a partial function (regardless of the size
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   761
      of the model), hence @{term "P Suc"} is undefined and no
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   762
      model will be found *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   763
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   764
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   765
lemma "nat_rec zero suc 0 = zero"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   766
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   767
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   768
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   769
lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   770
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   771
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   772
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   773
lemma "P (nat_rec zero suc x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   774
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   775
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   776
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   777
lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   778
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   779
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   780
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   781
text {* 'a list *}
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   782
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   783
lemma "P (xs::'a list)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   784
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   785
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   786
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   787
lemma "\<forall>xs::'a list. P xs"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   788
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   789
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   790
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   791
lemma "P [x, y]"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   792
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   793
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   794
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   795
lemma "list_rec nil cons [] = nil"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   796
refute [maxsize = 3, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   797
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   798
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   799
lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   800
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   801
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   802
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   803
lemma "P (list_rec nil cons xs)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   804
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   805
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   806
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   807
lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   808
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   809
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   810
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   811
lemma "(xs::'a list) = ys"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   812
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   813
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   814
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   815
lemma "a # xs = b # xs"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   816
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   817
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   818
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   819
datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   820
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   821
lemma "P (x::BitList)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   822
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   823
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   824
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   825
lemma "\<forall>x::BitList. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   826
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   827
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   828
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   829
lemma "P (Bit0 (Bit1 BitListNil))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   830
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   831
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   832
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   833
lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   834
refute [maxsize = 4, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   835
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   836
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   837
lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   838
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   839
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   840
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   841
lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   842
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   843
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   844
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   845
lemma "P (BitList_rec nil bit0 bit1 x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   846
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   847
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   848
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   849
datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   850
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   851
lemma "P (x::'a BinTree)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   852
refute [expect = potential]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   853
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   854
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   855
lemma "\<forall>x::'a BinTree. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   856
refute [expect = potential]
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   857
oops
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   858
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
   859
lemma "P (Node (Leaf x) (Leaf y))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   860
refute [expect = potential]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   861
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   862
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   863
lemma "BinTree_rec l n (Leaf x) = l x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   864
  refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   865
  (* The "maxsize = 1" tests are a bit pointless: for some formulae
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   866
     below, refute will find no countermodel simply because this
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   867
     size makes involved terms undefined.  Unfortunately, any
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   868
     larger size already takes too long. *)
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   869
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   870
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   871
lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   872
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   873
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   874
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   875
lemma "P (BinTree_rec l n x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   876
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   877
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   878
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   879
lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   880
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   881
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   882
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
   883
text {* Mutually recursive datatypes *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   884
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   885
datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   886
     and 'a bexp = Equal "'a aexp" "'a aexp"
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   887
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   888
lemma "P (x::'a aexp)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   889
refute [expect = potential]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   890
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   891
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   892
lemma "\<forall>x::'a aexp. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   893
refute [expect = potential]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   894
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   895
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   896
lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   897
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   898
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   899
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   900
lemma "P (x::'a bexp)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   901
refute [expect = potential]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   902
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   903
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   904
lemma "\<forall>x::'a bexp. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   905
refute [expect = potential]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   906
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   907
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   908
lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   909
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   910
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   911
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   912
lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   913
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   914
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   915
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   916
lemma "P (aexp_bexp_rec_1 number ite equal x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   917
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   918
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   919
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   920
lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   921
refute [expect = potential]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   922
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   923
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   924
lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   925
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   926
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   927
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   928
lemma "P (aexp_bexp_rec_2 number ite equal x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   929
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   930
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   931
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   932
lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   933
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   934
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
   935
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   936
datatype X = A | B X | C Y
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   937
     and Y = D X | E Y | F
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   938
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   939
lemma "P (x::X)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   940
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   941
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   942
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   943
lemma "P (y::Y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   944
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   945
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   946
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   947
lemma "P (B (B A))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   948
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   949
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   950
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   951
lemma "P (B (C F))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   952
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   953
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   954
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   955
lemma "P (C (D A))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   956
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   957
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   958
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   959
lemma "P (C (E F))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   960
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   961
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   962
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   963
lemma "P (D (B A))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   964
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   965
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   966
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   967
lemma "P (D (C F))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   968
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   969
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   970
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   971
lemma "P (E (D A))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   972
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   973
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   974
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   975
lemma "P (E (E F))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   976
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   977
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   978
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   979
lemma "P (C (D (C F)))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   980
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   981
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   982
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   983
lemma "X_Y_rec_1 a b c d e f A = a"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   984
refute [maxsize = 3, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   985
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   986
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   987
lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   988
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   989
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   990
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   991
lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   992
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   993
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   994
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   995
lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   996
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
   997
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   998
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
   999
lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1000
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1001
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1002
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1003
lemma "X_Y_rec_2 a b c d e f F = f"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1004
refute [maxsize = 3, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1005
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1006
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1007
lemma "P (X_Y_rec_1 a b c d e f x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1008
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1009
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1010
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1011
lemma "P (X_Y_rec_2 a b c d e f y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1012
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1013
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1014
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
  1015
text {* Other datatype examples *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
  1016
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1017
text {* Indirect recursion is implemented via mutual recursion. *}
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1018
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1019
datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1020
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1021
lemma "P (x::XOpt)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1022
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1023
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1024
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1025
lemma "P (CX None)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1026
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1027
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1028
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1029
lemma "P (CX (Some (CX None)))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1030
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1031
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1032
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1033
lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1034
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1035
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1036
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1037
lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1038
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1039
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1040
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1041
lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1042
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1043
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1044
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1045
lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1046
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1047
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1048
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1049
lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1050
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1051
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1052
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1053
lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1054
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1055
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1056
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1057
lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1058
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1059
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1060
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1061
lemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1062
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1063
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1064
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1065
lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1066
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1067
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1068
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1069
datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1070
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1071
lemma "P (x::'a YOpt)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1072
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1073
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1074
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1075
lemma "P (CY None)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1076
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1077
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1078
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1079
lemma "P (CY (Some (\<lambda>a. CY None)))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1080
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1081
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1082
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1083
lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1084
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1085
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1086
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1087
lemma "YOpt_rec_2 cy n s None = n"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1088
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1089
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1090
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1091
lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1092
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1093
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1094
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1095
lemma "P (YOpt_rec_1 cy n s x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1096
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1097
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1098
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1099
lemma "P (YOpt_rec_2 cy n s x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1100
refute [expect = potential]
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1101
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1102
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1103
datatype Trie = TR "Trie list"
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1104
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1105
lemma "P (x::Trie)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1106
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1107
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1108
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1109
lemma "\<forall>x::Trie. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1110
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1111
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1112
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1113
lemma "P (TR [TR []])"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1114
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1115
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1116
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1117
lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1118
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1119
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1120
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1121
lemma "Trie_rec_2 tr nil cons [] = nil"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1122
refute [maxsize = 3, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1123
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1124
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1125
lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1126
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1127
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1128
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1129
lemma "P (Trie_rec_1 tr nil cons x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1130
refute [expect = potential]
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1131
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1132
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1133
lemma "P (Trie_rec_2 tr nil cons x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1134
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1135
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1136
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
  1137
datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
  1138
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
  1139
lemma "P (x::InfTree)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1140
refute [expect = potential]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
  1141
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
  1142
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1143
lemma "\<forall>x::InfTree. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1144
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1145
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1146
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1147
lemma "P (Node (\<lambda>n. Leaf))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1148
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1149
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1150
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1151
lemma "InfTree_rec leaf node Leaf = leaf"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1152
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1153
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1154
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1155
lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1156
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1157
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1158
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1159
lemma "P (InfTree_rec leaf node x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1160
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1161
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1162
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
  1163
datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
  1164
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1165
lemma "P (x::'a lambda)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1166
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1167
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1168
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1169
lemma "\<forall>x::'a lambda. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1170
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1171
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1172
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1173
lemma "P (Lam (\<lambda>a. Var a))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1174
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1175
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1176
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1177
lemma "lambda_rec var app lam (Var x) = var x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1178
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1179
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1180
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1181
lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1182
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1183
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1184
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1185
lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1186
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1187
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1188
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1189
lemma "P (lambda_rec v a l x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1190
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1191
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1192
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1193
text {* Taken from "Inductive datatypes in HOL", p.8: *}
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1194
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1195
datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1196
datatype 'c U = E "('c, 'c U) T"
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1197
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1198
lemma "P (x::'c U)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1199
refute [expect = potential]
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1200
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1201
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1202
lemma "\<forall>x::'c U. P x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1203
refute [expect = potential]
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1204
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1205
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1206
lemma "P (E (C (\<lambda>a. True)))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1207
refute [expect = potential]
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1208
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1209
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1210
lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1211
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1212
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1213
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1214
lemma "U_rec_2 e c d nil cons (C x) = c x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1215
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1216
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1217
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1218
lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1219
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1220
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1221
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1222
lemma "U_rec_3 e c d nil cons [] = nil"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1223
refute [maxsize = 2, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1224
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1225
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1226
lemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1227
refute [maxsize = 1, expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1228
by simp
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1229
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1230
lemma "P (U_rec_1 e c d nil cons x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1231
refute [expect = potential]
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1232
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1233
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1234
lemma "P (U_rec_2 e c d nil cons x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1235
refute [expect = potential]
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1236
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1237
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1238
lemma "P (U_rec_3 e c d nil cons x)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1239
refute [expect = potential]
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1240
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1241
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1242
(*****************************************************************************)
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1243
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
  1244
subsubsection {* Records *}
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1245
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1246
(*TODO: make use of pair types, rather than typedef, for record types*)
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1247
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1248
record ('a, 'b) point =
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1249
  xpos :: 'a
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1250
  ypos :: 'b
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1251
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1252
lemma "(x::('a, 'b) point) = y"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1253
refute
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1254
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1255
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1256
record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1257
  ext :: 'c
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1258
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1259
lemma "(x::('a, 'b, 'c) extpoint) = y"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1260
refute
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1261
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1262
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1263
(*****************************************************************************)
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1264
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
  1265
subsubsection {* Inductively defined sets *}
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1266
23778
18f426a137a9 Adapted to new inductive definition package.
berghofe
parents: 23219
diff changeset
  1267
inductive_set arbitrarySet :: "'a set"
18f426a137a9 Adapted to new inductive definition package.
berghofe
parents: 23219
diff changeset
  1268
where
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 25032
diff changeset
  1269
  "undefined : arbitrarySet"
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1270
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1271
lemma "x : arbitrarySet"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1272
refute
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1273
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1274
23778
18f426a137a9 Adapted to new inductive definition package.
berghofe
parents: 23219
diff changeset
  1275
inductive_set evenCard :: "'a set set"
18f426a137a9 Adapted to new inductive definition package.
berghofe
parents: 23219
diff changeset
  1276
where
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1277
  "{} : evenCard"
23778
18f426a137a9 Adapted to new inductive definition package.
berghofe
parents: 23219
diff changeset
  1278
| "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1279
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1280
lemma "S : evenCard"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1281
refute
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1282
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1283
23778
18f426a137a9 Adapted to new inductive definition package.
berghofe
parents: 23219
diff changeset
  1284
inductive_set
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1285
  even :: "nat set"
23778
18f426a137a9 Adapted to new inductive definition package.
berghofe
parents: 23219
diff changeset
  1286
  and odd  :: "nat set"
18f426a137a9 Adapted to new inductive definition package.
berghofe
parents: 23219
diff changeset
  1287
where
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1288
  "0 : even"
23778
18f426a137a9 Adapted to new inductive definition package.
berghofe
parents: 23219
diff changeset
  1289
| "n : even \<Longrightarrow> Suc n : odd"
18f426a137a9 Adapted to new inductive definition package.
berghofe
parents: 23219
diff changeset
  1290
| "n : odd \<Longrightarrow> Suc n : even"
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1291
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1292
lemma "n : odd"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1293
(* refute *)  (* TODO: there seems to be an issue here with undefined terms
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1294
                       because of the recursive datatype "nat" *)
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1295
oops
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1296
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1297
consts f :: "'a \<Rightarrow> 'a"
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1298
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1299
inductive_set
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1300
  a_even :: "'a set"
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1301
  and a_odd :: "'a set"
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1302
where
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 25032
diff changeset
  1303
  "undefined : a_even"
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1304
| "x : a_even \<Longrightarrow> f x : a_odd"
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1305
| "x : a_odd \<Longrightarrow> f x : a_even"
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1306
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1307
lemma "x : a_odd"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1308
(* refute [expect = genuine] -- {* finds a model of size 2 *}
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1309
   NO LONGER WORKS since "lfp"'s interpreter is disabled *)
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1310
oops
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1311
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1312
(*****************************************************************************)
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1313
23219
87ad6e8a5f2c tuned document;
wenzelm
parents: 22284
diff changeset
  1314
subsubsection {* Examples involving special functions *}
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1315
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1316
lemma "card x = 0"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1317
refute
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1318
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1319
15767
8ed9fcc004fe support for recursion over mutually recursive IDTs
webertj
parents: 15547
diff changeset
  1320
lemma "finite x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1321
refute -- {* no finite countermodel exists *}
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1322
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1323
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1324
lemma "(x::nat) + y = 0"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1325
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1326
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1327
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1328
lemma "(x::nat) = x + x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1329
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1330
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1331
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1332
lemma "(x::nat) - y + y = x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1333
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1334
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1335
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1336
lemma "(x::nat) = x * x"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1337
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1338
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1339
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1340
lemma "(x::nat) < x + y"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1341
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1342
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1343
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
  1344
lemma "xs @ [] = ys @ []"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1345
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1346
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1347
21985
acfb13e8819e constants are unfolded, universal quantifiers are stripped, some minor changes
webertj
parents: 21559
diff changeset
  1348
lemma "xs @ ys = ys @ xs"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1349
refute [expect = potential]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1350
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1351
16050
828fc32f390f interpreters for lfp/gfp added
webertj
parents: 15767
diff changeset
  1352
lemma "f (lfp f) = lfp f"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1353
refute
16050
828fc32f390f interpreters for lfp/gfp added
webertj
parents: 15767
diff changeset
  1354
oops
828fc32f390f interpreters for lfp/gfp added
webertj
parents: 15767
diff changeset
  1355
828fc32f390f interpreters for lfp/gfp added
webertj
parents: 15767
diff changeset
  1356
lemma "f (gfp f) = gfp f"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1357
refute
16050
828fc32f390f interpreters for lfp/gfp added
webertj
parents: 15767
diff changeset
  1358
oops
828fc32f390f interpreters for lfp/gfp added
webertj
parents: 15767
diff changeset
  1359
828fc32f390f interpreters for lfp/gfp added
webertj
parents: 15767
diff changeset
  1360
lemma "lfp f = gfp f"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1361
refute
16050
828fc32f390f interpreters for lfp/gfp added
webertj
parents: 15767
diff changeset
  1362
oops
828fc32f390f interpreters for lfp/gfp added
webertj
parents: 15767
diff changeset
  1363
25014
b711b0af178e significant code overhaul, bugfix for inductive data types
webertj
parents: 24447
diff changeset
  1364
(*****************************************************************************)
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1365
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 34120
diff changeset
  1366
subsubsection {* Type classes and overloading *}
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1367
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1368
text {* A type class without axioms: *}
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1369
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 34120
diff changeset
  1370
class classA
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1371
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1372
lemma "P (x::'a::classA)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1373
refute [expect = genuine]
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
  1374
oops
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
  1375
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1376
text {* An axiom with a type variable (denoting types which have at least two elements): *}
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1377
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 34120
diff changeset
  1378
class classC =
fbdc860d87a3 dropped axclass
haftmann
parents: 34120
diff changeset
  1379
  assumes classC_ax: "\<exists>x y. x \<noteq> y"
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1380
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1381
lemma "P (x::'a::classC)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1382
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1383
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1384
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1385
lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1386
(* refute [expect = none] FIXME *)
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1387
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1388
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1389
text {* A type class for which a constant is defined: *}
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1390
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 34120
diff changeset
  1391
class classD =
fbdc860d87a3 dropped axclass
haftmann
parents: 34120
diff changeset
  1392
  fixes classD_const :: "'a \<Rightarrow> 'a"
fbdc860d87a3 dropped axclass
haftmann
parents: 34120
diff changeset
  1393
  assumes classD_ax: "classD_const (classD_const x) = classD_const x"
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1394
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1395
lemma "P (x::'a::classD)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1396
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1397
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1398
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1399
text {* A type class with multiple superclasses: *}
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1400
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 34120
diff changeset
  1401
class classE = classC + classD
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1402
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1403
lemma "P (x::'a::classE)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1404
refute [expect = genuine]
14809
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
  1405
oops
eaa5d6987ba2 mainly new/different datatype examples
webertj
parents: 14489
diff changeset
  1406
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1407
text {* OFCLASS: *}
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1408
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1409
lemma "OFCLASS('a::type, type_class)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1410
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1411
by intro_classes
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1412
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1413
lemma "OFCLASS('a::classC, type_class)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1414
refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1415
by intro_classes
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1416
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1417
lemma "OFCLASS('a::type, classC_class)"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1418
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1419
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1420
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1421
text {* Overloading: *}
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1422
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1423
consts inverse :: "'a \<Rightarrow> 'a"
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1424
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1425
defs (overloaded)
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1426
  inverse_bool: "inverse (b::bool)   == ~ b"
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1427
  inverse_set : "inverse (S::'a set) == -S"
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1428
  inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1429
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1430
lemma "inverse b"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1431
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1432
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1433
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1434
lemma "P (inverse (S::'a set))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1435
refute [expect = genuine]
15547
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1436
oops
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1437
f08e2d83681e major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
webertj
parents: 15297
diff changeset
  1438
lemma "P (inverse (p::'a\<times>'b))"
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1439
refute [expect = genuine]
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
  1440
oops
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
  1441
34120
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 32968
diff changeset
  1442
text {* Structured proofs *}
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 32968
diff changeset
  1443
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 32968
diff changeset
  1444
lemma "x = y"
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 32968
diff changeset
  1445
proof cases
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 32968
diff changeset
  1446
  assume "x = y"
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 32968
diff changeset
  1447
  show ?thesis
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1448
  refute [expect = none]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1449
  refute [no_assms, expect = genuine]
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1450
  refute [no_assms = false, expect = none]
34120
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 32968
diff changeset
  1451
oops
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 32968
diff changeset
  1452
46099
40ac5ae6d16f reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
blanchet
parents: 45972
diff changeset
  1453
refute_params [satsolver = "auto"]
18774
7cf74a743c32 works with DPLL solver now
webertj
parents: 16910
diff changeset
  1454
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
  1455
end