equal
deleted
inserted
replaced
1 theory AbsRepTest |
1 theory AbsRepTest |
2 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List |
2 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List |
3 begin |
3 begin |
4 |
4 |
5 |
|
6 (* |
|
7 quotient_type |
5 quotient_type |
8 fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
6 fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
9 apply(rule equivpI) |
7 apply(rule equivpI) |
10 unfolding reflp_def symp_def transp_def |
8 unfolding reflp_def symp_def transp_def |
11 apply(auto) |
9 apply(auto) |
12 sorry |
|
13 done |
10 done |
14 *) |
|
15 |
|
16 inductive |
|
17 list_eq (infix "\<approx>" 50) |
|
18 where |
|
19 "a#b#xs \<approx> b#a#xs" |
|
20 | "[] \<approx> []" |
|
21 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs" |
|
22 | "a#a#xs \<approx> a#xs" |
|
23 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
|
24 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
|
25 |
|
26 quotient_type |
|
27 fset = "'a list" / "list_eq" |
|
28 sorry |
|
29 |
|
30 |
11 |
31 fun |
12 fun |
32 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
13 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
33 where |
14 where |
34 "intrel (x, y) (u, v) = (x + v = u + y)" |
15 "intrel (x, y) (u, v) = (x + v = u + y)" |
35 |
16 |
36 quotient_type int = "nat \<times> nat" / intrel |
17 quotient_type int = "nat \<times> nat" / intrel |
37 sorry |
18 sorry |
38 |
|
39 |
19 |
40 ML {* |
20 ML {* |
41 open Quotient_Term; |
21 open Quotient_Term; |
42 *} |
22 *} |
43 |
23 |