equal
deleted
inserted
replaced
700 fixes z |
700 fixes z |
701 assumes a: "xs \<approx> ys" |
701 assumes a: "xs \<approx> ys" |
702 shows "(z # xs) \<approx> (z # ys)" |
702 shows "(z # xs) \<approx> (z # ys)" |
703 using a by (rule QuotMain.list_eq.intros(5)) |
703 using a by (rule QuotMain.list_eq.intros(5)) |
704 |
704 |
|
705 lemma fs1_strong_cases: |
|
706 fixes X :: "'a list" |
|
707 shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))" |
|
708 apply (induct X) |
|
709 apply (simp) |
|
710 apply (erule disjE) |
|
711 apply (metis QuotMain.m1 list_eq_refl) |
|
712 apply (metis QUOT_TYPE_I_fset.R_sym QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons) |
|
713 done |
705 |
714 |
706 text {* |
715 text {* |
707 Unlam_def converts a definition given as |
716 Unlam_def converts a definition given as |
708 |
717 |
709 c \<equiv> %x. %y. f x y |
718 c \<equiv> %x. %y. f x y |
1252 | INVOKE1 "obj1 \<Rightarrow> string" |
1261 | INVOKE1 "obj1 \<Rightarrow> string" |
1253 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)" |
1262 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)" |
1254 *) |
1263 *) |
1255 |
1264 |
1256 end |
1265 end |
1257 |
|