346 |
346 |
347 val dvdc = \<^cterm>\<open>(dvd) :: int => _\<close>; |
347 val dvdc = \<^cterm>\<open>(dvd) :: int => _\<close>; |
348 |
348 |
349 fun unify ctxt q = |
349 fun unify ctxt q = |
350 let |
350 let |
351 val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE |
351 val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs |
352 val x = Thm.term_of cx |
352 val x = Thm.term_of cx |
353 val ins = insert (op = : int * int -> bool) |
353 val ins = insert (op = : int * int -> bool) |
354 fun h (acc,dacc) t = |
354 fun h (acc,dacc) t = |
355 case Thm.term_of t of |
355 case Thm.term_of t of |
356 Const(s,_)$(Const(\<^const_name>\<open>Groups.times\<close>,_)$c$y)$ _ => |
356 Const(s,_)$(Const(\<^const_name>\<open>Groups.times\<close>,_)$c$y)$ _ => |
434 val insert_tm = \<^cterm>\<open>insert :: int => _\<close>; |
434 val insert_tm = \<^cterm>\<open>insert :: int => _\<close>; |
435 fun mkISet cts = fold_rev (Thm.apply insert_tm #> Thm.apply) cts emptyIS; |
435 fun mkISet cts = fold_rev (Thm.apply insert_tm #> Thm.apply) cts emptyIS; |
436 val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1; |
436 val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1; |
437 val [A_v,B_v] = |
437 val [A_v,B_v] = |
438 map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg |
438 map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg |
439 |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg |
439 |> Thm.dest_abs |> snd |> Thm.dest_arg1 |> Thm.dest_arg |
440 |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg |
440 |> Thm.dest_abs |> snd |> Thm.dest_fun |> Thm.dest_arg |
441 |> Thm.term_of |> dest_Var) [asetP, bsetP]; |
441 |> Thm.term_of |> dest_Var) [asetP, bsetP]; |
442 |
442 |
443 val D_v = (("D", 0), \<^typ>\<open>int\<close>); |
443 val D_v = (("D", 0), \<^typ>\<open>int\<close>); |
444 |
444 |
445 fun cooperex_conv ctxt vs q = |
445 fun cooperex_conv ctxt vs q = |
446 let |
446 let |
447 |
447 |
448 val uth = unify ctxt q |
448 val uth = unify ctxt q |
449 val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth)) |
449 val (x,p) = Thm.dest_abs (Thm.dest_arg (Thm.rhs_of uth)) |
450 val ins = insert (op aconvc) |
450 val ins = insert (op aconvc) |
451 fun h t (bacc,aacc,dacc) = |
451 fun h t (bacc,aacc,dacc) = |
452 case (whatis x t) of |
452 case (whatis x t) of |
453 And (p,q) => h q (h p (bacc,aacc,dacc)) |
453 And (p,q) => h q (h p (bacc,aacc,dacc)) |
454 | Or (p,q) => h q (h p (bacc,aacc,dacc)) |
454 | Or (p,q) => h q (h p (bacc,aacc,dacc)) |
715 | _ => [ct]); |
715 | _ => [ct]); |
716 |
716 |
717 fun strip_objall ct = |
717 fun strip_objall ct = |
718 case Thm.term_of ct of |
718 case Thm.term_of ct of |
719 Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn,_,_) => |
719 Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn,_,_) => |
720 let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct |
720 let val (a,(v,t')) = (apsnd (Thm.dest_abs_name xn) o Thm.dest_comb) ct |
721 in apfst (cons (a,v)) (strip_objall t') |
721 in apfst (cons (a,v)) (strip_objall t') |
722 end |
722 end |
723 | _ => ([],ct); |
723 | _ => ([],ct); |
724 |
724 |
725 local |
725 local |
796 let |
796 let |
797 val cts = snd (get ctxt) |
797 val cts = snd (get ctxt) |
798 fun h acc t = if ty cts t then insert (op aconvc) t acc else |
798 fun h acc t = if ty cts t then insert (op aconvc) t acc else |
799 case Thm.term_of t of |
799 case Thm.term_of t of |
800 _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) |
800 _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) |
801 | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc)) |
801 | Abs(_,_,_) => Thm.dest_abs t ||> h acc |> uncurry (remove (op aconvc)) |
802 | _ => acc |
802 | _ => acc |
803 in h [] ct end |
803 in h [] ct end |
804 end; |
804 end; |
805 |
805 |
806 fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st => |
806 fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st => |