683 Const (@{const_name True}, _) => t |
683 Const (@{const_name True}, _) => t |
684 | (* redundant, since 'False' is also an IDT constructor *) |
684 | (* redundant, since 'False' is also an IDT constructor *) |
685 Const (@{const_name False}, _) => t |
685 Const (@{const_name False}, _) => t |
686 | Const (@{const_name undefined}, _) => t |
686 | Const (@{const_name undefined}, _) => t |
687 | Const (@{const_name The}, _) => t |
687 | Const (@{const_name The}, _) => t |
688 | Const ("Hilbert_Choice.Eps", _) => t |
688 | Const (@{const_name Hilbert_Choice.Eps}, _) => t |
689 | Const (@{const_name All}, _) => t |
689 | Const (@{const_name All}, _) => t |
690 | Const (@{const_name Ex}, _) => t |
690 | Const (@{const_name Ex}, _) => t |
691 | Const (@{const_name "op ="}, _) => t |
691 | Const (@{const_name "op ="}, _) => t |
692 | Const (@{const_name "op &"}, _) => t |
692 | Const (@{const_name "op &"}, _) => t |
693 | Const (@{const_name "op |"}, _) => t |
693 | Const (@{const_name "op |"}, _) => t |
694 | Const (@{const_name "op -->"}, _) => t |
694 | Const (@{const_name "op -->"}, _) => t |
695 (* sets *) |
695 (* sets *) |
696 | Const (@{const_name Collect}, _) => t |
696 | Const (@{const_name Collect}, _) => t |
697 | Const (@{const_name "op :"}, _) => t |
697 | Const (@{const_name "op :"}, _) => t |
698 (* other optimizations *) |
698 (* other optimizations *) |
699 | Const ("Finite_Set.card", _) => t |
699 | Const (@{const_name Finite_Set.card}, _) => t |
700 | Const ("Finite_Set.finite", _) => t |
700 | Const (@{const_name Finite_Set.finite}, _) => t |
701 | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []), |
701 | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []), |
702 Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t |
702 Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t |
703 | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []), |
703 | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []), |
704 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t |
704 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t |
705 | Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []), |
705 | Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []), |
706 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t |
706 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t |
707 | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []), |
707 | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []), |
708 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t |
708 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t |
709 | Const ("List.append", _) => t |
709 | Const (@{const_name List.append}, _) => t |
710 | Const (@{const_name lfp}, _) => t |
710 | Const (@{const_name lfp}, _) => t |
711 | Const (@{const_name gfp}, _) => t |
711 | Const (@{const_name gfp}, _) => t |
712 | Const ("Product_Type.fst", _) => t |
712 | Const (@{const_name fst}, _) => t |
713 | Const ("Product_Type.snd", _) => t |
713 | Const (@{const_name snd}, _) => t |
714 (* simply-typed lambda calculus *) |
714 (* simply-typed lambda calculus *) |
715 | Const (s, T) => |
715 | Const (s, T) => |
716 (if is_IDT_constructor thy (s, T) |
716 (if is_IDT_constructor thy (s, T) |
717 orelse is_IDT_recursor thy (s, T) then |
717 orelse is_IDT_recursor thy (s, T) then |
718 t (* do not unfold IDT constructors/recursors *) |
718 t (* do not unfold IDT constructors/recursors *) |
879 | Const (@{const_name "op -->"}, _) => axs |
880 | Const (@{const_name "op -->"}, _) => axs |
880 (* sets *) |
881 (* sets *) |
881 | Const (@{const_name Collect}, T) => collect_type_axioms (axs, T) |
882 | Const (@{const_name Collect}, T) => collect_type_axioms (axs, T) |
882 | Const (@{const_name "op :"}, T) => collect_type_axioms (axs, T) |
883 | Const (@{const_name "op :"}, T) => collect_type_axioms (axs, T) |
883 (* other optimizations *) |
884 (* other optimizations *) |
884 | Const ("Finite_Set.card", T) => collect_type_axioms (axs, T) |
885 | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms (axs, T) |
885 | Const ("Finite_Set.finite", T) => collect_type_axioms (axs, T) |
886 | Const (@{const_name Finite_Set.finite}, T) => |
|
887 collect_type_axioms (axs, T) |
886 | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []), |
888 | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []), |
887 Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => |
889 Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => |
888 collect_type_axioms (axs, T) |
890 collect_type_axioms (axs, T) |
889 | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []), |
891 | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []), |
890 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => |
892 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => |
893 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => |
895 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => |
894 collect_type_axioms (axs, T) |
896 collect_type_axioms (axs, T) |
895 | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []), |
897 | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []), |
896 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => |
898 Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => |
897 collect_type_axioms (axs, T) |
899 collect_type_axioms (axs, T) |
898 | Const ("List.append", T) => collect_type_axioms (axs, T) |
900 | Const (@{const_name List.append}, T) => collect_type_axioms (axs, T) |
899 | Const (@{const_name lfp}, T) => collect_type_axioms (axs, T) |
901 | Const (@{const_name lfp}, T) => collect_type_axioms (axs, T) |
900 | Const (@{const_name gfp}, T) => collect_type_axioms (axs, T) |
902 | Const (@{const_name gfp}, T) => collect_type_axioms (axs, T) |
901 | Const ("Product_Type.fst", T) => collect_type_axioms (axs, T) |
903 | Const (@{const_name fst}, T) => collect_type_axioms (axs, T) |
902 | Const ("Product_Type.snd", T) => collect_type_axioms (axs, T) |
904 | Const (@{const_name snd}, T) => collect_type_axioms (axs, T) |
903 (* simply-typed lambda calculus *) |
905 (* simply-typed lambda calculus *) |
904 | Const (s, T) => |
906 | Const (s, T) => |
905 if is_const_of_class thy (s, T) then |
907 if is_const_of_class thy (s, T) then |
906 (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *) |
908 (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *) |
907 (* and the class definition *) |
909 (* and the class definition *) |
1314 (* while the SAT solver searches for an interpretation for Free's. *) |
1316 (* while the SAT solver searches for an interpretation for Free's. *) |
1315 (* Also we get more information back that way, namely an *) |
1317 (* Also we get more information back that way, namely an *) |
1316 (* interpretation which includes values for the (formerly) *) |
1318 (* interpretation which includes values for the (formerly) *) |
1317 (* quantified variables. *) |
1319 (* quantified variables. *) |
1318 (* maps !!x1...xn. !xk...xm. t to t *) |
1320 (* maps !!x1...xn. !xk...xm. t to t *) |
1319 fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) = strip_all_body t |
1321 fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) = |
1320 | strip_all_body (Const (@{const_name Trueprop}, _) $ t) = strip_all_body t |
1322 strip_all_body t |
1321 | strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) = strip_all_body t |
1323 | strip_all_body (Const (@{const_name Trueprop}, _) $ t) = |
|
1324 strip_all_body t |
|
1325 | strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) = |
|
1326 strip_all_body t |
1322 | strip_all_body t = t |
1327 | strip_all_body t = t |
1323 (* maps !!x1...xn. !xk...xm. t to [x1, ..., xn, xk, ..., xm] *) |
1328 (* maps !!x1...xn. !xk...xm. t to [x1, ..., xn, xk, ..., xm] *) |
1324 fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) = |
1329 fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) = |
1325 (a, T) :: strip_all_vars t |
1330 (a, T) :: strip_all_vars t |
1326 | strip_all_vars (Const (@{const_name Trueprop}, _) $ t) = |
1331 | strip_all_vars (Const (@{const_name Trueprop}, _) $ t) = |
2707 (* interpreters available already (using its definition), but the code *) |
2713 (* interpreters available already (using its definition), but the code *) |
2708 (* below is more efficient *) |
2714 (* below is more efficient *) |
2709 |
2715 |
2710 fun Finite_Set_finite_interpreter thy model args t = |
2716 fun Finite_Set_finite_interpreter thy model args t = |
2711 case t of |
2717 case t of |
2712 Const ("Finite_Set.finite", |
2718 Const (@{const_name Finite_Set.finite}, |
2713 Type ("fun", [Type ("set", [T]), Type ("bool", [])])) $ _ => |
2719 Type ("fun", [Type ("set", [T]), Type ("bool", [])])) $ _ => |
2714 (* we only consider finite models anyway, hence EVERY set is *) |
2720 (* we only consider finite models anyway, hence EVERY set is *) |
2715 (* "finite" *) |
2721 (* "finite" *) |
2716 SOME (TT, model, args) |
2722 SOME (TT, model, args) |
2717 | Const ("Finite_Set.finite", |
2723 | Const (@{const_name Finite_Set.finite}, |
2718 Type ("fun", [Type ("set", [T]), Type ("bool", [])])) => |
2724 Type ("fun", [Type ("set", [T]), Type ("bool", [])])) => |
2719 let |
2725 let |
2720 val size_of_set = size_of_type thy model (Type ("set", [T])) |
2726 val size_of_set = size_of_type thy model (Type ("set", [T])) |
2721 in |
2727 in |
2722 (* we only consider finite models anyway, hence EVERY set is *) |
2728 (* we only consider finite models anyway, hence EVERY set is *) |
2846 (* interpreters available already (using its definition), but the code *) |
2852 (* interpreters available already (using its definition), but the code *) |
2847 (* below is more efficient *) |
2853 (* below is more efficient *) |
2848 |
2854 |
2849 fun List_append_interpreter thy model args t = |
2855 fun List_append_interpreter thy model args t = |
2850 case t of |
2856 case t of |
2851 Const ("List.append", Type ("fun", [Type ("List.list", [T]), Type ("fun", |
2857 Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun", |
2852 [Type ("List.list", [_]), Type ("List.list", [_])])])) => |
2858 [Type ("List.list", [_]), Type ("List.list", [_])])])) => |
2853 let |
2859 let |
2854 val size_elem = size_of_type thy model T |
2860 val size_elem = size_of_type thy model T |
2855 val size_list = size_of_type thy model (Type ("List.list", [T])) |
2861 val size_list = size_of_type thy model (Type ("List.list", [T])) |
2856 (* maximal length of lists; 0 if we only consider the empty list *) |
2862 (* maximal length of lists; 0 if we only consider the empty list *) |