96 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
96 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
97 val perm_eqs = maps perm_eq descr; |
97 val perm_eqs = maps perm_eq descr; |
98 val lthy = |
98 val lthy = |
99 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
99 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
100 (* TODO: Use the version of prmrec that gives the names explicitely. *) |
100 (* TODO: Use the version of prmrec that gives the names explicitely. *) |
101 val ((_, perm_ldef), lthy') = |
101 val ((perm_frees, perm_ldef), lthy') = |
102 Primrec.add_primrec |
102 Primrec.add_primrec |
103 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
103 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
104 val perm_frees = |
|
105 (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); |
|
106 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); |
104 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); |
107 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) |
105 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) |
108 val perms_name = space_implode "_" perm_names' |
106 val perms_name = space_implode "_" perm_names' |
109 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
107 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
110 val perms_append_bind = Binding.name (perms_name ^ "_append") |
108 val perms_append_bind = Binding.name (perms_name ^ "_append") |
111 fun tac _ (_, simps) = |
109 fun tac _ (_, simps, _) = |
112 (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); |
110 (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); |
113 fun morphism phi (dfs, simps) = (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); |
111 fun morphism phi (dfs, simps, fvs) = |
|
112 (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); |
114 in |
113 in |
115 lthy' |
114 lthy' |
116 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |
115 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |
117 |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) |
116 |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) |
118 |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms)) |
117 |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees) |
119 end |
118 end |
120 |
119 |
121 *} |
120 *} |
122 |
121 |
123 ML {* |
122 ML {* |