107 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
107 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
108 val perm_frees = |
108 val perm_frees = |
109 (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); |
109 (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); |
110 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); |
110 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); |
111 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) |
111 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) |
112 fun tac ctxt perm_thms = |
112 val perms_name = space_implode "_" perm_names' |
|
113 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
|
114 val perms_append_bind = Binding.name (perms_name ^ "_append") |
|
115 fun tac _ perm_thms = |
113 (Class.intro_classes_tac []) THEN (ALLGOALS ( |
116 (Class.intro_classes_tac []) THEN (ALLGOALS ( |
114 simp_tac (HOL_ss addsimps perm_thms |
117 simp_tac (HOL_ss addsimps perm_thms |
115 ))); |
118 ))); |
116 fun morphism phi = map (Morphism.thm phi); |
119 fun morphism phi = map (Morphism.thm phi); |
117 in |
120 in |
118 Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) lthy' |
121 lthy' |
|
122 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |
|
123 |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) |
|
124 |> Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) |
119 end |
125 end |
120 |
126 |
121 *} |
127 *} |
122 |
128 |
123 (* Test |
129 (* Test |