src/HOL/Metis_Examples/Abstraction.thy
author haftmann
Tue, 13 Jul 2010 16:00:56 +0200
changeset 37804 0145e59c1f6c
parent 36571 16ec4fe058cb
child 38991 0e2798f30087
permissions -rw-r--r--
qualified names for (almost) all array operations
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 32864
diff changeset
     1
(*  Title:      HOL/Metis_Examples/Abstraction.thy
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     3
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 32864
diff changeset
     4
Testing the metis method.
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     5
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     6
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 26819
diff changeset
     7
theory Abstraction
9f90ac19e32b established Plain theory and image
haftmann
parents: 26819
diff changeset
     8
imports Main FuncSet
23449
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
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
    24
declare [[ atp_problem_prefix = "Abstraction__Collect_triv" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    25
lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    26
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    27
  assume "a \<in> {x. P x}"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    28
  hence "a \<in> P" by (metis Collect_def)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    29
  hence "P a" by (metis mem_def)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    30
  thus "P a" by metis
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    31
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    32
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    33
lemma Collect_triv: "a \<in> {x. P x} ==> P a"
23756
14008ce7df96 Adapted to changes in Predicate theory.
berghofe
parents: 23519
diff changeset
    34
by (metis mem_Collect_eq)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    35
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    36
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
    37
declare [[ atp_problem_prefix = "Abstraction__Collect_mp" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    38
lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    39
  by (metis Collect_imp_eq ComplD UnE)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    40
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
    41
declare [[ atp_problem_prefix = "Abstraction__Sigma_triv" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    42
lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    43
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    44
  assume A1: "(a, b) \<in> Sigma A B"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    45
  hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    46
  have F2: "a \<in> A" by (metis A1 mem_Sigma_iff)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    47
  have "b \<in> B a" by (metis F1)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    48
  thus "a \<in> A \<and> b \<in> B a" by (metis F2)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    49
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    50
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    51
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
    52
by (metis SigmaD1 SigmaD2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    53
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
    54
declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect" ]]
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    55
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    56
(* Metis says this is satisfiable!
29676
cfa3378decf7 Updated comments.
paulson
parents: 28592
diff changeset
    57
by (metis CollectD SigmaD1 SigmaD2)
cfa3378decf7 Updated comments.
paulson
parents: 28592
diff changeset
    58
*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    59
by (meson CollectD SigmaD1 SigmaD2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    60
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    61
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    62
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    63
by (metis mem_Sigma_iff singleton_conv2 vimage_Collect_eq vimage_singleton_eq)
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    64
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    65
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    66
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    67
  assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    68
  have F1: "\<forall>u. {u} = op = u" by (metis singleton_conv2 Collect_def)
36571
16ec4fe058cb minor improvements
blanchet
parents: 36566
diff changeset
    69
  have F2: "\<forall>y w v. v \<in> w -` op = y \<longrightarrow> w v = y"
16ec4fe058cb minor improvements
blanchet
parents: 36566
diff changeset
    70
    by (metis F1 vimage_singleton_eq)
16ec4fe058cb minor improvements
blanchet
parents: 36566
diff changeset
    71
  have F3: "\<forall>x w. (\<lambda>R. w (x R)) = x -` w"
16ec4fe058cb minor improvements
blanchet
parents: 36566
diff changeset
    72
    by (metis vimage_Collect_eq Collect_def)
16ec4fe058cb minor improvements
blanchet
parents: 36566
diff changeset
    73
  show "a \<in> A \<and> a = f b" by (metis A1 F2 F3 mem_Sigma_iff Collect_def)
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    74
qed
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    75
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    76
(* Alternative structured proof *)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    77
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    78
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    79
  assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    80
  hence F1: "a \<in> A" by (metis mem_Sigma_iff)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    81
  have "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    82
  hence F2: "b \<in> (\<lambda>R. a = f R)" by (metis Collect_def)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    83
  hence "a = f b" by (unfold mem_def)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    84
  thus "a \<in> A \<and> a = f b" by (metis F1)
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    85
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    86
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    87
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
    88
declare [[ atp_problem_prefix = "Abstraction__CLF_eq_in_pp" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    89
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
    90
by (metis Collect_mem_eq SigmaD2)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    91
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24632
diff changeset
    92
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    93
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    94
  assume A1: "(cl, f) \<in> CLF"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    95
  assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    96
  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    97
  have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    98
  hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis F1 Collect_def)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    99
  hence "f \<in> pset cl" by (metis A1)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   100
  thus "f \<in> pset cl" by metis
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   101
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   102
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   103
declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Pi" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   104
lemma
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   105
    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   106
    f \<in> pset cl \<rightarrow> pset cl"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   107
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   108
  assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   109
  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   110
  have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   111
  hence "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   112
  thus "f \<in> pset cl \<rightarrow> pset cl" by metis
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   113
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   114
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   115
declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Int" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   116
lemma
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   117
    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   118
   f \<in> pset cl \<inter> cl"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   119
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   120
  assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   121
  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   122
  have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   123
  hence "f \<in> Id_on cl `` pset cl" by (metis F1 Int_commute Image_Id_on Collect_def)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   124
  hence "f \<in> Id_on cl `` pset cl" by metis
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   125
  hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   126
  thus "f \<in> pset cl \<inter> cl" by (metis Int_commute)
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   127
qed
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   128
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   129
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   130
declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Pi_mono" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   131
lemma
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   132
    "(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
   133
   (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   134
by auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   135
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   136
declare [[ atp_problem_prefix = "Abstraction__CLF_subset_Collect_Int" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   137
lemma "(cl,f) \<in> CLF ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   138
   CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   139
   f \<in> pset cl \<inter> cl"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   140
by auto
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 26819
diff changeset
   141
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   142
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   143
declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   144
lemma "(cl,f) \<in> CLF ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   145
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   146
   f \<in> pset cl \<inter> cl"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   147
by auto
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   148
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   149
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   150
declare [[ atp_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   151
lemma 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   152
   "(cl,f) \<in> CLF ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   153
    CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   154
    f \<in> pset cl \<rightarrow> pset cl"
31754
b5260f5272a4 tuned FuncSet
nipkow
parents: 29676
diff changeset
   155
by fast
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   156
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   157
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   158
declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   159
lemma 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   160
  "(cl,f) \<in> CLF ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   161
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   162
   f \<in> pset cl \<rightarrow> pset cl"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   163
by auto
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   164
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   165
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   166
declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   167
lemma 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   168
  "(cl,f) \<in> CLF ==> 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   169
   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
   170
   (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   171
by auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   172
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   173
declare [[ atp_problem_prefix = "Abstraction__map_eq_zipA" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   174
lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   175
apply (induct xs)
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   176
 apply (metis map_is_Nil_conv zip.simps(1))
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   177
by auto
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   178
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   179
declare [[ atp_problem_prefix = "Abstraction__map_eq_zipB" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   180
lemma "map (%w. (w -> w, w \<times> w)) xs = 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   181
       zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   182
apply (induct xs)
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   183
 apply (metis Nil_is_map_conv zip_Nil)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   184
by auto
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   185
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   186
declare [[ atp_problem_prefix = "Abstraction__image_evenA" ]]
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   187
lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   188
by (metis Collect_def image_subset_iff mem_def)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   189
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   190
declare [[ atp_problem_prefix = "Abstraction__image_evenB" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   191
lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   192
       ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   193
by (metis Collect_def imageI image_image image_subset_iff mem_def)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   194
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   195
declare [[ atp_problem_prefix = "Abstraction__image_curry" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   196
lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" 
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   197
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   198
by auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   199
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   200
declare [[ atp_problem_prefix = "Abstraction__image_TimesA" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   201
lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   202
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   203
apply (rule equalityI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   204
(***Even the two inclusions are far too difficult
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   205
using [[ atp_problem_prefix = "Abstraction__image_TimesA_simpler"]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   206
***)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   207
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   208
apply (erule imageE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   209
(*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   210
apply (erule ssubst)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   211
apply (erule SigmaE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   212
(*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   213
apply (erule ssubst)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   214
apply (subst split_conv)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   215
apply (rule SigmaI) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   216
apply (erule imageI) +
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   217
txt{*subgoal 2*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   218
apply (clarify );
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   219
apply (simp add: );  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   220
apply (rule rev_image_eqI)  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   221
apply (blast intro: elim:); 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   222
apply (simp add: );
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   223
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   224
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   225
(*Given the difficulty of the previous problem, these two are probably
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   226
impossible*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   227
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   228
declare [[ atp_problem_prefix = "Abstraction__image_TimesB" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   229
lemma image_TimesB:
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   230
    "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   231
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   232
by force
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   233
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 31754
diff changeset
   234
declare [[ atp_problem_prefix = "Abstraction__image_TimesC" ]]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   235
lemma image_TimesC:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   236
    "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   237
     ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" 
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   238
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   239
by auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   240
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   241
end