IntEx.thy
author Christian Urban <urbanc@in.tum.de>
Thu, 03 Dec 2009 14:02:05 +0100
changeset 505 6cdba30c6d66
parent 504 bb23a7393de3
parent 500 184d74813679
child 506 91c374abde06
permissions -rw-r--r--
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory IntEx
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
imports QuotMain
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
504
Christian Urban <urbanc@in.tum.de>
parents: 494
diff changeset
     4
  
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
fun
281
46e6d06efe3f Experiments with lifting partially applied constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 276
diff changeset
     7
  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
where
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
  "intrel (x, y) (u, v) = (x + v = u + y)"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
quotient my_int = "nat \<times> nat" / intrel
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
  apply(unfold EQUIV_def)
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
  apply(auto simp add: mem_def expand_fun_eq)
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
  done
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
321
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
    16
thm my_int_equiv
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
    17
239
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 228
diff changeset
    18
print_theorems
274
df225aa45770 simplified the quotient_def code
Christian Urban <urbanc@in.tum.de>
parents: 268
diff changeset
    19
print_quotients
239
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 228
diff changeset
    20
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
    21
quotient_def 
218
df05cd030d2f added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 210
diff changeset
    22
  ZERO::"my_int"
df05cd030d2f added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 210
diff changeset
    23
where
df05cd030d2f added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 210
diff changeset
    24
  "ZERO \<equiv> (0::nat, 0::nat)"
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
318
746b17e1d6d8 fixed the storage of qconst definitions
Christian Urban <urbanc@in.tum.de>
parents: 312
diff changeset
    26
ML {* print_qconstinfo @{context} *}
746b17e1d6d8 fixed the storage of qconst definitions
Christian Urban <urbanc@in.tum.de>
parents: 312
diff changeset
    27
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
    28
term ZERO
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
    29
thm ZERO_def
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
290
a0be84b0c707 removed typing information from get_fun in quotient_def; *potentially* dangerous
Christian Urban <urbanc@in.tum.de>
parents: 286
diff changeset
    31
ML {* prop_of @{thm ZERO_def} *}
a0be84b0c707 removed typing information from get_fun in quotient_def; *potentially* dangerous
Christian Urban <urbanc@in.tum.de>
parents: 286
diff changeset
    32
318
746b17e1d6d8 fixed the storage of qconst definitions
Christian Urban <urbanc@in.tum.de>
parents: 312
diff changeset
    33
ML {* separate *}
746b17e1d6d8 fixed the storage of qconst definitions
Christian Urban <urbanc@in.tum.de>
parents: 312
diff changeset
    34
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
    35
quotient_def 
218
df05cd030d2f added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 210
diff changeset
    36
  ONE::"my_int"
193
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
    37
where
218
df05cd030d2f added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 210
diff changeset
    38
  "ONE \<equiv> (1::nat, 0::nat)"
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
318
746b17e1d6d8 fixed the storage of qconst definitions
Christian Urban <urbanc@in.tum.de>
parents: 312
diff changeset
    40
ML {* print_qconstinfo @{context} *}
746b17e1d6d8 fixed the storage of qconst definitions
Christian Urban <urbanc@in.tum.de>
parents: 312
diff changeset
    41
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
term ONE
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
thm ONE_def
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
fun
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
  my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
where
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
  "my_plus (x, y) (u, v) = (x + u, y + v)"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
    50
quotient_def 
218
df05cd030d2f added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 210
diff changeset
    51
  PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
df05cd030d2f added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 210
diff changeset
    52
where
275
34ad627ac5d5 fixed definition of PLUS
Christian Urban <urbanc@in.tum.de>
parents: 274
diff changeset
    53
  "PLUS \<equiv> my_plus"
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
318
746b17e1d6d8 fixed the storage of qconst definitions
Christian Urban <urbanc@in.tum.de>
parents: 312
diff changeset
    55
term my_plus
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
term PLUS
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
thm PLUS_def
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
fun
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
  my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
where
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
  "my_neg (x, y) = (y, x)"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
    64
quotient_def 
220
af951c8fb80a updated all definitions
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    65
  NEG::"my_int \<Rightarrow> my_int"
af951c8fb80a updated all definitions
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    66
where
af951c8fb80a updated all definitions
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    67
  "NEG \<equiv> my_neg"
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
term NEG
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
thm NEG_def
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
definition
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
  MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
where
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
  "MINUS z w = PLUS z (NEG w)"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
fun
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
  my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
where
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
  "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
    82
quotient_def 
220
af951c8fb80a updated all definitions
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    83
  MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
af951c8fb80a updated all definitions
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    84
where
af951c8fb80a updated all definitions
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    85
  "MULT \<equiv> my_mult"
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
term MULT
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
thm MULT_def
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
(* NOT SURE WETHER THIS DEFINITION IS CORRECT *)
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
fun
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
  my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
where
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
  "my_le (x, y) (u, v) = (x+v \<le> u+y)"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
268
4d58c02289ca simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents: 263
diff changeset
    96
quotient_def 
220
af951c8fb80a updated all definitions
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    97
  LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
af951c8fb80a updated all definitions
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    98
where
af951c8fb80a updated all definitions
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    99
  "LE \<equiv> my_le"
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
term LE
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
thm LE_def
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
321
f46dc0ca08c3 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents: 320
diff changeset
   104
181
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
definition
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
  LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
where
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
  "LESS z w = (LE z w \<and> z \<noteq> w)"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
term LESS
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   111
thm LESS_def
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   113
definition
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
  ABS :: "my_int \<Rightarrow> my_int"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
where
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
  "ABS i = (if (LESS i ZERO) then (NEG i) else i)"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
definition
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
  SIGN :: "my_int \<Rightarrow> my_int"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
where
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
 "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
3e53081ad53a added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
310
fec6301a1989 added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   123
ML {* print_qconstinfo @{context} *}
fec6301a1989 added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
parents: 306
diff changeset
   124
199
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
   125
lemma plus_sym_pre:
281
46e6d06efe3f Experiments with lifting partially applied constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 276
diff changeset
   126
  shows "my_plus a b \<approx> my_plus b a"
199
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
   127
  apply(cases a)
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
   128
  apply(cases b)
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
   129
  apply(auto)
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
   130
  done
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
   131
450
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 446
diff changeset
   132
lemma ho_plus_rsp[quot_rsp]:
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 446
diff changeset
   133
  shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
2dc708ddb93a introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents: 446
diff changeset
   134
by (simp)
192
a296bf1a3b09 Simplifying code in int
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 191
diff changeset
   135
a296bf1a3b09 Simplifying code in int
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 191
diff changeset
   136
ML {* val qty = @{typ "my_int"} *}
239
02b14a21761a Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 228
diff changeset
   137
ML {* val ty_name = "my_int" *}
458
44a70e69ef92 Code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 455
diff changeset
   138
ML {* val rsp_thms = @{thms ho_plus_rsp} *}
377
edd71fd83a2d cleaning in MyInt
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 374
diff changeset
   139
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
edd71fd83a2d cleaning in MyInt
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 374
diff changeset
   140
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
197
c0f2db9a243b Further reordering in Int code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 196
diff changeset
   141
500
184d74813679 Updated the examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 494
diff changeset
   142
ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] *}
423
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 419
diff changeset
   143
489
2b7b349e470f deleted now obsolete argument rty everywhere
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   144
ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
2b7b349e470f deleted now obsolete argument rty everywhere
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   145
ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
423
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 419
diff changeset
   146
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 419
diff changeset
   147
377
edd71fd83a2d cleaning in MyInt
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 374
diff changeset
   148
lemma "PLUS a b = PLUS b a"
423
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 419
diff changeset
   149
apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 423
diff changeset
   150
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
423
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 419
diff changeset
   151
prefer 2
500
184d74813679 Updated the examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 494
diff changeset
   152
apply(tactic {* clean_tac @{context} [quot] 1 *})
445
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   153
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   154
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   155
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   156
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   157
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   158
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   159
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   160
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   161
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   162
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   163
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   164
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   165
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   166
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   167
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   168
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   169
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   170
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   171
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   172
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   173
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   174
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   175
apply(tactic {* inj_repabs_tac_intex @{context} 1*})
423
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 419
diff changeset
   176
done
342
eb15be678ac4 lift_thm with a goal.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 340
diff changeset
   177
198
ff4425e000db Completely cleaned Int.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 197
diff changeset
   178
lemma plus_assoc_pre:
281
46e6d06efe3f Experiments with lifting partially applied constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 276
diff changeset
   179
  shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
198
ff4425e000db Completely cleaned Int.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 197
diff changeset
   180
  apply (cases i)
ff4425e000db Completely cleaned Int.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 197
diff changeset
   181
  apply (cases j)
ff4425e000db Completely cleaned Int.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 197
diff changeset
   182
  apply (cases k)
224
f9a25fe22037 Cleaning the unnecessary theorems in 'IntEx'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 222
diff changeset
   183
  apply (simp)
198
ff4425e000db Completely cleaned Int.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 197
diff changeset
   184
  done
ff4425e000db Completely cleaned Int.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 197
diff changeset
   185
377
edd71fd83a2d cleaning in MyInt
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 374
diff changeset
   186
lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
423
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 419
diff changeset
   187
apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
432
9c33c0809733 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 423
diff changeset
   188
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
445
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   189
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
500
184d74813679 Updated the examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 494
diff changeset
   190
apply(tactic {* clean_tac @{context} [quot] 1 *})
423
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 419
diff changeset
   191
done
354
2eb6d527dfe4 addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
parents: 347
diff changeset
   192
379
57bde65f6eb2 Removed unused things from QuotMain.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 377
diff changeset
   193
lemma ho_tst: "foldl my_plus x [] = x"
57bde65f6eb2 Removed unused things from QuotMain.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 377
diff changeset
   194
apply simp
57bde65f6eb2 Removed unused things from QuotMain.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 377
diff changeset
   195
done
57bde65f6eb2 Removed unused things from QuotMain.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 377
diff changeset
   196
485
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   197
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   198
lemma foldr_prs:
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   199
  assumes a: "QUOTIENT R1 abs1 rep1"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   200
  and     b: "QUOTIENT R2 abs2 rep2"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   201
  shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   202
apply (induct l)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   203
apply (simp add: QUOTIENT_ABS_REP[OF b])
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   204
apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   205
done
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   206
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   207
lemma foldl_prs:
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   208
  assumes a: "QUOTIENT R1 abs1 rep1"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   209
  and     b: "QUOTIENT R2 abs2 rep2"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   210
  shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   211
apply (induct l arbitrary:e)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   212
apply (simp add: QUOTIENT_ABS_REP[OF a])
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   213
apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   214
done
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   215
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   216
lemma map_prs:
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   217
  assumes a: "QUOTIENT R1 abs1 rep1"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   218
  and     b: "QUOTIENT R2 abs2 rep2"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   219
  shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   220
apply (induct l)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   221
apply (simp)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   222
apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   223
done
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   224
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   225
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   226
(* Removed unneeded assumption: "QUOTIENT R abs1 rep1" *)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   227
lemma nil_prs:
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   228
  shows "map abs1 [] = []"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   229
by simp
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   230
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   231
lemma cons_prs:
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   232
  assumes a: "QUOTIENT R1 abs1 rep1"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   233
  shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   234
  apply (induct t)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   235
by (simp_all add: QUOTIENT_ABS_REP[OF a])
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   236
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   237
lemma cons_rsp[quot_rsp]:
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   238
  "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   239
by simp
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   240
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   241
(* I believe it's true. *)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   242
lemma foldl_rsp[quot_rsp]:
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   243
  "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   244
apply (simp only: FUN_REL.simps)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   245
apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   246
apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   247
apply (rule impI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   248
apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   249
apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   250
apply (rule impI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   251
apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   252
apply (rule allI)
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   253
apply (rule impI)
489
2b7b349e470f deleted now obsolete argument rty everywhere
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   254
apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
414
4dad34ca50db Minor cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 409
diff changeset
   255
sorry
4dad34ca50db Minor cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 409
diff changeset
   256
485
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   257
lemma nil_listrel_rsp[quot_rsp]:
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   258
  "(LIST_REL R) [] []"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   259
by simp
416
3f3927f793d4 Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 414
diff changeset
   260
493
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   261
thm LAMBDA_PRS[no_vars]
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   262
thm all_prs[no_vars]
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   263
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   264
lemma test_all_prs:
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   265
  "\<lbrakk>QUOTIENT R absf repf; f = g\<rbrakk> \<Longrightarrow> Ball (Respects R) ((absf ---> id) f) = All g"
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   266
apply(drule all_prs)
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   267
apply(simp)
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   268
done
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   269
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   270
lemma test:
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   271
  "\<lbrakk>QUOTIENT R1 Abs1 Rep1; QUOTIENT R2 Abs2 Rep2; 
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   272
    (\<lambda>x. Rep2 (f (Abs1 x))) = lhs \<rbrakk> \<Longrightarrow> (Rep1 ---> Abs2) lhs = f"
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   273
apply -
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   274
thm LAMBDA_PRS
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   275
apply(drule LAMBDA_PRS)
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   276
apply(assumption)
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   277
apply(auto)
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   278
done
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   279
672b94510e7d deleted some dead code
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   280
379
57bde65f6eb2 Removed unused things from QuotMain.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 377
diff changeset
   281
lemma "foldl PLUS x [] = x"
445
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   282
apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   283
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
f1c0a66284d3 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de>
parents: 433
diff changeset
   284
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
485
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   285
apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   286
apply(simp only: nil_prs)
500
184d74813679 Updated the examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 494
diff changeset
   287
apply(tactic {* clean_tac @{context} [quot] 1 *})
423
2f0ad33f0241 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents: 419
diff changeset
   288
done
359
64c3c83e0ed4 New cleaning tactic
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 358
diff changeset
   289
485
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   290
lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   291
sorry
327
22c8bf90cadb tried to prove the repabs_inj lemma, but failed for the moment
Christian Urban <urbanc@in.tum.de>
parents: 326
diff changeset
   292
485
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   293
lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   294
apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   295
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   296
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   297
apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   298
apply(simp only: cons_prs[OF QUOTIENT_my_int])
500
184d74813679 Updated the examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 494
diff changeset
   299
apply(tactic {* clean_tac @{context} [quot] 1 *})
485
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   300
done
4efb104514f7 More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 466
diff changeset
   301