37 end; |
37 end; |
38 |
38 |
39 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
39 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
40 struct |
40 struct |
41 |
41 |
|
42 fun get_ps trm = |
|
43 case trm of |
|
44 Const (@{const_name permute}, _) $ p $ (Bound _) => raise TERM ("get_ps", [trm]) |
|
45 | Const (@{const_name permute}, _) $ p $ _ => [p] |
|
46 | t $ u => get_ps t @ get_ps u |
|
47 | Abs (_, _, t) => get_ps t |
|
48 | _ => [] |
|
49 |
|
50 fun put_p p trm = |
|
51 case trm of |
|
52 Bound _ => trm |
|
53 | Const _ => trm |
|
54 | t $ u => put_p p t $ put_p p u |
|
55 | Abs (x, ty, t) => Abs (x, ty, put_p p t) |
|
56 | _ => mk_perm p trm |
|
57 |
|
58 (* tests whether the lists of ps all agree, and that there is at least one p *) |
|
59 fun is_bad_list [] = true |
|
60 | is_bad_list [_] = false |
|
61 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
|
62 |
|
63 |
42 structure EqvtData = Generic_Data |
64 structure EqvtData = Generic_Data |
43 ( type T = thm Item_Net.T; |
65 ( type T = thm Item_Net.T; |
44 val empty = Thm.full_rules; |
66 val empty = Thm.full_rules; |
45 val extend = I; |
67 val extend = I; |
46 val merge = Item_Net.merge ); |
68 val merge = Item_Net.merge ); |
60 val add_thm = EqvtData.map o Item_Net.update; |
82 val add_thm = EqvtData.map o Item_Net.update; |
61 val del_thm = EqvtData.map o Item_Net.remove; |
83 val del_thm = EqvtData.map o Item_Net.remove; |
62 |
84 |
63 fun add_raw_thm thm = |
85 fun add_raw_thm thm = |
64 case prop_of thm of |
86 case prop_of thm of |
65 Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm) |
87 Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update (zero_var_indexes thm)) |
66 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
88 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
67 |
89 |
68 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
90 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
69 |
91 |
70 fun eq_transform_tac thm = REPEAT o FIRST' |
92 fun eq_transform_tac thm = |
71 [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), |
93 let |
72 rtac (thm RS @{thm trans}), |
94 val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all} |
73 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
95 in |
|
96 REPEAT o FIRST' |
|
97 [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms), |
|
98 rtac (thm RS @{thm trans}), |
|
99 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
|
100 end |
74 |
101 |
75 (* transform equations into the "p o c = c"-form *) |
102 (* transform equations into the "p o c = c"-form *) |
76 fun transform_eq ctxt thm = |
103 fun transform_eq ctxt thm = |
77 let |
104 let |
78 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) |
105 val ((p, t), rhs) = apfst dest_perm |
79 val (p, t) = dest_perm lhs |
106 (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) |
80 val (c, args) = strip_comb t |
107 handle TERM _ => error "Eqvt lemma is not of the form p \<bullet> c... = c..." |
81 val (c', args') = strip_comb rhs |
108 val ps = get_ps rhs handle TERM _ => [] |
82 val eargs = map Envir.eta_contract args |
109 val (c, c') = (head_of t, head_of rhs) |
83 val eargs' = map Envir.eta_contract args' |
|
84 val p_str = fst (fst (dest_Var p)) |
|
85 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
|
86 in |
110 in |
87 if c <> c' |
111 if c <> c' |
88 then error "Eqvt lemma is not of the right form (constants do not agree)" |
112 then error "Eqvt lemma is not of the right form (constants do not agree)" |
89 else if eargs' <> map (mk_perm p) eargs |
113 else if is_bad_list (p::ps) |
|
114 then error "Eqvt lemma is not of the right form (permutations do not agree)" |
|
115 else if not (rhs aconv (put_p p t)) |
90 then error "Eqvt lemma is not of the right form (arguments do not agree)" |
116 then error "Eqvt lemma is not of the right form (arguments do not agree)" |
91 else if args = [] |
117 else if is_Const t |
92 then thm |
118 then thm |
93 else Goal.prove ctxt [p_str] [] goal |
119 else |
94 (fn _ => eq_transform_tac thm 1) |
120 let |
|
121 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
|
122 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
|
123 in |
|
124 Goal.prove ctxt [] [] goal' (fn _ => eq_transform_tac thm 1) |
|
125 |> singleton (ProofContext.export ctxt' ctxt) |
|
126 end |
95 end |
127 end |
96 |
|
97 |
|
98 (* tests whether the lists of pis all agree, and that there is at least one p *) |
|
99 fun is_bad_list [] = true |
|
100 | is_bad_list [_] = false |
|
101 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
|
102 |
|
103 |
128 |
104 fun imp_transform_tac thy p p' thm = |
129 fun imp_transform_tac thy p p' thm = |
105 let |
130 let |
106 val cp = Thm.cterm_of thy p |
131 val cp = Thm.cterm_of thy p |
107 val cp' = Thm.cterm_of thy (mk_minus p') |
132 val cp' = Thm.cterm_of thy (mk_minus p') |
114 |
139 |
115 fun transform_imp ctxt thm = |
140 fun transform_imp ctxt thm = |
116 let |
141 let |
117 val thy = ProofContext.theory_of ctxt |
142 val thy = ProofContext.theory_of ctxt |
118 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
143 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
119 val (c, prem_args) = strip_comb prem |
144 val (c, c') = (head_of prem, head_of concl) |
120 val (c', concl_args) = strip_comb concl |
145 val ps = get_ps concl handle TERM _ => [] |
121 val ps = map (fst o dest_perm) concl_args handle TERM _ => [] |
|
122 val p = try hd ps |
146 val p = try hd ps |
123 in |
147 in |
124 if c <> c' |
148 if c <> c' |
125 then error "Eqvt lemma is not of the right form (constants do not agree)" |
149 then error "Eqvt lemma is not of the right form (constants do not agree)" |
126 else if is_bad_list ps |
150 else if is_bad_list ps |
127 then error "Eqvt lemma is not of the right form (permutations do not agree)" |
151 then error "Eqvt lemma is not of the right form (permutations do not agree)" |
128 else if concl_args <> map (mk_perm (the p)) prem_args |
152 else if not (concl aconv (put_p (the p) prem)) |
129 then error "Eqvt lemma is not of the right form (arguments do not agree)" |
153 then error "Eqvt lemma is not of the right form (arguments do not agree)" |
130 else |
154 else |
131 let |
155 let |
132 val prem' = Const (@{const_name "permute"}, @{typ "perm => bool => bool"}) $ (the p) $ prem |
156 val prem' = mk_perm (the p) prem |
133 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
157 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
134 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
158 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
135 in |
159 in |
136 Goal.prove ctxt' [] [] goal' |
160 Goal.prove ctxt' [] [] goal' |
137 (fn _ => imp_transform_tac thy (the p) p' thm 1) |
161 (fn _ => imp_transform_tac thy (the p) p' thm 1) |