src/HOL/MetisExamples/Abstraction.thy
author paulson
Thu, 04 Oct 2007 12:32:58 +0200
changeset 24827 646bdc51eb7d
parent 24783 5a3e336a2e37
child 26819 56036226028b
permissions -rw-r--r--
combinator translation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     1
(*  Title:      HOL/MetisExamples/Abstraction.thy
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     2
    ID:         $Id$
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     4
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     5
Testing the metis method
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     6
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     7
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     8
theory Abstraction imports FuncSet
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     9
begin
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    10
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    11
(*For Christoph Benzmueller*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    12
lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))";
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    13
  by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    14
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    15
(*this is a theorem, but we can't prove it unless ext is applied explicitly
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    16
lemma "(op=) = (%x y. y=x)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    17
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    18
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    19
consts
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    20
  monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    21
  pset  :: "'a set => 'a set"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    22
  order :: "'a set => ('a * 'a) set"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    23
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    24
ML{*ResAtp.problem_name := "Abstraction__Collect_triv"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    25
lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    26
proof (neg_clausify)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    27
assume 0: "(a\<Colon>'a\<Colon>type) \<in> Collect (P\<Colon>'a\<Colon>type \<Rightarrow> bool)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    28
assume 1: "\<not> (P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    29
have 2: "(P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    30
  by (metis CollectD 0)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    31
show "False"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    32
  by (metis 2 1)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    33
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    34
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    35
lemma Collect_triv: "a \<in> {x. P x} ==> P a"
23756
14008ce7df96 Adapted to changes in Predicate theory.
berghofe
parents: 23519
diff changeset
    36
by (metis mem_Collect_eq)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    37
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    38
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    39
ML{*ResAtp.problem_name := "Abstraction__Collect_mp"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    40
lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
23756
14008ce7df96 Adapted to changes in Predicate theory.
berghofe
parents: 23519
diff changeset
    41
  by (metis CollectI Collect_imp_eq ComplD UnE mem_Collect_eq);
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    42
  --{*34 secs*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    43
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    44
ML{*ResAtp.problem_name := "Abstraction__Sigma_triv"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    45
lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    46
proof (neg_clausify)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    47
assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type) \<in> Sigma (A\<Colon>'a\<Colon>type set) (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    48
assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> (b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) a"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    49
have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    50
  by (metis SigmaD1 0)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    51
have 3: "(b\<Colon>'b\<Colon>type) \<in> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    52
  by (metis SigmaD2 0)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    53
have 4: "(b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    54
  by (metis 1 2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    55
show "False"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    56
  by (metis 3 4)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    57
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    58
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    59
lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    60
by (metis SigmaD1 SigmaD2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    61
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    62
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    63
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    64
(*???metis cannot prove this
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    65
by (metis CollectD SigmaD1 SigmaD2 UN_eq)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    66
Also, UN_eq is unnecessary*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    67
by (meson CollectD SigmaD1 SigmaD2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    68
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    69
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    70
(*single-step*)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    71
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    72
by (metis SigmaD1 SigmaD2 insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def vimage_singleton_eq)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    73
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    74
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    75
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    76
proof (neg_clausify)
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    77
assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    78
\<in> Sigma (A\<Colon>'a\<Colon>type set)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    79
   (COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)))"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    80
assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> a \<noteq> (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type)"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    81
have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    82
  by (metis 0 SigmaD1)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    83
have 3: "(b\<Colon>'b\<Colon>type)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    84
\<in> COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)) (a\<Colon>'a\<Colon>type)"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    85
  by (metis 0 SigmaD2) 
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    86
have 4: "(b\<Colon>'b\<Colon>type) \<in> Collect (COMBB (op = (a\<Colon>'a\<Colon>type)) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type))"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    87
  by (metis 3)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    88
have 5: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) \<noteq> (a\<Colon>'a\<Colon>type)"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    89
  by (metis 1 2)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    90
have 6: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) = (a\<Colon>'a\<Colon>type)"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    91
  by (metis 4 vimage_singleton_eq insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    92
show "False"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    93
  by (metis 5 6)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    94
qed
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    95
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    96
(*Alternative structured proof, untyped*)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    97
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    98
proof (neg_clausify)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    99
assume 0: "(a, b) \<in> Sigma A (COMBB Collect (COMBC (COMBB COMBB op =) f))"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   100
have 1: "b \<in> Collect (COMBB (op = a) f)"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   101
  by (metis 0 SigmaD2)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   102
have 2: "f b = a"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   103
  by (metis 1 vimage_Collect_eq singleton_conv2 insert_def union_empty2 vimage_singleton_eq vimage_def)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   104
assume 3: "a \<notin> A \<or> a \<noteq> f b"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   105
have 4: "a \<in> A"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   106
  by (metis 0 SigmaD1)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   107
have 5: "f b \<noteq> a"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   108
  by (metis 4 3)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   109
show "False"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   110
  by (metis 5 2)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   111
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   112
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   113
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   114
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_in_pp"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   115
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   116
by (metis Collect_mem_eq SigmaD2)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   117
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24632
diff changeset
   118
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24632
diff changeset
   119
proof (neg_clausify)
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   120
assume 0: "(cl, f) \<in> CLF"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   121
assume 1: "CLF = Sigma CL (COMBB Collect (COMBB (COMBC op \<in>) pset))"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   122
assume 2: "f \<notin> pset cl"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   123
have 3: "\<And>X1 X2. X2 \<in> COMBB Collect (COMBB (COMBC op \<in>) pset) X1 \<or> (X1, X2) \<notin> CLF"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   124
  by (metis SigmaD2 1)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   125
have 4: "\<And>X1 X2. X2 \<in> pset X1 \<or> (X1, X2) \<notin> CLF"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   126
  by (metis 3 Collect_mem_eq)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   127
have 5: "(cl, f) \<notin> CLF"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   128
  by (metis 2 4)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   129
show "False"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   130
  by (metis 5 0)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   131
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   132
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   133
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   134
lemma
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   135
    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   136
    f \<in> pset cl \<rightarrow> pset cl"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   137
proof (neg_clausify)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   138
assume 0: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   139
assume 1: "(cl, f)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   140
\<in> Sigma CL
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   141
   (COMBB Collect
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   142
     (COMBB (COMBC op \<in>) (COMBS (COMBB Pi pset) (COMBB COMBK pset))))"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   143
show "False"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   144
(*  by (metis 0 Collect_mem_eq SigmaD2 1) ??doesn't terminate*)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   145
  by (insert 0 1, simp add: COMBB_def COMBS_def COMBC_def)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   146
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   147
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   148
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   149
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   150
lemma
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   151
    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   152
   f \<in> pset cl \<inter> cl"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   153
proof (neg_clausify)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   154
assume 0: "(cl, f)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   155
\<in> Sigma CL
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   156
   (COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)))"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   157
assume 1: "f \<notin> pset cl \<inter> cl"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   158
have 2: "f \<in> COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)) cl" 
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   159
  by (insert 0, simp add: COMBB_def) 
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   160
(*  by (metis SigmaD2 0)  ??doesn't terminate*)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   161
have 3: "f \<in> COMBS (COMBB op \<inter> pset) COMBI cl"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   162
  by (metis 2 Collect_mem_eq)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   163
have 4: "f \<notin> cl \<inter> pset cl"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   164
  by (metis 1 Int_commute)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   165
have 5: "f \<in> cl \<inter> pset cl"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   166
  by (metis 3 Int_commute)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   167
show "False"
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   168
  by (metis 5 4)
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   169
qed
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   170
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   171
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   172
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   173
lemma
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   174
    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   175
   (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   176
by auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   177
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   178
ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Int"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   179
lemma "(cl,f) \<in> CLF ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   180
   CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   181
   f \<in> pset cl \<inter> cl"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   182
by auto
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   183
(*??no longer terminates, with combinators
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   184
by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   185
  --{*@{text Int_def} is redundant}
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   186
*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   187
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   188
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   189
lemma "(cl,f) \<in> CLF ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   190
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   191
   f \<in> pset cl \<inter> cl"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   192
by auto
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   193
(*??no longer terminates, with combinators
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   194
by (metis Collect_mem_eq Int_commute SigmaD2)
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   195
*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   196
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   197
ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   198
lemma 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   199
   "(cl,f) \<in> CLF ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   200
    CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   201
    f \<in> pset cl \<rightarrow> pset cl"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   202
by auto
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   203
(*??no longer terminates, with combinators
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   204
by (metis Collect_mem_eq SigmaD2 subsetD)
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   205
*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   206
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   207
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   208
lemma 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   209
  "(cl,f) \<in> CLF ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   210
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   211
   f \<in> pset cl \<rightarrow> pset cl"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   212
by auto
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   213
(*??no longer terminates, with combinators
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   214
by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   215
*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   216
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   217
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   218
lemma 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   219
  "(cl,f) \<in> CLF ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   220
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   221
   (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   222
by auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   223
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   224
ML{*ResAtp.problem_name := "Abstraction__map_eq_zipA"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   225
lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   226
apply (induct xs)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   227
(*sledgehammer*)  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   228
apply auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   229
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   230
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   231
ML{*ResAtp.problem_name := "Abstraction__map_eq_zipB"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   232
lemma "map (%w. (w -> w, w \<times> w)) xs = 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   233
       zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   234
apply (induct xs)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   235
(*sledgehammer*)  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   236
apply auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   237
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   238
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   239
ML{*ResAtp.problem_name := "Abstraction__image_evenA"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   240
lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)";
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   241
(*sledgehammer*)  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   242
by auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   243
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   244
ML{*ResAtp.problem_name := "Abstraction__image_evenB"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   245
lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   246
       ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   247
(*sledgehammer*)  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   248
by auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   249
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   250
ML{*ResAtp.problem_name := "Abstraction__image_curry"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   251
lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   252
(*sledgehammer*)  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   253
by auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   254
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   255
ML{*ResAtp.problem_name := "Abstraction__image_TimesA"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   256
lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   257
(*sledgehammer*) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   258
apply (rule equalityI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   259
(***Even the two inclusions are far too difficult
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   260
ML{*ResAtp.problem_name := "Abstraction__image_TimesA_simpler"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   261
***)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   262
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   263
apply (erule imageE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   264
(*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   265
apply (erule ssubst)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   266
apply (erule SigmaE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   267
(*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   268
apply (erule ssubst)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   269
apply (subst split_conv)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   270
apply (rule SigmaI) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   271
apply (erule imageI) +
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   272
txt{*subgoal 2*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   273
apply (clarify );
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   274
apply (simp add: );  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   275
apply (rule rev_image_eqI)  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   276
apply (blast intro: elim:); 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   277
apply (simp add: );
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   278
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   279
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   280
(*Given the difficulty of the previous problem, these two are probably
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   281
impossible*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   282
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   283
ML{*ResAtp.problem_name := "Abstraction__image_TimesB"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   284
lemma image_TimesB:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   285
    "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)" 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   286
(*sledgehammer*) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   287
by force
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   288
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   289
ML{*ResAtp.problem_name := "Abstraction__image_TimesC"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   290
lemma image_TimesC:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   291
    "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   292
     ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   293
(*sledgehammer*) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   294
by auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   295
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   296
end