equal
deleted
inserted
replaced
95 | defs (l::ls) r = one_def l (%%:@{const_name cfst}`r) :: defs ls (%%:@{const_name csnd}`r); |
95 | defs (l::ls) r = one_def l (%%:@{const_name cfst}`r) :: defs ls (%%:@{const_name csnd}`r); |
96 val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint); |
96 val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint); |
97 |
97 |
98 val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs; |
98 val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs; |
99 val (fixdef_thms, thy') = |
99 val (fixdef_thms, thy') = |
100 PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy; |
100 PureThy.add_defs false (map Thm.no_attributes fixdefs) thy; |
101 val ctuple_fixdef_thm = foldr1 (fn (x,y) => @{thm cpair_equalI} OF [x,y]) fixdef_thms; |
101 val ctuple_fixdef_thm = foldr1 (fn (x,y) => @{thm cpair_equalI} OF [x,y]) fixdef_thms; |
102 |
102 |
103 val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss)); |
103 val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss)); |
104 val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold |
104 val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold |
105 (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1, |
105 (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1, |