equal
deleted
inserted
replaced
4 Copyright 1997 Technische Universitaet Muenchen |
4 Copyright 1997 Technische Universitaet Muenchen |
5 |
5 |
6 *) |
6 *) |
7 open FRACT; |
7 open FRACT; |
8 |
8 |
9 goalw thy [per_def,per_NP_def] |
9 Goalw [per_def,per_NP_def] |
10 "(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"; |
10 "(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"; |
11 fr refl; |
11 fr refl; |
12 qed "inst_NP_per"; |
12 qed "inst_NP_per"; |
13 |
13 |
14 |
14 |
15 goalw thy [half_def] "half = <[abs_NP(n,2*n)]>"; |
15 Goalw [half_def] "half = <[abs_NP(n,2*n)]>"; |
16 fr per_class_eqI; |
16 fr per_class_eqI; |
17 by (simp_tac (simpset() addsimps [inst_NP_per]) 1); |
17 by (simp_tac (simpset() addsimps [inst_NP_per]) 1); |
18 qed "test"; |
18 qed "test"; |