# HG changeset patch # User paulson # Date 1094199999 -7200 # Node ID 2fd60846f485b7642b6d9a051a1e684660288771 # Parent b62f7b493360f674cf5f96ccb87b5f91a097e848 listrel operator for lifting relations to lists diff -r b62f7b493360 -r 2fd60846f485 src/HOL/List.thy --- a/src/HOL/List.thy Fri Sep 03 00:35:38 2004 +0200 +++ b/src/HOL/List.thy Fri Sep 03 10:26:39 2004 +0200 @@ -679,6 +679,63 @@ "listset(A#As) = set_Cons A (listset As)" +subsection{*Lifting a Relation on List Elements to the Lists*} +consts listrel :: "('a * 'a)set => ('a list * 'a list)set" + +inductive "listrel(r)" + intros + Nil: "([],[]) \ listrel r" + Cons: "[| (x,y) \ r; (xs,ys) \ listrel r |] ==> (x#xs, y#ys) \ listrel r" + +inductive_cases listrel_Nil1 [elim!]: "([],xs) \ listrel r" +inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \ listrel r" +inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \ listrel r" +inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \ listrel r" + + +lemma listrel_mono: "r \ s \ listrel r \ listrel s" +apply clarify +apply (erule listrel.induct) +apply (blast intro: listrel.intros)+ +done + +lemma listrel_subset: "r \ A \ A \ listrel r \ lists A \ lists A" +apply clarify +apply (erule listrel.induct, auto) +done + +lemma listrel_refl: "refl A r \ refl (lists A) (listrel r)" +apply (simp add: refl_def listrel_subset Ball_def) +apply (rule allI) +apply (induct_tac x) +apply (auto intro: listrel.intros) +done + +lemma listrel_sym: "sym r \ sym (listrel r)" +apply (auto simp add: sym_def) +apply (erule listrel.induct) +apply (blast intro: listrel.intros)+ +done + +lemma listrel_trans: "trans r \ trans (listrel r)" +apply (simp add: trans_def) +apply (intro allI) +apply (rule impI) +apply (erule listrel.induct) +apply (blast intro: listrel.intros)+ +done + +theorem equiv_listrel: "equiv A r \ equiv (lists A) (listrel r)" +by (simp add: equiv_def listrel_refl listrel_sym listrel_trans) + +lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}" +by (blast intro: listrel.intros) + +lemma listrel_Cons: + "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"; +by (auto simp add: set_Cons_def intro: listrel.intros) + + subsection {* @{text mem} *} lemma set_mem_eq: "(x mem xs) = (x : set xs)"