Quot/Examples/AbsRepTest.thy
author Christian Urban <urbanc@in.tum.de>
Sun, 24 Jan 2010 23:41:27 +0100
changeset 918 7be9b054f672
parent 852 67e5da3a356a
child 922 a2589b4bc442
permissions -rw-r--r--
test with splits
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
779
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory AbsRepTest
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
918
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
     5
ML_command "ProofContext.debug := false"
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
     6
ML_command "ProofContext.verbose := false"
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
     7
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
     8
ML {*
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
     9
val ctxt0 = @{context}
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    10
val ty = Syntax.read_typ ctxt0 "bool"  
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    11
val ctxt1 = Variable.declare_typ ty ctxt0 
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    12
val trm = Syntax.parse_term ctxt1 "A \<and> B"
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    13
val trm' = Syntax.type_constraint ty trm
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    14
val trm'' = Syntax.check_term ctxt1 trm'
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    15
val ctxt2 = Variable.declare_term trm'' ctxt1 
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    16
*}
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    17
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    18
term "split"
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    19
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    20
term "Ex1 (\<lambda>(x, y). P x y)" 
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    21
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    22
lemma "(Ex1 (\<lambda>(x, y). P x y)) \<Longrightarrow> (\<exists>! x. \<exists>! y. P x y)"
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    23
apply(erule ex1E)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    24
apply(case_tac x)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    25
apply(clarify)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    26
apply(rule_tac a="aa" in ex1I)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    27
apply(rule ex1I)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    28
apply(assumption)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    29
apply(blast)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    30
apply(blast)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    31
done
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    32
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    33
(*
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    34
lemma "(\<exists>! x. \<exists>! y. P x y) \<Longrightarrow> (Ex1 (\<lambda>(x, y). P x y))"
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    35
apply(erule ex1E)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    36
apply(erule ex1E)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    37
apply(rule_tac a="(x, y)" in ex1I)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    38
apply(clarify)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    39
apply(case_tac xa)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    40
apply(clarify)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    41
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    42
apply(rule ex1I)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    43
apply(assumption)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    44
apply(blast)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    45
apply(blast)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    46
done
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    47
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    48
apply(metis)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    49
*)
7be9b054f672 test with splits
Christian Urban <urbanc@in.tum.de>
parents: 852
diff changeset
    50
790
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    51
ML {* open Quotient_Term *}
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    52
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    53
ML {*
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    54
fun test_funs flag ctxt (rty, qty) =
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    55
  (absrep_fun_chk flag ctxt (rty, qty)
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    56
   |> Syntax.string_of_term ctxt
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    57
   |> writeln;
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    58
   equiv_relation_chk ctxt (rty, qty) 
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    59
   |> Syntax.string_of_term ctxt
807
a5495a323b49 added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents: 803
diff changeset
    60
   |> writeln)
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    61
*}
790
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    62
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    63
definition
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    64
  erel1 (infixl "\<approx>1" 50)
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    65
where
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    66
  "erel1 \<equiv> \<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
787
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given
Christian Urban <urbanc@in.tum.de>
parents: 786
diff changeset
    67
5cf83fa5b36c made the quotient_type definition more like typedef; now type variables need to be explicitly given
Christian Urban <urbanc@in.tum.de>
parents: 786
diff changeset
    68
quotient_type 
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    69
  'a fset = "'a list" / erel1
779
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
  apply(rule equivpI)
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    71
  unfolding erel1_def reflp_def symp_def transp_def
790
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    72
  by auto
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    73
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    74
definition
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    75
  erel2 (infixl "\<approx>2" 50)
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    76
where
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    77
  "erel2 \<equiv> \<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    78
790
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    79
quotient_type 
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    80
  'a foo = "('a * 'a) list" / erel2
790
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    81
  apply(rule equivpI)
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    82
  unfolding erel2_def reflp_def symp_def transp_def
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    83
  by auto
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    84
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    85
definition
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    86
  erel3 (infixl "\<approx>3" 50)
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    87
where
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    88
  "erel3 \<equiv> \<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    89
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    90
quotient_type 
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    91
  'a bar = "('a * int) list" / "erel3"
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    92
  apply(rule equivpI)
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    93
  unfolding erel3_def reflp_def symp_def transp_def
790
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    94
  by auto
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    95
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    96
fun
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
    97
  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infixl "\<approx>4" 50)
790
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    98
where
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
    99
  "intrel (x, y) (u, v) = (x + v = u + y)"
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   100
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   101
quotient_type myint = "nat \<times> nat" / intrel
790
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   102
  by (auto simp add: equivp_def expand_fun_eq)
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   103
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   104
ML {*
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   105
test_funs absF @{context} 
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   106
     (@{typ "nat \<times> nat"}, 
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   107
      @{typ "myint"})
790
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   108
*}
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   109
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   110
ML {*
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   111
test_funs absF @{context} 
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   112
     (@{typ "('a * 'a) list"}, 
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   113
      @{typ "'a foo"})
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   114
*}
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   115
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   116
ML {*
803
6f6ee78c7357 a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents: 796
diff changeset
   117
test_funs repF @{context} 
6f6ee78c7357 a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents: 796
diff changeset
   118
     (@{typ "(('a * 'a) list * 'b)"}, 
6f6ee78c7357 a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents: 796
diff changeset
   119
      @{typ "('a foo * 'b)"})
6f6ee78c7357 a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents: 796
diff changeset
   120
*}
6f6ee78c7357 a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents: 796
diff changeset
   121
6f6ee78c7357 a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents: 796
diff changeset
   122
ML {*
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   123
test_funs absF @{context} 
790
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   124
     (@{typ "(('a list) * int) list"}, 
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   125
      @{typ "('a fset) bar"})
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   126
*}
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   127
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   128
ML {*
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   129
test_funs absF @{context} 
807
a5495a323b49 added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents: 803
diff changeset
   130
     (@{typ "('a list)"}, 
a5495a323b49 added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents: 803
diff changeset
   131
      @{typ "('a fset)"})
a5495a323b49 added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents: 803
diff changeset
   132
*}
a5495a323b49 added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents: 803
diff changeset
   133
a5495a323b49 added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents: 803
diff changeset
   134
ML {*
a5495a323b49 added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents: 803
diff changeset
   135
test_funs absF @{context} 
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   136
     (@{typ "('a list) list"}, 
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   137
      @{typ "('a fset) fset"})
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   138
*}
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   139
808
90bde96f5dd1 proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
parents: 807
diff changeset
   140
811
Christian Urban <urbanc@in.tum.de>
parents: 810
diff changeset
   141
ML {*
Christian Urban <urbanc@in.tum.de>
parents: 810
diff changeset
   142
test_funs absF @{context} 
Christian Urban <urbanc@in.tum.de>
parents: 810
diff changeset
   143
     (@{typ "((nat * nat) list) list"}, 
Christian Urban <urbanc@in.tum.de>
parents: 810
diff changeset
   144
      @{typ "((myint) fset) fset"})
Christian Urban <urbanc@in.tum.de>
parents: 810
diff changeset
   145
*}
808
90bde96f5dd1 proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
parents: 807
diff changeset
   146
795
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   147
ML {*
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   148
test_funs absF @{context} 
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   149
     (@{typ "(('a * 'a) list) list"}, 
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   150
      @{typ "(('a * 'a) fset) fset"})
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   151
*}
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   152
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   153
ML {*
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   154
test_funs absF @{context} 
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   155
      (@{typ "(nat * nat) list"}, 
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   156
       @{typ "myint fset"})
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   157
*}
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   158
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   159
ML {*
a28f805df355 renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents: 790
diff changeset
   160
test_funs absF @{context} 
796
64f9c76f70c7 corrected wrong [quot_respect] attribute; tuned
Christian Urban <urbanc@in.tum.de>
parents: 795
diff changeset
   161
     (@{typ "('a list) list \<Rightarrow> 'a list"}, 
64f9c76f70c7 corrected wrong [quot_respect] attribute; tuned
Christian Urban <urbanc@in.tum.de>
parents: 795
diff changeset
   162
      @{typ "('a fset) fset \<Rightarrow> 'a fset"})
790
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   163
*}
3a48ffcf0f9a generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents: 787
diff changeset
   164
822
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   165
lemma OO_sym_inv:
809
e9e0d1810217 Trying to state composition quotient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 808
diff changeset
   166
  assumes sr: "symp r"
e9e0d1810217 Trying to state composition quotient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 808
diff changeset
   167
  and     ss: "symp s"
e9e0d1810217 Trying to state composition quotient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 808
diff changeset
   168
  shows "(r OO s) x y = (s OO r) y x"
822
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   169
  using sr ss
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   170
  unfolding symp_def
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   171
  apply (metis pred_comp.intros pred_compE ss symp_def)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   172
  done
809
e9e0d1810217 Trying to state composition quotient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 808
diff changeset
   173
812
18b71981c1f0 Trying the proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 810
diff changeset
   174
lemma abs_o_rep:
18b71981c1f0 Trying the proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 810
diff changeset
   175
  assumes a: "Quotient r absf repf"
18b71981c1f0 Trying the proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 810
diff changeset
   176
  shows "absf o repf = id"
18b71981c1f0 Trying the proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 810
diff changeset
   177
  apply(rule ext)
18b71981c1f0 Trying the proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 810
diff changeset
   178
  apply(simp add: Quotient_abs_rep[OF a])
822
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   179
  done
812
18b71981c1f0 Trying the proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 810
diff changeset
   180
824
cedfe2a71298 Proved concat_empty.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 823
diff changeset
   181
lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
822
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   182
  apply (rule eq_reflection)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   183
  apply auto
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   184
  done
816
5edb6facc833 Further in the proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 813
diff changeset
   185
822
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   186
lemma map_rel_cong: "b \<approx>1 ba \<Longrightarrow> map f b \<approx>1 map f ba"
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   187
  unfolding erel1_def
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   188
  apply(simp only: set_map set_in_eq)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   189
  done
821
c2ebb7fcf9d0 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 820
diff changeset
   190
c2ebb7fcf9d0 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 820
diff changeset
   191
lemma quotient_compose_list_gen_pre:
c2ebb7fcf9d0 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 820
diff changeset
   192
  assumes a: "equivp r2"
c2ebb7fcf9d0 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 820
diff changeset
   193
  and b: "Quotient r2 abs2 rep2"
852
67e5da3a356a Finished replacing OO by OOO
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 831
diff changeset
   194
  shows  "(list_rel r2 OOO op \<approx>1) r s =
67e5da3a356a Finished replacing OO by OOO
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 831
diff changeset
   195
          ((list_rel r2 OOO op \<approx>1) r r \<and> (list_rel r2 OOO op \<approx>1) s s \<and>
821
c2ebb7fcf9d0 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 820
diff changeset
   196
           abs_fset (map abs2 r) = abs_fset (map abs2 s))"
822
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   197
  apply rule
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   198
  apply rule
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   199
  apply rule
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   200
  apply (rule list_rel_refl)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   201
  apply (metis equivp_def a)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   202
  apply rule
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   203
  apply (rule equivp_reflp[OF fset_equivp])
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   204
  apply (rule list_rel_refl)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   205
  apply (metis equivp_def a)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   206
  apply(rule)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   207
  apply rule
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   208
  apply (rule list_rel_refl)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   209
  apply (metis equivp_def a)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   210
  apply rule
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   211
  apply (rule equivp_reflp[OF fset_equivp])
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   212
  apply (rule list_rel_refl)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   213
  apply (metis equivp_def a)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   214
  apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   215
  apply (metis Quotient_rel[OF Quotient_fset])
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   216
  apply (auto)[1]
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   217
  apply (subgoal_tac "map abs2 r = map abs2 b")
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   218
  prefer 2
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   219
  apply (metis Quotient_rel[OF list_quotient[OF b]])
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   220
  apply (subgoal_tac "map abs2 s = map abs2 ba")
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   221
  prefer 2
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   222
  apply (metis Quotient_rel[OF list_quotient[OF b]])
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   223
  apply (simp add: map_rel_cong)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   224
  apply rule
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   225
  apply (rule rep_abs_rsp[of "list_rel r2" "map abs2"])
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   226
  apply (rule list_quotient)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   227
  apply (rule b)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   228
  apply (rule list_rel_refl)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   229
  apply (metis equivp_def a)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   230
  apply rule
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   231
  prefer 2
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   232
  apply (rule rep_abs_rsp_left[of "list_rel r2" "map abs2"])
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   233
  apply (rule list_quotient)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   234
  apply (rule b)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   235
  apply (rule list_rel_refl)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   236
  apply (metis equivp_def a)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   237
  apply (erule conjE)+
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   238
  apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   239
  apply (rule map_rel_cong)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   240
  apply (assumption)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   241
  apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   242
  done
821
c2ebb7fcf9d0 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 820
diff changeset
   243
820
162e38c14f24 The working proof of the special case.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 819
diff changeset
   244
lemma quotient_compose_list_gen:
821
c2ebb7fcf9d0 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 820
diff changeset
   245
  assumes a: "Quotient r2 abs2 rep2"
823
ae3ed7a68e80 Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 822
diff changeset
   246
  and     b: "equivp r2" (* reflp is not enough *)
852
67e5da3a356a Finished replacing OO by OOO
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 831
diff changeset
   247
  shows  "Quotient ((list_rel r2) OOO (op \<approx>1))
811
Christian Urban <urbanc@in.tum.de>
parents: 810
diff changeset
   248
               (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
812
18b71981c1f0 Trying the proof
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 810
diff changeset
   249
  unfolding Quotient_def comp_def
822
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   250
  apply (rule)+
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   251
  apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset])
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   252
  apply (rule)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   253
  apply (rule)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   254
  apply (rule)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   255
  apply (rule list_rel_refl)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   256
  apply (metis b equivp_def)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   257
  apply (rule)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   258
  apply (rule equivp_reflp[OF fset_equivp])
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   259
  apply (rule list_rel_refl)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   260
  apply (metis b equivp_def)
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   261
  apply rule
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   262
  apply rule
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   263
  apply(rule quotient_compose_list_gen_pre[OF b a])
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   264
  done
809
e9e0d1810217 Trying to state composition quotient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 808
diff changeset
   265
821
c2ebb7fcf9d0 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 820
diff changeset
   266
(* This is the general statement but the types of abs2 and rep2
c2ebb7fcf9d0 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 820
diff changeset
   267
   are wrong as can be seen in following exanples *)
818
9ab49dc166d6 More cleaning and commenting AbsRepTest. Now tests work; just slow.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 817
diff changeset
   268
lemma quotient_compose_general:
821
c2ebb7fcf9d0 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 820
diff changeset
   269
  assumes a2: "Quotient r1 abs1 rep1"
810
f73e2f5f17b2 Struggling with composition
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 809
diff changeset
   270
  and         "Quotient r2 abs2 rep2"
852
67e5da3a356a Finished replacing OO by OOO
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 831
diff changeset
   271
  shows  "Quotient ((list_rel r2) OOO r1)
821
c2ebb7fcf9d0 First generalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 820
diff changeset
   272
               (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)"
810
f73e2f5f17b2 Struggling with composition
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 809
diff changeset
   273
sorry
f73e2f5f17b2 Struggling with composition
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 809
diff changeset
   274
822
5527430f9b6f some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 821
diff changeset
   275
thm quotient_compose_list_gen[OF Quotient_fset fset_equivp]
818
9ab49dc166d6 More cleaning and commenting AbsRepTest. Now tests work; just slow.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 817
diff changeset
   276
thm quotient_compose_general[OF Quotient_fset]
817
11a23fe266c4 cleaning in AbsRepTest.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 816
diff changeset
   277
(* Doesn't work: *)
818
9ab49dc166d6 More cleaning and commenting AbsRepTest. Now tests work; just slow.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 817
diff changeset
   278
(* thm quotient_compose_general[OF Quotient_fset Quotient_fset] *)
779
3b21b24a5fb6 corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   279
809
e9e0d1810217 Trying to state composition quotient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 808
diff changeset
   280
end