On 08/12/2011 01:01 PM, Lawrence Paulson wrote:
(I'm trying to imagine
some sort of magic operator to ease the transition between sets with
various forms of tupling and relations.)
These tools exist to some extent, as the attributes [to_set] and
[to_pred]. It is used a few times in the development of HOL, but
otherwise not very well-known:
krauss@lapbroy38:~/wd/isabelle/src/HOL$ egrep -r '\[to_(pred|set)\]' .
./List.thy:lemmas lists_IntI = listsp_infI [to_set]
./List.thy:lemmas append_in_lists_conv [iff] = append_in_listsp_conv
[to_set]
./List.thy:lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
./List.thy:lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]
./List.thy:lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
./Transitive_Closure.thy:lemmas rtrancl_mono = rtranclp_mono [to_set]
./Transitive_Closure.thy:lemmas rtrancl_induct [induct set: rtrancl] =
rtranclp_induct [to_set]
./Transitive_Closure.thy:lemmas converse_rtrancl_into_rtrancl =
converse_rtranclp_into_rtranclp [to_set]
./Transitive_Closure.thy:lemmas rtrancl_idemp [simp] = rtranclp_idemp
[to_set]
./Transitive_Closure.thy:lemmas rtrancl_subset = rtranclp_subset [to_set]
./Transitive_Closure.thy:lemmas rtrancl_Un_rtrancl =
rtranclp_sup_rtranclp [to_set]
./Transitive_Closure.thy:lemmas rtrancl_reflcl [simp] = rtranclp_reflcl
[to_set]
./Transitive_Closure.thy:lemmas rtrancl_converseD = rtranclp_converseD
[to_set]
./Transitive_Closure.thy:lemmas rtrancl_converseI = rtranclp_converseI
[to_set]
./Transitive_Closure.thy:lemmas converse_rtrancl_induct =
converse_rtranclp_induct [to_set]
./Transitive_Closure.thy:lemmas converse_rtranclE = converse_rtranclpE
[to_set]
./Transitive_Closure.thy:lemmas trancl_into_rtrancl =
tranclp_into_rtranclp [to_set]
./Transitive_Closure.thy:lemmas rtrancl_into_trancl1 =
rtranclp_into_tranclp1 [to_set]
./Transitive_Closure.thy:lemmas rtrancl_into_trancl2 =
rtranclp_into_tranclp2 [to_set]
./Transitive_Closure.thy:lemmas trancl_induct [induct set: trancl] =
tranclp_induct [to_set]
./Transitive_Closure.thy:lemmas trancl_trans_induct =
tranclp_trans_induct [to_set]
./Transitive_Closure.thy:lemmas rtrancl_trancl_trancl =
rtranclp_tranclp_tranclp [to_set]
./Transitive_Closure.thy:lemmas trancl_into_trancl2 =
tranclp_into_tranclp2 [to_set]
./Transitive_Closure.thy:lemmas trancl_converseI = tranclp_converseI
[to_set]
./Transitive_Closure.thy:lemmas trancl_converseD = tranclp_converseD
[to_set]
./Transitive_Closure.thy:lemmas trancl_converse = tranclp_converse [to_set]
./Transitive_Closure.thy:lemmas converse_trancl_induct =
converse_tranclp_induct [to_set]
./Transitive_Closure.thy:lemmas tranclD = tranclpD [to_set]
./Transitive_Closure.thy:lemmas converse_tranclE = converse_tranclpE
[to_set]
./Transitive_Closure.thy:lemmas reflcl_trancl [simp] = reflcl_tranclp
[to_set]
./Transitive_Closure.thy:lemmas rtranclD = rtranclpD [to_set]
./Transitive_Closure.thy:lemmas trancl_rtrancl_trancl =
tranclp_rtranclp_tranclp [to_set]
./Wellfounded.thy:lemmas wfPUNIVI = wfUNIVI [to_pred]
./Wellfounded.thy:lemmas wfP_induct = wf_induct [to_pred]
./Wellfounded.thy:lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
./Wellfounded.thy:lemmas wfP_trancl = wf_trancl [to_pred]
./Wellfounded.thy:lemmas wfP_subset = wf_subset [to_pred]
./Wellfounded.thy:lemmas wfP_acyclicP = wf_acyclic [to_pred]
./Wellfounded.thy:lemmas acyclicP_converse [iff] = acyclic_converse
[to_pred]
./Wellfounded.thy:lemmas acc_induct = accp_induct [to_set]
./Wellfounded.thy:lemmas acc_downward = accp_downward [to_set]
./Wellfounded.thy:lemmas not_acc_down = not_accp_down [to_set]
./Wellfounded.thy:lemmas acc_downwards_aux = accp_downwards_aux [to_set]
./Wellfounded.thy:lemmas acc_downwards = accp_downwards [to_set]
./Wellfounded.thy:lemmas acc_wfI = accp_wfPI [to_set]
./Wellfounded.thy:lemmas acc_wfD = accp_wfPD [to_set]
./Wellfounded.thy:lemmas wf_acc_iff = wfP_accp_iff [to_set]
krauss@lapbroy38:~/wd/isabelle/src/HOL$
krauss@lapbroy38:~/wd/afp/thys$ egrep -r '\[to_(pred|set)\]' .
./Simpl/AlternativeSmallStep.thy: by (rule renumber [to_pred])
./Simpl/AlternativeSmallStep.thy: by (rule renumber [to_pred])
./Simpl/SmallStep.thy: by (rule renumber [to_pred])
./Simpl/SmallStep.thy: by (rule renumber [to_pred])
krauss@lapbroy38:~/wd/afp/thys$
Alex
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
