70 let |
70 let |
71 val constr_name = |
71 val constr_name = |
72 constraint_def |> Thm.prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq |
72 constraint_def |> Thm.prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq |
73 |> head_of |> fst o dest_Const |
73 |> head_of |> fst o dest_Const |
74 val live = live_of_bnf bnf |
74 val live = live_of_bnf bnf |
75 val (((As, Bs), Ds), ctxt) = ctxt |
75 val (((As, Bs), Ds), ctxt') = ctxt |
76 |> mk_TFrees live |
76 |> mk_TFrees live |
77 ||>> mk_TFrees live |
77 ||>> mk_TFrees live |
78 ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf)) |
78 ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf)) |
79 |
79 |
80 val relator = mk_rel_of_bnf Ds As Bs bnf |
80 val relator = mk_rel_of_bnf Ds As Bs bnf |
81 val relsT = map2 mk_pred2T As Bs |
81 val relsT = map2 mk_pred2T As Bs |
82 val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt |
82 val (args, ctxt'') = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt' |
83 val concl = HOLogic.mk_Trueprop (mk_relation_constraint constr_name (list_comb (relator, args))) |
83 val concl = HOLogic.mk_Trueprop (mk_relation_constraint constr_name (list_comb (relator, args))) |
84 val assms = map (HOLogic.mk_Trueprop o (mk_relation_constraint constr_name)) args |
84 val assms = map (HOLogic.mk_Trueprop o (mk_relation_constraint constr_name)) args |
85 val goal = Logic.list_implies (assms, concl) |
85 val goal = Logic.list_implies (assms, concl) |
86 in |
86 in |
87 (goal, ctxt) |
87 (goal, ctxt'') |
88 end |
88 end |
89 |
89 |
90 fun prove_relation_side_constraint ctxt bnf constraint_def = |
90 fun prove_relation_side_constraint ctxt bnf constraint_def = |
91 let |
91 let |
92 val old_ctxt = ctxt |
92 val (goal, ctxt') = generate_relation_constraint_goal ctxt bnf constraint_def |
93 val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def |
93 in |
94 val thm = Goal.prove_sorry ctxt [] [] goal |
94 Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} => |
95 (fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1) |
95 side_constraint_tac bnf [constraint_def] goal_ctxt 1) |
96 |> Thm.close_derivation |
96 |> Thm.close_derivation |
97 in |
97 |> singleton (Variable.export ctxt' ctxt) |
98 Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) |
98 |> Drule.zero_var_indexes |
99 end |
99 end |
100 |
100 |
101 fun prove_relation_bi_constraint ctxt bnf constraint_def side_constraints = |
101 fun prove_relation_bi_constraint ctxt bnf constraint_def side_constraints = |
102 let |
102 let |
103 val old_ctxt = ctxt |
103 val (goal, ctxt') = generate_relation_constraint_goal ctxt bnf constraint_def |
104 val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def |
104 in |
105 val thm = Goal.prove_sorry ctxt [] [] goal |
105 Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} => |
106 (fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1) |
106 bi_constraint_tac constraint_def side_constraints goal_ctxt 1) |
107 |> Thm.close_derivation |
107 |> Thm.close_derivation |
108 in |
108 |> singleton (Variable.export ctxt' ctxt) |
109 Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) |
109 |> Drule.zero_var_indexes |
110 end |
110 end |
111 |
111 |
112 val defs = [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}), |
112 val defs = |
|
113 [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}), |
113 ("left_unique_rel", @{thm left_unique_alt_def}), ("right_unique_rel", @{thm right_unique_alt_def})] |
114 ("left_unique_rel", @{thm left_unique_alt_def}), ("right_unique_rel", @{thm right_unique_alt_def})] |
114 |
115 |
115 fun prove_relation_constraints bnf lthy = |
116 fun prove_relation_constraints bnf ctxt = |
116 let |
117 let |
117 val transfer_attr = @{attributes [transfer_rule]} |
118 val transfer_attr = @{attributes [transfer_rule]} |
118 val Tname = base_name_of_bnf bnf |
119 val Tname = base_name_of_bnf bnf |
119 |
120 |
120 val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs |
121 val defs = map (apsnd (prove_relation_side_constraint ctxt bnf)) defs |
121 val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def} |
122 val bi_total = prove_relation_bi_constraint ctxt bnf @{thm bi_total_alt_def} |
122 [snd (nth defs 0), snd (nth defs 1)] |
123 [snd (nth defs 0), snd (nth defs 1)] |
123 val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def} |
124 val bi_unique = prove_relation_bi_constraint ctxt bnf @{thm bi_unique_alt_def} |
124 [snd (nth defs 2), snd (nth defs 3)] |
125 [snd (nth defs 2), snd (nth defs 3)] |
125 val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs |
126 val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs |
126 in |
127 in |
127 maps (fn (a, thm) => [((Binding.qualify_name true Tname a, []), [([thm], transfer_attr)])]) defs |
128 maps (fn (a, thm) => [((Binding.qualify_name true Tname a, []), [([thm], transfer_attr)])]) defs |
128 end |
129 end |
172 end |
173 end |
173 |
174 |
174 fun prove_Domainp_rel ctxt bnf pred_def = |
175 fun prove_Domainp_rel ctxt bnf pred_def = |
175 let |
176 let |
176 val live = live_of_bnf bnf |
177 val live = live_of_bnf bnf |
177 val old_ctxt = ctxt |
178 val (((As, Bs), Ds), ctxt') = ctxt |
178 val (((As, Bs), Ds), ctxt) = ctxt |
|
179 |> mk_TFrees live |
179 |> mk_TFrees live |
180 ||>> mk_TFrees live |
180 ||>> mk_TFrees live |
181 ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf)) |
181 ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf)) |
182 |
182 |
183 val relator = mk_rel_of_bnf Ds As Bs bnf |
183 val relator = mk_rel_of_bnf Ds As Bs bnf |
184 val relsT = map2 mk_pred2T As Bs |
184 val relsT = map2 mk_pred2T As Bs |
185 val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt |
185 val (args, ctxt'') = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt' |
186 val lhs = mk_Domainp (list_comb (relator, args)) |
186 val lhs = mk_Domainp (list_comb (relator, args)) |
187 val rhs = Term.list_comb (mk_pred_of_bnf Ds As bnf, map mk_Domainp args) |
187 val rhs = Term.list_comb (mk_pred_of_bnf Ds As bnf, map mk_Domainp args) |
188 val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop |
188 val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop |
189 val thm = Goal.prove_sorry ctxt [] [] goal |
189 in |
190 (fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1) |
190 Goal.prove_sorry ctxt'' [] [] goal (fn {context = goal_ctxt, ...} => |
191 |> Thm.close_derivation |
191 Domainp_tac bnf pred_def goal_ctxt 1) |
192 in |
192 |> Thm.close_derivation |
193 Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) |
193 |> singleton (Variable.export ctxt'' ctxt) |
|
194 |> Drule.zero_var_indexes |
194 end |
195 end |
195 |
196 |
196 fun predicator bnf lthy = |
197 fun predicator bnf lthy = |
197 let |
198 let |
198 val pred_def = pred_set_of_bnf bnf |
199 val pred_def = pred_set_of_bnf bnf |