[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Alexander Krauss]

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 at 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 at lapbroy38:~/wd/isabelle/src/HOL$


krauss at 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 at lapbroy38:~/wd/afp/thys$

Alex